sig
module Value_results :
sig
type results
val get_results : unit -> Eva.Value_results.results
val set_results : Eva.Value_results.results -> unit
val merge :
Eva.Value_results.results ->
Eva.Value_results.results -> Eva.Value_results.results
val change_callstacks :
(Value_types.callstack -> Value_types.callstack) ->
Eva.Value_results.results -> Eva.Value_results.results
end
module Value_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 Eval_terms :
sig
type eval_env
type logic_deps = Locations.Zone.t Cil_datatype.Logic_label.Map.t
type labels_states = Db.Value.state Cil_datatype.Logic_label.Map.t
val env_annot :
?c_labels:Eva.Eval_terms.labels_states ->
pre:Db.Value.state ->
here:Db.Value.state -> unit -> Eva.Eval_terms.eval_env
val predicate_deps :
Eva.Eval_terms.eval_env ->
Cil_types.predicate -> Eva.Eval_terms.logic_deps option
end
module Unit_tests : sig val run : unit -> 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 flow_annotation =
FlowSplit of Cil_types.term
| FlowMerge of Cil_types.term
val add_slevel_annot :
emitter:Emitter.t ->
loc:Cil_types.location ->
Cil_types.stmt -> Eva.Eva_annotations.slevel_annotation -> unit
val add_unroll_annot :
emitter:Emitter.t ->
loc:Cil_types.location ->
Cil_types.stmt -> Eva.Eva_annotations.unroll_annotation -> unit
val add_flow_annot :
emitter:Emitter.t ->
loc:Cil_types.location ->
Cil_types.stmt -> Eva.Eva_annotations.flow_annotation -> unit
val add_subdivision_annot :
emitter:Emitter.t ->
loc:Cil_types.location -> Cil_types.stmt -> int -> unit
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 = 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
end