Common VerCors error messages

This page is to explain what the different error messages in VerCors mean. We try to keep this page alphabetically ordered by error message (case insensitive sorting. For sentences: spaces come before letters in the alphabet). If you have a question about error messages, please add a question to this wiki page. If you know the answer to a question asked here, please replace the question with the answer (or with a link to the answer elsewhere on the wiki).

AssignmentFailed: insufficient permission

This means you are trying to write to a variable (at the left hand side of an assignment) to which VerCors cannot establish a write-permission. The statement assert(Perm(lhs,1)); in which lhs is the left hand side of this assignment will fail at this point in your code, but should be provable.

Illegal argument count

This is a internal VerCors error, that might be due to a parse-error in your script. We have opened a issue for this here.

Illegal iteration invariant

This seems to happen when you try to specify a loop_invariant in a for-loop, where you're using a resource as invariant. Try using context (short for ensures and requires combined) instead. Are you getting this message in a different situation? Do let us know!

java.lang.*

This is never supposed to happen, but unfortunately, it did. Thank you for finding this bug in VerCors. Try searching our issue tracker to see if you believe this bug is already being addressed. If not, please let us know about it by adding it!

No viable alternative at ...

This is a parsing error, you may have made a typo, or inadvertently used a reserved keyword as a variable. Check your code at the position indicated. If this is the start of a line, make sure there is a semicolon ; at the previous line.

NotWellFormed:InsufficientPermission

This error is shown at a specification. We require rules to be 'self framing', this means that you need read-permission in order to access variables, even inside specifications. Furthermore, checks like array accesses being within bounds need to hold. The order of the specifications makes a difference here: the lines of your specifications are checked from top to bottom, and from left to right. In order to establish permissions and bounds, add a line of specification before the line that gives you trouble, asserting that you have read permission, or that the access is within bounds.

If you see this error in the \old(..) part of an ensures expression, you need permission to that variable before executing the function. For constructors (e.g. foo method of class foo), there is no \old(this.x), as the variable this.x is only created when the constructor is called.

Pre-condition of constructor may not refer to this

When calling the constructor method of a class, the class variables are not yet initialised. Therefore, you should not refer to them. Do you need write-permission? Don't worry, the class constructor already has it by definition (as it implicitly creates the variables)! In particular, use ensures instead of context.

Type of left/right argument is Resource rather than Boolean:

This is a type error. You are using a symbol like && that requires boolean values on both sides. Changing && to **, or breaking up your specification into multiple lines might solve the problem for you.

Verification aborted exceptionally: java.util.concurrent.ExecutionException: java.util.concurrent.ExecutionException: java.util.NoSuchElementException: None.get

See VerCors crashes when predicates are unfolded.

"Not injective", or "resource may not be unique with regards to the quantified variables", or similar

Viper requires that all forall with permission expressions (forall* in VerCors) are "injective". That means that different values for the quantified variable(s) must result in different memory locations in the permission expression. For example in (\forall* int k; 0<=k && k<arr.length; Perm(arr[k].myField, 1)), different k must point to different array elements, i.e. arr[i] must be different from arr[j] if i!=j. You need to add a condition like (\forall int i, int j; 0<=i && i<j && j<arr.length; arr[i] != arr[j]) before the quantifier that "may not be unique". And if myField is an object, you might need to do the same for arr[i].myField and arr[j].myField. More info is here.