Parameter MakeAbstractInterpreterWithConfig.3-TransferFunctions

include TransferFunctions.S with type instr := HilInstr.t
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 -> ProcCfg.InstrNode.instr_index -> 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