From b886a66352da2dfb18edad2703997f7e40696ada Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 27 Sep 2019 10:40:24 +0200
Subject: [PATCH] [Eva] Comments the optional argument [subdivnb] in the
evaluation signature.
---
src/plugins/value/engine/evaluation.mli | 20 ++++++++++++++------
1 file changed, 14 insertions(+), 6 deletions(-)
diff --git a/src/plugins/value/engine/evaluation.mli b/src/plugins/value/engine/evaluation.mli
index c950639322f..638cf44f01d 100644
--- a/src/plugins/value/engine/evaluation.mli
+++ b/src/plugins/value/engine/evaluation.mli
@@ -47,10 +47,14 @@ module type S = sig
for the expression [expr], and [valuation] contains all the intermediate
results of the evaluation.
- The [valuation] argument is a cache of already computed expressions.
- It is empty by default.
- The [reduction] argument allows deactivating the backward reduction
- performed after the forward evaluation. *)
+ Optional arguments are:
+ - [valuation] is a cache of already computed expressions; empty by default.
+ - [reduction] is true by default, but allows deactivating the backward
+ reduction performed after the forward evaluation.
+ - [subdivnb] is the maximum number of subdivisions performed on non-linear
+ expressions: if a lvalue occurs several times in an expression, its
+ value can be split up to [subdivnb] times to gain more precision.
+ Set to the value of the option -eva-subdivide-non-linear by default. *)
val evaluate :
?valuation:Valuation.t -> ?reduction:bool -> ?subdivnb:int ->
state -> exp -> (Valuation.t * value) evaluated
@@ -60,7 +64,9 @@ module type S = sig
Also returns the alarms resulting of the evaluation of the lvalue location,
and a valuation containing all the intermediate results of the evaluation.
The [valuation] argument is a cache of already computed expressions.
- It is empty by default. *)
+ It is empty by default.
+ [subdivnb] is the maximum number of subdivisions performed on non-linear
+ expressions. *)
val copy_lvalue :
?valuation:Valuation.t -> ?subdivnb:int ->
state -> lval -> (Valuation.t * value flagged_value) evaluated
@@ -70,7 +76,9 @@ module type S = sig
but evaluates the lvalue into a location and its type.
The boolean [for_writing] indicates whether the lvalue is evaluated to be
read or written. It is useful for the emission of the alarms, and for the
- reduction of the location. *)
+ reduction of the location.
+ [subdivnb] is the maximum number of subdivisions performed on non-linear
+ expressions (including the possible pointer and offset of the lvalue). *)
val lvaluate :
?valuation:Valuation.t -> ?subdivnb:int -> for_writing:bool ->
state -> lval -> (Valuation.t * loc * typ) evaluated
--
GitLab