Malte Schwerhoff
Malte Schwerhoff
Consider the following program: ```plain predicate p(a: Ref, b: Ref) method m(x: Ref, s: Set[Ref], t: Seq[Ref]) { exhale forall a: Int, b: Ref :: b in s && 0...
```text field f: Ref field g: Bool method test03a(rs: Set[Ref]) requires forall r: Ref :: {r in rs} r in rs ==> acc(r.f, 1/2) requires forall r: Ref :: {r...
Carbon issue corresponding to [Silver issue #455](https://github.com/viperproject/silver/issues/455).
Originally filed as viperproject/silicon#366. According to that issue, for CAV'17 example [FollyRWSpinlock_err_mod](https://github.com/viperproject/examples/blob/master/cav2017/FollyRWSpinlock_err_mod.sil), the following line fails: ``` 85: .. 86: fetchUpdate(bits,value,value - 4, true,true) // fetchUpdate is a macro 87:...
For the program method foo() { assert false } the assertion failure is reported as `Assert might fail. Assertion false might not hold. ([email protected])`. However line 2, columns 9-10 identify...
The following example was originally reported by @bobismijnnaam as [Silicon issue #574](https://github.com/viperproject/silicon/issues/574#issuecomment-933603209). Observe that requires-clause and assert-statement contain literally the same assertion. ``` domain VectorIndex { function vrange(lo: Int, hi:...
Git/GitHub and Sbt version are currently out of sync. For example, [release v.21.01](https://github.com/viperproject/silver/releases/tag/v.21.01-release) is tagged as ` v.21.01-release`, but it's [Sbt version ](https://github.com/viperproject/silver/blob/d2ebc840305c13ed8c5551c4f86925422cfb0820/build.sbt#L39) is still `0.1-SNAPSHOT`. Silicon uses a combination...
Viper currently allows wildcards in compound expressions, but semantics and practical relevance of such expressions are unclear. Viper should therefore reject such expressions, via suitable consistency checks. A few invalid...
When updating to Scala 3, we should also attend to the 60+ compiler warnings, and the numerous IntelliJ code improvement suggestions.
Background: Test suite starts failing with 4.8.8 (Carbon and Silicon); newer versions result in even more failing tests. With Z3 4.8.10 and 4.8.11-nightly, about half of the 55 tests in...