[e-acsl:tests] update tests

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

 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 void duffcopy(char *to, char *from, int count)

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

 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 char *__gen_e_acsl_literal_string;

src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-91.c

@@ -36,24 +36,6 @@ void __e_acsl_globals_init(void)
     __e_acsl_full_init((void *)(& b));
     __e_acsl_store_block((void *)(& a),(size_t)2);
     __e_acsl_full_init((void *)(& a));
-    __e_acsl_store_block((void *)(& __fc_p_tmpnam),(size_t)8);
-    __e_acsl_full_init((void *)(& __fc_p_tmpnam));
-    __e_acsl_store_block((void *)(__fc_tmpnam),(size_t)2048);
-    __e_acsl_full_init((void *)(& __fc_tmpnam));
-    __e_acsl_store_block((void *)(& __fc_p_fopen),(size_t)8);
-    __e_acsl_full_init((void *)(& __fc_p_fopen));
-    __e_acsl_store_block((void *)(__fc_fopen),(size_t)128);
-    __e_acsl_full_init((void *)(& __fc_fopen));
-    __e_acsl_store_block((void *)(& stdin),(size_t)8);
-    __e_acsl_full_init((void *)(& stdin));
-    __e_acsl_store_block((void *)(& __fc_p_random48_counter),(size_t)8);
-    __e_acsl_full_init((void *)(& __fc_p_random48_counter));
-    __e_acsl_store_block((void *)(random48_counter),(size_t)6);
-    __e_acsl_full_init((void *)(& random48_counter));
-    __e_acsl_store_block((void *)(& __fc_random48_init),(size_t)4);
-    __e_acsl_full_init((void *)(& __fc_random48_init));
-    __e_acsl_store_block((void *)(& __fc_rand_max),(size_t)8);
-    __e_acsl_full_init((void *)(& __fc_rand_max));
   }
   return;
 }
@@ -62,15 +44,6 @@ void __e_acsl_globals_delete(void)
 {
   __e_acsl_delete_block((void *)(& b));
   __e_acsl_delete_block((void *)(& a));
-  __e_acsl_delete_block((void *)(& __fc_p_tmpnam));
-  __e_acsl_delete_block((void *)(__fc_tmpnam));
-  __e_acsl_delete_block((void *)(& __fc_p_fopen));
-  __e_acsl_delete_block((void *)(__fc_fopen));
-  __e_acsl_delete_block((void *)(& stdin));
-  __e_acsl_delete_block((void *)(& __fc_p_random48_counter));
-  __e_acsl_delete_block((void *)(random48_counter));
-  __e_acsl_delete_block((void *)(& __fc_random48_init));
-  __e_acsl_delete_block((void *)(& __fc_rand_max));
 }
 
 int main(void)

src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf.c

@@ -35,24 +35,6 @@ void __e_acsl_globals_init(void)
     __e_acsl_already_run = 1;
     __e_acsl_store_block((void *)(& f),(size_t)1);
     __e_acsl_full_init((void *)(& f));
-    __e_acsl_store_block((void *)(& __fc_p_tmpnam),(size_t)8);
-    __e_acsl_full_init((void *)(& __fc_p_tmpnam));
-    __e_acsl_store_block((void *)(__fc_tmpnam),(size_t)2048);
-    __e_acsl_full_init((void *)(& __fc_tmpnam));
-    __e_acsl_store_block((void *)(& __fc_p_fopen),(size_t)8);
-    __e_acsl_full_init((void *)(& __fc_p_fopen));
-    __e_acsl_store_block((void *)(__fc_fopen),(size_t)128);
-    __e_acsl_full_init((void *)(& __fc_fopen));
-    __e_acsl_store_block((void *)(& stdin),(size_t)8);
-    __e_acsl_full_init((void *)(& stdin));
-    __e_acsl_store_block((void *)(& __fc_p_random48_counter),(size_t)8);
-    __e_acsl_full_init((void *)(& __fc_p_random48_counter));
-    __e_acsl_store_block((void *)(random48_counter),(size_t)6);
-    __e_acsl_full_init((void *)(& random48_counter));
-    __e_acsl_store_block((void *)(& __fc_random48_init),(size_t)4);
-    __e_acsl_full_init((void *)(& __fc_random48_init));
-    __e_acsl_store_block((void *)(& __fc_rand_max),(size_t)8);
-    __e_acsl_full_init((void *)(& __fc_rand_max));
   }
   return;
 }
@@ -60,15 +42,6 @@ void __e_acsl_globals_init(void)
 void __e_acsl_globals_delete(void)
 {
   __e_acsl_delete_block((void *)(& f));
-  __e_acsl_delete_block((void *)(& __fc_p_tmpnam));
-  __e_acsl_delete_block((void *)(__fc_tmpnam));
-  __e_acsl_delete_block((void *)(& __fc_p_fopen));
-  __e_acsl_delete_block((void *)(__fc_fopen));
-  __e_acsl_delete_block((void *)(& stdin));
-  __e_acsl_delete_block((void *)(& __fc_p_random48_counter));
-  __e_acsl_delete_block((void *)(random48_counter));
-  __e_acsl_delete_block((void *)(& __fc_random48_init));
-  __e_acsl_delete_block((void *)(& __fc_rand_max));
 }
 
 int main(void)

