Lars - he/him

Multiple quantifiers to memory locations of same type

4

So this is not per se a bug report, more something I run into. I'm wondering if there are workarounds, or something fundamental what is needed here. For my research...

Small fix

2

Some small fixes I needed: * Increases stack size to 128m: I was running into stack overflow errors again. But if you rather have dev not have such a big...

Slow VerCors passes for simple program

9

I wanted to share the following programs, which I investigated for run times. These are the verification times: data/quant_s1.pvl 8.662854194641113 success data/quant_s2.pvl 7.364089488983154 success data/quant_s3.pvl 7.336841583251953 success data/quant_s4.pvl 7.506519317626953 success...

GPU programs do not give fault for to much permission, which leads to incomplete verification

2

So this file: ```cuda //:: cases BasicCuda //:: tool silicon //:: verdict Pass #include /*@ context \pointer_index(a, threadIdx.x, write); @*/ __global__ void example(int a[], int len) { int tid =...

Mostly a reminder to self to fix. Due to the fact of how barriers are encoded, and the SimplifyNestedQuantifyRelations work when you write for instance: ```cuda //@ blockDim.y == 1...

VerCors throws an error when Specifying a resource as trigger

1

``` resource test(int i) = i > 0; void main(){ loop_invariant i >= 0 && i

Vector support in C, OpenCL and CUDA + Vector ADT in PVL

1

* I've added support for vectors in C, OpenCL, CUDA and added a custom ADT in PVL. * PVL/use in annotations: * a vector type: `vector a4` * A vector...

Division defaults to rationals instead of integer floor division when using --backend-file-base

1

Minor bug, when writing: ```java context xs != null; context xs.length >= 4; context (\forall* int i; 0

I noticed that in our examples for OpenCL we write: ```opencl //:: cases BasicOpenCL //:: verdict Pass #include /*@ context_everywhere get_global_size(0) == 1; context \pointer_index(a, \ltid*2, write); context \pointer_index(a, \ltid*2+1,...

Relation and equality operators in C have int as return type

1

In C relational (, =) and equality operators actually have resulting type `int`. It has `0` for false value and `1` for true value. (See Section 6.5.8.6 and 6.5.9.3 of...