Lukas Armborst

Obviously true precondition "doesn't hold" when using predicate

1

The file below is a reduced version to highlight the problem: ``` function nonNull(): Ref ensures result != null function check(min_value1: Ref): Bool requires min_value1 != null predicate pred(nl: Ref)...

Bool/Int coercion for C is incomplete

3

The PR #1170 started implementing a coercion between boolean and integer values in C, since booleans are a type of integer there. It works for simple examples like https://github.com/utwente-fmt/vercors/blob/9b74fd74a18ad232784329ba78fab55d623a1511/examples/technical/intBoolCoercion.c. But...

Bool/Int type coercion

1

Before merging this PR, please check the following: - [x] I made sure the wiki is updated in accordance with the changes in this PR. For example, syntax changes, semantics...

Broken position when reporting incompatible modifier

1

The following Java program uses `static`, which is not allowed for pure methods inside classes: ```java class C { /*@ ghost static pure int max() = 0; @*/ } ```...

Cannot define permissions for global structs in C

3

The C example below has a global variable that is a struct pointer. It is impossible to define the permissions for that struct. ```c struct accounts { int len; };...

VerCors crashes when predicate is missing argument in C

2

The C code below invokes a predicate without arguments, even though it is defined to take some. ```c //@ resource pred(int i) = true; void main() { //@ fold pred();...

Specification cannot resolve value for C "define" macro

2

The C code below uses a `#define` macro, and uses the defined value in code as well as in spec. ```c #define DBL_MAX 1E+37 //@ requires a < DBL_MAX; int...

The program below has a function that calls itself recursively in its contract. Viper requires a termination measure for such functions, but none is provided here. ```java class T {...

VerCors crashes on modulo with zero

2

The following C program computes a modulo with `k`, which might be zero: ```c int main() { int i; int k = i; //@ assert (i % k == 0...

VerCors does not find global declarations if given multiple files

2

If global declarations are defined in one file and used in another, VerCors does not make the connection. I have file A.java ```java /*@ resource p(A a) = true; @*/...