package jasmin

  1. Overview
  2. Docs
package jasmin
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Parameter Make.L

type domain

Type of the domain used for the analysis

val initialize : ('info, 'asm) Jasmin.Prog.func -> domain Annotation.annotation

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)
val included : domain -> domain -> bool

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