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 functions used to handle conditionnal branches. assume condition d returns a pair of domain d1,d2 such that :

• d1 is the domain d updated with the knowledge that condition is true
• d2 is the domain d updated with the knowledge that condition is false

args :

• Jasmin.Prog.expr (condition to test)
• domain (domain to split)

returns :

• domain * domain

Merge two domains. merge a b returns a domain that is the result of the merge of a and b.

args :

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

returns :

• domain (merged domain)

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