sig
module Analysis :
sig
val compute : unit -> unit
val is_computed : unit -> bool
val self : State.t
type computation_state = NotComputed | Computing | Computed | Aborted
val current_computation_state : unit -> Eva.Analysis.computation_state
val register_computation_hook :
?on:Eva.Analysis.computation_state ->
(Eva.Analysis.computation_state -> unit) -> unit
type results = Complete | Partial | NoResults
type status =
Unreachable
| SpecUsed
| Builtin of string
| Analyzed of Eva.Analysis.results
val status : Cil_types.kernel_function -> Eva.Analysis.status
val use_spec_instead_of_definition : Cil_types.kernel_function -> bool
val save_results : Cil_types.kernel_function -> bool
end
module Results :
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
module Parameters :
sig
val enabled_domains : unit -> (string * string) list
val use_builtin : Cil_types.kernel_function -> string -> unit
val use_global_value_partitioning : Cil_types.varinfo -> unit
end
module Eva_annotations :
sig
type slevel_annotation =
SlevelMerge
| SlevelDefault
| SlevelLocal of int
| SlevelFull
type unroll_annotation = UnrollAmount of Cil_types.term | UnrollFull
type split_kind = Static | Dynamic
type split_term =
Expression of Cil_types.exp
| Predicate of Cil_types.predicate
type flow_annotation =
FlowSplit of Eva.Eva_annotations.split_term *
Eva.Eva_annotations.split_kind
| FlowMerge of Eva.Eva_annotations.split_term
type allocation_kind = By_stack | Fresh | Fresh_weak | Imprecise
type array_segmentation =
Cil_types.varinfo * Cil_types.offset * Cil_types.exp list
type domain_scope = string * Cil_types.varinfo list
val get_slevel_annot :
Cil_types.stmt -> Eva.Eva_annotations.slevel_annotation option
val get_unroll_annot :
Cil_types.stmt -> Eva.Eva_annotations.unroll_annotation list
val get_flow_annot :
Cil_types.stmt -> Eva.Eva_annotations.flow_annotation list
val get_subdivision_annot : Cil_types.stmt -> int list
val get_allocation :
Cil_types.stmt -> Eva.Eva_annotations.allocation_kind
val add_slevel_annot :
emitter:Emitter.t ->
Cil_types.stmt -> Eva.Eva_annotations.slevel_annotation -> unit
val add_unroll_annot :
emitter:Emitter.t ->
Cil_types.stmt -> Eva.Eva_annotations.unroll_annotation -> unit
val add_flow_annot :
emitter:Emitter.t ->
Cil_types.stmt -> Eva.Eva_annotations.flow_annotation -> unit
val add_subdivision_annot :
emitter:Emitter.t -> Cil_types.stmt -> int -> unit
val add_array_segmentation :
emitter:Emitter.t ->
Cil_types.stmt -> Eva.Eva_annotations.array_segmentation -> unit
val add_domain_scope :
emitter:Emitter.t ->
Cil_types.stmt -> Eva.Eva_annotations.domain_scope -> unit
end
module Eval : sig type cacheable = Cacheable | NoCache | NoCacheCallers end
module Builtins :
sig
exception Invalid_nb_of_args of int
exception Outside_builtin_possibilities
type builtin_type = unit -> Cil_types.typ * Cil_types.typ list
type cacheable =
Eva.Eval.cacheable =
Cacheable
| NoCache
| NoCacheCallers
type full_result = {
c_values : (Cvalue.V.t option * Cvalue.Model.t) list;
c_clobbered : Base.SetLattice.t;
c_from : (Function_Froms.froms * Locations.Zone.t) option;
}
type call_result =
States of Cvalue.Model.t list
| Result of Cvalue.V.t list
| Full of Eva.Builtins.full_result
type builtin =
Cvalue.Model.t ->
(Cil_types.exp * Cvalue.V.t) list -> Eva.Builtins.call_result
val register_builtin :
string ->
?replace:string ->
?typ:Eva.Builtins.builtin_type ->
Eva.Builtins.cacheable -> Eva.Builtins.builtin -> unit
val is_builtin : string -> bool
end
module Eval_terms :
sig
val annot_predicate_deps :
pre:Cvalue.Model.t ->
here:Cvalue.Model.t -> Cil_types.predicate -> Locations.Zone.t option
end
module Eva_results :
sig
type results
val get_results : unit -> Eva.Eva_results.results
val set_results : Eva.Eva_results.results -> unit
val merge :
Eva.Eva_results.results ->
Eva.Eva_results.results -> Eva.Eva_results.results
val change_callstacks :
(Value_types.callstack -> Value_types.callstack) ->
Eva.Eva_results.results -> Eva.Eva_results.results
end
module Unit_tests : sig val run : unit -> unit end
end