Marco Eilers
Marco Eilers
The following program crashes Silicon: ``` import import import field left : Ref // true case field right: Ref // false case field id : Int // var from code...
Silicon verifies that predicate bodies, function preconditions, and method pre- and postconditions are self-framing and well-defined. As a result, it is not necessary to re-verify well-definedness when using them (but...
The following example verifies in Silicon, as I think it should, but not in Carbon, where the ``assert false`` fails: ``` field data: Int method bar(x: Ref) requires acc(x.data) {...
Gobra frequently generates permission amounts like ``1 / 4000 / 2`` for SCION code by @jcp19. These are intended to be a fractional permission ``1/4000`` divided by two, i.e., the...
Viper would benefit from having some additional built-in types. For example, lots of Viper examples (e.g. in the tutorial) abstract list data structures on the heap to Viper's pure sequences....
The following program misbehaves in both Silicon and Carbon: ``` predicate P(r: Int) method m() { exhale forall i: Int :: i > 0 && i < 123 ==> [i...
This is basically a duplicate of Silicon issue https://github.com/viperproject/silicon/issues/844. The following code does not verify (both asserts in the main method fail), but I think it should: ``` method main1(tid:...
At least the following: - issues/carbon/0179 (unsound because of incorrect treatment of perm-expressions, will be fixed in PR #853) - issues/silicon/0008 (expected incompleteness, --conditionalizePermissions introduces disjunctive aliasing, works with MCE)...
If WorkerBorrowingForkJoinWorkerThread.onStart throws an InterruptedException for some subset of the worker threads, - a stack trace is printed but Silicon does not crash completely - for some reason onStart is...
For the following program, both backends report that ``len`` might not terminate: ``` field elem: Int field nxt: Ref predicate ll(r: Ref) { acc(r.elem) && acc(r.nxt) && (r.nxt != null...