TransferFunctions (infer.Absint.AbstractInterpreter.MakeDisjunctive.TransferFunctions)

include TransferFunctions.S
  with type instr := IR.Sil.instr
  with type analysis_data = T.analysis_data
  with module CFG = T.CFG
  with type Domain.t = T.DisjDomain.t list * T.NonDisjDomain.t

module CFG = T.CFG

module Domain : 
  AbstractDomain.S with type t = T.DisjDomain.t list * T.NonDisjDomain.t

abstract domain whose state we propagate

type analysis_data = T.analysis_data

read-only extra state (results of previous analyses, globals, etc.)

val exec_instr : 
  Domain.t ->
  analysis_data ->
  CFG.Node.t ->
  ProcCfg.InstrNode.instr_index ->
  IR.Sil.instr ->
  Domain.t

exec_instr astate proc_data node idx instr should usually return astate' such that {astate} instr {astate'} is a valid Hoare triple. In other words, exec_instr defines how executing an instruction from a given abstract state changes that state into a new one. This is usually called the transfer function in Abstract Interpretation terms. node is the node containing the current instruction and idx is the index of the instruction in the node.

val pp_session_name : CFG.Node.t -> Stdlib.Format.formatter -> unit

print session name for HTML debug