diff --git a/.gitattributes b/.gitattributes
index 814b5192782889c63c4185edd2b033ca4b1e8c05..0a54755f6279846d8f92196e3766d9657c6ef3df 100644
--- a/.gitattributes
+++ b/.gitattributes
@@ -91,9 +91,7 @@ Make* header_spec=CEA_LGPL
*.js header_spec=CEA_LGPL
*.ml header_spec=CEA_LGPL
-*.ml.in header_spec=CEA_LGPL
*.mli header_spec=CEA_LGPL
-*.mli.in header_spec=CEA_LGPL
*.mll header_spec=CEA_LGPL
*.mly header_spec=CEA_LGPL
diff --git a/.gitignore b/.gitignore
index 49567453cf9a0f1ae1c1923e222e49c40f753a6c..d51531fef5e9551be01a4aa9b5cfe8b3dc047750 100644
--- a/.gitignore
+++ b/.gitignore
@@ -208,7 +208,6 @@ Makefile.plugin.generated
/src/plugins/gui/GSourceView.mli
/src/plugins/gui/gtk_compat.ml
/src/plugins/markdown-report/META
-/src/plugins/eva/Eva.mli
# generated tar.gz files
diff --git a/src/plugins/eva/Eva.ml.in b/src/plugins/eva/Eva.header
similarity index 64%
rename from src/plugins/eva/Eva.ml.in
rename to src/plugins/eva/Eva.header
index 9931040bf9c5e1673271d57bac9d1f99a26c09d9..4976cba0a115437862d21e95989fb39c206b2319 100644
--- a/src/plugins/eva/Eva.ml.in
+++ b/src/plugins/eva/Eva.header
@@ -20,28 +20,19 @@
(* *)
(**************************************************************************)
-module Private = struct
- module Abstractions = Eva__Abstractions
- module Analysis = Eva__Analysis
- module Alarmset = Eva__Alarmset
- module Parameters = Parameters
- module Main_values = Eva__Main_values
- module Eval = Eva__Eval
- module Eval_terms = Eva__Eval_terms
- module Eva_utils = Eva_utils
- module Eva_results = Eva_results
- module Self = Self
- module Red_statuses = Eva__Red_statuses
- module Abstract_value = Eva__Abstract_value
- module Abstract_domain = Eva__Abstract_domain
- module Active_behaviors = Active_behaviors
- module Function_calls = Function_calls
- module Simple_memory = Eva__Simple_memory
- module Structure = Eva__Structure
- module Eval_typ = Eva__Eval_typ
- module Eval_op = Eva__Eval_op
- module Domain_builder = Eva__Domain_builder
- module Main_locations = Eva__Main_locations
- module Eval_annots = Eva__Eval_annots
- module Eva_dynamic = Eva_dynamic
-end
+(** Eva public API.
+
+ The main modules are:
+ - Analysis: run the analysis.
+ - Results: access analysis results, especially the values of expressions
+ and memory locations of lvalues at each program point.
+
+ The following modules allow configuring the Eva analysis:
+ - Parameters: change the configuration of the analysis.
+ - Eva_annotations: add local annotations to guide the analysis.
+ - Builtins: register ocaml builtins to be used by the cvalue domain
+ instead of analysing the body of some C functions.
+
+ Other modules are for internal use only. *)
+
+(* This file is generated. Do not edit. *)
diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
new file mode 100644
index 0000000000000000000000000000000000000000..fc8896e0d68517d862d8a0670e7605de21fff13f
--- /dev/null
+++ b/src/plugins/eva/Eva.mli
@@ -0,0 +1,641 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2022 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** Eva public API.
+
+ The main modules are:
+ - Analysis: run the analysis.
+ - Results: access analysis results, especially the values of expressions
+ and memory locations of lvalues at each program point.
+
+ The following modules allow configuring the Eva analysis:
+ - Parameters: change the configuration of the analysis.
+ - Eva_annotations: add local annotations to guide the analysis.
+ - Builtins: register ocaml builtins to be used by the cvalue domain
+ instead of analysing the body of some C functions.
+
+ Other modules are for internal use only. *)
+
+(* This file is generated. Do not edit. *)
+
+module Analysis: sig
+ val compute : unit -> unit
+ (** Computes the Eva analysis, if not already computed, using the entry point
+ of the current project. You may set it with {!Globals.set_entry_point}.
+ @raise Globals.No_such_entry_point if the entry point is incorrect
+ @raise Db.Value.Incorrect_number_of_arguments if some arguments are
+ specified for the entry point using {!Db.Value.fun_set_args}, and
+ an incorrect number of them is given.
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
+
+ val is_computed : unit -> bool
+ (** Return [true] iff the Eva analysis has been done.
+ @plugin development guide
+ *)
+
+ val self : State.t
+ (** Internal state of Eva analysis from projects viewpoint. *)
+
+ type computation_state = NotComputed | Computing | Computed | Aborted
+ (** Computation state of the analysis. *)
+
+ val current_computation_state : unit -> computation_state
+ (** Get the current computation state of the analysis, updated by
+ [force_compute] and states updates. *)
+
+ val register_computation_hook: ?on:computation_state ->
+ (computation_state -> unit) -> unit
+ (** Registers a hook that will be called each time the analysis starts or
+ finishes. If [on] is given, the hook will only be called when the
+ analysis switches to this specific state. *)
+
+ (** Kind of results for the analysis of a function body. *)
+ type results =
+ | Complete
+ (** The results are complete: they cover all possible call contexts of the
+ given function. *)
+ | Partial
+ (** The results are partial, as the functions has not been analyzed in all
+ possible call contexts. This happens for recursive functions that are
+ not completely unrolled, or if the analysis has stopped unexpectedly. *)
+ | NoResults
+ (** No results were saved for the function, due to option -eva-no-results.
+ Any request at a statement of this function will lead to a Top result. *)
+
+ (* Analysis status of a function. *)
+ type status =
+ | Unreachable
+ (** The function has not been reached by the analysis. Any request in this
+ function will lead to a Bottom result. *)
+ | SpecUsed
+ (** The function specification has been used to interpret its calls:
+ its body has not been analyzed. Any request at a statement of this
+ function will lead to a Bottom result. *)
+ | Builtin of string
+ (** The builtin of the given name has been used to interpret the function:
+ its body has not been analyzed. Any request at a statement of this
+ function will lead to a Bottom result. *)
+ | Analyzed of results
+ (** The function body has been analyzed. *)
+
+ (** Returns the analysis status of a given function. *)
+ val status: Cil_types.kernel_function -> status
+
+ (** Does the analysis ignores the body of a given function, and uses instead
+ its specification or a builtin to interpret it?
+ Please use {!Eva.Results.are_available} instead to known whether results
+ are available for a given function. *)
+ val use_spec_instead_of_definition: Cil_types.kernel_function -> bool
+
+ (** Returns [true] if the user has requested that no results should be recorded
+ for the given function. Please use {!Eva.Results.are_available} instead
+ to known whether results are available for a given function. *)
+ val save_results: Cil_types.kernel_function -> bool
+end
+
+module Results: sig
+
+ (** Eva's result API is a new interface to access the results of an analysis,
+ once it is completed. It may slightly change in the future. It aims at
+ replacing most uses of [Db.Value], and has some advantages over Db's :
+
+ - evaluations uses every available domains and not only Cvalue;
+ - the caller may distinguish failure cases when a request is unsucessful;
+ - working with callstacks is easy;
+ - some common shortcuts are provided (e.g. for extracting ival directly);
+ - overall, individual functions are simpler.
+
+ The idea behind this API is that requests must be decomposed in several
+ steps. For instance, to evaluate an expression :
+
+ 1. first, you have to state where you want to evaluate it,
+ 2. optionally, you may specify in which callstack,
+ 3. you choose the expression to evaluate,
+ 4. you require a destination type to evaluate into.
+
+ Usage sketch :
+
+ Eva.Results.(
+ before stmt |> in_callstack cs |>
+ eval_var vi |> as_int |> default 0)
+
+ or equivalently, if you prefer
+
+ Eva.Results.(
+ default O (as_int (eval_var vi (in_callstack cs (before stmt))))
+ *)
+
+ (** Are results available for a given function? True if the function body has
+ been has been analyzed and the results have been saved.
+ False if:
+ - the function has not been reached by the analysis: all requests in the
+ function will lead to a Bottom error.
+ - a specification or a builtin has been used instead of analyzing the
+ function body: all requests in the function will lead to a Bottom error.
+ - results have not been saved, due to the [-eva-no-results] parameter:
+ all requests in the function will lead to a Top error. *)
+ 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,error) Result.t
+
+
+ (** Results handling *)
+
+ (** Translates an error to a human readable string. *)
+ val string_of_error : error -> string
+
+ (** Pretty printer for errors. *)
+ val pretty_error : Format.formatter -> error -> unit
+
+ (** Pretty printer for API's results. *)
+ val pretty_result : (Format.formatter -> 'a -> unit) ->
+ Format.formatter -> 'a result -> unit
+
+ (** [default d r] extracts the value of [r] if [r] is Ok,
+ or use the default value [d] otherwise.
+ Equivalent to [Result.value ~default:d r] *)
+ val default : 'a -> 'a result -> 'a
+
+
+ (** Control point selection *)
+
+ (** At the start of the analysis, but after the initialization of globals. *)
+ val at_start : request
+
+ (** At the end of the analysis, after the main function has returned. *)
+ val at_end : unit -> request
+
+ (** At the start of the given function. *)
+ val at_start_of : Cil_types.kernel_function -> request
+
+ (** At the end of the given function.
+ @raises Kernel_function.No_statement if the function has no body. *)
+ val at_end_of : Cil_types.kernel_function -> request
+
+ (** Just before a statement is executed. *)
+ val before : Cil_types.stmt -> request
+
+ (** Just after a statement is executed. *)
+ val after : Cil_types.stmt -> request
+
+ (** Just before a statement or at the start of the analysis. *)
+ val before_kinstr : Cil_types.kinstr -> request
+
+
+ (** Callstack selection *)
+
+ (** Only consider the given callstack.
+ Replaces previous calls to [in_callstack] or [in_callstacks]. *)
+ val in_callstack : callstack -> request -> request
+
+ (** Only consider the callstacks from the given list.
+ Replaces previous calls to [in_callstack] or [in_callstacks]. *)
+ val in_callstacks : callstack list -> request -> request
+
+ (** Only consider callstacks satisfying the given predicate. Several filters
+ can be added. If callstacks are also selected with [in_callstack] or
+ [in_callstacks], only the selected callstacks will be filtered. *)
+ val filter_callstack : (callstack -> bool) -> request -> request
+
+
+ (** Working with callstacks *)
+
+ (** Returns the list of reachable callstacks from the given request.
+ An empty list is returned if the request control point has not been
+ reached by the analysis, or if no information has been saved at this point
+ (for instance with the -eva-no-results option).
+ Use [is_empty request] to distinguish these two cases. *)
+ val callstacks : request -> callstack list
+
+ (** Returns a list of subrequests for each reachable callstack from
+ the given request. *)
+ val by_callstack : request -> (callstack * request) list
+
+
+ (** State requests *)
+
+ (** Returns the list of expressions which have been inferred to be equal to
+ the given expression by the Equality domain. *)
+ val equality_class : Cil_types.exp -> request -> Cil_types.exp list result
+
+ (** Returns the Cvalue state. Error cases are converted into the bottom or top
+ cvalue state accordingly. *)
+ val get_cvalue_model : request -> Cvalue.Model.t
+
+ (** Returns the Cvalue model. *)
+ val get_cvalue_model_result : request -> Cvalue.Model.t result
+
+ (** Returns a textual representation of the internal domain states for the given
+ request. If [filter] is provided, states are filtered on the given bases
+ (for domains that support this feature).
+ Returns a list of pair (name, state) for all available domains. *)
+ val print_states: ?filter:Base.Hptset.t -> request -> (string * string) list
+
+ (** Dependencies *)
+
+ (** Computes (an overapproximation of) the memory zones that must be read to
+ evaluate the given expression, including all adresses computations. *)
+ val expr_deps : Cil_types.exp -> request -> Locations.Zone.t
+
+ (** Computes (an overapproximation of) the memory zones that must be read to
+ evaluate the given lvalue, including the lvalue zone itself. *)
+ val lval_deps : Cil_types.lval -> request -> Locations.Zone.t
+
+ (** Computes (an overapproximation of) the memory zones that must be read to
+ evaluate the given lvalue, excluding the lvalue zone itself. *)
+ val address_deps : Cil_types.lval -> request -> Locations.Zone.t
+
+
+ (** Evaluation *)
+
+ (** Returns (an overapproximation of) the possible values of the variable. *)
+ val eval_var : Cil_types.varinfo -> request -> value evaluation
+
+ (** Returns (an overapproximation of) the possible values of the lvalue. *)
+ val eval_lval : Cil_types.lval -> request -> value evaluation
+
+ (** Returns (an overapproximation of) the possible values of the expression. *)
+ val eval_exp : Cil_types.exp -> request -> value evaluation
+
+
+ (** Returns (an overapproximation of) the possible addresses of the lvalue. *)
+ val eval_address : ?for_writing:bool ->
+ Cil_types.lval -> request -> address evaluation
+
+
+ (** Returns the kernel functions into which the given expression may evaluate.
+ If the callee expression doesn't always evaluate to a function, those
+ spurious values are ignored. If it always evaluate to a non-function value
+ then the returned list is empty.
+ Raises [Stdlib.Invalid_argument] if the callee expression is not an lvalue
+ without offset.
+ Also see [callee] for a function which applies directly on Call
+ statements. *)
+ val eval_callee : Cil_types.exp -> request -> Kernel_function.t list result
+
+
+ (** Evaluated values conversion *)
+
+ (** In all functions below, if the abstract value inferred by Eva does not fit
+ in the required type, [Error Top] is returned, as Top is the only possible
+ over-approximation of the request. *)
+
+ (** Converts the value into a singleton ocaml int. *)
+ val as_int : value evaluation -> int result
+
+ (** Converts the value into a singleton unbounded integer. *)
+ val as_integer : value evaluation -> Integer.t result
+
+ (** Converts the value into a floating point number. *)
+ val as_float : value evaluation -> float result
+
+ (** Converts the value into a C number abstraction. *)
+ val as_ival : value evaluation -> Ival.t result
+
+ (** Converts the value into a floating point abstraction. *)
+ val as_fval : value evaluation -> Fval.t result
+
+ (** Converts the value into a Cvalue abstraction. Converts error cases
+ into bottom and top values accordingly. *)
+ val as_cvalue : value evaluation -> Cvalue.V.t
+
+ (** Converts the value into a Cvalue abstraction. *)
+ val as_cvalue_result : value evaluation -> Cvalue.V.t result
+
+ (** Converts the value into a Cvalue abstraction with 'undefined' and 'escaping
+ addresses' flags. *)
+ val as_cvalue_or_uninitialized : value evaluation -> Cvalue.V_Or_Uninitialized.t
+
+
+ (** Converts into a C location abstraction. *)
+ val as_location : address evaluation -> Locations.location result
+
+ (** Converts into a Zone. Error cases are converted into bottom or top zones
+ accordingly. *)
+ val as_zone: address evaluation -> Locations.Zone.t
+
+ (** Converts into a Zone result. *)
+ val as_zone_result : address evaluation -> Locations.Zone.t result
+
+
+ (** Evaluation properties *)
+
+
+ (** Does the evaluated abstraction represents only one possible C value or
+ memory location? *)
+ val is_singleton : 'a evaluation -> bool
+
+ (** Returns whether the evaluated value is initialized or not. If the value have
+ been evaluated from a Cil expression, it is always initialized. *)
+ val is_initialized : value evaluation -> bool
+
+ (** Returns the set of alarms emitted during the evaluation. *)
+ val alarms : 'a evaluation -> Alarms.t list
+
+
+ (** Reachability *)
+
+ (** Returns true if there are no reachable states for the given request. *)
+ val is_empty : request -> bool
+
+ (** Returns true if an evaluation leads to bottom, i.e. if the given expression
+ or lvalue cannot be evaluated to a valid result for the given request. *)
+ val is_bottom : 'a evaluation -> bool
+
+ (** Returns true if the function has been analyzed. *)
+ val is_called : Cil_types.kernel_function -> bool
+
+ (** Returns true if the statement has been reached by the analysis. *)
+ val is_reachable : Cil_types.stmt -> bool
+
+ (** Returns true if the statement has been reached by the analysis, or if
+ the main function has been analyzed for [Kglobal]. *)
+ val is_reachable_kinstr : Cil_types.kinstr -> bool
+
+ val condition_truth_value: Cil_types.stmt -> bool * bool
+ (** Provided [stmt] is an 'if' construct, [fst (condition_truth_value stmt)]
+ (resp. snd) is true if and only if the condition of the 'if' has been
+ evaluated to true (resp. false) at least once during the analysis. *)
+
+ (*** Callers / Callees / Callsites *)
+
+ (** Returns the list of inferred callers of the given function. *)
+ val callers : Cil_types.kernel_function -> Cil_types.kernel_function list
+
+ (** Returns the list of inferred callers, and for each of them, the list
+ of callsites (the call statements) inside. *)
+ val callsites : Cil_types.kernel_function ->
+ (Cil_types.kernel_function * Cil_types.stmt list) list
+
+
+ (** Returns the kernel functions called in the given statement.
+ If the callee expression doesn't always evaluate to a function, those
+ spurious values are ignored. If it always evaluate to a non-function value
+ then the returned list is empty.
+ Raises [Stdlib.Invalid_argument] if the statement is not a [Call]
+ instruction or a [Local_init] with [ConsInit] initializer. *)
+ val callee : Cil_types.stmt -> Kernel_function.t list
+
+end
+
+module Parameters: sig
+
+ (** Configuration of the analysis. *)
+
+ (** Returns the list (name, descr) of currently enabled abstract domains. *)
+ val enabled_domains: unit -> (string * string) list
+
+ (** [use_builtin kf name] instructs the analysis to use the builtin [name]
+ to interpret calls to function [kf].
+ Raises [Not_found] if there is no builtin of name [name]. *)
+ val use_builtin: Cil_types.kernel_function -> string -> unit
+
+ (** [use_global_value_partitioning vi] instructs the analysis to use
+ value partitioning on the global variable [vi]. *)
+ val use_global_value_partitioning: Cil_types.varinfo -> unit
+end
+
+module Eva_annotations: sig
+
+ (** Register special annotations to locally guide the Eva analysis:
+
+ - slevel annotations: "slevel default", "slevel merge" and "slevel i"
+ - loop unroll annotations: "loop unroll term"
+ - value partitioning annotations: "split term" and "merge term"
+ - subdivision annotations: "subdivide i"
+ *)
+
+ (** Annotations tweaking the behavior of the -eva-slevel parameter. *)
+ type slevel_annotation =
+ | SlevelMerge (** Join all states separated by slevel. *)
+ | SlevelDefault (** Use the limit defined by -eva-slevel. *)
+ | SlevelLocal of int (** Use the given limit instead of -eva-slevel. *)
+ | SlevelFull (** Remove the limit of number of separated states. *)
+
+ (** Loop unroll annotations. *)
+ type unroll_annotation =
+ | UnrollAmount of Cil_types.term (** Unroll the n first iterations. *)
+ | UnrollFull (** Unroll amount defined by -eva-default-loop-unroll. *)
+
+ type split_kind = Static | Dynamic
+
+ type split_term =
+ | Expression of Cil_types.exp
+ | Predicate of Cil_types.predicate
+
+ (** Split/merge annotations for value partitioning. *)
+ type flow_annotation =
+ | FlowSplit of split_term * split_kind
+ (** Split states according to a term. *)
+ | FlowMerge of split_term
+ (** Merge states separated by a previous split. *)
+
+ 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 (* domain *) *
+ Cil_types.varinfo list (* variables that must be tracked by the domain *)
+
+ val get_slevel_annot : Cil_types.stmt -> slevel_annotation option
+ val get_unroll_annot : Cil_types.stmt -> unroll_annotation list
+ val get_flow_annot : Cil_types.stmt -> flow_annotation list
+ val get_subdivision_annot : Cil_types.stmt -> int list
+ val get_allocation: Cil_types.stmt -> allocation_kind
+
+ val add_slevel_annot : emitter:Emitter.t ->
+ Cil_types.stmt -> slevel_annotation -> unit
+ val add_unroll_annot : emitter:Emitter.t ->
+ Cil_types.stmt -> unroll_annotation -> unit
+ val add_flow_annot : emitter:Emitter.t ->
+ Cil_types.stmt -> 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 -> array_segmentation -> unit
+ val add_domain_scope : emitter:Emitter.t ->
+ Cil_types.stmt -> domain_scope -> unit
+end
+
+module Eval: sig
+
+ (** Can the results of a function call be cached with memexec? *)
+ type cacheable =
+ | Cacheable (** Functions whose result can be safely cached. *)
+ | NoCache (** Functions whose result should not be cached, but for
+ which the caller can still be cached. Typically,
+ functions printing something during the analysis. *)
+ | NoCacheCallers (** Functions for which neither the call, neither the
+ callers, can be cached. *)
+end
+
+module Builtins: sig
+
+ (** Eva analysis builtins for the cvalue domain, more efficient than their
+ equivalent in C. *)
+
+ open Cil_types
+
+ exception Invalid_nb_of_args of int
+ exception Outside_builtin_possibilities
+
+ (* Signature of a builtin: type of the result, and type of the arguments. *)
+ type builtin_type = unit -> typ * typ list
+
+ (** Can the results of a builtin be cached? See {!Eval} for more details.*)
+ type cacheable = Eval.cacheable = Cacheable | NoCache | NoCacheCallers
+
+ type full_result = {
+ c_values: (Cvalue.V.t option * Cvalue.Model.t) list;
+ (** A list of results, consisting of:
+ - the value returned (ie. what is after the 'return' C keyword)
+ - the memory state after the function has been executed. *)
+ c_clobbered: Base.SetLattice.t;
+ (** An over-approximation of the bases in which addresses of local variables
+ might have been written *)
+ c_from: (Function_Froms.froms * Locations.Zone.t) option;
+ (** If not None, the froms of the function, and its sure outputs;
+ i.e. the dependencies of the result and of each zone written to. *)
+ }
+
+ (** The result of a builtin can be given in different forms. *)
+ type call_result =
+ | States of Cvalue.Model.t list
+ (** A disjunctive list of post-states at the end of the C function.
+ Can only be used if the C function does not write the address of local
+ variables, does not read other locations than the call arguments, and
+ does not write other locations than the result. *)
+ | Result of Cvalue.V.t list
+ (** A disjunctive list of resulting values. The specification is used to
+ compute the post-state, in which the result is replaced by the values
+ computed by the builtin. *)
+ | Full of full_result
+ (** See [full_result] type. *)
+
+ (** Type of a cvalue builtin, whose arguments are:
+ - the memory state at the beginning of the function call;
+ - the list of arguments of the function call. *)
+ type builtin = Cvalue.Model.t -> (exp * Cvalue.V.t) list -> call_result
+
+ (** [register_builtin name ?replace ?typ cacheable f] registers the function [f]
+ as a builtin to be used instead of the C function of name [name].
+ If [replace] is provided, the builtin is also used instead of the C function
+ of name [replace], unless option -eva-builtin-auto is disabled.
+ If [typ] is provided, consistency between the expected [typ] and the type of
+ the C function is checked before using the builtin.
+ The results of the builtin are cached according to [cacheable]. *)
+ val register_builtin:
+ string -> ?replace:string -> ?typ:builtin_type -> cacheable -> builtin -> unit
+
+ (** Has a builtin been registered with the given name? *)
+ val is_builtin: string -> bool
+end
+
+module Cvalue_callbacks: sig
+
+ (** Register actions to performed during the Eva analysis,
+ with access to the states of the cvalue domain. *)
+
+ type callstack = (Cil_types.kernel_function * Cil_types.kinstr) list
+ type state = Cvalue.Model.t
+
+ type analysis_kind =
+ [ `Builtin of Value_types.call_froms
+ | `Spec of Cil_types.funspec
+ | `Def
+ | `Memexec ]
+
+ (** Registers a function to be applied at the beginning of the analysis of each
+ function call. Arguments of the callback are the callstack of the call,
+ the function called, the kind of analysis performed by Eva for this call,
+ and the cvalue state at the beginning of the call. *)
+ val register_call_hook:
+ (callstack -> Cil_types.kernel_function -> analysis_kind -> state -> unit)
+ -> unit
+
+
+ type state_by_stmt = (state Cil_datatype.Stmt.Hashtbl.t) Lazy.t
+ type results = { before_stmts: state_by_stmt; after_stmts: state_by_stmt }
+
+ (** Results of a function call. *)
+ type call_results =
+ | Store of results * int
+ (** Cvalue states before and after each statement of the given function,
+ plus a unique integer id for the call. *)
+ | Reuse of int
+ (** The results are the same as a previous call with the given integer id,
+ previously recorded with the [Store] constructor. *)
+
+ (** Registers a function to be applied at the end of the analysis of each
+ function call. Arguments of the callback are the callstack of the call,
+ the function called and the cvalue states resulting from its analysis. *)
+ val register_call_results_hook:
+ (callstack -> Cil_types.kernel_function -> call_results -> unit)
+ -> unit
+
+end
+
+module Eval_terms: sig
+
+ (** [annot_predicate_deps ~pre ~here p] computes the logic dependencies needed
+ to evaluate the predicate [p] in a code annotation in cvalue state [here],
+ in a function whose pre-state is [pre].
+ Returns None on either an evaluation error or on unsupported construct. *)
+ 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 -> results
+ val set_results: results -> unit
+ val merge: results -> results -> results
+
+ (** Change the callstacks for the results for which this is meaningful.
+ For technical reasons, the top of the callstack must currently
+ be preserved. *)
+ val change_callstacks:
+ (Value_types.callstack -> Value_types.callstack) -> results -> results
+
+end
+
+module Unit_tests: sig
+
+ (** Currently tested by this module:
+ - semantics of sign values. *)
+
+ (** Runs some programmatic tests on Eva. *)
+ val run: unit -> unit
+end
diff --git a/src/plugins/eva/values/numerors/numerors_arithmetics.ml b/src/plugins/eva/domains/numerors/numerors_arithmetics.ml
similarity index 100%
rename from src/plugins/eva/values/numerors/numerors_arithmetics.ml
rename to src/plugins/eva/domains/numerors/numerors_arithmetics.ml
diff --git a/src/plugins/eva/values/numerors/numerors_arithmetics.mli b/src/plugins/eva/domains/numerors/numerors_arithmetics.mli
similarity index 100%
rename from src/plugins/eva/values/numerors/numerors_arithmetics.mli
rename to src/plugins/eva/domains/numerors/numerors_arithmetics.mli
diff --git a/src/plugins/eva/values/numerors/numerors_float.ml b/src/plugins/eva/domains/numerors/numerors_float.ml
similarity index 100%
rename from src/plugins/eva/values/numerors/numerors_float.ml
rename to src/plugins/eva/domains/numerors/numerors_float.ml
diff --git a/src/plugins/eva/values/numerors/numerors_float.mli b/src/plugins/eva/domains/numerors/numerors_float.mli
similarity index 100%
rename from src/plugins/eva/values/numerors/numerors_float.mli
rename to src/plugins/eva/domains/numerors/numerors_float.mli
diff --git a/src/plugins/eva/values/numerors/numerors_interval.ml b/src/plugins/eva/domains/numerors/numerors_interval.ml
similarity index 100%
rename from src/plugins/eva/values/numerors/numerors_interval.ml
rename to src/plugins/eva/domains/numerors/numerors_interval.ml
diff --git a/src/plugins/eva/values/numerors/numerors_interval.mli b/src/plugins/eva/domains/numerors/numerors_interval.mli
similarity index 100%
rename from src/plugins/eva/values/numerors/numerors_interval.mli
rename to src/plugins/eva/domains/numerors/numerors_interval.mli
diff --git a/src/plugins/eva/values/numerors/numerors_utils.ml b/src/plugins/eva/domains/numerors/numerors_utils.ml
similarity index 100%
rename from src/plugins/eva/values/numerors/numerors_utils.ml
rename to src/plugins/eva/domains/numerors/numerors_utils.ml
diff --git a/src/plugins/eva/values/numerors/numerors_utils.mli b/src/plugins/eva/domains/numerors/numerors_utils.mli
similarity index 100%
rename from src/plugins/eva/values/numerors/numerors_utils.mli
rename to src/plugins/eva/domains/numerors/numerors_utils.mli
diff --git a/src/plugins/eva/values/numerors/numerors_value.ml b/src/plugins/eva/domains/numerors/numerors_value.ml
similarity index 100%
rename from src/plugins/eva/values/numerors/numerors_value.ml
rename to src/plugins/eva/domains/numerors/numerors_value.ml
diff --git a/src/plugins/eva/values/numerors/numerors_value.mli b/src/plugins/eva/domains/numerors/numerors_value.mli
similarity index 100%
rename from src/plugins/eva/values/numerors/numerors_value.mli
rename to src/plugins/eva/domains/numerors/numerors_value.mli
diff --git a/src/plugins/eva/dune b/src/plugins/eva/dune
index d0285778cc47660df0c498af1f40fde13967ba14..502fec6d6edf50ebae146a7f34a37b63502fcad6 100644
--- a/src/plugins/eva/dune
+++ b/src/plugins/eva/dune
@@ -23,186 +23,82 @@
(rule
(alias frama-c-configure)
(deps (universe))
- (action (progn
- (echo "EVA:" %{lib-available:frama-c-eva.core} "\n")
- (echo "Numerors:" %{lib-available:frama-c-eva.numerors.core} "\n")
- (echo " - MLMPFR:" %{lib-available:mlmpfr} "\n")
- (echo "Apron domains:" %{lib-available:frama-c-eva.apron} "\n")
- (echo " - apron.octMPQ:" %{lib-available:apron.octMPQ} "\n")
- (echo " - apron.boxMPQ:" %{lib-available:apron.boxMPQ} "\n")
- (echo " - apron.polkaMPQ:" %{lib-available:apron.polkaMPQ} "\n")
- (echo " - apron.apron:" %{lib-available:apron.apron} "\n")
- )
- )
-)
+ (action
+ (progn
+ (echo "EVA:" %{lib-available:frama-c-eva.core} "\n")
+ (echo "Numerors:" %{lib-available:frama-c-eva.numerors.core} "\n")
+ (echo " - MLMPFR:" %{lib-available:mlmpfr} "\n")
+ (echo "Apron domains:" %{lib-available:frama-c-eva.apron} "\n")
+ (echo " - apron.octMPQ:" %{lib-available:apron.octMPQ} "\n")
+ (echo " - apron.boxMPQ:" %{lib-available:apron.boxMPQ} "\n")
+ (echo " - apron.polkaMPQ:" %{lib-available:apron.polkaMPQ} "\n")
+ (echo " - apron.apron:" %{lib-available:apron.apron} "\n"))))
-( library
- (name eva)
- (optional)
- (public_name frama-c-eva.core)
- (modules
- abstract
- abstract_domain
- abstract_location
- abstract_memory
- abstract_offset
- abstract_structure
- abstract_value
- abstractions
- active_behaviors
- alarmset
- analysis
- auto_loop_unroll
- backward_formals
- builtins
- builtins_float
- builtins_malloc
- builtins_memory
- builtins_misc
- builtins_print_c
- builtins_split
- builtins_string
- builtins_watchpoint
- compute_functions
- cvalue_backward
- cvalue_callbacks
- cvalue_domain
- cvalue_forward
- cvalue_init
- cvalue_offsetmap
- cvalue_specification
- cvalue_transfer
- domain_builder
- domain_lift
- domain_mode
- domain_product
- domain_store
- equality
- equality_domain
- eva
- eva_annotations
- eva_audit
- eva_dynamic
- eva_perf
- eva_results
- eva_utils
- eval
- eval_annots
- eval_op
- eval_terms
- eval_typ
- evaluation
- function_args
- function_calls
- gauges_domain
- general_requests
- hcexprs
- initialization
- inout_domain
- iterator
- library_functions
- locals_scoping
- location_lift
- main_locations
- main_values
- mem_exec
- multidim
- multidim_domain
- octagons
- offsm_domain
- offsm_value
- parameters
- partition
- partitioning_index
- partitioning_parameters
- per_stmt_slevel
- powerset
- printer_domain
- pretty_memory
- recursion
- red_statuses
- register
- results
- segmentation
- self
- sign_domain
- sign_value
- simple_memory
- simpler_domains
- split_return
- split_strategy
- structure
- subdivided_evaluation
- summary
- symbolic_locs
- taint_domain
- trace_partitioning
- traces_domain
- transfer_logic
- transfer_specification
- transfer_stmt
- typed_memory
- unit_domain
- unit_tests
- value_product
- values_request
- warn
- widen
- widen_hints_ext
-)
+(library
+ (name eva)
+ (optional)
+ (public_name frama-c-eva.core)
+ (flags -open Frama_c_kernel :standard -w -9)
+ (libraries frama-c.kernel frama-c-server.core))
-; (public_interfaces (Eva))
- (flags -open Frama_c_kernel :standard -w -9)
- (libraries frama-c.kernel frama-c-server.core
- ; frama-c-callgraph.core frama-c-rtegen.core frama-c-loop-analysis.core
- ; frama-c-scope.core
- )
-)
+(plugin
+ (name eva)
+ (optional)
+ (libraries frama-c-eva.core)
+ (site (frama-c plugins)))
-(plugin (optional) (name eva) (libraries frama-c-eva.core) (site (frama-c plugins)))
+(include_subdirs unqualified)
-(rule
- (targets Eva.ml Eva.mli)
- (deps
- gen-api.sh Eva.ml.in Eva.mli.in
- engine/analysis.mli utils/results.mli parameters.mli utils/eva_annotations.mli eval.mli
- domains/cvalue/builtins.mli utils/cvalue_callbacks.mli legacy/eval_terms.mli utils/eva_results.mli utils/unit_tests.mli
- )
- (action (run %{deps}))
-)
+(subdir gui (include_subdirs no))
+(subdir gui
+ (library
+ (name eva_gui)
+ (optional)
+ (public_name frama-c-eva.gui)
+ (flags -open Frama_c_kernel -open Frama_c_gui -open Eva__Private :standard -w -9)
+ (libraries eva frama-c.kernel frama-c.gui)))
+
+(plugin
+ (name eva-gui)
+ (optional)
+ (libraries frama-c-eva.gui)
+ (site (frama-c plugins_gui)))
-( library
+(subdir domains/numerors (include_subdirs no))
+(subdir domains/numerors
+ (library
(name numerors)
- (public_name frama-c-eva.numerors.core)
- (flags -open Frama_c_kernel -open Eva.Private :standard)
- (modules numerors_domain numerors_utils numerors_float numerors_interval numerors_arithmetics numerors_value)
- (libraries frama-c.kernel frama-c-eva.core mlmpfr)
(optional)
-)
+ (public_name frama-c-eva.numerors.core)
+ (flags -open Frama_c_kernel -open Eva__Private :standard)
+ (libraries frama-c.kernel frama-c-eva.core mlmpfr)))
-(plugin (optional) (name eva.numerors) (libraries frama-c-eva.numerors.core) (site (frama-c plugins)))
+(plugin
+ (name eva.numerors)
+ (optional)
+ (libraries frama-c-eva.numerors.core)
+ (site (frama-c plugins)))
-( library
+(subdir domains/apron (include_subdirs no))
+(subdir domains/apron
+ (library
(name apron_domain)
- (public_name frama-c-eva.apron)
- (flags -open Frama_c_kernel -open Eva.Private :standard -w -9)
- (modules apron_domain)
- (libraries frama-c.kernel frama-c-eva.core apron.octMPQ apron.boxMPQ apron.polkaMPQ apron.apron)
(optional)
-)
+ (public_name frama-c-eva.apron)
+ (flags -open Frama_c_kernel -open Eva__Private :standard -w -9)
+ (libraries
+ frama-c.kernel frama-c-eva.core
+ apron.octMPQ apron.boxMPQ apron.polkaMPQ apron.apron)))
;(plugin (optional) (name eva-apron) (libraries frama-c-eva.apron) (site (frama-c plugins)))
-( library
- (name eva_gui)
- (public_name frama-c-eva.gui)
- (optional)
- (modules gui_callstacks_filters gui_callstacks_manager gui_eval gui_types register_gui gui_red)
-; (public_interfaces ())
- (flags -open Frama_c_kernel -open Frama_c_gui -open Eva -open Eva.Private :standard -w -9)
- (libraries eva frama-c.kernel frama-c.gui)
-)
-
-(plugin (optional) (name eva-gui) (libraries frama-c-eva.gui) (site (frama-c plugins_gui)))
-
-(include_subdirs unqualified)
+(rule
+ (targets Eva.ml Eva.mli)
+ (mode (promote (only Eva.mli)))
+ (deps
+ gen-api.sh Eva.header
+ engine/analysis.mli utils/results.mli parameters.mli
+ utils/eva_annotations.mli eval.mli domains/cvalue/builtins.mli
+ utils/cvalue_callbacks.mli legacy/eval_terms.mli utils/eva_results.mli
+ utils/unit_tests.mli)
+ (action (run %{deps})))
diff --git a/src/plugins/eva/gen-api.sh b/src/plugins/eva/gen-api.sh
index dea87c497c5aa1b3f4abde3ced38687892beedb8..2ce5c9b97aaa867602d723687c7ef56aaa40d40d 100755
--- a/src/plugins/eva/gen-api.sh
+++ b/src/plugins/eva/gen-api.sh
@@ -27,28 +27,11 @@ dir=$(dirname $0)
# Generate MLI
-cat $dir/Eva.mli.in >> Eva.mli
-
-printf '\n(** Eva public API.
-
- The main modules are:
- - Analysis: run the analysis.
- - Results: access analysis results, especially the values of expressions
- and memory locations of lvalues at each program point.
-
- The following modules allow configuring the Eva analysis:
- - Parameters: change the configuration of the analysis.
- - Eva_annotations: add local annotations to guide the analysis.
- - Builtins: register ocaml builtins to be used by the cvalue domain
- instead of analysing the body of some C functions.
-
- Other modules are for internal use only. *)\n' >> Eva.mli
-
-printf '\n(* This file is generated. Do not edit. *)\n' >> Eva.mli
+cat $dir/Eva.header >> Eva.mli
for i in "$@"
do
- if [[ ! "$i" =~ [.]in$ ]]; then
+ if [[ ! "$i" =~ [.]header$ ]]; then
file=$(basename $i)
module=${file%.*}
Module="$(echo "${module:0:1}" | tr '[:lower:]' '[:upper:]')${module:1}"
@@ -60,11 +43,11 @@ done
# Generate ML
-cat $dir/Eva.ml.in >> Eva.ml
+cat $dir/Eva.header >> Eva.ml
for i in "$@"
do
- if [[ ! "$i" =~ [.]in$ ]]; then
+ if [[ ! "$i" =~ [.]header$ ]]; then
file=$(basename $i)
module=${file%.*}
Module="$(echo "${module:0:1}" | tr '[:lower:]' '[:upper:]')${module:1}"
diff --git a/src/plugins/eva/gui_files/gui_callstacks_filters.ml b/src/plugins/eva/gui/gui_callstacks_filters.ml
similarity index 100%
rename from src/plugins/eva/gui_files/gui_callstacks_filters.ml
rename to src/plugins/eva/gui/gui_callstacks_filters.ml
diff --git a/src/plugins/eva/gui_files/gui_callstacks_filters.mli b/src/plugins/eva/gui/gui_callstacks_filters.mli
similarity index 100%
rename from src/plugins/eva/gui_files/gui_callstacks_filters.mli
rename to src/plugins/eva/gui/gui_callstacks_filters.mli
diff --git a/src/plugins/eva/gui_files/gui_callstacks_manager.ml b/src/plugins/eva/gui/gui_callstacks_manager.ml
similarity index 100%
rename from src/plugins/eva/gui_files/gui_callstacks_manager.ml
rename to src/plugins/eva/gui/gui_callstacks_manager.ml
diff --git a/src/plugins/eva/gui_files/gui_callstacks_manager.mli b/src/plugins/eva/gui/gui_callstacks_manager.mli
similarity index 100%
rename from src/plugins/eva/gui_files/gui_callstacks_manager.mli
rename to src/plugins/eva/gui/gui_callstacks_manager.mli
diff --git a/src/plugins/eva/gui_files/gui_eval.ml b/src/plugins/eva/gui/gui_eval.ml
similarity index 100%
rename from src/plugins/eva/gui_files/gui_eval.ml
rename to src/plugins/eva/gui/gui_eval.ml
diff --git a/src/plugins/eva/gui_files/gui_eval.mli b/src/plugins/eva/gui/gui_eval.mli
similarity index 100%
rename from src/plugins/eva/gui_files/gui_eval.mli
rename to src/plugins/eva/gui/gui_eval.mli
diff --git a/src/plugins/eva/gui_files/gui_red.ml b/src/plugins/eva/gui/gui_red.ml
similarity index 100%
rename from src/plugins/eva/gui_files/gui_red.ml
rename to src/plugins/eva/gui/gui_red.ml
diff --git a/src/plugins/eva/gui_files/gui_red.mli b/src/plugins/eva/gui/gui_red.mli
similarity index 100%
rename from src/plugins/eva/gui_files/gui_red.mli
rename to src/plugins/eva/gui/gui_red.mli
diff --git a/src/plugins/eva/gui_files/gui_types.ml b/src/plugins/eva/gui/gui_types.ml
similarity index 100%
rename from src/plugins/eva/gui_files/gui_types.ml
rename to src/plugins/eva/gui/gui_types.ml
diff --git a/src/plugins/eva/gui_files/gui_types.mli b/src/plugins/eva/gui/gui_types.mli
similarity index 100%
rename from src/plugins/eva/gui_files/gui_types.mli
rename to src/plugins/eva/gui/gui_types.mli
diff --git a/src/plugins/eva/gui_files/register_gui.ml b/src/plugins/eva/gui/register_gui.ml
similarity index 100%
rename from src/plugins/eva/gui_files/register_gui.ml
rename to src/plugins/eva/gui/register_gui.ml
diff --git a/src/plugins/eva/gui_files/register_gui.mli b/src/plugins/eva/gui/register_gui.mli
similarity index 100%
rename from src/plugins/eva/gui_files/register_gui.mli
rename to src/plugins/eva/gui/register_gui.mli
diff --git a/src/plugins/eva/utils/eva_results.mli b/src/plugins/eva/utils/eva_results.mli
index 09c2bd8d36b9e45847560ad7e5ed5180728dc9ff..6144615c2e453f9366bd1c1c096c4418784439ab 100644
--- a/src/plugins/eva/utils/eva_results.mli
+++ b/src/plugins/eva/utils/eva_results.mli
@@ -35,11 +35,12 @@ type results
val get_results: unit -> results
val set_results: results -> unit
val merge: results -> results -> results
-val change_callstacks:
- (Value_types.callstack -> Value_types.callstack) -> results -> results
+
(** Change the callstacks for the results for which this is meaningful.
For technical reasons, the top of the callstack must currently
be preserved. *)
+val change_callstacks:
+ (Value_types.callstack -> Value_types.callstack) -> results -> results
[@@@ api_end]
diff --git a/src/plugins/eva/Eva.mli.in b/src/plugins/eva/utils/private.ml
similarity index 63%
rename from src/plugins/eva/Eva.mli.in
rename to src/plugins/eva/utils/private.ml
index ee97ccf3957db006495ed5f04f863e94bfd56989..c5a16ae11951cb4fec6bec7762131939b13ab083 100644
--- a/src/plugins/eva/Eva.mli.in
+++ b/src/plugins/eva/utils/private.ml
@@ -20,35 +20,27 @@
(* *)
(**************************************************************************)
-(** ../.. *)
-
-(** For internal use *)
-(* Private first so that we do not override internal modules with public ones *)
-
-module Private: sig
- module Abstractions = Abstractions
- module Analysis = Analysis
- module Alarmset = Alarmset
- module Parameters = Parameters
- module Main_values = Main_values
- module Eval = Eval
- module Eva_utils = Eva_utils
- module Eva_results = Eva_results
- module Self = Self
- module Eval_terms = Eval_terms
- module Red_statuses = Red_statuses
- module Abstract_value = Abstract_value
- module Abstract_domain = Abstract_domain
- module Active_behaviors = Active_behaviors
- module Function_calls = Function_calls
- module Simple_memory = Simple_memory
- module Structure = Structure
- module Eval_typ = Eval_typ
- module Eval_op = Eval_op
- module Domain_builder = Domain_builder
- module Main_locations = Main_locations
- module Eval_annots = Eval_annots
- module Eva_dynamic = Eva_dynamic
-end
-
-(** ../.. *)
+module Abstract_domain = Abstract_domain
+module Abstract_value = Abstract_value
+module Abstractions = Abstractions
+module Active_behaviors = Active_behaviors
+module Alarmset = Alarmset
+module Analysis = Analysis
+module Domain_builder = Domain_builder
+module Eva_dynamic = Eva_dynamic
+module Eva_results = Eva_results
+module Eva_utils = Eva_utils
+module Eval = Eval
+module Eval_annots = Eval_annots
+module Eval_op = Eval_op
+module Eval_terms = Eval_terms
+module Eval_typ = Eval_typ
+module Function_calls = Function_calls
+module Main_locations = Main_locations
+module Main_values = Main_values
+module Parameters = Parameters
+module Red_statuses = Red_statuses
+module Results = Results
+module Self = Self
+module Simple_memory = Simple_memory
+module Structure = Structure
diff --git a/src/plugins/eva/utils/private.mli b/src/plugins/eva/utils/private.mli
new file mode 100644
index 0000000000000000000000000000000000000000..d4c64ac5ad0f0992d3ca624cae53a5b64421d9df
--- /dev/null
+++ b/src/plugins/eva/utils/private.mli
@@ -0,0 +1,50 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2022 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** For internal use only: the Eva gui and optional domains (numerors and apron)
+ are compiled separately from the Eva core. This is used to give them access
+ to the internal modules of Eva they need. *)
+
+module Abstract_domain = Abstract_domain
+module Abstract_value = Abstract_value
+module Abstractions = Abstractions
+module Active_behaviors = Active_behaviors
+module Alarmset = Alarmset
+module Analysis = Analysis
+module Domain_builder = Domain_builder
+module Eva_dynamic = Eva_dynamic
+module Eva_results = Eva_results
+module Eva_utils = Eva_utils
+module Eval = Eval
+module Eval_annots = Eval_annots
+module Eval_op = Eval_op
+module Eval_terms = Eval_terms
+module Eval_typ = Eval_typ
+module Function_calls = Function_calls
+module Main_locations = Main_locations
+module Main_values = Main_values
+module Parameters = Parameters
+module Red_statuses = Red_statuses
+module Results = Results
+module Self = Self
+module Simple_memory = Simple_memory
+module Structure = Structure
diff --git a/src/plugins/inout/operational_inputs.ml b/src/plugins/inout/operational_inputs.ml
index 632d4a4bd1a12115325af5944788a0bf50df5447..adddc088f623ecfedc193549263e561afeb335df 100644
--- a/src/plugins/inout/operational_inputs.ml
+++ b/src/plugins/inout/operational_inputs.ml
@@ -378,7 +378,7 @@ module Computer(Fenv:Dataflows.FUNCTION_ENV)(X:sig
let pre = X.kf_pre_state
and here = X.stmt_state stmt in
let deps =
- Eva.Private.Eval_terms.annot_predicate_deps ~pre ~here p.tp_statement
+ Eva.Eval_terms.annot_predicate_deps ~pre ~here p.tp_statement
in
match deps with
| None ->