[tests] Test for separate handling of string constants

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/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;
+}
+
+