Module Wp.CfgCompilerSource

Control Flow Graphs

The semantics of a cfg is a collection of execution traces. We introduce the notion of node which represent a program point. In case of loop unrolling of function inlining, a node generalize the notion of stmt : two distinct nodes may refer to the same instruction at different memory states.

We introduce an interpretation I as a partial mapping from nodes n:node to memory states s:M.sigma, denoted I(n). The notation I(n) seen as a predicate indicates if `n` is in the partial mapping.

Given a cfg, a node can be associated to assumptions to filter interpretation against the memory state at this point.

Effects and predicates are defined wrt some fresh memory states, and can be duplicated at different nodes, each instance being mapped to different memory states.