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

include S with type TransferFunctions.analysis_data = T.analysis_data and module TransferFunctions.CFG = T.CFG and type TransferFunctions.Domain.t = T.DisjDomain.t list * T.NonDisjDomain.t
module InvariantMap = TransferFunctions.CFG.Node.IdMap

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.

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

val get_cfg_metadata : unit -> DisjunctiveMetadata.t

return CFG-wide metadata about the analysis