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
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
end