dafny
dafny copied to clipboard
Calling a method that modifies an unassigned value gives an unclear error
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.