[tests] update wrt support of literal strings

mend

src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle

@@ -10,6 +10,8 @@
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
   __memory_size ∈ [--..--]
+  __e_acsl_literal_string ∈ {0}
+  __e_acsl_literal_string_2 ∈ {0}
 [value] using specification for function __store_block
 [value] using specification for function __full_init
 [value] using specification for function __literal_string

src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle

@@ -34,8 +34,5 @@
   S___fc_real_data_0_S___fc_stdout[0..1] ∈ [--..--]
   S___fc_inode_1_S___fc_stdout[0..1] ∈ [--..--]
   S___fc_real_data_1_S___fc_stdout[0..1] ∈ [--..--]
-[value] using specification for function __store_block
-[value] using specification for function __full_init
-[value] using specification for function __literal_string
 [value] using specification for function printf
 [value] done for function main

src/plugins/e-acsl/tests/bts/oracle/bts1837.1.res.oracle

@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]

src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle

+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
+  __fc_heap_status ∈ [--..--]
+  __e_acsl_init ∈ [--..--]
+  __e_acsl_internal_heap ∈ [--..--]
+  __memory_size ∈ [--..--]
+  S ∈ {0}
+  __e_acsl_literal_string ∈ {0}
+  __e_acsl_literal_string_2 ∈ {0}
+  __e_acsl_literal_string_3 ∈ {0}
+[value] using specification for function __store_block
+[value] using specification for function __full_init
+[value] using specification for function __literal_string
+tests/bts/bts1837.i:19:[value] entering loop for the first time
+tests/bts/bts1837.i:21:[value] Assertion got status valid.
+[value] using specification for function __initialized
+[value] using specification for function __valid_read
+[value] using specification for function e_acsl_assert
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+tests/bts/bts1837.i:22:[value] Assertion got status valid.
+[value] using specification for function __valid
+[value] using specification for function __delete_block
+tests/bts/bts1837.i:19:[kernel] warning: signed overflow. assert -2147483648 ≤ i-1;
+tests/bts/bts1837.i:11:[value] Assertion got status valid.
+tests/bts/bts1837.i:12:[value] Assertion got status valid.
+tests/bts/bts1837.i:13:[value] Assertion got status valid.
+[value] using specification for function __e_acsl_memory_clean
+[value] done for function main

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

@@ -21,8 +21,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@

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

 /* Generated by Frama-C */
