L (p.jasmin.2026.03.0.doc.jasmin.linter.Linter.BackwardAnalyser.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)

val pp : Format.formatter -> (Jasmin.Location.i_loc * domain) -> unit

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)

val account : 
  Jasmin.Prog.expr ->
  domain Annotation.annotation ->
  domain Annotation.annotation ->
  domain Annotation.annotation

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)

val forget : Jasmin.Prog.var_i -> domain -> domain Annotation.annotation

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)

val funcall : 
  Jasmin.Location.i_loc ->
  Jasmin.Prog.lvals ->
  Jasmin.CoreIdent.funname ->
  Jasmin.Prog.exprs ->
  domain ->
  domain Annotation.annotation

Function to handle function call instruction

val syscall : 
  Jasmin.Location.i_loc ->
  Jasmin.Prog.lvals ->
  (Jasmin.Wsize.wsize * Jasmin.BinNums.positive) Jasmin.Syscall_t.syscall_t ->
  Jasmin.Prog.exprs ->
  domain ->
  domain Annotation.annotation

Function to handle syscall instruction

val assign : 
  Jasmin.Location.i_loc ->
  Jasmin.Prog.lval ->
  Jasmin.Expr.assgn_tag ->
  Jasmin.Prog.ty ->
  Jasmin.Prog.expr ->
  domain ->
  domain Annotation.annotation

Function to handle assign instruction

val opn : 
  Jasmin.Location.i_loc ->
  Jasmin.Prog.lvals ->
  Jasmin.Expr.assgn_tag ->
  'asm Jasmin.Sopn.sopn ->
  Jasmin.Prog.exprs ->
  domain ->
  domain Annotation.annotation

Function to handle opn instruction

val assertion : 
  Jasmin.Location.i_loc ->
  string ->
  Jasmin.Prog.expr ->
  domain ->
  domain Annotation.annotation

Function to handle assert instruction