[Eva] Comments the optional argument [subdivnb] in the evaluation signature.

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