ThomasMayerl

At the first run of a program (with F5), PC is set to 00h instead of 4200h. At pressing F5 at the last command and rerun the program with F5...

DCE depends on order

2

In some cases, the compiler's ability to eliminate dead code depends on the order of the sub-expressions within the if. LLVM detects that the if expression in the following code...

DCE breaks by adding redundant terms

2

Sometimes, DCE breaks by adding a redundant term. In the following example, the if statement always evaluates to false. LLVM (14) detects that and removes the dead code: ```c #include...

DCE affected by inserting double negations

1

Sometimes the compiler's ability to detect and eliminate dead code decreases when double negations are inserted. LLVM detects that in the following snippet the if expression is always false and...

Sometimes the compiler's ability to detect and eliminate dead code is affected by applying De Morgan's law. In the following snippet, the compiler detects the dead code and thus removes...

Gobra generates invalid triggers

6

In some cases Gobra generates invalid triggers. For example, in the following code Gobra generates invalid triggers when the element Bar in Foo is of type Bar instead of *Bar:...

Assuming the following definitions: ```go type Foo struct { Bar int } var globalCache = map[string][]string{} var globalFooCache = map[string]*Foo{} ``` In the following function, Gobra cannot automatically infer injectivity...

Gobra crashes when specifying invariants over a key or value of a range over a map

1

The invariant in the following code makes Gobra crash with the error message `java.util.concurrent.ExecutionException: java.util.concurrent.ExecutionException: java.util.NoSuchElementException`: ```go var cache = map[string]*int{} requires acc(cache, _) requires forall s string :: s...

The following code verifies because the syntax error is commented out: ```go var mapstrstr = map[string][]string{} preserves acc(mapstrstr) preserves let val, ok := mapstrstr[str] in acc(val) func test(str string) //preserves...

When trying to access the elements of a slice that is in a struct behind a pointer using a for-range loop, Gobra reports that there might be insufficient read permissions...