Module BackwardAnalyser.Make

Functor used to create a module implementing forward analysis.

It takes a module implementing the Logic interface and returns a module implementing the S signature.

Each instruction is annotated with its OUT domain and the IN domain is passed to the next instruction. Domain are updated using the functions provided by the Logic module. Control flow is handled as follow :

• if bloc : * we analyse blocs then and else with the input domain d, producing two annotations a_then a_else * we merge the two annotations using the Logic.account function
• while bloc (b1, condition, b2) : * we account the condition with OUT annotation (corresponding to the out of while loop) and an Empty annotation (corresponding to the body of while loop) * we loop and analyse the body of the while bloc (b1,b2,condition) until we reach a fixpoint * we return the corresponding domain
• for bloc : * we convert the for loop to a while loop using a proxy variable for the loop variable : inline int i; for i = 0 to 10 { ... }

becomes :

inline int i; inline int i_proxy = 0; while (i_proxy < 10) { i = i_proxy; ... i_proxy++; } * we analyse the while loop with the while loop logic * we forget the proxy variable introduced by the for loop