From fbdf2f8a462f64806058e92a45bea39603ec44d8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 6 Sep 2019 10:08:18 +0200
Subject: [PATCH] [Eva] Fixes minor typos to some comments.
---
src/plugins/value/domains/abstract_domain.mli | 12 +++++-------
src/plugins/value/engine/abstractions.ml | 2 +-
src/plugins/value/eval.mli | 2 +-
3 files changed, 7 insertions(+), 9 deletions(-)
diff --git a/src/plugins/value/domains/abstract_domain.mli b/src/plugins/value/domains/abstract_domain.mli
index ca999ade675..9ddb17082d7 100644
--- a/src/plugins/value/domains/abstract_domain.mli
+++ b/src/plugins/value/domains/abstract_domain.mli
@@ -193,17 +193,15 @@ module type Transfer = sig
assignment has been performed.
- [kinstr] is the statement of the assignment, or Kglobal for the
initialization of a global variable.
+ - when the kinstr is a function call, [expr] is the special variable in
+ [!Eval.call.return].
- [v] carries the value being assigned to [lv], i.e. the value of the
expression [expr]. [v] also denotes the kind of assignment: Assign for
the default assignment of the value, or Copy for the exact copy of a
location if the right expression [expr] is a lvalue.
- [valuation] is a cache of all sub-expressions and locations computed
for the evaluation of [lval] and [expr]; it can also be used to reduce
- the state.
-
- A special case must be noted when the kinstr is a function call,
- the exp in this case is the special variable in [!Eval.call.return].
- *)
+ the state. *)
val assign :
kinstr -> location left_value -> exp -> (location, value) assigned ->
valuation -> state -> state or_bottom
@@ -474,8 +472,8 @@ module type Store = sig
val register_state_before_stmt: Value_types.callstack -> stmt -> state -> unit
val register_state_after_stmt: Value_types.callstack -> stmt -> state -> unit
- (** Allows to access state information after value analysis have
- been computed with the domain *)
+ (** Allows accessing the states inferred by an Eva analysis after it has
+ been computed with the domain enabled. *)
val get_global_state: unit -> state or_bottom
val get_initial_state: kernel_function -> state or_bottom
val get_initial_state_by_callstack:
diff --git a/src/plugins/value/engine/abstractions.ml b/src/plugins/value/engine/abstractions.ml
index 92695943032..256fe3fd89b 100644
--- a/src/plugins/value/engine/abstractions.ml
+++ b/src/plugins/value/engine/abstractions.ml
@@ -416,7 +416,7 @@ let add_errors abstract =
end : Abstract)
(* -------------------------------------------------------------------------- *)
-(* Gauges *)
+(* Traces *)
(* -------------------------------------------------------------------------- *)
let add_traces =
diff --git a/src/plugins/value/eval.mli b/src/plugins/value/eval.mli
index 5e9c39649ac..ce35bfe07f5 100644
--- a/src/plugins/value/eval.mli
+++ b/src/plugins/value/eval.mli
@@ -216,7 +216,7 @@ type ('loc, 'value) call = {
return: varinfo option; (** Fake varinfo to store the
return value of the call.
Same varinfo for every
- call to a function. *)
+ call to a given function. *)
recursive: bool;
}
--
GitLab