Parameter MakeRPO.1-TransferFunctions
include TransferFunctions.S with type instr := IR.Sil.instr
module Domain : AbstractDomain.S
abstract domain whose state we propagate
val exec_instr : Domain.t -> analysis_data -> CFG.Node.t -> instr -> Domain.t
exec_instr astate proc_data node instr
should usually returnastate'
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