Marco Eilers

Carbon implementation of the new backend-independent counterexample format (see https://github.com/viperproject/silver/pull/883), written by @rvandoren in his practical work project.

The following program verifies in Silicon but crashes Carbon: ``` field f: Int method m(r: Ref) { package acc(r.f, wildcard) --* acc(r.f, wildcard) } ``` The error message says ``Verification...

Adapting Carbon to the changes in https://github.com/viperproject/silver/pull/867.

This PR adds the core components for a backend-independent counterexample model, to be used in either backend using the command line parameter ``--counterexample=extended``. Unlike the current ``--counterexample=variables`` option, it contains...

I recently saw a Viper program where some consistency checks that need the call graph between functions took literal minutes, because various parts of the code calculating that graph use...

Silicon implementation of the new backend-independent counterexample format (see https://github.com/viperproject/silver/pull/883), written by @rvandoren in his practical work project.

Something is wrong with predicate triggers for functions

1

Silicon triggers definitions of functions both when they are called directly and when predicates are unfolded that they depend on. For example, in the Viper program below, we get the...

Adapting Silicon to the changes in https://github.com/viperproject/silver/pull/867, and also changing its State to avoid Viper functions/predicates as keys in maps for the same reason.