diff --git a/src/plugins/value/domains/abstract_domain.mli b/src/plugins/value/domains/abstract_domain.mli index ca999ade6757a6fe4f168d1ac5f72226ccfae2a0..9ddb17082d70603ad752fecbcb7898de4d857cf4 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 92695943032cf557756fa4c4ff3b1bf06c117fd1..256fe3fd89b4c89ca13976f788b4c4ecccde0aca 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 5e9c39649ace774f6571536883f2c771c0415224..ce35bfe07f5ea405e13dd3ad98d6076aa8f89bf1 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; }