package jasmin

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

Parameter Make.Logic

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 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
val merge : domain -> 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