src/plugins/e-acsl/tests/memory/oracle_ci/gen_constructor.c

 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 char *__gen_e_acsl_literal_string_2;

src/plugins/e-acsl/tests/memory/oracle_ci/gen_errno.c

 /* Generated by Frama-C */
 #include "errno.h"
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 void __e_acsl_globals_init(void)

src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_goto.c

 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 char *__gen_e_acsl_literal_string_2;

src/plugins/e-acsl/tests/memory/oracle_ci/gen_mainargs.c

 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 #include "string.h"

src/plugins/e-acsl/tests/memory/oracle_ci/gen_memalign.c

 /* Generated by Frama-C */
 #include "stdio.h"
 #include "stdlib.h"
+extern int __e_acsl_sound_verdict;
+
+/*@ requires valid_memptr: \valid(memptr);
+    requires
+      alignment_is_a_suitable_power_of_two:
+        alignment ≥ sizeof(void *) ∧
+        ((size_t)alignment & ((size_t)alignment - 1)) ≡ 0;
+    assigns __fc_heap_status, \result;
+    assigns __fc_heap_status
+      \from (indirect: alignment), size, __fc_heap_status;
+    assigns \result
+      \from (indirect: alignment), (indirect: size),
+            (indirect: __fc_heap_status);
+    allocates *\old(memptr);
+    
+    behavior allocation:
+      assumes can_allocate: is_allocable(size);
+      ensures allocation: \fresh{Old, Here}(*\old(memptr),\old(size));
+      ensures result_zero: \result ≡ 0;
+      assigns __fc_heap_status, \result;
+      assigns __fc_heap_status
+        \from (indirect: alignment), size, __fc_heap_status;
+      assigns \result
+        \from (indirect: alignment), (indirect: size),
+              (indirect: __fc_heap_status);
+    
+    behavior no_allocation:
+      assumes cannot_allocate: ¬is_allocable(size);
+      ensures result_non_zero: \result < 0 ∨ \result > 0;
+      assigns \result;
+      assigns \result \from (indirect: alignment);
+      allocates \nothing;
+    
+    complete behaviors no_allocation, allocation;
+    disjoint behaviors no_allocation, allocation;
+ */
+int __gen_e_acsl_posix_memalign(void **memptr, size_t alignment, size_t size);
+
+void *aligned_alloc(size_t alignment, size_t size);
+
 int main(int argc, char const **argv)
 {
   int __retres;
@@ -11,7 +51,8 @@ int main(int argc, char const **argv)
   __e_acsl_store_block((void *)(& memptr),(size_t)8);
   __e_acsl_full_init((void *)(& memptr));
   int res2 =
-    posix_memalign((void **)memptr,(unsigned long)256,(unsigned long)15);
+    __gen_e_acsl_posix_memalign((void **)memptr,(unsigned long)256,
+                                (unsigned long)15);
   /*@ assert Eva: initialization: \initialized(memptr); */
   char *p = *memptr;
   __e_acsl_store_block((void *)(& p),(size_t)8);
@@ -138,4 +179,82 @@ int main(int argc, char const **argv)
   return __retres;
 }
 
