Merge branch 'feature/basile/eacsl-remove-fc-dev-output' into 'master'

[eacsl] Update tests

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

src/plugins/e-acsl/tests/arith/oracle_dev/arith.res.oracle

-[kernel] Parsing tests/arith/arith.i (no preprocessing)

src/plugins/e-acsl/tests/arith/oracle_dev/array.res.oracle

-[kernel] Parsing tests/arith/array.i (no preprocessing)

src/plugins/e-acsl/tests/arith/oracle_dev/at.res.oracle

-[kernel] Parsing tests/arith/at.i (no preprocessing)

src/plugins/e-acsl/tests/arith/oracle_dev/at_on-purely-logic-variables.res.oracle

-[kernel] Parsing tests/arith/at_on-purely-logic-variables.c (with preprocessing)

src/plugins/e-acsl/tests/arith/oracle_dev/bitwise.res.oracle

-[kernel] Parsing tests/arith/bitwise.c (with preprocessing)

src/plugins/e-acsl/tests/arith/oracle_dev/cast.res.oracle

-[kernel] Parsing tests/arith/cast.i (no preprocessing)

src/plugins/e-acsl/tests/arith/oracle_dev/comparison.res.oracle

-[kernel] Parsing tests/arith/comparison.i (no preprocessing)

src/plugins/e-acsl/tests/arith/oracle_dev/functions.res.oracle

-[kernel] Parsing tests/arith/functions.c (with preprocessing)

src/plugins/e-acsl/tests/arith/oracle_dev/functions_rec.res.oracle

-[kernel] Parsing tests/arith/functions_rec.c (with preprocessing)

src/plugins/e-acsl/tests/arith/oracle_dev/integer_constant.res.oracle

-[kernel] Parsing tests/arith/integer_constant.i (no preprocessing)

src/plugins/e-acsl/tests/arith/oracle_dev/let.res.oracle

-[kernel] Parsing tests/arith/let.c (with preprocessing)

src/plugins/e-acsl/tests/arith/oracle_dev/longlong.res.oracle

-[kernel] Parsing tests/arith/longlong.i (no preprocessing)

src/plugins/e-acsl/tests/arith/oracle_dev/not.res.oracle

-[kernel] Parsing tests/arith/not.i (no preprocessing)

src/plugins/e-acsl/tests/arith/oracle_dev/quantif.res.oracle

-[kernel] Parsing tests/arith/quantif.i (no preprocessing)

src/plugins/e-acsl/tests/arith/oracle_dev/rationals.res.oracle

-[kernel] Parsing tests/arith/rationals.c (with preprocessing)
-[kernel:parser:decimal-float] tests/arith/rationals.c:19: Warning: 
-  Floating-point constant 0.2f is not represented exactly. Will use 0x1.99999a0000000p-3.
-  (warn-once: no further messages from category 'parser:decimal-float' will be emitted)

src/plugins/e-acsl/tests/bts/bts2252.c

@@ -3,6 +3,7 @@
 */
 
 #include <stdlib.h>
