Linard Arquint

Hi Greg, Thanks for your interest in Gobra. While we support verifying `.go` files, it is indeed unfortunate that this is not yet reflected in the tutorial. If you put...

Gobra incorrectly ignores the switch / select context of a `break` stmt and associates it with the surrounding loop

@jcp19 Felix suggested to merge the 2nd and 3rd input mode: `-d --projectRoot ` takes the provided list of directories and searches (recursively!) for packages in them. `--includePackage` and `--excludePackage`...

Interesting! For me, `includePackages` is very handy: I configure the Gobra command once more a particular module (consisting of various packages in its subfolders) by specifying the project root (i.e....

I'd say that's the reason. More specifically, if I don't add `--includePackages` it will verify all and if I provide it (usually with only a single package name) verification is...

> The problem is that you may have different packages with the same name, in which case this approach is no longer expressive enough That's correct. I think in that...

This issue might have been fixed by #239

`--checkConsistency` does not complain but pointing Viper-IDE at the generated Viper program results in 2 invalid trigger errors as the inferred triggers are ternary expressions

Manually specifying the following triggers solves the problem: ``` package test5 type Bar struct { } type FooCacheEntry struct { Bar Bar } var fooCache = map[string]*FooCacheEntry{} preserves acc(fooCache, _)...

This seems to be a minimal example to reproduce this issue. Note that `Bar` is needed and replacing the `b` field by an int makes the issue disappear: ``` package...