+/*@ requires valid_memptr: \valid(memptr);
+    requires
+      alignment_is_a_suitable_power_of_two:
+        alignment ≥ sizeof(void *) ∧
+        ((size_t)alignment & ((size_t)alignment - 1)) ≡ 0;
+    assigns __fc_heap_status, \result;
+    assigns __fc_heap_status
+      \from (indirect: alignment), size, __fc_heap_status;
+    assigns \result
+      \from (indirect: alignment), (indirect: size),
+            (indirect: __fc_heap_status);
+    allocates *\old(memptr);
+    
+    behavior allocation:
+      assumes can_allocate: is_allocable(size);
+      ensures allocation: \fresh{Old, Here}(*\old(memptr),\old(size));
+      ensures result_zero: \result ≡ 0;
+      assigns __fc_heap_status, \result;
+      assigns __fc_heap_status
+        \from (indirect: alignment), size, __fc_heap_status;
+      assigns \result
+        \from (indirect: alignment), (indirect: size),
+              (indirect: __fc_heap_status);
+    
+    behavior no_allocation:
+      assumes cannot_allocate: ¬is_allocable(size);
+      ensures result_non_zero: \result < 0 ∨ \result > 0;
+      assigns \result;
+      assigns \result \from (indirect: alignment);
+      allocates \nothing;
+    
+    complete behaviors no_allocation, allocation;
+    disjoint behaviors no_allocation, allocation;
+ */
+int __gen_e_acsl_posix_memalign(void **memptr, size_t alignment, size_t size)
+{
+  int __retres;
+  {
+    int __gen_e_acsl_valid;
+    int __gen_e_acsl_and;
+    __e_acsl_store_block((void *)(& memptr),(size_t)8);
+    __gen_e_acsl_valid = __e_acsl_valid((void *)memptr,sizeof(void *),
+                                        (void *)memptr,(void *)(& memptr));
+    __e_acsl_assert(__gen_e_acsl_valid,"Precondition","posix_memalign",
+                    "\\valid(memptr)","FRAMAC_SHARE/libc/stdlib.h",666);
+    if (alignment >= 8UL) {
+      __e_acsl_mpz_t __gen_e_acsl_;
+      __e_acsl_mpz_t __gen_e_acsl__2;
+      __e_acsl_mpz_t __gen_e_acsl_sub;
+      __e_acsl_mpz_t __gen_e_acsl_band;
+      unsigned long __gen_e_acsl__3;
+      __gmpz_init_set_ui(__gen_e_acsl_,alignment);
+      __gmpz_init_set_si(__gen_e_acsl__2,1L);
+      __gmpz_init(__gen_e_acsl_sub);
+      __gmpz_sub(__gen_e_acsl_sub,
+                 (__e_acsl_mpz_struct const *)(__gen_e_acsl_),
+                 (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+      __gmpz_init(__gen_e_acsl_band);
+      __gmpz_and(__gen_e_acsl_band,
+                 (__e_acsl_mpz_struct const *)(__gen_e_acsl_),
+                 (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub));
+      __gen_e_acsl__3 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_band));
+      __gen_e_acsl_and = __gen_e_acsl__3 == 0UL;
+      __gmpz_clear(__gen_e_acsl_);
+      __gmpz_clear(__gen_e_acsl__2);
+      __gmpz_clear(__gen_e_acsl_sub);
+      __gmpz_clear(__gen_e_acsl_band);
+    }
+    else __gen_e_acsl_and = 0;
+    __e_acsl_assert(__gen_e_acsl_and,"Precondition","posix_memalign",
+                    "alignment >= sizeof(void *) &&\n((size_t)alignment & ((size_t)alignment - 1)) == 0",
+                    "FRAMAC_SHARE/libc/stdlib.h",668);
+  }
+  __retres = posix_memalign(memptr,alignment,size);
+  __e_acsl_delete_block((void *)(& memptr));
+  return __retres;
+}
+
 

src/plugins/e-acsl/tests/memory/oracle_ci/gen_memsize.c

 /* Generated by Frama-C */
 #include "stdio.h"
 #include "stdlib.h"
+extern size_t __e_acsl_heap_allocation_size;
+
 int main(int argc, char **argv)
 {
   int __retres;

src/plugins/e-acsl/tests/memory/oracle_ci/gen_stdout.c

 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 void __e_acsl_globals_init(void)

src/plugins/e-acsl/tests/memory/oracle_ci/memalign.res.oracle

 [e-acsl] beginning translation.
+[e-acsl] Warning: annotating undefined function `posix_memalign':
+  the generated program may miss memory instrumentation
+  if there are memory-related annotations.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:665: Warning: 
+  E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+[e-acsl] tests/memory/memalign.c:38: Warning: 
+  E-ACSL construct `complete behaviors' is not yet supported.
+  Ignoring annotation.
+[e-acsl] tests/memory/memalign.c:38: Warning: 
+  E-ACSL construct `disjoint behaviors' is not yet supported.
+  Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:669: Warning: 
+  E-ACSL construct `assigns clause in behavior' is not yet supported.
+  Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:675: Warning: 
+  E-ACSL construct `predicate performing read accesses' is not yet supported.
+  Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:675: Warning: 
+  E-ACSL construct `assigns clause in behavior' is not yet supported.
+  Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:682: Warning: 
+  E-ACSL construct `predicate performing read accesses' is not yet supported.
+  Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
+[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:668: Warning: 
+  function __e_acsl_assert: precondition got status unknown.
+[eva] FRAMAC_SHARE/libc/stdlib.h:665: Warning: 
+  ignoring unsupported \allocates clause
+[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:679: Warning: 
+  function __gen_e_acsl_posix_memalign, behavior allocation: postcondition 'allocation' got status unknown.
 [eva:alarm] tests/memory/memalign.c:14: Warning: 
   accessing uninitialized left-value. assert \initialized(memptr);

src/plugins/e-acsl/tests/special/e-acsl-valid.c

 /* run.config_ci, run.config_dev
    COMMENT: test option -e-acsl-no-valid
-   STDOPT: #"@MACHDEP@ -eva -eva-verbose 0 -then -no-eva -e-acsl-no-valid"
+   STDOPT: #"@GLOBAL@ -eva -eva-verbose 0 -then -no-eva -e-acsl-no-valid"
    MACRO: ROOT_EACSL_GCC_FC_EXTRA_EXT -eva -eva-verbose 0
    MACRO: ROOT_EACSL_GCC_OPTS_EXT --then --e-acsl-extra -e-acsl-no-valid
 */

src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_args.c

 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 int main(int argc, char const **argv)

src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_local_init.c

 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 char *__gen_e_acsl_literal_string_4;

src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_memcpy.c

 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 #include "string.h"