+#include <string.h>
 
 int main() {
   char* srcbuf = "Test Code";

src/plugins/e-acsl/tests/bts/oracle_ci/bts2252.res.oracle

-[kernel:typing:implicit-function-declaration] tests/bts/bts2252.c:22: Warning: 
-  Calling undeclared function strncpy. Old style K&R code?
 [e-acsl] beginning translation.
+[e-acsl] Warning: annotating undefined function `strncpy':
+  the generated program may miss memory instrumentation
+  if there are memory-related annotations.
+[e-acsl] FRAMAC_SHARE/libc/string.h:362: Warning: 
+  E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:363: Warning: 
+  E-ACSL construct `logic functions with labels' is not yet supported.
+  Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:366: Warning: 
+  E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:372: Warning: 
+  E-ACSL construct `logic functions performing read accesses'
+  is not yet supported.
+  Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:372: Warning: 
+  E-ACSL construct `assigns clause in behavior' is not yet supported.
+  Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:375: Warning: 
+  E-ACSL construct `logic functions performing read accesses'
+  is not yet supported.
+  Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/bts/bts2252.c:17: Warning: 
+[eva:alarm] tests/bts/bts2252.c:18: Warning: 
   out of bounds read. assert \valid_read(srcbuf + i);

src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2252.c

 /* Generated by Frama-C */
 #include "stdio.h"
 #include "stdlib.h"
+#include "string.h"
 char *__gen_e_acsl_literal_string;
-extern int ( /* missing proto */ strncpy)(char *x_0, char *x_1, int x_2);
+extern int __e_acsl_sound_verdict;
+
+/*@ requires valid_nstring_src: valid_read_nstring(src, n);
+    requires room_nstring: \valid(dest + (0 .. n - 1));
+    requires separation: \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
+    ensures result_ptr: \result ≡ \old(dest);
+    ensures initialization: \initialized(\old(dest) + (0 .. \old(n) - 1));
+    assigns *(dest + (0 .. n - 1)), \result;
+    assigns *(dest + (0 .. n - 1)) \from *(src + (0 .. n - 1));
+    assigns \result \from dest;
+    
+    behavior complete:
+      assumes src_fits: strlen(src) < n;
+      ensures equal_after_copy: strcmp(\old(dest), \old(src)) ≡ 0;
+    
+    behavior partial:
+      assumes src_too_long: n ≤ strlen(src);
+      ensures
+        equal_prefix:
+          memcmp{Post, Post}(\old(dest), \old(src), \old(n)) ≡ 0;
+ */
+char *__gen_e_acsl_strncpy(char * __restrict dest,
+                           char const * __restrict src, size_t n);
+
+/*@ requires valid_nstring_src: valid_read_nstring(src, n);
+    requires room_nstring: \valid(dest + (0 .. n - 1));
+    requires separation: \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
+    ensures result_ptr: \result ≡ \old(dest);
+    ensures initialization: \initialized(\old(dest) + (0 .. \old(n) - 1));
+    assigns *(dest + (0 .. n - 1)), \result;
+    assigns *(dest + (0 .. n - 1)) \from *(src + (0 .. n - 1));
+    assigns \result \from dest;
+    
+    behavior complete:
+      assumes src_fits: strlen(src) < n;
+      ensures equal_after_copy: strcmp(\old(dest), \old(src)) ≡ 0;
+    
+    behavior partial:
+      assumes src_too_long: n ≤ strlen(src);
+      ensures
+        equal_prefix:
+          memcmp{Post, Post}(\old(dest), \old(src), \old(n)) ≡ 0;
+ */
+char *__gen_e_acsl_strncpy(char * __restrict dest,
+                           char const * __restrict src, size_t n)
+{
+  __e_acsl_mpz_t __gen_e_acsl_at_3;
+  char *__gen_e_acsl_at_2;
+  char *__gen_e_acsl_at;
+  char *__retres;
+  {
+    __e_acsl_mpz_t __gen_e_acsl_n;
+    __e_acsl_mpz_t __gen_e_acsl_;
+    __e_acsl_mpz_t __gen_e_acsl_sub;
+    __e_acsl_mpz_t __gen_e_acsl__2;
+    __e_acsl_mpz_t __gen_e_acsl_sub_2;
+    __e_acsl_mpz_t __gen_e_acsl_add;
+    unsigned long __gen_e_acsl__3;
+    int __gen_e_acsl_valid;
+    __e_acsl_store_block((void *)(& dest),(size_t)8);
+    __gmpz_init_set_ui(__gen_e_acsl_n,n);
+    __gmpz_init_set_si(__gen_e_acsl_,1L);
+    __gmpz_init(__gen_e_acsl_sub);
+    __gmpz_sub(__gen_e_acsl_sub,
+               (__e_acsl_mpz_struct const *)(__gen_e_acsl_n),
+               (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+    __gmpz_init_set_si(__gen_e_acsl__2,0L);
+    __gmpz_init(__gen_e_acsl_sub_2);
+    __gmpz_sub(__gen_e_acsl_sub_2,
+               (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub),
+               (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+    __gmpz_init(__gen_e_acsl_add);
+    __gmpz_add(__gen_e_acsl_add,
+               (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_2),
+               (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+    __gen_e_acsl__3 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
+    __gen_e_acsl_valid = __e_acsl_valid((void *)(dest + 1 * 0),
+                                        __gen_e_acsl__3,(void *)dest,
+                                        (void *)(& dest));
+    __e_acsl_assert(__gen_e_acsl_valid,"Precondition","strncpy",
+                    "\\valid(dest + (0 .. n - 1))",
+                    "FRAMAC_SHARE/libc/string.h",364);
+    __gmpz_clear(__gen_e_acsl_n);
+    __gmpz_clear(__gen_e_acsl_);
+    __gmpz_clear(__gen_e_acsl_sub);
+    __gmpz_clear(__gen_e_acsl__2);
+    __gmpz_clear(__gen_e_acsl_sub_2);
+    __gmpz_clear(__gen_e_acsl_add);
+  }
+  {
+    __e_acsl_mpz_t __gen_e_acsl_n_2;
+    __gmpz_init_set_ui(__gen_e_acsl_n_2,n);
+    __gmpz_init_set(__gen_e_acsl_at_3,
+                    (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_2));
+    __gmpz_clear(__gen_e_acsl_n_2);
+  }
+  __gen_e_acsl_at_2 = dest;
+  __gen_e_acsl_at = dest;
+  __retres = strncpy(dest,src,n);
+  {
+    __e_acsl_mpz_t __gen_e_acsl__4;
+    __e_acsl_mpz_t __gen_e_acsl_sub_3;
+    __e_acsl_mpz_t __gen_e_acsl__5;
+    __e_acsl_mpz_t __gen_e_acsl_sub_4;
+    __e_acsl_mpz_t __gen_e_acsl_add_2;
+    unsigned long __gen_e_acsl__6;
+    int __gen_e_acsl_initialized;
+    __e_acsl_assert(__retres == __gen_e_acsl_at,"Postcondition","strncpy",
+                    "\\result == \\old(dest)","FRAMAC_SHARE/libc/string.h",
+                    369);
+    __gmpz_init_set_si(__gen_e_acsl__4,1L);
+    __gmpz_init(__gen_e_acsl_sub_3);
+    __gmpz_sub(__gen_e_acsl_sub_3,
+               (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_3),
+               (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
+    __gmpz_init_set_si(__gen_e_acsl__5,0L);
+    __gmpz_init(__gen_e_acsl_sub_4);
+    __gmpz_sub(__gen_e_acsl_sub_4,
+               (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_3),
+               (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
+    __gmpz_init(__gen_e_acsl_add_2);
+    __gmpz_add(__gen_e_acsl_add_2,
+               (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_4),
+               (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
+    __gen_e_acsl__6 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2));
+    __gen_e_acsl_initialized = __e_acsl_initialized((void *)(__gen_e_acsl_at_2 + 
+                                                             1 * 0),
+                                                    __gen_e_acsl__6);
+    __e_acsl_assert(__gen_e_acsl_initialized,"Postcondition","strncpy",
+                    "\\initialized(\\old(dest) + (0 .. \\old(n) - 1))",
+                    "FRAMAC_SHARE/libc/string.h",370);
+    __e_acsl_delete_block((void *)(& dest));
+    __gmpz_clear(__gen_e_acsl__4);
+    __gmpz_clear(__gen_e_acsl_sub_3);
+    __gmpz_clear(__gen_e_acsl__5);
+    __gmpz_clear(__gen_e_acsl_sub_4);
+    __gmpz_clear(__gen_e_acsl_add_2);
+    __gmpz_clear(__gen_e_acsl_at_3);
+    return __retres;
+  }
+}
 
 void __e_acsl_globals_init(void)
 {
@@ -29,6 +170,8 @@ int main(void)
   __e_acsl_full_init((void *)(& srcbuf));
   int loc = 1;
   char *destbuf = malloc((unsigned long)10 * sizeof(char));
+  __e_acsl_store_block((void *)(& destbuf),(size_t)8);
+  __e_acsl_full_init((void *)(& destbuf));
   char ch = (char)'o';
   if (destbuf != (char *)0) {
     i = -1;
@@ -40,17 +183,19 @@ int main(void)
                                                       (void *)srcbuf,
                                                       (void *)(& srcbuf));
         __e_acsl_assert(! __gen_e_acsl_valid_read,"Assertion","main",
-                        "!\\valid_read(srcbuf + i)","tests/bts/bts2252.c",16);
+                        "!\\valid_read(srcbuf + i)","tests/bts/bts2252.c",17);
       }
       /*@ assert ¬\valid_read(srcbuf + i); */ ;
       /*@ assert Eva: mem_access: \valid_read(srcbuf + i); */
       if ((int)*(srcbuf + i) == (int)ch) loc = i;
       i ++;
     }
-    strncpy(destbuf + loc,srcbuf + loc,1);
+    __gen_e_acsl_strncpy(destbuf + loc,(char const *)(srcbuf + loc),
+                         (unsigned long)1);
     free((void *)destbuf);
   }
   __retres = 0;
+  __e_acsl_delete_block((void *)(& destbuf));
   __e_acsl_delete_block((void *)(& srcbuf));
   __e_acsl_memory_clean();
   return __retres;

src/plugins/e-acsl/tests/bts/oracle_dev/bts1304.res.oracle

-[kernel] Parsing tests/bts/bts1304.i (no preprocessing)

src/plugins/e-acsl/tests/bts/oracle_dev/bts1307.res.oracle

-[kernel] Parsing tests/bts/bts1307.i (no preprocessing)
-[kernel:parser:decimal-float] tests/bts/bts1307.i:17: Warning: 
-  Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2.
-  (warn-once: no further messages from category 'parser:decimal-float' will be emitted)