sig
val are_available : Cil_types.kernel_function -> bool
type callstack = (Cil_types.kernel_function * Cil_types.kinstr) list
type request
type value
type address
type 'a evaluation
type error = Bottom | Top | DisabledDomain
type 'a result = ('a, Results.error) Result.t
val string_of_error : Results.error -> string
val pretty_error : Stdlib.Format.formatter -> Results.error -> unit
val pretty_result :
(Stdlib.Format.formatter -> 'a -> unit) ->
Stdlib.Format.formatter -> 'a Results.result -> unit
val default : 'a -> 'a Results.result -> 'a
val at_start : Results.request
val at_end : unit -> Results.request
val at_start_of : Cil_types.kernel_function -> Results.request
val at_end_of : Cil_types.kernel_function -> Results.request
val before : Cil_types.stmt -> Results.request
val after : Cil_types.stmt -> Results.request
val before_kinstr : Cil_types.kinstr -> Results.request
val in_callstack : Results.callstack -> Results.request -> Results.request
val in_callstacks :
Results.callstack list -> Results.request -> Results.request
val filter_callstack :
(Results.callstack -> bool) -> Results.request -> Results.request
val callstacks : Results.request -> Results.callstack list
val by_callstack :
Results.request -> (Results.callstack * Results.request) list
val equality_class :
Cil_types.exp -> Results.request -> Cil_types.exp list Results.result
val get_cvalue_model : Results.request -> Cvalue.Model.t
val get_cvalue_model_result :
Results.request -> Cvalue.Model.t Results.result
val expr_deps : Cil_types.exp -> Results.request -> Locations.Zone.t
val lval_deps : Cil_types.lval -> Results.request -> Locations.Zone.t
val address_deps : Cil_types.lval -> Results.request -> Locations.Zone.t
val eval_var :
Cil_types.varinfo -> Results.request -> Results.value Results.evaluation
val eval_lval :
Cil_types.lval -> Results.request -> Results.value Results.evaluation
val eval_exp :
Cil_types.exp -> Results.request -> Results.value Results.evaluation
val eval_address :
?for_writing:bool ->
Cil_types.lval -> Results.request -> Results.address Results.evaluation
val eval_callee :
Cil_types.exp -> Results.request -> Kernel_function.t list Results.result
val as_int : Results.value Results.evaluation -> int Results.result
val as_integer :
Results.value Results.evaluation -> Integer.t Results.result
val as_float : Results.value Results.evaluation -> float Results.result
val as_ival : Results.value Results.evaluation -> Ival.t Results.result
val as_fval : Results.value Results.evaluation -> Fval.t Results.result
val as_cvalue : Results.value Results.evaluation -> Cvalue.V.t
val as_cvalue_result :
Results.value Results.evaluation -> Cvalue.V.t Results.result
val as_cvalue_or_uninitialized :
Results.value Results.evaluation -> Cvalue.V_Or_Uninitialized.t
val as_location :
Results.address Results.evaluation -> Locations.location Results.result
val as_zone : Results.address Results.evaluation -> Locations.Zone.t
val as_zone_result :
Results.address Results.evaluation -> Locations.Zone.t Results.result
val is_singleton : 'a Results.evaluation -> bool
val is_initialized : Results.value Results.evaluation -> bool
val alarms : 'a Results.evaluation -> Alarms.t list
val is_empty : Results.request -> bool
val is_bottom : 'a Results.evaluation -> bool
val is_called : Cil_types.kernel_function -> bool
val is_reachable : Cil_types.stmt -> bool
val is_reachable_kinstr : Cil_types.kinstr -> bool
val condition_truth_value : Cil_types.stmt -> bool * bool
val callers : Cil_types.kernel_function -> Cil_types.kernel_function list
val callsites :
Cil_types.kernel_function ->
(Cil_types.kernel_function * Cil_types.stmt list) list
val callee : Cil_types.stmt -> Kernel_function.t list
end