Module ForwardAnalyser.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 IN domain and the OUT 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 assume the condition of the if bloc to produce two domains d1 and d2 * we analyse the first branch (then branch) with the domain d1 * we analyse the second branch (else branch) with the domain d2 * we merge the two domains to produce the final domain for the if bloc
• while bloc (b1, condition, b2) : * we analyse the first bloc b1 with the input domain d * we loop and analyse the body of the while bloc (b2,b1,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