search

gradual-verification / gvc0

Gradually Verified C0
6 stars 5 forks source link

Exception when emitting conditional check on re-assigned value #13

Closed conradz closed 2 years ago

conradz commented 2 years ago

The following example crashes because a conditional check, depending on a previous value of x, is required:

void test(bool x, int y)
//@requires ?;
{
  if (x)
  {
    x = true;
    //@assert y == 0;
  }
}

with the following error:

Verification aborted exceptionally: java.util.concurrent.ExecutionException: java.util.concurrent.ExecutionException: java.lang.RuntimeException: Argument variable x@2@03 with sort Bool was not present in the symbolic store!
conradz commented 2 years ago

Fix should be possible in the verifier backend by resolving the branch condition to an AST node at the point of branching, which then does not require x to be resolved after it is re-assigned.

conradz commented 2 years ago

This is actually caused by reassignment to parameters, which is not supported by Viper. This is fixed by 547baf08c21a54c739ab7fd1a7f20375f4038408.