Lars - he/him

Running the examples of the wiki during the test CI

11

So I've just tried to run all the examples of the wiki, since I've noticed not everything seemed to be always working. This was also some feedback we got after...

Crash report: Missing: Quantified resource aloc(optGet1(boxes), i).ref.value might not be injective.

2

This is from the current tutorial # Crash Message ``` Missing: Quantified resource aloc(optGet1(boxes), i).ref.value might not be injective. at viper.api.backend.SilverBackend.getFailure(SilverBackend.scala:398) at viper.api.backend.SilverBackend.getFailure$(SilverBackend.scala:385) at viper.api.backend.silicon.Silicon.getFailure(Silicon.scala:34) at viper.api.backend.SilverBackend.processError(SilverBackend.scala:200) at viper.api.backend.SilverBackend.processError$(SilverBackend.scala:173) at...

Changed behaviour of ADTs (bags, seq)

4

```java //:: cases axiomatic-data-types-bag-constructing-bags-from-existing-bags-1 //:: verdict Pass //:: tools silicon class Test { void test() { bag b9 = bag { 3 }; bag b10 = bag { 3, 4...

Fix pointer array which is allocated in loop

1

Checklist: - [x] The wiki is updated in accordance with the changes in this PR. For example: syntax changes, semantics changes, VerCors flags changes, etc. # PR description The following...