Type of the domain used for the analysis

Build the initial value of the domain using the function passed as argument.

args :

• ('info,'asm) Prog.func (function to analyse)

returns :

• domain (intial domain)

Pretty printer for the domain.

args :

• Format.formatter (formatter to use)
• domain (domain to print)

Inclusion test for the domain. included a b test if a is included in b

args :

• domain (first domain)
• domain (second domain)

returns :

• bool (true if first domain is included in the second one)

Control flow function used to handle conditionnal branches. assume build an annotation such that : for all A1, A2, e, s ; s in I(account e A1 A2) => s in I(if es then A1 else A2)

Function to remove a variable from a domain. This function is needed because of the way we handle for loops. args :

• Jasmin.Prog.var_i (variable to remove)
• domain (domain to update)

returns :

• domain Annotation.annotation (updated domain wrap with annotation type)

Function to handle function call instruction

Function to handle syscall instruction

Function to handle assign instruction

Function to handle opn instruction