functor
(AnalysisParam : sig
val kf : Cil_types.kernel_function
val initial_states : State_set.t
val active_behaviors : Eval_annots.ActiveBehaviors.t
end) ->
sig
val debug : bool
val name : string
val current_kf : Cil_types.kernel_function
val current_fundec : Cil_types.fundec
val return : Cil_types.stmt
val return_lv : Cil_types.lval option
val is_natural_loop : Cil_datatype.Stmt.Set.elt -> bool
val is_basic_loop : Cil_types.stmt -> bool
val is_loop : Cil_datatype.Stmt.Set.elt -> bool
val slevel_merge_after_loop : Value_parameters.SlevelMergeAfterLoop.t
val obviously_terminates : Value_parameters.ObviouslyTerminatesAll.t
val slevel : Per_stmt_slevel.slevel
val slevel : Cil_types.stmt -> int
val initial_state : Cvalue.Model.t
val current_table : Current_table.t
val states_after : Cvalue.Model.t Cil_datatype.Stmt.Hashtbl.t
val store_state_after_during_dataflow :
Cil_types.stmt -> Cil_types.stmt -> bool
val local_after_states :
Cvalue.Model.t Cil_datatype.Stmt.Hashtbl.t Lazy.t ->
Cvalue.Model.t Cil_datatype.Stmt.Hashtbl.t lazy_t
val merge_after :
Cvalue.Model.t Cil_datatype.Stmt.Hashtbl.t Lazy.t ->
Db.Value.callstack -> unit
val conditions_table : int Cil_datatype.Stmt.Hashtbl.t
val merge_results : unit -> Db.Value.Record_Value_After_Callbacks.result
type u = { mutable to_propagate : State_set.t; }
module StmtStartData :
sig
type data = u
val clear : unit -> unit
val mem : Cil_types.stmt -> bool
val find : Cil_types.stmt -> data
val replace : Cil_types.stmt -> data -> unit
val add : Cil_types.stmt -> data -> unit
val iter : (Cil_types.stmt -> data -> unit) -> unit
val length : unit -> int
end
val mark_degeneration : unit -> unit
type t = Eval_slevel.Computer.u
val copy : Eval_slevel.Computer.t -> Eval_slevel.Computer.t
val display_one : Format.formatter -> Eval_slevel.Computer.u -> unit
val pretty : Format.formatter -> Eval_slevel.Computer.t -> unit
val computeFirstPredecessor :
Cil_types.stmt -> Eval_slevel.Computer.u -> Eval_slevel.Computer.u
val counter_unroll_target : Value_parameters.ShowSlevel.t Pervasives.ref
val is_return : Cil_types.stmt -> bool
val combinePredecessors :
Cil_types.stmt ->
old:Eval_slevel.Computer.u ->
Eval_slevel.Computer.u -> Eval_slevel.Computer.u option
val clob : Locals_scoping.clobbered_set
val cacheable : Value_types.cacheable Pervasives.ref
val interp_call :
Cil_types.stmt ->
Cil_types.lval option ->
Cil_types.exp -> Cil_types.exp list -> State_set.t -> State_set.t
val doInstr :
Cil_types.stmt ->
Cil_types.instr -> Eval_slevel.Computer.t -> Eval_slevel.Computer.t
val doStmtSpecific : Cil_types.stmt -> 'a -> State_set.t -> State_set.t
val merge_if_loop : Cil_types.stmt -> Eval_slevel.Computer.t -> unit
val doStmt :
Cil_types.stmt ->
Eval_slevel.Computer.t -> Eval_slevel.Computer.u Dataflow2.stmtaction
val doEdge :
Cil_datatype.Stmt.Hashtbl.key ->
Cil_types.stmt -> Eval_slevel.Computer.u -> Eval_slevel.Computer.u
val checkConvergence : unit -> unit
val final_states : unit -> State_set.t
val externalize :
State_set.t -> (Cvalue.V_Offsetmap.t option * Cvalue.Model.t) list
val results : unit -> Value_types.call_result
val doGuardOneCond :
Cil_types.stmt ->
CilE.syntactic_context ->
Cil_types.exp ->
Eval_slevel.Computer.u -> Eval_slevel.Computer.u Dataflow2.guardaction
val mask_then : int
val mask_else : int
val mask_both : int
val doGuard :
Cil_datatype.Stmt.Hashtbl.key ->
Cil_types.exp ->
Eval_slevel.Computer.u ->
Eval_slevel.Computer.u Dataflow2.guardaction *
Eval_slevel.Computer.u Dataflow2.guardaction
end