Merge branch 'feature/eva/abs' into 'master'

[Eva] Supports the ACSL mathematical operator \abs.

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

src/kernel_services/abstract_interp/int_interval.ml

@@ -482,6 +482,20 @@ let neg t =
     ~rem:(Int.e_rem (Int.neg t.rem) t.modu)
     ~modu:t.modu
 
+let abs t =
+  match t.min, t.max with
+  | Some mn, _ when Int.(ge mn zero) -> t
+  | _, Some mx when Int.(le mx zero) -> neg t
+  | _, _ ->
+    let max =
+      match t.min, t.max with
+      | Some mn, Some mx -> Some (Int.(max (neg mn) mx))
+      | _, _ -> None
+    in
+    let modu = Int.(pgcd t.modu (add t.rem t.rem)) in
+    let rem = Int.e_rem t.rem modu in
+    build_interval ~min:(Some Int.zero) ~max ~rem ~modu
+
 type ext_value = Ninf | Pinf | Val of Int.t
 let inject_min = function None -> Ninf | Some m -> Val m
 let inject_max = function None -> Pinf | Some m -> Val m

src/kernel_services/abstract_interp/int_interval.mli

@@ -77,6 +77,7 @@ val add_singleton_int: Integer.t -> t -> t
 val add: t -> t -> t
 val add_under: t -> t -> t or_bottom
 val neg: t -> t
+val abs: t -> t
 
 val scale: Integer.t -> t -> t
 val scale_div: pos:bool -> Integer.t -> t -> t

src/kernel_services/abstract_interp/int_set.ml

@@ -604,6 +604,13 @@ let add_under s1 s2 =
 
 let neg s = map_set_strict_decr Int.neg s
 
+let abs s =
+  if Int.(ge s.(0) zero)
+  then s
+  else if Int.(le s.(Array.length s - 1) zero)
+  then neg s
+  else map Int.abs s
+
 let scale f s =
   if Int.ge f Int.zero
   then apply_bin_1_strict_incr Int.mul f s

src/kernel_services/abstract_interp/int_set.mli

@@ -117,6 +117,7 @@ val add_singleton: Integer.t -> t -> t
 val add: t -> t -> set_or_top
 val add_under: t -> t -> set_or_top
 val neg: t -> t
+val abs: t -> t
 
 val mul: t -> t -> set_or_top
 val c_rem: t -> t -> set_or_top_or_bottom

src/kernel_services/abstract_interp/int_val.ml

@@ -436,6 +436,10 @@ let neg = function
   | Set s -> Set (Int_set.neg s)
   | Itv i -> Itv (Int_interval.neg i)
 
+let abs = function
+  | Set s -> Set (Int_set.abs s)
+  | Itv i -> inject_itv (Int_interval.abs i)
+
 
 let scale f v =
   if Int.is_zero f

src/kernel_services/abstract_interp/int_val.mli

@@ -126,6 +126,9 @@ val add_singleton: Integer.t -> t -> t
 val neg: t -> t
 (** Negation of an integer abstraction. *)
 
+val abs: t -> t
+(** Absolute value of an integer abstraction. *)
+
 val scale: Integer.t -> t -> t
 (** [scale f v] returns an abstraction of the integers [f * x]
     for all [x] in [v]. This operation is exact. *)

src/kernel_services/abstract_interp/ival.ml

@@ -445,6 +445,11 @@ let neg_int = function
   | Float _ -> assert false
   | Int i -> inject_int (Int_val.neg i)
 
+let abs_int = function
+  | Bottom -> bottom
+  | Float _ -> assert false
+  | Int i -> inject_int (Int_val.abs i)
+
 let sub_int v1 v2 = add_int v1 (neg_int v2)
 let sub_int_under v1 v2 = add_int_under v1 (neg_int v2)
 

src/kernel_services/abstract_interp/ival.mli

