Merge branch 'fix/andre/eva-silence-warning-16' into 'master'

[Eva] avoid triggering warning 16 (unerasable-optional-argument)

See merge request frama-c/frama-c!3054

src/plugins/value/values/numerors/numerors_arithmetics.ml

@@ -331,16 +331,16 @@ module Exact : Arithmetic with type forward = I.t = struct
       I.narrow x.exact (I.neg r.exact)
 
     let add x y r = [x ; y ; r] >>+ fun _ ->
-      I.backward_add ~prec:P.Real ~left:x.exact ~right:y.exact ~result:r.exact
+      I.backward_add ~prec:P.Real ~left:x.exact ~right:y.exact ~result:r.exact ()
 
     let sub x y r = [x ; y ; r] >>+ fun _ ->
-      I.backward_sub ~prec:P.Real ~left:x.exact ~right:y.exact ~result:r.exact
+      I.backward_sub ~prec:P.Real ~left:x.exact ~right:y.exact ~result:r.exact ()
 
     let mul x y r = [x ; y ; r] >>+ fun _ ->
-      I.backward_mul ~prec:P.Real ~left:x.exact ~right:y.exact ~result:r.exact
+      I.backward_mul ~prec:P.Real ~left:x.exact ~right:y.exact ~result:r.exact ()
 
     let div x y r = [x ; y ; r] >>+ fun _ ->
-      I.backward_div ~prec:P.Real ~left:x.exact ~right:y.exact ~result:r.exact
+      I.backward_div ~prec:P.Real ~left:x.exact ~right:y.exact ~result:r.exact ()
 
   end
 
@@ -378,16 +378,16 @@ module Approx : Arithmetic with type forward = I.t = struct
       I.narrow x.approx (I.neg r.approx)
 
     let add x y r = [x ; y ; r] >>+ fun prec ->
-      I.backward_add ~prec ~left:x.approx ~right:y.approx ~result:r.approx
+      I.backward_add ~prec ~left:x.approx ~right:y.approx ~result:r.approx ()
 
     let sub x y r = [x ; y ; r] >>+ fun prec ->
-      I.backward_sub ~prec ~left:x.approx ~right:y.approx ~result:r.approx
+      I.backward_sub ~prec ~left:x.approx ~right:y.approx ~result:r.approx ()
 
     let mul x y r = [x ; y ; r] >>+ fun prec ->
-      I.backward_mul ~prec ~left:x.approx ~right:y.approx ~result:r.approx
+      I.backward_mul ~prec ~left:x.approx ~right:y.approx ~result:r.approx ()
 
     let div x y r = [x ; y ; r] >>+ fun prec ->
-      I.backward_div ~prec ~left:x.approx ~right:y.approx ~result:r.approx
+      I.backward_div ~prec ~left:x.approx ~right:y.approx ~result:r.approx ()
 
   end
 

src/plugins/value/values/numerors/numerors_interval.ml

@@ -441,7 +441,7 @@ let finite_values ~prec = function
     let max = F.min (F.maximal_pos_float prec) y in
     if max < min then None else Some (min, max)
 
-let backward_op (op : operator) fnan ?(prec = Precisions.Real) value result =
+let backward_op (op : operator) fnan ?(prec = Precisions.Real) value result () =
   if contains_infinity result || (contains_nan value && contains_nan result)
   then `Value (top prec)
   else
@@ -471,7 +471,7 @@ let synthetize left right =
   | `Value left, `Value right -> `Value (left, right)
 [@@inline]
 
-let backward_add ?(prec = Precisions.Real) ~left ~right ~result =
+let backward_add ?(prec = Precisions.Real) ~left ~right ~result () =
   let reduce_for_nan value =
     match contains_pos_infinity value, contains_neg_infinity value with
     | true , true   -> I (F.neg_inf prec, F.pos_inf prec, true)
@@ -479,38 +479,38 @@ let backward_add ?(prec = Precisions.Real) ~left ~right ~result =
     | false, true   -> I (F.pos_inf prec, F.pos_inf prec, true)
     | false, false  -> NaN prec
   in
-  let right' = backward_op F.sub reduce_for_nan ~prec left  result in
-  let left'  = backward_op F.sub reduce_for_nan ~prec right result in
+  let right' = backward_op F.sub reduce_for_nan ~prec left  result () in
+  let left'  = backward_op F.sub reduce_for_nan ~prec right result () in
   synthetize left' right'
 
-let backward_sub ?(prec = Precisions.Real) ~left ~right ~result =
-  match backward_add ~prec ~left ~right:(neg right) ~result with
+let backward_sub ?(prec = Precisions.Real) ~left ~right ~result () =
+  match backward_add ~prec ~left ~right:(neg right) ~result () with
   | `Bottom -> `Bottom
   | `Value (left, right) -> `Value (left, neg right)
 
-let backward_mul ?(prec = Precisions.Real) ~left ~right ~result =
+let backward_mul ?(prec = Precisions.Real) ~left ~right ~result () =
   let reduce_for_nan value =
     match contains_infinity value, contains_a_zero value with
     | true, _ | _, true -> I (F.neg_inf prec, F.pos_inf prec, true)
     | false, false -> NaN prec
   in
-  let right' = backward_op F.div reduce_for_nan ~prec left  result in
-  let left'  = backward_op F.div reduce_for_nan ~prec right result in
+  let right' = backward_op F.div reduce_for_nan ~prec left  result () in
+  let left'  = backward_op F.div reduce_for_nan ~prec right result () in
   synthetize left' right'
 
-let backward_div ?(prec = Precisions.Real) ~left ~right ~result =
+let backward_div ?(prec = Precisions.Real) ~left ~right ~result () =
   let reduce_for_nan value =
     match contains_infinity value, contains_a_zero value with
     | true, _ | _, true -> I (F.neg_inf prec, F.pos_inf prec, true)
     | false, false -> NaN prec
   in
   let right' =
-    match backward_op F.div reduce_for_nan ~prec left  result with
+    match backward_op F.div reduce_for_nan ~prec left  result () with
     | `Value right' ->
       let one = F.of_int ~prec 1 in
       let one = I (one, one, false) in
       `Value (div ~prec one right')
     | `Bottom -> `Bottom
   in
-  let left'  = backward_op F.div reduce_for_nan ~prec right result in
+  let left'  = backward_op F.div reduce_for_nan ~prec right result () in
   synthetize left' right'

src/plugins/value/values/numerors/numerors_interval.mli

@@ -182,10 +182,10 @@ val backward_gt : ?prec:Precisions.t -> t -> t -> t Bottom.or_bottom
 
 (** These functions perform backward propagation for arithmetic *)
 val backward_add : ?prec:Precisions.t -> left:t -> right:t ->
-  result:t -> (t * t) Bottom.or_bottom
+  result:t -> unit -> (t * t) Bottom.or_bottom
 val backward_sub : ?prec:Precisions.t -> left:t -> right:t ->
-  result:t -> (t * t) Bottom.or_bottom
+  result:t -> unit -> (t * t) Bottom.or_bottom
 val backward_mul : ?prec:Precisions.t -> left:t -> right:t ->
-  result:t -> (t * t) Bottom.or_bottom
+  result:t -> unit -> (t * t) Bottom.or_bottom
 val backward_div : ?prec:Precisions.t -> left:t -> right:t ->
-  result:t -> (t * t) Bottom.or_bottom
+  result:t -> unit -> (t * t) Bottom.or_bottom