AbstractInterpreter.MakeDisjunctiveIn 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.
module T : TransferFunctions.DisjReadyinclude 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.tmodule TransferFunctions :
TransferFunctions.SIL
with type analysis_data = T.analysis_data
with module CFG = T.CFG
with type Domain.t = T.DisjDomain.t list * T.NonDisjDomain.tmodule InvariantMap = TransferFunctions.CFG.Node.IdMaptype invariant_map = TransferFunctions.Domain.t State.t InvariantMap.tinvariant 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 optioncompute 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_mapcompute 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_mapcompute and return invariant map for the given procedure starting from initial
val extract_post :
TransferFunctions.CFG.Node.id ->
'a State.t InvariantMap.t ->
'a optionextract the postcondition for a node id from the given invariant map
val extract_pre :
TransferFunctions.CFG.Node.id ->
'a State.t InvariantMap.t ->
'a optionextract the precondition for a node id from the given invariant map
val extract_state :
TransferFunctions.CFG.Node.id ->
'a InvariantMap.t ->
'a optionextract the state for a node id from the given invariant map
val get_cfg_metadata : unit -> DisjunctiveMetadata.treturn CFG-wide metadata about the analysis