@@ -63,6 +63,8 @@ val add_singleton_int: Integer.t -> t -> t
 
 val neg_int : t -> t
 (** Negation of an integer ival. Exact operation. *)
+val abs_int: t -> t
+(** Absolute value of an integer. *)
 val sub_int : t -> t -> t
 val sub_int_under: t -> t -> t
 

src/plugins/value/legacy/eval_terms.ml

@@ -720,6 +720,7 @@ let known_logic_funs = [
   "\\sign", ACSL;
   "\\min", ACSL;
   "\\max", ACSL;
+  "\\abs", ACSL;
   "\\neg_float",ACSL;
   "\\add_float",ACSL;
   "\\sub_float",ACSL;
@@ -1412,6 +1413,21 @@ and eval_known_logic_function ~alarm_mode env li labels args =
       | _ -> assert false
     end
 
+  | "\\abs", Some typ, _, [t] ->
+    begin
+      let r = eval_term ~alarm_mode env t in
+      try
+        let ival = Cvalue.V.project_ival r.eover in
+        let result =
+          match typ with
+          | Linteger -> einteger (Cvalue.V.inject_ival (Ival.abs_int ival))
+          | Lreal -> ereal Fval.(abs Real (Ival.project_float ival))
+          | _ -> assert false
+        in
+        { result with empty = r.empty; ldeps = r.ldeps; }
+      with Cvalue.V.Not_based_on_null -> c_alarm ()
+    end
+
   | _ -> assert false
 
 and eval_float_builtin_arity2  ~alarm_mode env name arg1 arg2 =

tests/value/logic.c

@@ -354,6 +354,89 @@ void min_max_quantifier () {
   /*@ check unknown: \min(i, j, \lambda integer i; t[i]) >= 0; */
 }
 
+#include <stdint.h>
+
+/*@ assigns \result \from x;
+    ensures \result == \abs(x); */
+int abs (int x);
+
+void int_abs () {
+  /* Singletons. */
+  int zero = abs(0);
+  int ten = abs(10);
+  int eleven = abs(-11);
+  int x;
+  /* Tests the set semantics. */
+  x = Frama_C_interval(-10, -5);
+  x = abs(x);
+  Frama_C_show_each_5_10(x);
+  x = Frama_C_interval(-4, 3);
+  x = abs(x);
+  Frama_C_show_each_0_4(x);
+  /* Tests the interval semantics. */
+  x = Frama_C_interval(10, 100);
+  x = abs(x);
+  Frama_C_show_each_10_100(x);
+  x = Frama_C_interval(0, 100);
+  x = abs(x);
+  Frama_C_show_each_0_100(x);
+  x = Frama_C_interval(-20, -10);
+  x = abs(x);
+  Frama_C_show_each_10_20(x);
+  x = Frama_C_interval(-4, 12);
+  x = abs(x);
+  Frama_C_show_each_0_12(x);
+  x = Frama_C_interval(-16, 16);
+  x = abs(x);
+  Frama_C_show_each_0_16(x);
+   /* Tests the congruence semantics. */
+  x = Frama_C_interval(-20, 20);
+  x = 4 * x + 2;
+  x = abs(x);
+  Frama_C_show_each_2_mod_4(x);
+  x = Frama_C_interval(-20, 20);
+  x = 4 * x + 3;
+  x = abs(x);
+  Frama_C_show_each_1_mod_2(x);
+  x = Frama_C_interval(-12, 5);
+  x = 3 * x + 1;
+  x = abs(x);
+  Frama_C_show_each_no_mod(x);
+  /* Tests small intervals becoming small sets. */
+  x = Frama_C_interval(-5, 5);
+  x = abs(x);
+  Frama_C_show_each_set(x);
+  /* Tests address semantics. */
+  x = (uintptr_t)&x;
+  x = abs(x);
+  Frama_C_show_each_gm(x);
+}
+
+/*@ assigns \result \from f;
+    ensures \is_finite(\result) && \result == \abs(f); */
+double fabs(double f);
+
+void float_abs () {
+  /* Singletons. */
+  double zero = fabs(-0.);
+  double ten = fabs(10.);
+  double eleven = fabs(-11.);
+  double x;
+  /* Interval semantics. */
+  x = Frama_C_double_interval(-0., 0.);
+  x = fabs(x);
+  Frama_C_show_each_zero(x);
+  x = Frama_C_double_interval(0.5, 2.);
+  x = fabs(x);
+  Frama_C_show_each_half_two(x);
+  x = Frama_C_double_interval(-10., -0.);
+  x = fabs(x);
+  Frama_C_show_each_0_10(x);
+  x = Frama_C_double_interval(-3., 1.5);
+  x = fabs(x);
+  Frama_C_show_each_0_3(x);
+}
+
 void main () {
   eq_tsets();
   eq_char();
@@ -368,4 +451,6 @@ void main () {
   assign_tsets();
   check_and_assert ();
   min_max_quantifier ();
+  int_abs();
+  float_abs();
 }

tests/value/oracle/logic.res.oracle

@@ -14,7 +14,7 @@
   arr_ptr[0..2] ∈ {0}
   arr_ptr_arr[0..5] ∈ {0}
 [eva] computing for function eq_tsets <- main.
-  Called from tests/value/logic.c:358.
+  Called from tests/value/logic.c:441.
 [eva] tests/value/logic.c:103: 
   cannot evaluate ACSL term, unsupported ACSL construct: == operation on non-supported type set<_#8>
 [eva:alarm] tests/value/logic.c:103: Warning: assertion got status unknown.
@@ -56,20 +56,20 @@
 [eva] Recording results for eq_tsets
 [eva] Done for function eq_tsets
 [eva] computing for function eq_char <- main.
-  Called from tests/value/logic.c:359.
+  Called from tests/value/logic.c:442.
 [eva] tests/value/logic.c:149: Frama_C_show_each: {-126}
 [eva] tests/value/logic.c:150: assertion got status valid.
 [eva] tests/value/logic.c:151: assertion got status valid.
 [eva] Recording results for eq_char
 [eva] Done for function eq_char
 [eva] computing for function casts <- main.
-  Called from tests/value/logic.c:360.
+  Called from tests/value/logic.c:443.
 [eva] tests/value/logic.c:155: assertion got status valid.
 [eva] tests/value/logic.c:156: assertion got status valid.
 [eva] Recording results for casts
 [eva] Done for function casts
 [eva] computing for function empty_tset <- main.
-  Called from tests/value/logic.c:361.
+  Called from tests/value/logic.c:444.
 [eva] computing for function f_empty_tset <- empty_tset <- main.
   Called from tests/value/logic.c:166.
 [eva] using specification for function f_empty_tset
@@ -82,7 +82,7 @@
 [eva] Recording results for empty_tset
 [eva] Done for function empty_tset
 [eva] computing for function reduce_by_equal <- main.
-  Called from tests/value/logic.c:362.
+  Called from tests/value/logic.c:445.
 [eva:alarm] tests/value/logic.c:172: Warning: 
   accessing out of bounds index. assert 0 ≤ v;
 [eva:alarm] tests/value/logic.c:172: Warning: 
@@ -92,7 +92,7 @@
 [eva] Recording results for reduce_by_equal
 [eva] Done for function reduce_by_equal
 [eva] computing for function alarms <- main.
-  Called from tests/value/logic.c:363.
+  Called from tests/value/logic.c:446.
 [eva:alarm] tests/value/logic.c:182: Warning: 
   assertion 'ASSUME' got status unknown.
 [eva:alarm] tests/value/logic.c:184: Warning: 
@@ -124,7 +124,7 @@
 [eva] Recording results for alarms
 [eva] Done for function alarms
 [eva] computing for function cond_in_lval <- main.
-  Called from tests/value/logic.c:364.
+  Called from tests/value/logic.c:447.
 [eva] computing for function select_like <- cond_in_lval <- main.
   Called from tests/value/logic.c:228.
 [eva] using specification for function select_like
@@ -152,7 +152,7 @@
 [eva] Recording results for cond_in_lval
 [eva] Done for function cond_in_lval
 [eva] computing for function pred <- main.
-  Called from tests/value/logic.c:365.
+  Called from tests/value/logic.c:448.
 [eva] tests/value/logic.c:90: assertion got status valid.
 [eva] tests/value/logic.c:91: assertion got status valid.
 [eva] tests/value/logic.c:31: 
@@ -201,7 +201,7 @@
 [eva] Recording results for pred
 [eva] Done for function pred
 [eva] computing for function float_sign <- main.
-  Called from tests/value/logic.c:366.
+  Called from tests/value/logic.c:449.
 [eva] tests/value/logic.c:251: assertion got status valid.
 [eva] tests/value/logic.c:252: assertion got status valid.
 [eva] tests/value/logic.c:253: assertion got status valid.
@@ -210,7 +210,7 @@
 [eva] Recording results for float_sign
 [eva] Done for function float_sign
 [eva] computing for function min_max <- main.
-  Called from tests/value/logic.c:367.
+  Called from tests/value/logic.c:450.
 [eva] computing for function Frama_C_interval <- min_max <- main.
   Called from tests/value/logic.c:274.
 [eva] using specification for function Frama_C_interval
@@ -235,7 +235,7 @@
 [eva] Recording results for min_max
 [eva] Done for function min_max
 [eva] computing for function assign_tsets <- main.
-  Called from tests/value/logic.c:368.
+  Called from tests/value/logic.c:451.
 [eva] computing for function assign_tsets_aux <- assign_tsets <- main.
   Called from tests/value/logic.c:269.
 [eva] using specification for function assign_tsets_aux
@@ -243,7 +243,7 @@
 [eva] Recording results for assign_tsets
 [eva] Done for function assign_tsets
 [eva] computing for function check_and_assert <- main.
-  Called from tests/value/logic.c:369.
+  Called from tests/value/logic.c:452.
 [eva:alarm] tests/value/logic.c:295: Warning: assertion got status unknown.
 [eva] tests/value/logic.c:296: Frama_C_show_each_42: {42}
 [eva] tests/value/logic.c:297: check got status valid.
@@ -258,7 +258,7 @@
 [eva] Recording results for check_and_assert
 [eva] Done for function check_and_assert
 [eva] computing for function min_max_quantifier <- main.
-  Called from tests/value/logic.c:370.
+  Called from tests/value/logic.c:453.
 [eva] tests/value/logic.c:321: check 'valid' got status valid.
 [eva] tests/value/logic.c:322: check 'valid' got status valid.
 [eva] tests/value/logic.c:323: check 'valid' got status valid.
@@ -331,6 +331,188 @@
   check 'unknown' got status unknown.
 [eva] Recording results for min_max_quantifier
 [eva] Done for function min_max_quantifier
+[eva] computing for function int_abs <- main.
+  Called from tests/value/logic.c:454.
+[eva] computing for function abs <- int_abs <- main.
+  Called from tests/value/logic.c:365.
+[eva] using specification for function abs
+[eva] Done for function abs
+[eva] computing for function abs <- int_abs <- main.
+  Called from tests/value/logic.c:366.
+[eva] Done for function abs
+[eva] computing for function abs <- int_abs <- main.
+  Called from tests/value/logic.c:367.
+[eva] Done for function abs
+[eva] computing for function Frama_C_interval <- int_abs <- main.
+  Called from tests/value/logic.c:370.
+[eva] tests/value/logic.c:370: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function abs <- int_abs <- main.
+  Called from tests/value/logic.c:371.
+[eva] Done for function abs
+[eva] tests/value/logic.c:372: Frama_C_show_each_5_10: {5; 6; 7; 8; 9; 10}
+[eva] computing for function Frama_C_interval <- int_abs <- main.
+  Called from tests/value/logic.c:373.
+[eva] tests/value/logic.c:373: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function abs <- int_abs <- main.
+  Called from tests/value/logic.c:374.
+[eva] Done for function abs
+[eva] tests/value/logic.c:375: Frama_C_show_each_0_4: {0; 1; 2; 3; 4}
+[eva] computing for function Frama_C_interval <- int_abs <- main.
+  Called from tests/value/logic.c:377.
+[eva] tests/value/logic.c:377: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function abs <- int_abs <- main.
+  Called from tests/value/logic.c:378.
+[eva] Done for function abs
+[eva] tests/value/logic.c:379: Frama_C_show_each_10_100: [10..100]
+[eva] computing for function Frama_C_interval <- int_abs <- main.
+  Called from tests/value/logic.c:380.
+[eva] tests/value/logic.c:380: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function abs <- int_abs <- main.
+  Called from tests/value/logic.c:381.
+[eva] Done for function abs
+[eva] tests/value/logic.c:382: Frama_C_show_each_0_100: [0..100]
+[eva] computing for function Frama_C_interval <- int_abs <- main.
+  Called from tests/value/logic.c:383.
+[eva] tests/value/logic.c:383: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function abs <- int_abs <- main.
+  Called from tests/value/logic.c:384.
+[eva] Done for function abs
+[eva] tests/value/logic.c:385: Frama_C_show_each_10_20: [10..20]
+[eva] computing for function Frama_C_interval <- int_abs <- main.
+  Called from tests/value/logic.c:386.
+[eva] tests/value/logic.c:386: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function abs <- int_abs <- main.
+  Called from tests/value/logic.c:387.
+[eva] Done for function abs
+[eva] tests/value/logic.c:388: Frama_C_show_each_0_12: [0..12]
+[eva] computing for function Frama_C_interval <- int_abs <- main.
+  Called from tests/value/logic.c:389.
+[eva] tests/value/logic.c:389: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function abs <- int_abs <- main.
+  Called from tests/value/logic.c:390.
+[eva] Done for function abs
+[eva] tests/value/logic.c:391: Frama_C_show_each_0_16: [0..16]
+[eva] computing for function Frama_C_interval <- int_abs <- main.
+  Called from tests/value/logic.c:393.
+[eva] tests/value/logic.c:393: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function abs <- int_abs <- main.
+  Called from tests/value/logic.c:395.
+[eva] Done for function abs
+[eva] tests/value/logic.c:396: Frama_C_show_each_2_mod_4: [2..82],2%4
+[eva] computing for function Frama_C_interval <- int_abs <- main.
+  Called from tests/value/logic.c:397.
+[eva] tests/value/logic.c:397: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function abs <- int_abs <- main.
+  Called from tests/value/logic.c:399.
+[eva] Done for function abs
+[eva] tests/value/logic.c:400: Frama_C_show_each_1_mod_2: [1..83],1%2
+[eva] computing for function Frama_C_interval <- int_abs <- main.
+  Called from tests/value/logic.c:401.
+[eva] tests/value/logic.c:401: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function abs <- int_abs <- main.
+  Called from tests/value/logic.c:403.
+[eva] Done for function abs
+[eva] tests/value/logic.c:404: Frama_C_show_each_no_mod: [0..35]
+[eva] computing for function Frama_C_interval <- int_abs <- main.
+  Called from tests/value/logic.c:406.
+[eva] tests/value/logic.c:406: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function abs <- int_abs <- main.
+  Called from tests/value/logic.c:407.
+[eva] Done for function abs
+[eva] tests/value/logic.c:408: Frama_C_show_each_set: {0; 1; 2; 3; 4; 5}
+[eva] computing for function abs <- int_abs <- main.
+  Called from tests/value/logic.c:411.
+[eva] Done for function abs
+[eva] tests/value/logic.c:411: 
+  Assigning imprecise value to x_0.
+  The imprecision originates from Library function {tests/value/logic.c:411}
+[eva] tests/value/logic.c:412: 
+  Frama_C_show_each_gm:
+  {{ garbled mix of &{x_0}
+  (origin: Library function {tests/value/logic.c:411}) }}
+[eva] Recording results for int_abs
+[eva] Done for function int_abs
+[eva] computing for function float_abs <- main.
+  Called from tests/value/logic.c:455.
+[eva] computing for function fabs <- float_abs <- main.
+  Called from tests/value/logic.c:421.
+[eva] using specification for function fabs
+[eva] Done for function fabs
+[eva] computing for function fabs <- float_abs <- main.
+  Called from tests/value/logic.c:422.
+[eva] Done for function fabs
+[eva] computing for function fabs <- float_abs <- main.
+  Called from tests/value/logic.c:423.
+[eva] Done for function fabs
+[eva] computing for function Frama_C_double_interval <- float_abs <- main.
+  Called from tests/value/logic.c:426.
+[eva] using specification for function Frama_C_double_interval
+[eva] tests/value/logic.c:426: 
+  function Frama_C_double_interval: precondition 'finite' got status valid.
+[eva] tests/value/logic.c:426: 
+  function Frama_C_double_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_double_interval
+[eva] computing for function fabs <- float_abs <- main.
+  Called from tests/value/logic.c:427.
+[eva] Done for function fabs
+[eva] tests/value/logic.c:428: Frama_C_show_each_zero: [-0. .. 0.]
+[eva] computing for function Frama_C_double_interval <- float_abs <- main.
+  Called from tests/value/logic.c:429.
+[eva] tests/value/logic.c:429: 
+  function Frama_C_double_interval: precondition 'finite' got status valid.
+[eva] tests/value/logic.c:429: 
+  function Frama_C_double_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_double_interval
+[eva] computing for function fabs <- float_abs <- main.
+  Called from tests/value/logic.c:430.
+[eva] Done for function fabs
+[eva] tests/value/logic.c:431: Frama_C_show_each_half_two: [0.5 .. 2.]
+[eva] computing for function Frama_C_double_interval <- float_abs <- main.
+  Called from tests/value/logic.c:432.
+[eva] tests/value/logic.c:432: 
+  function Frama_C_double_interval: precondition 'finite' got status valid.
+[eva] tests/value/logic.c:432: 
+  function Frama_C_double_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_double_interval
+[eva] computing for function fabs <- float_abs <- main.
+  Called from tests/value/logic.c:433.
+[eva] Done for function fabs
+[eva] tests/value/logic.c:434: Frama_C_show_each_0_10: [-0. .. 10.]
+[eva] computing for function Frama_C_double_interval <- float_abs <- main.
+  Called from tests/value/logic.c:435.
+[eva] tests/value/logic.c:435: 
+  function Frama_C_double_interval: precondition 'finite' got status valid.
+[eva] tests/value/logic.c:435: 
+  function Frama_C_double_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_double_interval
+[eva] computing for function fabs <- float_abs <- main.
+  Called from tests/value/logic.c:436.
+[eva] Done for function fabs
+[eva] tests/value/logic.c:437: Frama_C_show_each_0_3: [-0. .. 3.]
+[eva] Recording results for float_abs
+[eva] Done for function float_abs
 [eva] Recording results for main
 [eva] done for function main
 [scope:rm_asserts] removing 5 assertion(s)
@@ -358,6 +540,12 @@
   temp_2 ∈ {0}
 [eva:final-states] Values at end of function empty_tset:
   T[0] ∈ {2}
+[eva:final-states] Values at end of function float_abs:
+  Frama_C_entropy_source ∈ [--..--]
+  zero ∈ [-0. .. 0.]
+  ten ∈ {10.}
+  eleven ∈ {11.}
+  x_0 ∈ [-0. .. 3.]
 [eva:final-states] Values at end of function float_sign:
   d ∈ [-0. .. 0.]
 [eva:final-states] Values at end of function g:
@@ -372,6 +560,14 @@
   j ∈ {6}
   p ∈ {{ &k }}
   q ∈ {{ &j }}
+[eva:final-states] Values at end of function int_abs:
+  Frama_C_entropy_source ∈ [--..--]
+  zero ∈ {0}
+  ten ∈ {10}
+  eleven ∈ {11}
+  x_0 ∈
+     {{ garbled mix of &{x_0}
+      (origin: Library function {tests/value/logic.c:411}) }}
 [eva:final-states] Values at end of function min_max:
   Frama_C_entropy_source ∈ [--..--]
   x_0 ∈ [3..17]
@@ -501,15 +697,25 @@
 [from] Computing for function f_empty_tset <-empty_tset
 [from] Done for function f_empty_tset
 [from] Done for function empty_tset
+[from] Computing for function float_abs
+[from] Computing for function fabs <-float_abs
+[from] Done for function fabs
+[from] Computing for function Frama_C_double_interval <-float_abs
+[from] Done for function Frama_C_double_interval
+[from] Done for function float_abs
 [from] Computing for function float_sign
 [from] Done for function float_sign
 [from] Computing for function g
 [from] Done for function g
 [from] Computing for function h
 [from] Done for function h
-[from] Computing for function min_max
-[from] Computing for function Frama_C_interval <-min_max
+[from] Computing for function int_abs
+[from] Computing for function abs <-int_abs
+[from] Done for function abs
+[from] Computing for function Frama_C_interval <-int_abs
 [from] Done for function Frama_C_interval
+[from] Done for function int_abs
+[from] Computing for function min_max
 [from] Done for function min_max
 [from] Computing for function min_max_quantifier
 [from] Done for function min_max_quantifier
@@ -527,9 +733,14 @@
 [from] Done for function main
 [from] ====== DEPENDENCIES COMPUTED ======
   These dependencies hold at termination for the executions that terminate:
+[from] Function Frama_C_double_interval:
+  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+  \result FROM Frama_C_entropy_source; min; max
 [from] Function Frama_C_interval:
   Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
   \result FROM Frama_C_entropy_source; min; max
+[from] Function abs:
+  \result FROM x
 [from] Function alarms:
   NO EFFECTS
 [from] Function assign_tsets_aux:
@@ -551,12 +762,18 @@
   NO EFFECTS
 [from] Function empty_tset:
   NO EFFECTS
+[from] Function fabs:
+  \result FROM f
+[from] Function float_abs:
+  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
 [from] Function float_sign:
   NO EFFECTS
 [from] Function g:
   NO EFFECTS
 [from] Function h:
   s1.f1 FROM \nothing
+[from] Function int_abs:
+  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
 [from] Function min_max:
   Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
 [from] Function min_max_quantifier:
@@ -613,6 +830,10 @@
     T[0]
 [inout] Inputs for function empty_tset:
     \nothing
+[inout] Out (internal) for function float_abs:
+    Frama_C_entropy_source; zero; ten; eleven; x_0
+[inout] Inputs for function float_abs:
+    Frama_C_entropy_source
 [inout] Out (internal) for function float_sign:
     d; tmp
 [inout] Inputs for function float_sign:
@@ -625,6 +846,10 @@
     s1.f1; x_0; y; k; j; p; q
 [inout] Inputs for function h:
     v
+[inout] Out (internal) for function int_abs:
+    Frama_C_entropy_source; zero; ten; eleven; x_0
+[inout] Inputs for function int_abs:
+    Frama_C_entropy_source
 [inout] Out (internal) for function min_max:
     Frama_C_entropy_source; x_0; y; z; r1; r2; r3; r4; a; b; d
 [inout] Inputs for function min_max: