[tests] Merge `literal_string` and `constmerge` test cases

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

-/* run.config
-   COMMENT: separate tracking of string constants
-*/
-
-const char *f = "the cat";
-const char *s = "the dog and the cat";
-
-#include <stdlib.h>
-
-char *strdup(const char*);
-
-int main(int argc, const char **argv) {
-  s++;
-  f++;
-  return 0;
-}

src/plugins/e-acsl/tests/runtime/literal_string.i

@@ -17,6 +17,9 @@ char *S2 = "foo2";
 int IDX = 1;
 int G2 = 2;
 
+const char *s_str = "the cat";
+const char *l_str = "the dog and the cat";
+
 int main(void) {
   char *SS = "ss";
   /*@ assert S[G2] == 'o'; */
@@ -24,6 +27,12 @@ int main(void) {
   /*@ assert \valid_read(S2); */
   /*@ assert ! \valid(SS); */
   f();
+
+  /* Make sure that compiler does not "merge strings", i.e., represents literal
+   * strings as separate memory blocks. An assertion enabled in the debug mode
+   * fails the execution if `s_str` is used as a part of `l_str`. */
+  s_str++;
+  l_str++;
   return 0;
 }
 

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

-[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
-[e-acsl] translation done in project "e-acsl".

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

-/* Generated by Frama-C */
-char *__gen_e_acsl_literal_string_2;
-char *__gen_e_acsl_literal_string;
-char const *f = "the cat";
-char const *s = "the dog and the cat";
-void __e_acsl_globals_init(void)
-{
-  __gen_e_acsl_literal_string_2 = "the dog and the cat";
-  __e_acsl_store_block((void *)__gen_e_acsl_literal_string_2,
-                       sizeof("the dog and the cat"));
-  __e_acsl_full_init((void *)__gen_e_acsl_literal_string_2);
-  __e_acsl_readonly((void *)__gen_e_acsl_literal_string_2);
-  __gen_e_acsl_literal_string = "the cat";
-  __e_acsl_store_block((void *)__gen_e_acsl_literal_string,sizeof("the cat"));
-  __e_acsl_full_init((void *)__gen_e_acsl_literal_string);
-  __e_acsl_readonly((void *)__gen_e_acsl_literal_string);
-  __e_acsl_store_block((void *)(& s),8UL);
-  __e_acsl_full_init((void *)(& s));
-  __e_acsl_store_block((void *)(& f),8UL);
-  __e_acsl_full_init((void *)(& f));
-  return;
-}
-
-int main(int argc, char const **argv)
-{
-  int __retres;
-  __e_acsl_memory_init(& argc,(char ***)(& argv),8UL);
-  __e_acsl_globals_init();
-  s ++;
-  f ++;
-  __retres = 0;
-  __e_acsl_delete_block((void *)(& s));
-  __e_acsl_delete_block((void *)(& f));
-  __e_acsl_memory_clean();
-  return __retres;
-}
-
-

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

 /* Generated by Frama-C */
+char *__gen_e_acsl_literal_string_6;
+char *__gen_e_acsl_literal_string_5;
 char *__gen_e_acsl_literal_string;
 char *__gen_e_acsl_literal_string_4;
 char *__gen_e_acsl_literal_string_3;
@@ -28,9 +30,21 @@ char *S = (char *)"foo";
 char *S2 = (char *)"foo2";
 int IDX = 1;
 int G2 = 2;
+char const *s_str = "the cat";
+char const *l_str = "the dog and the cat";
 char *U = (char *)"baz";
 void __e_acsl_globals_init(void)
 {
+  __gen_e_acsl_literal_string_6 = "the dog and the cat";
+  __e_acsl_store_block((void *)__gen_e_acsl_literal_string_6,
+                       sizeof("the dog and the cat"));
+  __e_acsl_full_init((void *)__gen_e_acsl_literal_string_6);
+  __e_acsl_readonly((void *)__gen_e_acsl_literal_string_6);
+  __gen_e_acsl_literal_string_5 = "the cat";
+  __e_acsl_store_block((void *)__gen_e_acsl_literal_string_5,
+                       sizeof("the cat"));
+  __e_acsl_full_init((void *)__gen_e_acsl_literal_string_5);
+  __e_acsl_readonly((void *)__gen_e_acsl_literal_string_5);
   __gen_e_acsl_literal_string = "ss";
   __e_acsl_store_block((void *)__gen_e_acsl_literal_string,sizeof("ss"));
   __e_acsl_full_init((void *)__gen_e_acsl_literal_string);
@@ -47,6 +61,10 @@ void __e_acsl_globals_init(void)
   __e_acsl_store_block((void *)__gen_e_acsl_literal_string_2,sizeof("bar"));
   __e_acsl_full_init((void *)__gen_e_acsl_literal_string_2);
   __e_acsl_readonly((void *)__gen_e_acsl_literal_string_2);
+  __e_acsl_store_block((void *)(& l_str),8UL);
+  __e_acsl_full_init((void *)(& l_str));
+  __e_acsl_store_block((void *)(& s_str),8UL);
+  __e_acsl_full_init((void *)(& s_str));
   __e_acsl_store_block((void *)(& S2),8UL);
   __e_acsl_full_init((void *)(& S2));
   __e_acsl_store_block((void *)(& S),8UL);
@@ -72,23 +90,23 @@ int main(void)
                                                   sizeof(char));
     __e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"main",
                     (char *)"mem_access: \\valid_read(S+(unsigned long)G2)",
-                    22);
+                    25);
     __e_acsl_assert(*(S + (unsigned long)G2) == 'o',(char *)"Assertion",
-                    (char *)"main",(char *)"*(S+G2) == \'o\'",22);
+                    (char *)"main",(char *)"*(S+G2) == \'o\'",25);
   }
   /*@ assert \initialized(S); */
   {
     int __gen_e_acsl_initialized;
     __gen_e_acsl_initialized = __e_acsl_initialized((void *)S,sizeof(char));
     __e_acsl_assert(__gen_e_acsl_initialized,(char *)"Assertion",
-                    (char *)"main",(char *)"\\initialized(S)",23);
+                    (char *)"main",(char *)"\\initialized(S)",26);
   }
   /*@ assert \valid_read(S2); */
   {
     int __gen_e_acsl_valid_read_2;
     __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)S2,sizeof(char));
     __e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"Assertion",
-                    (char *)"main",(char *)"\\valid_read(S2)",24);
+                    (char *)"main",(char *)"\\valid_read(S2)",27);
   }
   /*@ assert ¬\valid(SS); */
   {
@@ -103,10 +121,14 @@ int main(void)
     }
     else __gen_e_acsl_and = 0;
     __e_acsl_assert(! __gen_e_acsl_and,(char *)"Assertion",(char *)"main",
-                    (char *)"!\\valid(SS)",25);
+                    (char *)"!\\valid(SS)",28);
   }
   f();
+  s_str ++;
+  l_str ++;
   __retres = 0;
+  __e_acsl_delete_block((void *)(& l_str));
+  __e_acsl_delete_block((void *)(& s_str));
   __e_acsl_delete_block((void *)(& S2));
   __e_acsl_delete_block((void *)(& S));
   __e_acsl_delete_block((void *)(& T));