T (infer.Absint.AbstractInterpreter.MakeBackwardRPO.T)

include TransferFunctions.SIL

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.)

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

val join_all : Domain.t list -> into:Domain.t option -> Domain.t option

Joins the abstract states from predecessors. It returns None when the given list is empty and into is None.

val filter_normal : Domain.t -> Domain.t

Refines the abstract state to select non-exceptional concrete states. Should return bottom if no such states exist

val filter_exceptional : Domain.t -> Domain.t

Refines the abstract state to select exceptional concrete states. Should return bottom if no such states exist

val transform_on_exceptional_edge : Domain.t -> Domain.t

Change the nature normal/exceptional when flowing through an exceptional edge. For a forward analysis, it should turn an exceptional state into normal. For a backward analysis, it should turn an normal state into exceptional.