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

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 assume : 
  Jasmin.Prog.expr ->
  domain Annotation.annotation ->
  domain Annotation.annotation * domain Annotation.annotation

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)

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