Lars - he/him

Rewrites lead to 'side' effects in annotations

3

The program ```java requires y != 0; ensures \result == (x/y)*y + x%y; int mod(int x, int y){ return x; } ``` Gives back the result ``` -------------------------------------- 1 2...

When a precondition of a header file function fails, the error is not processed correctly. E.g. I changed the file `/res/universal/res/c/assert.h` towards ```c #ifndef ASSERT_H #define ASSERT_H #include /*@ requires...

Unrelated fold removes knowledge of quantifier with predicate unside

2

The following program does not verify. Whilst if you remove `fold acc(hide1(x1, n, i),1/2)` from line 21, it does verify. And I believe that line 21 should be unrelated to...

Unique specifier for types leading to using different fields in the backend

2

- [ ] The wiki is updated in accordance with the changes in this PR. For example: syntax changes, semantics changes, VerCors flags changes, etc. # PR Description Having many...

So with C/CUDA/OpenCL files we can and should include headers. These headers are automatically inserted in the file send to VerCors, due to the preprocessor. But if functionality of a...

Wand is not correctly documented.

1

I was trying to write a simple example of wands, and the tutorial does not help at the moment: [link](https://vercors.ewi.utwente.nl/wiki/#magic-wands) This example does work, so maybe we could replace it...

Verification error not correctly thrown for non injective quantifier.

3

The following program (given by @dzagieboylo) does throw an error, but does not give a verification error. Discussed briefly with @superaxander, probably an origin is passed as blame somewhere. But...

Inconsistent test: cuda_blur.cu

3

The test `examples/concepts/gpgpu/cuda_blur.cu` gives inconsistent results. See this failed test run: https://github.com/utwente-fmt/vercors/actions/runs/14242974330 And this working test run: https://github.com/utwente-fmt/vercors/actions/runs/14240074043 With no code changes. Same happens locally. ~50% change of failure/succesfull. I...

Crash report: None.get, it does not like 'requires x'

1

So if I write 'requires x' the program crashes when verification fails. Requires 'x==true' works as expected. It looks strange, in ProcessError (SilverBackend.scala:199) the reason.offendingNode is 'x==true' when I use...

# Crash Message ``` The silver AST delivered to viper is not valid: - Consistency error: Perm and forperm in this context are only allowed if nested under inhale-exhale assertions....