Wytse Oortwijn

PaigeTarjanMinimization.minimizeDFA does not guarantee minimal result

1

The following code snippet creates and then minimizes a simple DFA: ``` public static void main(String[] args) throws IOException { CompactDFA dfa = new CompactDFA(new ArrayAlphabet("e1", "e2", "e3")); int s0...

Better handling of reserved Gobra keywords

1

The specification language of Gobra has several extra reserved keywords, in addition to the ones already reserved by Go. One example would be the `get(e)` destructor for expressions `e` of...

Internal AST nodes sometimes throw violations when encountering an unexpected type. See for example: https://github.com/viperproject/gobra/blob/26d14130b7b757648e62b7a5a6ff24ace342b1e7/src/main/scala/viper/gobra/ast/internal/Program.scala#L258-L261 However, such code would fail if the type is wrapped into a defined type, like...

Permission strangeness: uniqueness of new allocated objects is not preserved

4

Perhaps I'm missing something obvious, by why doesn't VerCors accept this: ```java class Cell { int val; } class Test { requires 0 < n; void test(int n) { seq...