Parameter Make.1-TransferFunctions

include TransferFunctions.S with type instr := IR.Sil.instr
module CFG : ProcCfg.S
module Domain : AbstractDomain.S

abstract domain whose state we propagate

type analysis_data

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

type instr

type of the instructions the transfer functions operate on

val exec_instr : Domain.t -> analysis_data -> CFG.Node.t -> instr -> Domain.t

exec_instr astate proc_data node 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.

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

print session name for HTML debug