call might violate context's modifies clause

[dreamqin68]

Hi All,

I have a question and hope to get help. Thanks.

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);
}

After compiling and running the above code, it shows Error: call might violate context's modifies clause.
Then I try to add a modify clause in the Main method.

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

It shows Error: modify statement might violate context's modifies clause.
Adding a modify clause doesn't solve this error, so how to solve this error?

[keyboardDrummer]

You can resolve your issue by assigning a value to a before passing it to test, like so:

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

method Main()
{
   var a : array<int> := new int[] [1,2,3];
   var element : int;
   assume a.Length > 2;
   test(element, a);
}

I guess you should view this as: you cannot call a method that modifies an unassigned value. I think your original program would crash if executed because it writes to an unassigned array. I will create an issue in Dafny because I do find that the error message is not clear about what the problem is. (#2171)

[dreamqin68]

Gotta. Thank you!