[tests] fix oracles

src/plugins/e-acsl/tests/e-acsl-runtime/bts1478.c

@@ -4,8 +4,9 @@
    EXECNOW: LOG gen_bts14782.c BIN gen_bts14782.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1478.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts14782.c > /dev/null && ./gcc_test.sh bts14782
 */
 
-int global_i = 0;
+int global_i;
 int* global_i_ptr = &global_i;
+int global_i = 0;
 
 /*@ requires global_i == 0;
     requires \valid(global_i_ptr);

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.res.oracle

@@ -22,9 +22,9 @@
   global_i_ptr ∈ {{ &global_i }}
 [value] using specification for function __store_block
 [value] using specification for function __full_init
-tests/e-acsl-runtime/bts1478.c:10:[value] Function __e_acsl_loop: precondition got status valid.
 tests/e-acsl-runtime/bts1478.c:11:[value] Function __e_acsl_loop: precondition got status valid.
 tests/e-acsl-runtime/bts1478.c:12:[value] Function __e_acsl_loop: precondition got status valid.
+tests/e-acsl-runtime/bts1478.c:13:[value] Function __e_acsl_loop: precondition got status valid.
 [value] using specification for function __gmpz_init_set_si
 FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
 [value] using specification for function __gmpz_cmp
@@ -36,9 +36,9 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
 FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
 [value] using specification for function __gmpz_clear
 FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
-tests/e-acsl-runtime/bts1478.c:10:[value] Function loop: precondition got status valid.
 tests/e-acsl-runtime/bts1478.c:11:[value] Function loop: precondition got status valid.
 tests/e-acsl-runtime/bts1478.c:12:[value] Function loop: precondition got status valid.
+tests/e-acsl-runtime/bts1478.c:13:[value] Function loop: precondition got status valid.
 [value] using specification for function __delete_block
 [value] using specification for function __e_acsl_memory_clean
 [value] done for function main

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.res.oracle

@@ -22,16 +22,16 @@
   global_i_ptr ∈ {{ &global_i }}
 [value] using specification for function __store_block
 [value] using specification for function __full_init
-tests/e-acsl-runtime/bts1478.c:10:[value] Function __e_acsl_loop: precondition got status valid.
 tests/e-acsl-runtime/bts1478.c:11:[value] Function __e_acsl_loop: precondition got status valid.
 tests/e-acsl-runtime/bts1478.c:12:[value] Function __e_acsl_loop: precondition got status valid.
+tests/e-acsl-runtime/bts1478.c:13:[value] Function __e_acsl_loop: precondition got status valid.
 [value] using specification for function e_acsl_assert
 FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
 [value] using specification for function __valid
 FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-tests/e-acsl-runtime/bts1478.c:10:[value] Function loop: precondition got status valid.
 tests/e-acsl-runtime/bts1478.c:11:[value] Function loop: precondition got status valid.
 tests/e-acsl-runtime/bts1478.c:12:[value] Function loop: precondition got status valid.
+tests/e-acsl-runtime/bts1478.c:13:[value] Function loop: precondition got status valid.
 [value] using specification for function __delete_block
 [value] using specification for function __e_acsl_memory_clean
 [value] done for function main

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c

@@ -62,8 +62,10 @@ extern size_t __memory_size;
 predicate diffSize{L1, L2}(ℤ i) =
   \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
  */
-int global_i = 0;
+int global_i;
+
 int *global_i_ptr = & global_i;
+int global_i = 0;
 /*@ requires global_i ≡ 0;
     requires \valid(global_i_ptr);
     requires global_i_ptr ≡ &global_i;
@@ -82,12 +84,12 @@ void __e_acsl_loop(void)
   {
     int __e_acsl_valid;
     e_acsl_assert(global_i == 0,(char *)"Precondition",(char *)"loop",
-                  (char *)"global_i == 0",10);
+                  (char *)"global_i == 0",11);
     __e_acsl_valid = __valid((void *)global_i_ptr,sizeof(int));
     e_acsl_assert(__e_acsl_valid,(char *)"Precondition",(char *)"loop",
-                  (char *)"\\valid(global_i_ptr)",11);
+                  (char *)"\\valid(global_i_ptr)",12);
     e_acsl_assert(global_i_ptr == & global_i,(char *)"Precondition",
-                  (char *)"loop",(char *)"global_i_ptr == &global_i",12);
+                  (char *)"loop",(char *)"global_i_ptr == &global_i",13);
     loop();
   }
   return;

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c

@@ -85,8 +85,10 @@ extern size_t __memory_size;
 predicate diffSize{L1, L2}(ℤ i) =
   \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
  */
-int global_i = 0;
+int global_i;
+
 int *global_i_ptr = & global_i;
+int global_i = 0;
 /*@ requires global_i ≡ 0;
     requires \valid(global_i_ptr);
     requires global_i_ptr ≡ &global_i;
@@ -112,12 +114,12 @@ void __e_acsl_loop(void)
     __e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__e_acsl_global_i),
                              (__mpz_struct const *)(__e_acsl));
     e_acsl_assert(__e_acsl_eq == 0,(char *)"Precondition",(char *)"loop",
-                  (char *)"global_i == 0",10);
+                  (char *)"global_i == 0",11);
     __e_acsl_valid = __valid((void *)global_i_ptr,sizeof(int));
     e_acsl_assert(__e_acsl_valid,(char *)"Precondition",(char *)"loop",
-                  (char *)"\\valid(global_i_ptr)",11);
+                  (char *)"\\valid(global_i_ptr)",12);
     e_acsl_assert(global_i_ptr == & global_i,(char *)"Precondition",
-                  (char *)"loop",(char *)"global_i_ptr == &global_i",12);
+                  (char *)"loop",(char *)"global_i_ptr == &global_i",13);
     __gmpz_clear(__e_acsl_global_i);
     __gmpz_clear(__e_acsl);
     loop();