PreAnalysisTransferFunctions (infer.Checkers.Liveness.PreAnalysisTransferFunctions)

Parameters

module CFG : Absint.ProcCfg.S

Signature

include Absint.TransferFunctions.SIL
  with module CFG = CFG
  with module Domain = ExtendedDomain
  with type analysis_data = IR.Procdesc.t

include Absint.TransferFunctions.S
  with type instr := IR.Sil.instr
  with module CFG = CFG
  with module Domain = ExtendedDomain
  with type analysis_data = IR.Procdesc.t

module CFG = CFG

module Domain = ExtendedDomain

abstract domain whose state we propagate

type analysis_data = IR.Procdesc.t

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

val exec_instr : 
  Domain.t ->
  analysis_data ->
  CFG.Node.t ->
  Absint.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.