Thomas Haas

Using the LKMM documentation referenced in #211, I think we can get rid of those somewhat magical `FenceCond` events. The reason is based on the following excerpt: ``` ===== From...

The forwarding is not applicable under Linux, because it can delete else-branches (which happens if those are empty). This causes the control-dependencies to end up being wrong (due to `IfAsJump`...

> As I see it, the semantics of our `Assume` event is the one described in point 3 (@ThomasHaas can you confirm this?). Yes, the `Assume` I implemented has these...

To address the overall issue: `assume_abort_if_not` acts like a "pseudo-assume". It is definitely not an `assert` cause it doesn't provide a safety specification (unless we look at termination instead of...

> This is how it used to be, however, there is an effort to reduce the use of SVCOMP specific functions and replace them with either functions having precise semantics...

Of course, the simple program in my example wouldn't have a problem since the `assert(false)` terminates the thread and hence the subsequent `assume(false)` is never reached. However, as soon as...

> @ThomasHaas is right that once an assertion is violated, the execution at the C level would just stop. For verification however, we "continue" the execution. I don't think this...

> > Well, that is where the problem with `assume` comes in, since a later assume may invalidate the execution if the assertion does not cause a complete termination (which...

> > That is not true if an assertion violation terminates the thread. > > Are you talking about "execution level" or "verification level"? If it is at the verification...

An alternative to these static assertions is to always produce standard assertions like in #557 and only give an error if the point of failure is dynamically reachable. Disadvantages of...