Felix Wolf

For a scion file (https://github.com/viperproject/VerifiedSCION/blob/master/pkg/slayers/doc.go), the `getPackageClause` of `PackageResolver.scala` matches "benchmarks" and not "slayers". It seems to me that the used regex is matching "benchmarks" of the comment "see the...

The following snippet fails to verify. The problem is that the fields used to encode the value pointed to by `*T` and `*int` are different. They are different because they...

Interface predicate instances imply that the interface argument is not nil

2

Title

Fix issue 491

2

This PR: - Fixes a bug in the encoding context, where using the copy constructor would cause the freshname generator to break. - Makes the length argument of array type...

The following code fails: ``` package main pred p(*int) { true } func test1() { var x@ int fold p(&x) f := requires p(&x) // fails func foo() { }...

The test fails due to a failing postcondition. What happens is that the postcondition of the encoded interface function fails even though it should hold trivially since the body of...

Gobra throws an exception for the following snippet: ``` requires forall i int :: 0 acc(&s[i]) ensures len(foo(s)) == len(s) ensures forall i int :: 0 s[i] == foo(s)[i] pure...

The code below fails. The problem is that is not clear whether `S()` refers to a conversion or a call of the interface method. In a meeting, we have decided...