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.