+char *__e_acsl_literal_string_2;
+char *__e_acsl_literal_string;
 struct __anonstruct___mpz_struct_1 {
    int _mp_alloc ;
    int _mp_size ;
@@ -127,6 +129,14 @@ FILE *__e_acsl_fopen(char const *filename, char const *mode)
 
 void __e_acsl_memory_init(void)
 {
+  __e_acsl_literal_string_2 = "wb";
+  __store_block((void *)__e_acsl_literal_string_2,sizeof("wb"));
+  __full_init((void *)__e_acsl_literal_string_2);
+  __literal_string((void *)__e_acsl_literal_string_2);
+  __e_acsl_literal_string = "foo";
+  __store_block((void *)__e_acsl_literal_string,sizeof("foo"));
+  __full_init((void *)__e_acsl_literal_string);
+  __literal_string((void *)__e_acsl_literal_string);
   __store_block((void *)(& stdout),8UL);
   __full_init((void *)(& stdout));
   return;
@@ -134,8 +144,6 @@ void __e_acsl_memory_init(void)
 
 int main(void)
 {
-  char *__e_acsl_literal_string_2;
-  char *__e_acsl_literal_string;
   int __retres;
   FILE *f;
   FILE *f2;
@@ -144,14 +152,6 @@ int main(void)
   __store_block((void *)(& f),8UL);
   __full_init((void *)(& f));
   f = stdout;
-  __e_acsl_literal_string = "foo";
-  __store_block((void *)__e_acsl_literal_string,sizeof("foo"));
-  __full_init((void *)__e_acsl_literal_string);
-  __literal_string((void *)__e_acsl_literal_string);
-  __e_acsl_literal_string_2 = "wb";
-  __store_block((void *)__e_acsl_literal_string_2,sizeof("wb"));
-  __full_init((void *)__e_acsl_literal_string_2);
-  __literal_string((void *)__e_acsl_literal_string_2);
   __full_init((void *)(& f2));
   f2 = __e_acsl_fopen(__e_acsl_literal_string,__e_acsl_literal_string_2);
   /*@ assert f ≡ __fc_stdout; */

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

 /* Generated by Frama-C */
+char *__e_acsl_literal_string_2;
+char *__e_acsl_literal_string;
 struct __anonstruct___mpz_struct_1 {
    int _mp_alloc ;
    int _mp_size ;
@@ -134,6 +136,14 @@ FILE *__e_acsl_fopen(char const *filename, char const *mode)
 
 void __e_acsl_memory_init(void)
 {
+  __e_acsl_literal_string_2 = "wb";
+  __store_block((void *)__e_acsl_literal_string_2,sizeof("wb"));
+  __full_init((void *)__e_acsl_literal_string_2);
+  __literal_string((void *)__e_acsl_literal_string_2);
+  __e_acsl_literal_string = "foo";
+  __store_block((void *)__e_acsl_literal_string,sizeof("foo"));
+  __full_init((void *)__e_acsl_literal_string);
+  __literal_string((void *)__e_acsl_literal_string);
   __store_block((void *)(& stdout),8UL);
   __full_init((void *)(& stdout));
   return;
@@ -141,8 +151,6 @@ void __e_acsl_memory_init(void)
 
 int main(void)
 {
-  char *__e_acsl_literal_string_2;
-  char *__e_acsl_literal_string;
   int __retres;
   FILE *f;
   FILE *f2;
@@ -151,14 +159,6 @@ int main(void)
   __store_block((void *)(& f),8UL);
   __full_init((void *)(& f));
   f = stdout;
-  __e_acsl_literal_string = "foo";
-  __store_block((void *)__e_acsl_literal_string,sizeof("foo"));
-  __full_init((void *)__e_acsl_literal_string);
-  __literal_string((void *)__e_acsl_literal_string);
-  __e_acsl_literal_string_2 = "wb";
-  __store_block((void *)__e_acsl_literal_string_2,sizeof("wb"));
-  __full_init((void *)__e_acsl_literal_string_2);
-  __literal_string((void *)__e_acsl_literal_string_2);
   __full_init((void *)(& f2));
   f2 = __e_acsl_fopen(__e_acsl_literal_string,__e_acsl_literal_string_2);
   /*@ assert f ≡ __fc_stdout; */

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

@@ -20,6 +20,8 @@ FRAMAC_SHARE/libc/stdio.h:95:[e-acsl] warning: E-ACSL construct `logic function
   stdout ∈ {{ NULL ; &S___fc_stdout[0] }}
   __fc_fopen[0..511] ∈ {0}
   _p__fc_fopen ∈ {{ &__fc_fopen[0] }}
+  __e_acsl_literal_string ∈ {0}
+  __e_acsl_literal_string_2 ∈ {0}
   S___fc_stdout[0]{.__fc_stdio_id; .__fc_position; .__fc_error; .__fc_eof} ∈
                [--..--]
                [0].[bits 80 to 95] ∈ UNINITIALIZED

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

@@ -20,6 +20,8 @@ FRAMAC_SHARE/libc/stdio.h:95:[e-acsl] warning: E-ACSL construct `logic function
   stdout ∈ {{ NULL ; &S___fc_stdout[0] }}
   __fc_fopen[0..511] ∈ {0}
   _p__fc_fopen ∈ {{ &__fc_fopen[0] }}
+  __e_acsl_literal_string ∈ {0}
+  __e_acsl_literal_string_2 ∈ {0}
   S___fc_stdout[0]{.__fc_stdio_id; .__fc_position; .__fc_error; .__fc_eof} ∈
                [--..--]
                [0].[bits 80 to 95] ∈ UNINITIALIZED