AbstractInterpreter.MakeBackwardRPO
module T : TransferFunctions
module TransferFunctions = 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