From d14f6e081b83957b72ac4b214371917fd65075ba Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Wed, 31 Aug 2016 10:58:47 +0200
Subject: [PATCH] [tests] Test for separate handling of string constants
---
src/plugins/e-acsl/tests/runtime/constmerge.c | 16 ++++++++
.../runtime/oracle/constmerge.err.oracle | 0
.../runtime/oracle/constmerge.res.oracle | 3 ++
.../tests/runtime/oracle/gen_constmerge.c | 38 +++++++++++++++++++
4 files changed, 57 insertions(+)
create mode 100644 src/plugins/e-acsl/tests/runtime/constmerge.c
create mode 100644 src/plugins/e-acsl/tests/runtime/oracle/constmerge.err.oracle
create mode 100644 src/plugins/e-acsl/tests/runtime/oracle/constmerge.res.oracle
create mode 100644 src/plugins/e-acsl/tests/runtime/oracle/gen_constmerge.c
diff --git a/src/plugins/e-acsl/tests/runtime/constmerge.c b/src/plugins/e-acsl/tests/runtime/constmerge.c
new file mode 100644
index 00000000000..c38e39aa567
--- /dev/null
+++ b/src/plugins/e-acsl/tests/runtime/constmerge.c
@@ -0,0 +1,16 @@
+/* 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;
+}
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/constmerge.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/constmerge.err.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/constmerge.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/constmerge.res.oracle
new file mode 100644
index 00000000000..b9986aac775
--- /dev/null
+++ b/src/plugins/e-acsl/tests/runtime/oracle/constmerge.res.oracle
@@ -0,0 +1,3 @@
+[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".
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_constmerge.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_constmerge.c
new file mode 100644
index 00000000000..6d8a7d8d387
--- /dev/null
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_constmerge.c
@@ -0,0 +1,38 @@
+/* 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;
+}
+
+
--
GitLab