From b95f378cd7d3a42755a8f1d301c691d36dd0f849 Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Tue, 17 Jan 2017 13:03:48 +0100
Subject: [PATCH] Test case for bypassed variables
---
.../e-acsl/tests/runtime/bypassed_var.c | 32 +++++++++
.../runtime/oracle/bypassed_var.err.oracle | 0
.../runtime/oracle/bypassed_var.res.oracle | 6 ++
.../tests/runtime/oracle/gen_bypassed_var.c | 71 +++++++++++++++++++
4 files changed, 109 insertions(+)
create mode 100644 src/plugins/e-acsl/tests/runtime/bypassed_var.c
create mode 100644 src/plugins/e-acsl/tests/runtime/oracle/bypassed_var.err.oracle
create mode 100644 src/plugins/e-acsl/tests/runtime/oracle/bypassed_var.res.oracle
create mode 100644 src/plugins/e-acsl/tests/runtime/oracle/gen_bypassed_var.c
diff --git a/src/plugins/e-acsl/tests/runtime/bypassed_var.c b/src/plugins/e-acsl/tests/runtime/bypassed_var.c
new file mode 100644
index 00000000000..58b31bc3917
--- /dev/null
+++ b/src/plugins/e-acsl/tests/runtime/bypassed_var.c
@@ -0,0 +1,32 @@
+/* run.config
+ COMMENT: Variable, which declaration is bypassed by a goto jump
+*/
+
+int bypassed_var(int i) {
+ int lst [2];
+ if (i)
+ goto L;
+
+ {
+ int *p;
+ p = &lst;
+ /* assert \valid(p); */
+
+ L:
+ p++; /* Important to keep this statement here to make sure
+ initialize is ran after store_block */
+
+ if (!i) {
+ /*@ assert \valid(p); */
+ } else {
+ /*@ assert !\valid(p); */
+ }
+ }
+ return i;
+}
+
+int main(int argc, char const **argv) {
+ bypassed_var(0);
+ bypassed_var(1);
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/bypassed_var.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/bypassed_var.err.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/bypassed_var.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/bypassed_var.res.oracle
new file mode 100644
index 00000000000..76ae740a2df
--- /dev/null
+++ b/src/plugins/e-acsl/tests/runtime/oracle/bypassed_var.res.oracle
@@ -0,0 +1,6 @@
+[e-acsl] beginning translation.
+FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+[e-acsl] warning: Declaration of local variable p at tests/runtime/bypassed_var.c:11 is bypassed by agoto statement at tests/runtime/bypassed_var.c:8
+[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.
+tests/runtime/bypassed_var.c:16:[value] warning: accessing uninitialized left-value. assert \initialized(&p);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_bypassed_var.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_bypassed_var.c
new file mode 100644
index 00000000000..a1eb4fce0d0
--- /dev/null
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_bypassed_var.c
@@ -0,0 +1,71 @@
+/* Generated by Frama-C */
+int bypassed_var(int i)
+{
+ int lst[2];
+ __e_acsl_store_block((void *)(lst),8UL);
+ if (i) goto L;
+ {
+ int *p;
+ __e_acsl_store_block((void *)(& p),8UL);
+ __e_acsl_full_init((void *)(& p));
+ p = (int *)(& lst);
+ L: __e_acsl_store_block_duplicate((void *)(& p),8UL);
+ __e_acsl_full_init((void *)(& p));
+ /*@ assert Value: initialisation: \initialized(&p); */
+ p ++;
+ if (! i) {
+ /*@ assert \valid(p); */
+ {
+ {
+ int __gen_e_acsl_initialized;
+ int __gen_e_acsl_and;
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& p),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized) {
+ int __gen_e_acsl_valid;
+ __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int));
+ __gen_e_acsl_and = __gen_e_acsl_valid;
+ }
+ else __gen_e_acsl_and = 0;
+ __e_acsl_assert(__gen_e_acsl_and,(char *)"Assertion",
+ (char *)"bypassed_var",(char *)"\\valid(p)",20);
+ }
+ }
+ }
+ else {
+ /*@ assert ¬\valid(p); */
+ {
+ {
+ int __gen_e_acsl_initialized_2;
+ int __gen_e_acsl_and_2;
+ __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(& p),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized_2) {
+ int __gen_e_acsl_valid_2;
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)p,sizeof(int));
+ __gen_e_acsl_and_2 = __gen_e_acsl_valid_2;
+ }
+ else __gen_e_acsl_and_2 = 0;
+ __e_acsl_assert(! __gen_e_acsl_and_2,(char *)"Assertion",
+ (char *)"bypassed_var",(char *)"!\\valid(p)",22);
+ }
+ }
+ }
+ __e_acsl_delete_block((void *)(& p));
+ }
+ __e_acsl_delete_block((void *)(lst));
+ return i;
+}
+
+int main(int argc, char const **argv)
+{
+ int __retres;
+ __e_acsl_memory_init(& argc,(char ***)(& argv),8UL);
+ bypassed_var(0);
+ bypassed_var(1);
+ __retres = 0;
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
--
GitLab