Why is Dafny allowing uninitialized return result?

mbrodersen 0
Viewed 33

In this method:

datatype Results = Foo | Bar

method test() returns (r:Result)
{
}

Dafny verifies OK and test() returns Foo. Which is technically correct (it does return a value of the correct type) however I was expecting Dafny to complain that the result has not been set by the method itself. What test() is doing is similar to doing:

return;

in a C function that is supposed to return an int.

Is there a way to make Dafny verify that a methods results are always set before the method returns?

dafny
1 Answers

The flag you want is /definiteAssignment:2:

  /definiteAssignment:<n>
      0 - ignores definite-assignment rules; this mode is for testing only--it is
          not sound
      1 (default) - enforces definite-assignment rules for compiled variables and fields
          whose types do not support auto-initialization and for ghost variables
          and fields whose type is possibly empty
      2 - enforces definite-assignment for all non-yield-parameter
          variables and fields, regardless of their types
      3 - like 2, but also performs checks in the compiler that no nondeterministic
          statements are used; thus, a program that passes at this level 3 is one
          that the language guarantees that values seen during execution will be
          the same in every run of the program

This is what Dafny says on your code says with that flag:

test.dfy(5,0): Error: out-parameter 'r', which is subject to definite-assignment rules, might be uninitialized at this return point

userPYU20
Related