MakeBackwardRPO (infer.Absint.AbstractInterpreter.MakeBackwardRPO)

Parameters

module T : TransferFunctions

Signature

module TransferFunctions = T

module InvariantMap = TransferFunctions.CFG.Node.IdMap

type invariant_map = TransferFunctions.Domain.t State.t InvariantMap.t

invariant map from node id -> state representing postcondition for node id

val compute_post : 
  ?do_narrowing:bool ->
  ?pp_instr:
    (TransferFunctions.Domain.t ->
      IR.Sil.instr ->
      (Stdlib.Format.formatter -> unit) option) ->
  TransferFunctions.analysis_data ->
  initial:TransferFunctions.Domain.t ->
  IR.Procdesc.t ->
  TransferFunctions.Domain.t option

compute and return the postcondition for the given IR.Procdesc.t starting from initial. pp_instr is used for the debug HTML and passed as a hook to handle both SIL and HIL CFGs.

val exec_cfg : 
  ?do_narrowing:bool ->
  TransferFunctions.CFG.t ->
  TransferFunctions.analysis_data ->
  initial:TransferFunctions.Domain.t ->
  invariant_map

compute and return invariant map for the given CFG/procedure starting from initial.

val exec_pdesc : 
  ?do_narrowing:bool ->
  TransferFunctions.analysis_data ->
  initial:TransferFunctions.Domain.t ->
  IR.Procdesc.t ->
  invariant_map

compute and return invariant map for the given procedure starting from initial

val extract_post : 
  TransferFunctions.CFG.Node.id ->
  'a State.t InvariantMap.t ->
  'a option

extract the postcondition for a node id from the given invariant map

val extract_pre : 
  TransferFunctions.CFG.Node.id ->
  'a State.t InvariantMap.t ->
  'a option

extract the precondition for a node id from the given invariant map

val extract_state : 
  TransferFunctions.CFG.Node.id ->
  'a InvariantMap.t ->
  'a option

extract the state for a node id from the given invariant map