sig
type state = Cvalue.Model.t
type t = Cvalue.V.t
exception Aborted
val emitter : Emitter.t Pervasives.ref
val self : State.t
val mark_as_computed : unit -> unit
val compute : (unit -> unit) Pervasives.ref
val is_computed : unit -> bool
module Table_By_Callstack :
sig
val self : State.t
val name : string
val mark_as_computed : ?project:Project.t -> unit -> unit
val is_computed : ?project:Project.t -> unit -> bool
module Datatype : Datatype.S
val add_hook_on_update : (Datatype.t -> unit) -> unit
val howto_marshal : (Datatype.t -> 'a) -> ('a -> Datatype.t) -> unit
type key = Cil_types.stmt
type data = state Value_types.Callstack.Hashtbl.t
val replace : key -> data -> unit
val add : key -> data -> unit
val clear : unit -> unit
val length : unit -> int
val iter : (key -> data -> unit) -> unit
val iter_sorted :
?cmp:(key -> key -> int) -> (key -> data -> unit) -> unit
val fold : (key -> data -> 'a -> 'a) -> 'a -> 'a
val fold_sorted :
?cmp:(key -> key -> int) -> (key -> data -> 'a -> 'a) -> 'a -> 'a
val memo : ?change:(data -> data) -> (key -> data) -> key -> data
val find : key -> data
val find_all : key -> data list
val mem : key -> bool
val remove : key -> unit
end
module AfterTable_By_Callstack :
sig
val self : State.t
val name : string
val mark_as_computed : ?project:Project.t -> unit -> unit
val is_computed : ?project:Project.t -> unit -> bool
module Datatype : Datatype.S
val add_hook_on_update : (Datatype.t -> unit) -> unit
val howto_marshal : (Datatype.t -> 'a) -> ('a -> Datatype.t) -> unit
type key = Cil_types.stmt
type data = state Value_types.Callstack.Hashtbl.t
val replace : key -> data -> unit
val add : key -> data -> unit
val clear : unit -> unit
val length : unit -> int
val iter : (key -> data -> unit) -> unit
val iter_sorted :
?cmp:(key -> key -> int) -> (key -> data -> unit) -> unit
val fold : (key -> data -> 'a -> 'a) -> 'a -> 'a
val fold_sorted :
?cmp:(key -> key -> int) -> (key -> data -> 'a -> 'a) -> 'a -> 'a
val memo : ?change:(data -> data) -> (key -> data) -> key -> data
val find : key -> data
val find_all : key -> data list
val mem : key -> bool
val remove : key -> unit
end
val ignored_recursive_call : Cil_types.kernel_function -> bool
val condition_truth_value : Cil_types.stmt -> bool * bool
exception Outside_builtin_possibilities
type builtin_sig =
Db.Value.state ->
(Cil_types.exp * Cvalue.V.t * Cvalue.V_Offsetmap.t) list ->
Value_types.call_result
val register_builtin :
(string -> ?replace:string -> Db.Value.builtin_sig -> unit)
Pervasives.ref
val registered_builtins :
(unit -> (string * Db.Value.builtin_sig) list) Pervasives.ref
val mem_builtin : (string -> bool) Pervasives.ref
val use_spec_instead_of_definition :
(Cil_types.kernel_function -> bool) Pervasives.ref
val fun_set_args : Db.Value.t list -> unit
val fun_use_default_args : unit -> unit
val fun_get_args : unit -> Db.Value.t list option
exception Incorrect_number_of_arguments
val globals_set_initial_state : Db.Value.state -> unit
val globals_use_default_initial_state : unit -> unit
val globals_state : unit -> Db.Value.state
val globals_use_supplied_state : unit -> bool
val get_initial_state : Cil_types.kernel_function -> Db.Value.state
val get_initial_state_callstack :
Cil_types.kernel_function ->
Db.Value.state Value_types.Callstack.Hashtbl.t option
val get_state : ?after:bool -> Cil_types.kinstr -> Db.Value.state
val get_stmt_state_callstack :
after:bool ->
Cil_types.stmt -> Db.Value.state Value_types.Callstack.Hashtbl.t option
val get_stmt_state : ?after:bool -> Cil_types.stmt -> Db.Value.state
val fold_stmt_state_callstack :
(Db.Value.state -> 'a -> 'a) -> 'a -> after:bool -> Cil_types.stmt -> 'a
val fold_state_callstack :
(Db.Value.state -> 'a -> 'a) ->
'a -> after:bool -> Cil_types.kinstr -> 'a
val find : Db.Value.state -> Locations.location -> Db.Value.t
val eval_lval :
(?with_alarms:CilE.warn_mode ->
Locations.Zone.t option ->
Db.Value.state -> Cil_types.lval -> Locations.Zone.t option * Db.Value.t)
Pervasives.ref
val eval_expr :
(?with_alarms:CilE.warn_mode ->
Db.Value.state -> Cil_types.exp -> Db.Value.t)
Pervasives.ref
val eval_expr_with_state :
(?with_alarms:CilE.warn_mode ->
Db.Value.state -> Cil_types.exp -> Db.Value.state * Db.Value.t)
Pervasives.ref
val reduce_by_cond :
(Db.Value.state -> Cil_types.exp -> bool -> Db.Value.state)
Pervasives.ref
val find_lv_plus :
(Cvalue.Model.t -> Cil_types.exp -> (Cil_types.lval * Ival.t) list)
Pervasives.ref
val expr_to_kernel_function :
(Cil_types.kinstr ->
?with_alarms:CilE.warn_mode ->
deps:Locations.Zone.t option ->
Cil_types.exp -> Locations.Zone.t * Kernel_function.Hptset.t)
Pervasives.ref
val expr_to_kernel_function_state :
(Db.Value.state ->
deps:Locations.Zone.t option ->
Cil_types.exp -> Locations.Zone.t * Kernel_function.Hptset.t)
Pervasives.ref
exception Not_a_call
val call_to_kernel_function : Cil_types.stmt -> Kernel_function.Hptset.t
val valid_behaviors :
(Cil_types.kernel_function ->
Db.Value.state -> Cil_types.funbehavior list)
Pervasives.ref
val add_formals_to_state :
(Db.Value.state ->
Cil_types.kernel_function -> Cil_types.exp list -> Db.Value.state)
Pervasives.ref
val is_accessible : Cil_types.kinstr -> bool
val is_reachable : Db.Value.state -> bool
val is_reachable_stmt : Cil_types.stmt -> bool
exception Void_Function
val find_return_loc : Cil_types.kernel_function -> Locations.location
val is_called : (Cil_types.kernel_function -> bool) Pervasives.ref
val callers :
(Cil_types.kernel_function ->
(Cil_types.kernel_function * Cil_types.stmt list) list)
Pervasives.ref
val access :
(Cil_types.kinstr -> Cil_types.lval -> Db.Value.t) Pervasives.ref
val access_expr :
(Cil_types.kinstr -> Cil_types.exp -> Db.Value.t) Pervasives.ref
val access_location :
(Cil_types.kinstr -> Locations.location -> Db.Value.t) Pervasives.ref
val lval_to_loc :
(Cil_types.kinstr ->
?with_alarms:CilE.warn_mode -> Cil_types.lval -> Locations.location)
Pervasives.ref
val lval_to_loc_with_deps :
(Cil_types.kinstr ->
?with_alarms:CilE.warn_mode ->
deps:Locations.Zone.t ->
Cil_types.lval -> Locations.Zone.t * Locations.location)
Pervasives.ref
val lval_to_loc_with_deps_state :
(Db.Value.state ->
deps:Locations.Zone.t ->
Cil_types.lval -> Locations.Zone.t * Locations.location)
Pervasives.ref
val lval_to_loc_state :
(Db.Value.state -> Cil_types.lval -> Locations.location) Pervasives.ref
val lval_to_offsetmap :
(Cil_types.kinstr ->
?with_alarms:CilE.warn_mode ->
Cil_types.lval -> Cvalue.V_Offsetmap.t option)
Pervasives.ref
val lval_to_offsetmap_state :
(Db.Value.state -> Cil_types.lval -> Cvalue.V_Offsetmap.t option)
Pervasives.ref
val lval_to_zone :
(Cil_types.kinstr ->
?with_alarms:CilE.warn_mode -> Cil_types.lval -> Locations.Zone.t)
Pervasives.ref
val lval_to_zone_state :
(Db.Value.state -> Cil_types.lval -> Locations.Zone.t) Pervasives.ref
val lval_to_zone_with_deps_state :
(Db.Value.state ->
for_writing:bool ->
deps:Locations.Zone.t option ->
Cil_types.lval -> Locations.Zone.t * Locations.Zone.t * bool)
Pervasives.ref
val lval_to_precise_loc_state :
(?with_alarms:CilE.warn_mode ->
Db.Value.state ->
Cil_types.lval ->
Db.Value.state * Precise_locs.precise_location * Cil_types.typ)
Pervasives.ref
val lval_to_precise_loc_with_deps_state :
(Db.Value.state ->
deps:Locations.Zone.t option ->
Cil_types.lval -> Locations.Zone.t * Precise_locs.precise_location)
Pervasives.ref
val assigns_inputs_to_zone :
(Db.Value.state -> Cil_types.assigns -> Locations.Zone.t) Pervasives.ref
val assigns_outputs_to_zone :
(Db.Value.state ->
result:Cil_types.varinfo option -> Cil_types.assigns -> Locations.Zone.t)
Pervasives.ref
val assigns_outputs_to_locations :
(Db.Value.state ->
result:Cil_types.varinfo option ->
Cil_types.assigns -> Locations.location list)
Pervasives.ref
val verify_assigns_froms :
(Kernel_function.t -> pre:Db.Value.state -> Function_Froms.t -> unit)
Pervasives.ref
module Logic :
sig
val eval_predicate :
(pre:Db.Value.state ->
here:Db.Value.state ->
Cil_types.predicate -> Property_status.emitted_status)
Pervasives.ref
end
type callstack = Value_types.callstack
module Record_Value_Callbacks :
sig
type param = callstack * state Cil_datatype.Stmt.Hashtbl.t Lazy.t
type result = unit
val extend : (param -> result) -> unit
val extend_once : (param -> result) -> unit
val apply : param -> result
val is_empty : unit -> bool
val clear : unit -> unit
val length : unit -> int
end
module Record_Value_Superposition_Callbacks :
sig
type param = callstack * state list Cil_datatype.Stmt.Hashtbl.t Lazy.t
type result = unit
val extend : (param -> result) -> unit
val extend_once : (param -> result) -> unit
val apply : param -> result
val is_empty : unit -> bool
val clear : unit -> unit
val length : unit -> int
end
module Record_Value_After_Callbacks :
sig
type param = callstack * state Cil_datatype.Stmt.Hashtbl.t Lazy.t
type result = unit
val extend : (param -> result) -> unit
val extend_once : (param -> result) -> unit
val apply : param -> result
val is_empty : unit -> bool
val clear : unit -> unit
val length : unit -> int
end
module Record_Value_Callbacks_New :
sig
type param =
callstack *
(state Cil_datatype.Stmt.Hashtbl.t Lazy.t *
state Cil_datatype.Stmt.Hashtbl.t Lazy.t)
Value_types.callback_result
type result = unit
val extend : (param -> result) -> unit
val extend_once : (param -> result) -> unit
val apply : param -> result
val is_empty : unit -> bool
val clear : unit -> unit
val length : unit -> int
end
val no_results : (Cil_types.fundec -> bool) Pervasives.ref
module Call_Value_Callbacks :
sig
type param = state * callstack
type result = unit
val extend : (param -> result) -> unit
val extend_once : (param -> result) -> unit
val apply : param -> result
val is_empty : unit -> bool
val clear : unit -> unit
val length : unit -> int
end
module Call_Type_Value_Callbacks :
sig
type param =
[ `Builtin of Value_types.call_result
| `Def
| `Memexec
| `Spec of Cil_types.funspec ] * state * callstack
type result = unit
val extend : (param -> result) -> unit
val extend_once : (param -> result) -> unit
val apply : param -> result
val is_empty : unit -> bool
val clear : unit -> unit
val length : unit -> int
end
module Compute_Statement_Callbacks :
sig
type param = Cil_types.stmt * callstack * state list
type result = unit
val extend : (param -> result) -> unit
val extend_once : (param -> result) -> unit
val apply : param -> result
val is_empty : unit -> bool
val clear : unit -> unit
val length : unit -> int
end
val rm_asserts : (unit -> unit) Pervasives.ref
val pretty : Format.formatter -> Db.Value.t -> unit
val pretty_state : Format.formatter -> Db.Value.state -> unit
val display :
(Format.formatter -> Cil_types.kernel_function -> unit) Pervasives.ref
val noassert_get_state : ?after:bool -> Cil_types.kinstr -> Db.Value.state
val recursive_call_occurred : Cil_types.kernel_function -> unit
val merge_conditions : int Cil_datatype.Stmt.Hashtbl.t -> unit
val mask_then : int
val mask_else : int
val initial_state_only_globals : (unit -> Db.Value.state) Pervasives.ref
val update_callstack_table :
after:bool ->
Cil_types.stmt -> Db.Value.callstack -> Db.Value.state -> unit
val memoize : (Cil_types.kernel_function -> unit) Pervasives.ref
val merge_initial_state : Db.Value.callstack -> Db.Value.state -> unit
val initial_state_changed : (unit -> unit) Pervasives.ref
end