Dionysios Spiliopoulos

This issue tracks all the tests that are ignored in the silicon test-suite that non deterministically time out. - all/third_party/stefan_recent/testTreeWandE1.vpr

The assertion in the following code snippet fails although it should be obvious from the type of x.m. ``` package pkg type A struct { m [6]int } requires acc(&x.m)...

Missing position of error

2

This program: ``` package pkg type A int pred (s *A) Q(buf []byte) { true } pred (s *A) P(buf []byte) { 3

The following file produces a gobra error: ``` package pkg type f func () int type A interface { g() f } ``` The error is the following: ``` 15:24:06.959...

This is an issue with the parser. The embedded interface solution might work out of the box if we adapt the parser.

Typechecking with multiAssignableTo.errors

1

Typechecking with multiAssignableTo.errors using two times the same identifier in 'lefts' in a short var declaration passes typechecking when it shouldn't. An example is the following: for i, i :=...

Gobra accepts the following 2 examples: ``` type A struct { x int } func main() { var x *A var y *A = &(*x) assert y == x }...

Implementation proof for a pointer to a type fails when a predicate for the type exists

1

The code below does not verify throwing a "Permission to ia.Mem() might not suffice." error. When the predicate for just IA is removed it verifies. ``` package test // type...