From f160c5e6adb86678aa4fdb7c338af0eeded624bb Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Mon, 23 May 2016 18:17:57 +0200
Subject: [PATCH] [tests] add test case for BTS #2191 which is solved by the
new type system
---
src/plugins/e-acsl/doc/Changelog | 4 ++
src/plugins/e-acsl/tests/bts/bts2191.c | 20 +++++++
.../tests/bts/oracle/bts2191.err.oracle | 0
.../tests/bts/oracle/bts2191.res.oracle | 3 +
.../e-acsl/tests/bts/oracle/gen_bts2191.c | 55 +++++++++++++++++++
5 files changed, 82 insertions(+)
create mode 100644 src/plugins/e-acsl/tests/bts/bts2191.c
create mode 100644 src/plugins/e-acsl/tests/bts/oracle/bts2191.err.oracle
create mode 100644 src/plugins/e-acsl/tests/bts/oracle/bts2191.res.oracle
create mode 100644 src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 8412b2c5074..b7ee31318d8 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,6 +15,10 @@
# E-ACSL: the Whole E-ACSL plug-in
###############################################################################
+- E-ACSL [2016/05/23] Re-implementation of the type system which
+ improves the efficiency of the generated code over integers.
+-* E-ACSL [2016/05/23] Fix bug #2191 about complicate structs and
+ literate string.
-* E-ACSL [2016/05/23] Fix bug #1395 about recursive functions.
-* E-ACSL [2016/04/07] Fix 'make install' when executed within Frama-C.
-* E-ACSL [2016/03/31] Improve performance of Patricia Trie memory model.
diff --git a/src/plugins/e-acsl/tests/bts/bts2191.c b/src/plugins/e-acsl/tests/bts/bts2191.c
new file mode 100644
index 00000000000..0291959acba
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/bts2191.c
@@ -0,0 +1,20 @@
+struct ST {
+ char *str;
+ int num;
+};
+
+struct ST _G[] = {
+ {
+ .str = "Struct_G[0]",
+ .num = 99
+ },
+ {
+ .str = "Struct_G[1]",
+ .num = 147
+ }
+};
+
+int main(int argc, char **argv) {
+ /*@ assert \valid_read(_G[0].str); */
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2191.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2191.err.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2191.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2191.res.oracle
new file mode 100644
index 00000000000..2aefad1798b
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts2191.res.oracle
@@ -0,0 +1,3 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c
new file mode 100644
index 00000000000..c274fbfcf2b
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c
@@ -0,0 +1,55 @@
+/* Generated by Frama-C */
+char *__gen_e_acsl_literal_string;
+char *__gen_e_acsl_literal_string_2;
+struct ST {
+ char *str ;
+ int num ;
+};
+struct ST _G[2] =
+ {{.str = (char *)"Struct_G[0]", .num = 99},
+ {.str = (char *)"Struct_G[1]", .num = 147}};
+void __e_acsl_globals_init(void)
+{
+ __gen_e_acsl_literal_string = "Struct_G[1]";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string,
+ sizeof("Struct_G[1]"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string);
+ __e_acsl_readonly((void *)__gen_e_acsl_literal_string);
+ __gen_e_acsl_literal_string_2 = "Struct_G[0]";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_2,
+ sizeof("Struct_G[0]"));
+ __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 *)(_G),32UL);
+ __e_acsl_full_init((void *)(& _G));
+ return;
+}
+
+int main(int argc, char **argv)
+{
+ int __retres;
+ __e_acsl_memory_init(& argc,& argv,8UL);
+ __e_acsl_globals_init();
+ /*@ assert \valid_read(_G[0].str); */
+ {
+ int __gen_e_acsl_initialized;
+ int __gen_e_acsl_and;
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& _G[0].str),
+ sizeof(char *));
+ if (__gen_e_acsl_initialized) {
+ int __gen_e_acsl_valid_read;
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)_G[0].str,
+ sizeof(char));
+ __gen_e_acsl_and = __gen_e_acsl_valid_read;
+ }
+ else __gen_e_acsl_and = 0;
+ __e_acsl_assert(__gen_e_acsl_and,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid_read(_G[0].str)",18);
+ }
+ __retres = 0;
+ __e_acsl_delete_block((void *)(_G));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
--
GitLab