Merge branch 'fix/andre/libc-imaxabs' into 'master'

[Libc] fix spec of imaxabs and add test

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

share/libc/inttypes.h

@@ -253,9 +253,12 @@ typedef struct __fc_imaxdiv_t
   } imaxdiv_t;
 
 /* ISO C: 7.8.2 */
-/*@ 
-  requires abs_representable: (intmax_t)(-c) != c ;
-  assigns \result \from c ; 
+/*@
+  requires abs_representable: c > INTMAX_MIN;
+  assigns \result \from c;
+  ensures positive_result: \result >= 0.;
+  ensures equal_magnitude_result: \result == c || \result == -c;
+  ensures logical_abs_result: \result == \abs(c);
 */
 extern intmax_t imaxabs(intmax_t c);
 

tests/libc/inttypes_h2.c

@@ -22,4 +22,11 @@ void main() {
   r = imaxdiv(a, b);
   //@ assert r.quot == 2;
   //@ assert r.rem == 1;
+
+  a = imaxabs(INTMAX_MAX);
+  //@ assert a == INTMAX_MAX;
+  a = imaxabs(INTMAX_MIN + 1);
+  //@ assert a >= 0;
+  a = imaxabs(0);
+  //@ assert a == 0;
 }

tests/libc/oracle/fc_libc.1.res.oracle

@@ -2671,7 +2671,11 @@ imaxdiv_t imaxdiv(intmax_t numer, intmax_t denom);
 extern intmax_t strtoimax(char const * __restrict nptr,
                           char ** __restrict endptr, int base);
 
-/*@ requires abs_representable: (long long)(-c) ≢ c;
+/*@ requires abs_representable: c > -9223372036854775807LL - 1LL;
+    ensures positive_result: \result ≥ 0.;
+    ensures
+      equal_magnitude_result: \result ≡ \old(c) ∨ \result ≡ -\old(c);
+    ensures logical_abs_result: \result ≡ \abs(\old(c));
     assigns \result;
     assigns \result \from c;
  */

tests/libc/oracle/inttypes_h2.res.oracle

@@ -28,11 +28,30 @@
 [eva] Done for function imaxdiv
 [eva] tests/libc/inttypes_h2.c:23: assertion got status valid.
 [eva] tests/libc/inttypes_h2.c:24: assertion got status valid.
+[eva] computing for function imaxabs <- main.
+  Called from tests/libc/inttypes_h2.c:26.
+[eva] using specification for function imaxabs
+[eva] tests/libc/inttypes_h2.c:26: 
+  function imaxabs: precondition 'abs_representable' got status valid.
+[eva] Done for function imaxabs
+[eva] tests/libc/inttypes_h2.c:27: assertion got status valid.
+[eva] computing for function imaxabs <- main.
+  Called from tests/libc/inttypes_h2.c:28.
+[eva] tests/libc/inttypes_h2.c:28: 
+  function imaxabs: precondition 'abs_representable' got status valid.
+[eva] Done for function imaxabs
+[eva] tests/libc/inttypes_h2.c:29: assertion got status valid.
+[eva] computing for function imaxabs <- main.
+  Called from tests/libc/inttypes_h2.c:30.
+[eva] tests/libc/inttypes_h2.c:30: 
+  function imaxabs: precondition 'abs_representable' got status valid.
+[eva] Done for function imaxabs
+[eva] tests/libc/inttypes_h2.c:31: assertion got status valid.
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
-  a ∈ {9223372036854775807}
+  a ∈ {0}
   b ∈ {4611686018427387903}
   r.quot ∈ {2}
    .rem ∈ {1}