silver

silver copied to clipboard

(Reported by a PV student:) ```viper method test() { { var i: Int } var i: Int } ``` This causes an AST construction error for the second declaration of...

Aurel300

The PR [836 for Silicon](https://github.com/viperproject/silicon/pull/836) fixes an issue that was mentioned in Issue [307](https://github.com/viperproject/silicon/issues/307/). For a 100% test score one must remove the `MissingOutput` flag in the test file `conditionals2.vpr`.

manud99

This PR introduces changes to the parser for the documentation generator in development: Comments starting with exactly three slashes are parsed as annotations with the key "doc". Moreover, annotations can...

fnussbaum

When defining a `goto` in a macro, its label is replaced, when it matches a macro argument. When defining a `label` in a macro, its label is **not** replaced, even...

Bibin112358

Viper-Extension tells me to report this bug: Using the following Viper Program ```vpr define outer_macro () { { define inner_macro 42 } } method test() { outer_macro() } ``` I...

Bibin112358

jogasser

Wrong optimization of signed integer divisions

1

Jonas made me realize that this optimization (used by Prusti) is wrong when `left < 0`, because in Viper `-3 / 2 == -2` but in Scala (and Rust) `-3...

fpoli

Replaces PR #673

ArquintL

Dspil

```js method test(m: Map[Int,Int]) requires(range(m) == domain(m)) { assume forall i: Int, j: Int :: i in m && j in m ==> (i != j ==> (m[i] != m[j]))...

tillarnold