Module `AbstractInterpreter.MakeRPO`

create an intraprocedural abstract interpreter from transfer functions using the reverse post-order scheduler

module TransferFunctions = TransferFunctions

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 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 : InvariantMap.key -> 'a State.t InvariantMap.t -> 'a option: extract the postcondition for a node id from the given invariant map

val extract_pre : InvariantMap.key -> 'a State.t InvariantMap.t -> 'a option: extract the precondition for a node id from the given invariant map

val extract_state : InvariantMap.key -> 'a InvariantMap.t -> 'a option: extract the state for a node id from the given invariant map