Frama-C API - D

States propagated by the dataflow analysis.

Merges two states coming from different paths.

widen v1 v2 is called on loop heads after each iteration of the analysis on the loop body: v1 is the previous state before the iteration, and v2 the new state after the iteration. The function must return Fixpoint if the analysis has reached a fixpoint for the loop: this is usually the case if join v1 v2 is equal to v1, as a new iteration would have the same entry state as the last one. Otherwise, it must return the new entry state for the next iteration, by over-approximating the join between v1 and v2 such that any sequence of successive widenings is ultimately stationary, i.e. …widen (widen (widen x0 x1) x2) x3… eventually returns Fixpoint. This ensures the analysis termination.

Transfer function for edges: transfer v e s computes the state after the transition e.edge_transition from the state s before, at vertex v. Returns None if the end of the transition is not reachable from the given state.