Felix Wolf

Currently, Gobra is not using label invariants. I do not have strong feelings about how invariants for non-head labels should be handled.

For external people, this is a joke. There are many things that can be verified with Gobra. This Issue will never be closed.

There is a `000166.gobra` in our test set, so I assume that this issue has been resolved. Open it again if that is not the case.

That looks like an error in the member resolution since the type `*IA` has the member Mem twice. You can make the implementation proof by the aliasing feature. The tutorial...

How important is this? If I am not missing something, this should be quite easy to implement.

This part of the language specifications seems relatively new to me. Back when I added literals, I did not find that the semantics for composite literals are specified so I...

Also, I would not mix code analysis and the desugarer. The necessary information for the desugaring step should be collecting by the Info object. The main concern is that the...

Here is a client that shows the transformation: ``` import viper.silver.{ast => vpr} import viper.silicon.Silicon import viper.silver.reporter.NoopReporter import viper.silver.verifier.{Failure, Success} import viper.silver.verifier.{AbstractVerificationError, errors => vprerr, reasons => vprrea} val v...

From my perspective, this is a design problem and not a problem of the encoding. Function literal names are not full specifications because the captured variables are missing. As a...

I though about is bit more. I am not completely sure whether the following approach works, but I wanted to document it for now: Currently, captured variables are encoded via...