Alexander Stekelenburg

The Java, C, and C++ frontends encode the division operator `/` as truncating division. If you use this operator to divide a permission value this crashes vercors. C test file:...

VeyMont pass EncodeChorBranchUnanimity crashes if loop condition is true

1

The following pvl program crashes VerCors: ``` choreography foo() { run { while (true) {} } } ``` This one also crashes because `StratifyUnpointedExpressions` changes the condition to true ```...

The following program unsoundly verifies: ```c #include int gi; short gs; //@ context Value(gi) ** Value(gs); //@ requires i != NULL && s != NULL; //@ requires i == (int...