Module `AbstractInterpreter.MakeDisjunctive`

In the disjunctive interpreter, the domain is a set of abstract states representing a disjunction between these states. The transfer functions are executed on each state in the disjunct independently. The join on the disjunctive state is governed by the policy described in DConfig.

Parameters

Signature

module TransferFunctions : TransferFunctions.SIL with type analysis_data = T.analysis_data and module CFG = T.CFG and type Domain.t = T.Domain.t list

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