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
.
module T : TransferFunctions.DisjReady
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 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.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
val get_cfg_metadata : unit -> DisjunctiveMetadata.t
return CFG-wide metadata about the analysis