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