dafny icon indicating copy to clipboard operation
dafny copied to clipboard

Calling a method that modifies an unassigned value gives an unclear error

Open keyboardDrummer opened this issue 3 years ago • 0 comments

Suppose we have the following program

method test(element:int, a:array<int>)
   requires a.Length > 2
   modifies a;
{
   a[0] := element;
}

method Main()
{
   var a : array<int>;
   var element : int;
   assume a.Length > 2;
   test(element, a);
}

that has an error which can be resolved by assigning a value to a before calling test. Dafny gives the error message "call might violate context's modifies clause", but that doesn't make it clear why the modifies clause is violated, which is because a was not initialised before the call.

keyboardDrummer avatar May 27 '22 08:05 keyboardDrummer