Update several test oracles as per Frama-C code generation changes.

src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c

@@ -8,8 +8,8 @@ typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
 typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
 typedef unsigned int size_t;
 struct spongeStateStruct {
-   unsigned char __attribute__((__aligned__(32))) state[200] ;
-   unsigned char __attribute__((__aligned__(32))) dataQueue[192] ;
+   unsigned char __attribute__((__aligned__(32))) state[1600 / 8] ;
+   unsigned char __attribute__((__aligned__(32))) dataQueue[1536 / 8] ;
    unsigned int bitsInQueue ;
 } __attribute__((__aligned__(32)));
 typedef struct spongeStateStruct spongeState;

src/plugins/e-acsl/tests/bts/oracle/gen_bts13992.c

@@ -8,8 +8,8 @@ typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
 typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
 typedef unsigned int size_t;
 struct spongeStateStruct {
-   unsigned char __attribute__((__aligned__(32))) state[200] ;
-   unsigned char __attribute__((__aligned__(32))) dataQueue[192] ;
+   unsigned char __attribute__((__aligned__(32))) state[1600 / 8] ;
+   unsigned char __attribute__((__aligned__(32))) dataQueue[1536 / 8] ;
    unsigned int bitsInQueue ;
 } __attribute__((__aligned__(32)));
 typedef struct spongeStateStruct spongeState;

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

@@ -150,7 +150,7 @@ int main(void)
   struct list *l;
   __store_block((void *)(& l),4U);
   __full_init((void *)(& l));
-  l = (struct list *)((void *)0);
+  l = (struct list *)0;
   __full_init((void *)(& l));
   l = add(l,4);
   __full_init((void *)(& l));

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

@@ -150,7 +150,7 @@ int main(void)
   struct list *l;
   __store_block((void *)(& l),4U);
   __full_init((void *)(& l));
-  l = (struct list *)((void *)0);
+  l = (struct list *)0;
   __full_init((void *)(& l));
   l = add(l,4);
   __full_init((void *)(& l));

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.0.res.oracle

@@ -24,11 +24,10 @@ tests/e-acsl-runtime/linear_search.i:20:[value] entering loop for the first time
 tests/e-acsl-runtime/linear_search.i:19:[value] Loop invariant got status valid.
 tests/e-acsl-runtime/linear_search.i:20:[value] Loop invariant got status unknown.
 tests/e-acsl-runtime/linear_search.i:21:[value] entering loop for the first time
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status invalid.
-tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/linear_search.i:12:[value] Function __e_acsl_search, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/linear_search.i:15:[value] Function __e_acsl_search, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/linear_search.i:33:[value] Assertion got status unknown.

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

@@ -47,10 +47,10 @@ tests/e-acsl-runtime/linear_search.i:19:[value] Loop invariant got status valid.
 tests/e-acsl-runtime/linear_search.i:20:[value] Loop invariant got status unknown.
 tests/e-acsl-runtime/linear_search.i:21:[value] entering loop for the first time
 tests/e-acsl-runtime/linear_search.i:20:[kernel] warning: accessing out of bounds index [0..4294967295]. assert __e_acsl_i_4 < 10;
-tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/linear_search.i:12:[value] Function __e_acsl_search, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/linear_search.i:15:[value] Function __e_acsl_search, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/linear_search.i:33:[value] Assertion got status unknown.

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

@@ -18,8 +18,8 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition g
 [value] using specification for function __gmpz_clear
 FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: 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 invalid.
 FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status invalid.
 tests/e-acsl-runtime/loop.i:10:[value] Loop invariant got status valid.
 tests/e-acsl-runtime/loop.i:17:[value] Loop invariant got status valid.
 [value] using specification for function __gmpz_init