Lars - he/him
Lars - he/him
Pointers of pointers, fun :p But yeah it makes sense now, Perm(&accs, read) would be consistent with the other things in C.
Is the solution as simple as just putting `ResolveExpressionSideChecks` before `ResolveExpressionSideEffects` in `vct/main/stages/Transformation.scala` or does it need more consideration?
Hi, For VerCors 2.0 I get this to verify: ```cuda #include /* 1 */ /* 2 */ /* 3 */ /*@ context gridDim.x == 1 && gridDim.y == 1 &&...
So this is almost ready to merge. I added `/*@ unique_pointer_field(xs) @*/` where a field of a struct which contains a pointer can be given an unique type. Adding /*@...
Note: I had to run the build action again on GiHub, since the first time it said "Out of heap memory" or something similar. The same I indicated on the...
Ok I think I got everything covered now. Everything we discussed above I've fixed now, and there are test present for those things. I've updated the original PR description to...
I tried to better fix those decrease failures. Should close #1232 and #1065 Although getting something like ```java public class MyClass { //@ decreases; private int f() { //@ decreases;...
No I meant #1232 notice the small but important difference between these two: ```java public class MyClass { //@ decreases; private int f() { //@ decreases; while (true) {} return...
https://github.com/utwente-fmt/vercors/issues/1133 was just a very different kind of beast. You have to check that the post-condition of a call only has a self reference towards the call, if the call...