Marco Eilers

Crash report: class vct.col.ast.Loop cannot be cast to class vct.col.ast.Invocation (vct.col.ast.Loop and vct.col.

1

# Crash Message ``` class vct.col.ast.Loop cannot be cast to class vct.col.ast.Invocation (vct.col.ast.Loop and vct.col.ast.Invocation are in unnamed module of loader 'app') at viper.api.backend.SilverBackend.processError(SilverBackend.scala:297) at viper.api.backend.SilverBackend.processError$(SilverBackend.scala:172) at viper.api.backend.silicon.Silicon.processError(Silicon.scala:34) at viper.api.backend.SilverBackend.$anonfun$submit$1(SilverBackend.scala:164)...

Desugaring quasihavocall to an exhale-inhale pair

2

This PR adds support for ``quasihavocall`` similar to the existing support for ``quasihavoc``, namely by desugaring it into an exhale-inhale pair (which unfortunately means that magic wands cannot be supported)....

The following fails to verify in Carbon: ``` field data: Int method foo1(x: Ref) requires acc(x.data) { package acc(x.data) --* false { assert acc(x.data) && acc(x.data) assert false // fails...

Addressing issue #291. With this PR, for ``predicate P(x: Ref, i: Int)``, we generate ``` function P(x: Ref, i: int): Field PredicateType_P FrameType; function P#sm(x: Ref, i: int): Field PredicateType_P...

- Added utility method ``Expressions.isKnownWellDefined`` to check whether some expression is statically known to be well-defined more efficiently than by explicitly computing ``Expressions.proofObligations``; additionally, the new method does not require...

Requires https://github.com/viperproject/silicon/pull/899 to be merged first.

This PR adds consistency checks that forbid inhale-exhale assertions in predicate bodies and in function preconditions. Currently, Silicon raises an internal error when it encounters these (see https://github.com/viperproject/silicon/issues/271), whereas Carbon...

Allow custom error message for assertion failures via @msg annotation

1

For example, ``` method test0(x: Ref) { @msg("Custom error message") assert x != null } ``` leads to Silicon output ``` Silicon found 1 error in 2.83s: [0] Custom error...

Information following from field access receiver not known when checking for permission

1

The following program verifies in Carbon but not in Silicon (with or without MCE): ``` field f: Int function flag(): Bool function assuming(b: Bool, r: Ref): Ref ensures b ensures...

Fixing QP snapshot merging analogous to https://github.com/viperproject/silicon/pull/904, as suggested by @superaxander. I haven't found a way to trigger the problem yet (and I won't merge this until I do), but...