Alexander Stekelenburg
Alexander Stekelenburg
The following program verifies erroneously: ```java class A { int a; } context Perm(a.a, write); ensures a.a == \old(a.a) + 1; ensures \result == a.a; int incr(A a); requires Perm(a.a,...
While attempting to replicate a VerCors [issue](https://github.com/utwente-fmt/vercors/issues/1275) I ran into this Viper crash (running with Silicon on the master branch): ``` java.lang.RuntimeException: type unification error - should report and not...
Hi, I've been looking into improving Silicon's performance on some of the VerCors case studies that I am trying out. Most of the bottlenecks that I run into have to...
Checklist: - [x] The wiki is updated in accordance with the changes in this PR. For example: syntax changes, semantics changes, VerCors flags changes, etc. # PR description - Rewrite...
Checklist: - [ ] The wiki is updated in accordance with the changes in this PR. For example: syntax changes, semantics changes, VerCors flags changes, etc. # PR description Very...
Because #1219 caused global variable initializers to no longer be thrown away we now get an error when a function is called in such an initializer . ``` ====================================== At...
In C we can declare variables inside a loop and take the address of these variables. If we do that, the variable will be replaced by a pointer. In the...
In Java the following program verifies where it shouldn't: ```java class Test { int a; //@ context Perm(a, write); //@ ensures a == \old(a) + 1; //@ ensures !\result; boolean...
Multiple places across VerCors assume that `Readable#fileName` will be a valid path to an existing path. This is not always true. (for example if an input originates from stdin) Places...
In the following program: ```c //@ requires \pointer(a, n, write); void foo(int *a, int n) { int half = n/2; int *b = a + half; //@ assert \pointer(b -...