What is the meaning and purpose of "after" column in Frama-C EVA plugin

Question

In the EVA tutorial, I found this screenshot: with an explanation:" The exact value that caused this is shown in column c5: -1. The C standard considers the left-shift of a negative number as undefined behavior. Because -1 is the only possible value in this callstack, the reduction caused by the alarm leads to a post-state that is ."

So, I want to ask:

What is the meaning and purpose of "after" column in Frama-C EVA plugin?

Is there any more detailed document to understand the term "reduction" and "post-state" used in EVA?

Answer 1

When you select a statement s in the GUI, there are two memory states that are relevant: the one before s (also called pre-state), and the one after the side-effects of s have been done (also called post-state). This is why you have two columns in the Values tab for each lval you're interested in. The notion of pre and post-state is quite standard in program verification and basically dates back to Hoare Logic.

The term "reduction" refers to the fact that after having emitting an alarm, EVA will attempt to remove from its abstract state the elements that correspond to concrete states that would definitely lead to undefined behavior. Indeed, the abstract state is supposed to be an over-approximation of all concrete states that can reach the statement without having triggered an undefined behavior beforehand: if something failed before s, there's no point in speculating what could happen when evaluating s. In the example you refer to, we have the particular case where all possible concrete states would lead to an error. Hence, we end up with the BOTTOM abstract state, representing an empty set of concrete states, and the analysis of this branch ends.