ThomasMayerl

Gobra reports reveal parser error if there is a parser error somewhere else

2

Similar to #899 using a reveal clause will mark the location of the reveal clause as a parser error if there is a syntax error somewhere else. For example, in...

Converting array behind pointer to slice using type definition crashes Gobra

1

For my project, I try to verify code where we have a type that represents an array (with a fixed number of elements). I need to convert this array into...

for-range: 0 <= i cannot be proven without len(x) > 0

1

In for-range loops, assertions concerning the current index cannot be verified if we don't assert that the length of the slice is larger than 0. For example, if we take...

If we have a function that takes some parameter of any type and we cast it to a map (by requiring that the parameter is a map dynamically), upon indexing...

If we assume a function that takes in a slice of strings and we want to convert that to a map mapping from strings to slices of strings (in the...

Adding slice to map removes permissions of other slices in map

6

In the following code, the first assert is successful. Based on the preconditions we know that, there is a key "found" in the map and thus, we have access to...

Unable to prove assert directly after equivalent assume

3

In the following code, we cannot prove the assert even though the assertion should be true because of the equivalent loop invariant. If we write an assume directly before the...

If I try to check if a parameter has a dynamic type of []map[string]interface{} (using `typeOf(var) == type[[]map[string]interface{}]`), Gobra crashes with the error message "encountered unsupported type expression: map[string]interface{}"

If we use append, Gobra is unable to prove that the slice we appended to is still different (by identity - comparing using ===/!==) from other slices. In the following...

Gobra doesn't terminate with unfold+fold and verification errors

6

In the following code, Gobra finds the verification error (the assert false) as expected: ```go type Foo struct { Bar []*Bar } pred FooBar(foo *Foo, minBar int) { acc(foo) &&...