From 6571bbb471e074cb4014a67a67626e4c7a8afa22 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Mon, 16 Mar 2020 11:27:40 +0100
Subject: [PATCH] [eacsl:codegen] Add tests for variables in switch tracking
---
.../e-acsl/known_bugs/decl_in_switch.c | 17 -
.../bts}/bts1386_complex_flowgraph.c | 0
src/plugins/e-acsl/tests/bts/issue-eacsl-91.c | 26 ++
.../bts1386_complex_flowgraph.res.oracle | 2 +
.../oracle_ci/gen_bts1386_complex_flowgraph.c | 289 +++++++++++++++
.../tests/bts/oracle_ci/gen_issue-eacsl-91.c | 86 +++++
.../bts/oracle_ci/issue-eacsl-91.res.oracle | 2 +
.../bts1386_complex_flowgraph.res.oracle | 1 +
.../bts/oracle_dev/issue-eacsl-91.res.oracle | 1 +
.../e-acsl/tests/memory/decl_in_switch.c | 118 +++++++
.../oracle_ci/decl_in_switch.err.oracle | 0
.../oracle_ci/decl_in_switch.res.oracle | 1 -
.../memory/oracle_ci/gen_decl_in_switch.c | 330 +++++++++++-------
.../oracle_dev/decl_in_switch.res.oracle | 1 +
14 files changed, 733 insertions(+), 141 deletions(-)
delete mode 100644 src/plugins/e-acsl/known_bugs/decl_in_switch.c
rename src/plugins/e-acsl/{known_bugs => tests/bts}/bts1386_complex_flowgraph.c (100%)
create mode 100644 src/plugins/e-acsl/tests/bts/issue-eacsl-91.c
create mode 100644 src/plugins/e-acsl/tests/bts/oracle_ci/bts1386_complex_flowgraph.res.oracle
create mode 100644 src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1386_complex_flowgraph.c
create mode 100644 src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-91.c
create mode 100644 src/plugins/e-acsl/tests/bts/oracle_ci/issue-eacsl-91.res.oracle
create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/bts1386_complex_flowgraph.res.oracle
create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-91.res.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/decl_in_switch.c
delete mode 100644 src/plugins/e-acsl/tests/memory/oracle_ci/decl_in_switch.err.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/decl_in_switch.res.oracle
diff --git a/src/plugins/e-acsl/known_bugs/decl_in_switch.c b/src/plugins/e-acsl/known_bugs/decl_in_switch.c
deleted file mode 100644
index 16ddbbf61bb..00000000000
--- a/src/plugins/e-acsl/known_bugs/decl_in_switch.c
+++ /dev/null
@@ -1,17 +0,0 @@
-/* run.config_ci
- DONTRUN:
- COMMENT: Variables declared in the body of switch statements so far cannot
- COMMENT: be tracked
-*/
-
-int main(int argc, char **argv) {
- switch(argc) {
- int *p;
- default: {
- p = &argc;
- /*! assert \valid(p); */
- break;
- }
- }
- return 0;
-}
diff --git a/src/plugins/e-acsl/known_bugs/bts1386_complex_flowgraph.c b/src/plugins/e-acsl/tests/bts/bts1386_complex_flowgraph.c
similarity index 100%
rename from src/plugins/e-acsl/known_bugs/bts1386_complex_flowgraph.c
rename to src/plugins/e-acsl/tests/bts/bts1386_complex_flowgraph.c
diff --git a/src/plugins/e-acsl/tests/bts/issue-eacsl-91.c b/src/plugins/e-acsl/tests/bts/issue-eacsl-91.c
new file mode 100644
index 00000000000..cc7640adddb
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/issue-eacsl-91.c
@@ -0,0 +1,26 @@
+/* run.config_ci
+ COMMENT: frama-c/e-acsl#91, test for misplaced delete_block of local variable
+ in switch.
+ STDOPT: #"-e-acsl-full-mmodel"
+*/
+short a;
+char b()
+{
+ switch (a)
+ {
+ int c = 0;
+ case 0:
+ goto d;
+ /* Empty if statement so that frama-c simplifies this in `int tmp = c;` */
+ if (c)
+ ;
+ }
+d:
+ return 2;
+}
+
+int main()
+{
+ b();
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/bts1386_complex_flowgraph.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1386_complex_flowgraph.res.oracle
new file mode 100644
index 00000000000..efd02631129
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1386_complex_flowgraph.res.oracle
@@ -0,0 +1,2 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1386_complex_flowgraph.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1386_complex_flowgraph.c
new file mode 100644
index 00000000000..545ac34e904
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1386_complex_flowgraph.c
@@ -0,0 +1,289 @@
+/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
+void duffcopy(char *to, char *from, int count)
+{
+ __e_acsl_store_block((void *)(& from),(size_t)8);
+ __e_acsl_store_block((void *)(& to),(size_t)8);
+ int n = (count + 7) / 8;
+ switch (count % 8)
+ case 0:
+ while (1) {
+ {
+ char *tmp;
+ char *tmp_0;
+ char *tmp_1;
+ char *tmp_2;
+ char *tmp_3;
+ char *tmp_4;
+ char *tmp_5;
+ char *tmp_6;
+ char *tmp_7;
+ char *tmp_8;
+ char *tmp_9;
+ char *tmp_10;
+ char *tmp_11;
+ char *tmp_12;
+ char *tmp_13;
+ char *tmp_14;
+ __e_acsl_store_block((void *)(& tmp_14),(size_t)8);
+ __e_acsl_store_block((void *)(& tmp_13),(size_t)8);
+ __e_acsl_store_block((void *)(& tmp_12),(size_t)8);
+ __e_acsl_store_block((void *)(& tmp_11),(size_t)8);
+ __e_acsl_store_block((void *)(& tmp_10),(size_t)8);
+ __e_acsl_store_block((void *)(& tmp_9),(size_t)8);
+ __e_acsl_store_block((void *)(& tmp_8),(size_t)8);
+ __e_acsl_store_block((void *)(& tmp_7),(size_t)8);
+ __e_acsl_store_block((void *)(& tmp_6),(size_t)8);
+ __e_acsl_store_block((void *)(& tmp_5),(size_t)8);
+ __e_acsl_store_block((void *)(& tmp_4),(size_t)8);
+ __e_acsl_store_block((void *)(& tmp_3),(size_t)8);
+ __e_acsl_store_block((void *)(& tmp_2),(size_t)8);
+ __e_acsl_store_block((void *)(& tmp_1),(size_t)8);
+ __e_acsl_store_block((void *)(& tmp_0),(size_t)8);
+ __e_acsl_store_block((void *)(& tmp),(size_t)8);
+ __e_acsl_full_init((void *)(& tmp));
+ tmp = to;
+ to ++;
+ __e_acsl_full_init((void *)(& tmp_0));
+ tmp_0 = from;
+ from ++;
+ __e_acsl_initialize((void *)tmp,sizeof(char));
+ *tmp = *tmp_0;
+ case 7: __e_acsl_store_block_duplicate((void *)(& tmp),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_0),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_1),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_2),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_3),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_4),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_5),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_6),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_7),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_8),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_9),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_10),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_11),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_12),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_13),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_14),(size_t)8);
+ __e_acsl_full_init((void *)(& tmp_1));
+ tmp_1 = to;
+ to ++;
+ __e_acsl_full_init((void *)(& tmp_2));
+ tmp_2 = from;
+ from ++;
+ __e_acsl_initialize((void *)tmp_1,sizeof(char));
+ *tmp_1 = *tmp_2;
+ case 6: __e_acsl_store_block_duplicate((void *)(& tmp),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_0),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_1),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_2),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_3),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_4),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_5),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_6),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_7),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_8),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_9),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_10),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_11),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_12),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_13),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_14),(size_t)8);
+ __e_acsl_full_init((void *)(& tmp_3));
+ tmp_3 = to;
+ to ++;
+ __e_acsl_full_init((void *)(& tmp_4));
+ tmp_4 = from;
+ from ++;
+ __e_acsl_initialize((void *)tmp_3,sizeof(char));
+ *tmp_3 = *tmp_4;
+ case 5: __e_acsl_store_block_duplicate((void *)(& tmp),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_0),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_1),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_2),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_3),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_4),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_5),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_6),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_7),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_8),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_9),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_10),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_11),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_12),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_13),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_14),(size_t)8);
+ __e_acsl_full_init((void *)(& tmp_5));
+ tmp_5 = to;
+ to ++;
+ __e_acsl_full_init((void *)(& tmp_6));
+ tmp_6 = from;
+ from ++;
+ __e_acsl_initialize((void *)tmp_5,sizeof(char));
+ *tmp_5 = *tmp_6;
+ case 4: __e_acsl_store_block_duplicate((void *)(& tmp),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_0),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_1),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_2),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_3),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_4),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_5),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_6),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_7),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_8),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_9),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_10),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_11),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_12),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_13),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_14),(size_t)8);
+ __e_acsl_full_init((void *)(& tmp_7));
+ tmp_7 = to;
+ to ++;
+ __e_acsl_full_init((void *)(& tmp_8));
+ tmp_8 = from;
+ from ++;
+ __e_acsl_initialize((void *)tmp_7,sizeof(char));
+ *tmp_7 = *tmp_8;
+ case 3: __e_acsl_store_block_duplicate((void *)(& tmp),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_0),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_1),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_2),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_3),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_4),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_5),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_6),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_7),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_8),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_9),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_10),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_11),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_12),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_13),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_14),(size_t)8);
+ __e_acsl_full_init((void *)(& tmp_9));
+ tmp_9 = to;
+ to ++;
+ __e_acsl_full_init((void *)(& tmp_10));
+ tmp_10 = from;
+ from ++;
+ __e_acsl_initialize((void *)tmp_9,sizeof(char));
+ *tmp_9 = *tmp_10;
+ case 2: __e_acsl_store_block_duplicate((void *)(& tmp),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_0),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_1),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_2),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_3),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_4),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_5),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_6),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_7),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_8),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_9),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_10),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_11),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_12),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_13),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_14),(size_t)8);
+ __e_acsl_full_init((void *)(& tmp_11));
+ tmp_11 = to;
+ to ++;
+ __e_acsl_full_init((void *)(& tmp_12));
+ tmp_12 = from;
+ from ++;
+ __e_acsl_initialize((void *)tmp_11,sizeof(char));
+ *tmp_11 = *tmp_12;
+ case 1: __e_acsl_store_block_duplicate((void *)(& tmp),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_0),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_1),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_2),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_3),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_4),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_5),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_6),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_7),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_8),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_9),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_10),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_11),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_12),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_13),(size_t)8);
+ __e_acsl_store_block_duplicate((void *)(& tmp_14),(size_t)8);
+ __e_acsl_full_init((void *)(& tmp_13));
+ tmp_13 = to;
+ to ++;
+ __e_acsl_full_init((void *)(& tmp_14));
+ tmp_14 = from;
+ from ++;
+ __e_acsl_initialize((void *)tmp_13,sizeof(char));
+ *tmp_13 = *tmp_14;
+ __e_acsl_delete_block((void *)(& tmp_14));
+ __e_acsl_delete_block((void *)(& tmp_13));
+ __e_acsl_delete_block((void *)(& tmp_12));
+ __e_acsl_delete_block((void *)(& tmp_11));
+ __e_acsl_delete_block((void *)(& tmp_10));
+ __e_acsl_delete_block((void *)(& tmp_9));
+ __e_acsl_delete_block((void *)(& tmp_8));
+ __e_acsl_delete_block((void *)(& tmp_7));
+ __e_acsl_delete_block((void *)(& tmp_6));
+ __e_acsl_delete_block((void *)(& tmp_5));
+ __e_acsl_delete_block((void *)(& tmp_4));
+ __e_acsl_delete_block((void *)(& tmp_3));
+ __e_acsl_delete_block((void *)(& tmp_2));
+ __e_acsl_delete_block((void *)(& tmp_1));
+ __e_acsl_delete_block((void *)(& tmp_0));
+ __e_acsl_delete_block((void *)(& tmp));
+ }
+ n --;
+ if (! (n > 0)) break;
+ }
+ __e_acsl_delete_block((void *)(& from));
+ __e_acsl_delete_block((void *)(& to));
+ return;
+}
+
+void initialize(char *arr, int length)
+{
+ int i;
+ __e_acsl_store_block((void *)(& arr),(size_t)8);
+ i = 0;
+ while (i < length) {
+ __e_acsl_initialize((void *)(arr + i),sizeof(char));
+ *(arr + i) = (char)(length - i);
+ i ++;
+ }
+ __e_acsl_delete_block((void *)(& arr));
+ return;
+}
+
+char source[100];
+char target[100];
+void __e_acsl_globals_init(void)
+{
+ static char __e_acsl_already_run = 0;
+ if (! __e_acsl_already_run) {
+ __e_acsl_already_run = 1;
+ __e_acsl_store_block((void *)(target),(size_t)100);
+ __e_acsl_full_init((void *)(& target));
+ __e_acsl_store_block((void *)(source),(size_t)100);
+ __e_acsl_full_init((void *)(& source));
+ }
+ return;
+}
+
+int main(void)
+{
+ int __retres;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_globals_init();
+ initialize(source,100);
+ duffcopy(source,target,43);
+ __retres = 0;
+ __e_acsl_delete_block((void *)(target));
+ __e_acsl_delete_block((void *)(source));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-91.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-91.c
new file mode 100644
index 00000000000..0a5c6762700
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-91.c
@@ -0,0 +1,86 @@
+/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
+short a;
+char b(void)
+{
+ char __retres;
+ __e_acsl_store_block((void *)(& __retres),(size_t)1);
+ switch ((int)a) {
+ int c = 0;
+ __e_acsl_store_block((void *)(& c),(size_t)4);
+ __e_acsl_full_init((void *)(& c));
+ case 0: __e_acsl_store_block_duplicate((void *)(& c),(size_t)4);
+ __e_acsl_delete_block((void *)(& c));
+ goto d;
+ int tmp = c;
+ __e_acsl_store_block((void *)(& tmp),(size_t)4);
+ __e_acsl_full_init((void *)(& tmp));
+ __e_acsl_delete_block((void *)(& tmp));
+ __e_acsl_delete_block((void *)(& c));
+ }
+ d: {
+ __e_acsl_full_init((void *)(& __retres));
+ __retres = (char)2;
+ }
+ __e_acsl_delete_block((void *)(& __retres));
+ return __retres;
+}
+
+void __e_acsl_globals_init(void)
+{
+ static char __e_acsl_already_run = 0;
+ if (! __e_acsl_already_run) {
+ __e_acsl_already_run = 1;
+ __e_acsl_store_block((void *)(& b),(size_t)1);
+ __e_acsl_full_init((void *)(& b));
+ __e_acsl_store_block((void *)(& a),(size_t)2);
+ __e_acsl_full_init((void *)(& a));
+ __e_acsl_store_block((void *)(& __fc_p_tmpnam),(size_t)8);
+ __e_acsl_full_init((void *)(& __fc_p_tmpnam));
+ __e_acsl_store_block((void *)(__fc_tmpnam),(size_t)2048);
+ __e_acsl_full_init((void *)(& __fc_tmpnam));
+ __e_acsl_store_block((void *)(& __fc_p_fopen),(size_t)8);
+ __e_acsl_full_init((void *)(& __fc_p_fopen));
+ __e_acsl_store_block((void *)(__fc_fopen),(size_t)128);
+ __e_acsl_full_init((void *)(& __fc_fopen));
+ __e_acsl_store_block((void *)(& stdin),(size_t)8);
+ __e_acsl_full_init((void *)(& stdin));
+ __e_acsl_store_block((void *)(& __fc_p_random48_counter),(size_t)8);
+ __e_acsl_full_init((void *)(& __fc_p_random48_counter));
+ __e_acsl_store_block((void *)(random48_counter),(size_t)6);
+ __e_acsl_full_init((void *)(& random48_counter));
+ __e_acsl_store_block((void *)(& __fc_random48_init),(size_t)4);
+ __e_acsl_full_init((void *)(& __fc_random48_init));
+ __e_acsl_store_block((void *)(& __fc_rand_max),(size_t)8);
+ __e_acsl_full_init((void *)(& __fc_rand_max));
+ }
+ return;
+}
+
+int main(void)
+{
+ int __retres;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_globals_init();
+ __e_acsl_store_block((void *)(& __retres),(size_t)4);
+ b();
+ __e_acsl_full_init((void *)(& __retres));
+ __retres = 0;
+ __e_acsl_delete_block((void *)(& b));
+ __e_acsl_delete_block((void *)(& a));
+ __e_acsl_delete_block((void *)(& __fc_p_tmpnam));
+ __e_acsl_delete_block((void *)(__fc_tmpnam));
+ __e_acsl_delete_block((void *)(& __fc_p_fopen));
+ __e_acsl_delete_block((void *)(__fc_fopen));
+ __e_acsl_delete_block((void *)(& stdin));
+ __e_acsl_delete_block((void *)(& __fc_p_random48_counter));
+ __e_acsl_delete_block((void *)(random48_counter));
+ __e_acsl_delete_block((void *)(& __fc_random48_init));
+ __e_acsl_delete_block((void *)(& __fc_rand_max));
+ __e_acsl_delete_block((void *)(& __retres));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/issue-eacsl-91.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/issue-eacsl-91.res.oracle
new file mode 100644
index 00000000000..efd02631129
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/issue-eacsl-91.res.oracle
@@ -0,0 +1,2 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1386_complex_flowgraph.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1386_complex_flowgraph.res.oracle
new file mode 100644
index 00000000000..93a1829d941
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1386_complex_flowgraph.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/bts/bts1386_complex_flowgraph.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-91.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-91.res.oracle
new file mode 100644
index 00000000000..2bd68e9f6dc
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-91.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/bts/issue-eacsl-91.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/decl_in_switch.c b/src/plugins/e-acsl/tests/memory/decl_in_switch.c
new file mode 100644
index 00000000000..bd12fc2105e
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/decl_in_switch.c
@@ -0,0 +1,118 @@
+/* run.config_ci
+ COMMENT: Check that variables declared in the body of switch statements are
+ correctly tracked.
+*/
+
+/// Simple declaration in switch
+void decl_in_switch(int value)
+{
+ switch (value)
+ {
+ int *p;
+ default:
+ {
+ p = &value;
+ /*! assert \valid(p); */
+ break;
+ }
+ }
+}
+
+/// Declaration and initialization in a single statement
+/// (local initializer)
+void compound_decl_and_init(int value)
+{
+ int a = 0;
+ /*@ assert \valid(&a); */
+
+ switch (value)
+ {
+ int b = 2;
+ /*@ assert \valid(&b); */
+
+ case 0:;
+ int c = 3;
+ /*@ assert \valid(&c); */
+ break;
+
+ case 1:;
+ int d = 4;
+ /*@ assert \valid(&d); */
+ break;
+ }
+}
+
+/// Separate statements for declaration and initialization
+/// (no local initializer)
+void separate_decl_and_init(int value)
+{
+ int a;
+ a = 1;
+ /*@ assert \valid(&a); */
+
+ switch (value)
+ {
+ int b;
+ b = 2;
+ /*@ assert \valid(&b); */
+
+ case 0:;
+ int c;
+ c = 3;
+ /*@ assert \valid(&c); */
+ break;
+
+ case 1:;
+ int d;
+ d = 4;
+ /*@ assert \valid(&d); */
+ break;
+ }
+}
+
+/// Check label in switch
+void label_in_switch(int value)
+{
+ int done = 0;
+
+ switch (value)
+ {
+ /* standalone label */
+ K:;
+ int d = 0;
+ /*@ assert \valid(&d); */
+
+ /* Label and case on the same statement */
+ L:
+ case 0:;
+ int e = 1;
+ /*@ assert \valid(&e); */
+ break;
+ case 1:;
+ int ff = 2;
+ /*@ assert \valid(&ff); */
+ break;
+ }
+
+ if (!done)
+ {
+ done = 1;
+ if (value < 10)
+ {
+ goto L;
+ }
+ else
+ {
+ goto K;
+ }
+ }
+}
+
+int main(int argc, char **argv)
+{
+ decl_in_switch(argc);
+ compound_decl_and_init(argc);
+ separate_decl_and_init(argc);
+ label_in_switch(argc);
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/decl_in_switch.err.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/decl_in_switch.err.oracle
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/decl_in_switch.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/decl_in_switch.res.oracle
index c33737e3cac..efd02631129 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/decl_in_switch.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/decl_in_switch.res.oracle
@@ -1,3 +1,2 @@
[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] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_decl_in_switch.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_decl_in_switch.c
index 44c5d1497e4..4c5ab738c91 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_decl_in_switch.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_decl_in_switch.c
@@ -1,145 +1,229 @@
/* Generated by Frama-C */
-typedef unsigned long size_t;
-struct __e_acsl_mpz_struct {
- int _mp_alloc ;
- int _mp_size ;
- unsigned long *_mp_d ;
-};
-typedef struct __e_acsl_mpz_struct __e_acsl_mpz_struct;
-typedef __e_acsl_mpz_struct ( __attribute__((__FC_BUILTIN__)) __e_acsl_mpz_t)[1];
-struct __e_acsl_mpq_struct {
- __e_acsl_mpz_struct _mp_num ;
- __e_acsl_mpz_struct _mp_den ;
-};
-typedef struct __e_acsl_mpq_struct __e_acsl_mpq_struct;
-typedef __e_acsl_mpq_struct ( __attribute__((__FC_BUILTIN__)) __e_acsl_mpq_t)[1];
-typedef struct _IO_FILE FILE;
-/*@ ghost extern int __e_acsl_init; */
-
-extern size_t __e_acsl_heap_allocation_size;
-
-typedef unsigned short __uint16_t;
-typedef unsigned int __uint32_t;
-typedef unsigned long __uint64_t;
-typedef long __off_t;
-typedef long __off64_t;
-struct _IO_FILE;
-typedef void _IO_lock_t;
-struct _IO_marker {
- struct _IO_marker *_next ;
- struct _IO_FILE *_sbuf ;
- int _pos ;
-};
-struct _IO_FILE {
- int _flags ;
- char *_IO_read_ptr ;
- char *_IO_read_end ;
- char *_IO_read_base ;
- char *_IO_write_base ;
- char *_IO_write_ptr ;
- char *_IO_write_end ;
- char *_IO_buf_base ;
- char *_IO_buf_end ;
- char *_IO_save_base ;
- char *_IO_backup_base ;
- char *_IO_save_end ;
- struct _IO_marker *_markers ;
- struct _IO_FILE *_chain ;
- int _fileno ;
- int _flags2 ;
- __off_t _old_offset ;
- unsigned short _cur_column ;
- signed char _vtable_offset ;
- char _shortbuf[1] ;
- _IO_lock_t *_lock ;
- __off64_t _offset ;
- void *__pad1 ;
- void *__pad2 ;
- void *__pad3 ;
- void *__pad4 ;
- size_t __pad5 ;
- int _mode ;
- char _unused2[((unsigned long)15 * sizeof(int) - (unsigned long)4 * sizeof(void *)) - sizeof(size_t)] ;
-};
-/* compiler builtin:
- unsigned int __builtin_bswap32(unsigned int); */
-/* compiler builtin:
- unsigned long __builtin_bswap64(unsigned long); */
-__inline static unsigned int __bswap_32(unsigned int __bsx)
-{
- unsigned int tmp;
- tmp = __builtin_bswap32(__bsx);
- return tmp;
-}
-
-__inline static __uint64_t __bswap_64(__uint64_t __bsx)
+#include "stdio.h"
+#include "stdlib.h"
+void decl_in_switch(int value)
{
- __uint64_t tmp;
- tmp = __builtin_bswap64(__bsx);
- return tmp;
+ __e_acsl_store_block((void *)(& value),(size_t)4);
+ switch (value) {
+ int *p;
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ default: __e_acsl_store_block_duplicate((void *)(& p),(size_t)8);
+ __e_acsl_full_init((void *)(& p));
+ p = & value;
+ __e_acsl_delete_block((void *)(& p));
+ break;
+ __e_acsl_delete_block((void *)(& p));
+ }
+ __e_acsl_delete_block((void *)(& value));
+ return;
}
-__inline static __uint16_t __uint16_identity(__uint16_t __x)
+void compound_decl_and_init(int value)
{
- return __x;
+ int a = 0;
+ __e_acsl_store_block((void *)(& a),(size_t)4);
+ __e_acsl_full_init((void *)(& a));
+ {
+ int __gen_e_acsl_valid;
+ __gen_e_acsl_valid = __e_acsl_valid((void *)(& a),sizeof(int),
+ (void *)(& a),(void *)0);
+ __e_acsl_assert(__gen_e_acsl_valid,"Assertion","compound_decl_and_init",
+ "\\valid(&a)","tests/memory/decl_in_switch.c",26);
+ }
+ /*@ assert \valid(&a); */ ;
+ switch (value) {
+ int b = 2;
+ {
+ int __gen_e_acsl_valid_2;
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& b),sizeof(int),
+ (void *)(& b),(void *)0);
+ __e_acsl_assert(__gen_e_acsl_valid_2,"Assertion",
+ "compound_decl_and_init","\\valid(&b)",
+ "tests/memory/decl_in_switch.c",31);
+ }
+ /*@ assert \valid(&b); */ ;
+ case 0: ;
+ int c = 3;
+ __e_acsl_store_block((void *)(& c),(size_t)4);
+ __e_acsl_full_init((void *)(& c));
+ {
+ int __gen_e_acsl_valid_3;
+ __gen_e_acsl_valid_3 = __e_acsl_valid((void *)(& c),sizeof(int),
+ (void *)(& c),(void *)0);
+ __e_acsl_assert(__gen_e_acsl_valid_3,"Assertion",
+ "compound_decl_and_init","\\valid(&c)",
+ "tests/memory/decl_in_switch.c",35);
+ }
+ /*@ assert \valid(&c); */ ;
+ __e_acsl_delete_block((void *)(& c));
+ break;
+ case 1: __e_acsl_store_block_duplicate((void *)(& c),(size_t)4);
+ ;
+ int d = 4;
+ __e_acsl_store_block((void *)(& d),(size_t)4);
+ __e_acsl_full_init((void *)(& d));
+ {
+ int __gen_e_acsl_valid_4;
+ __gen_e_acsl_valid_4 = __e_acsl_valid((void *)(& d),sizeof(int),
+ (void *)(& d),(void *)0);
+ __e_acsl_assert(__gen_e_acsl_valid_4,"Assertion",
+ "compound_decl_and_init","\\valid(&d)",
+ "tests/memory/decl_in_switch.c",40);
+ }
+ /*@ assert \valid(&d); */ ;
+ __e_acsl_delete_block((void *)(& c));
+ __e_acsl_delete_block((void *)(& d));
+ break;
+ __e_acsl_delete_block((void *)(& d));
+ __e_acsl_delete_block((void *)(& c));
+ }
+ __e_acsl_delete_block((void *)(& a));
+ return;
}
-__inline static __uint32_t __uint32_identity(__uint32_t __x)
+void separate_decl_and_init(int value)
{
- return __x;
+ int a;
+ __e_acsl_store_block((void *)(& a),(size_t)4);
+ __e_acsl_full_init((void *)(& a));
+ a = 1;
+ {
+ int __gen_e_acsl_valid;
+ __gen_e_acsl_valid = __e_acsl_valid((void *)(& a),sizeof(int),
+ (void *)(& a),(void *)0);
+ __e_acsl_assert(__gen_e_acsl_valid,"Assertion","separate_decl_and_init",
+ "\\valid(&a)","tests/memory/decl_in_switch.c",51);
+ }
+ /*@ assert \valid(&a); */ ;
+ switch (value) {
+ int b;
+ int c;
+ int d;
+ __e_acsl_store_block((void *)(& d),(size_t)4);
+ __e_acsl_store_block((void *)(& c),(size_t)4);
+ b = 2;
+ {
+ int __gen_e_acsl_valid_2;
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& b),sizeof(int),
+ (void *)(& b),(void *)0);
+ __e_acsl_assert(__gen_e_acsl_valid_2,"Assertion",
+ "separate_decl_and_init","\\valid(&b)",
+ "tests/memory/decl_in_switch.c",57);
+ }
+ /*@ assert \valid(&b); */ ;
+ case 0: __e_acsl_store_block_duplicate((void *)(& c),(size_t)4);
+ __e_acsl_store_block_duplicate((void *)(& d),(size_t)4);
+ ;
+ __e_acsl_full_init((void *)(& c));
+ c = 3;
+ {
+ int __gen_e_acsl_valid_3;
+ __gen_e_acsl_valid_3 = __e_acsl_valid((void *)(& c),sizeof(int),
+ (void *)(& c),(void *)0);
+ __e_acsl_assert(__gen_e_acsl_valid_3,"Assertion",
+ "separate_decl_and_init","\\valid(&c)",
+ "tests/memory/decl_in_switch.c",62);
+ }
+ /*@ assert \valid(&c); */ ;
+ __e_acsl_delete_block((void *)(& c));
+ __e_acsl_delete_block((void *)(& d));
+ break;
+ case 1: __e_acsl_store_block_duplicate((void *)(& c),(size_t)4);
+ __e_acsl_store_block_duplicate((void *)(& d),(size_t)4);
+ ;
+ __e_acsl_full_init((void *)(& d));
+ d = 4;
+ {
+ int __gen_e_acsl_valid_4;
+ __gen_e_acsl_valid_4 = __e_acsl_valid((void *)(& d),sizeof(int),
+ (void *)(& d),(void *)0);
+ __e_acsl_assert(__gen_e_acsl_valid_4,"Assertion",
+ "separate_decl_and_init","\\valid(&d)",
+ "tests/memory/decl_in_switch.c",68);
+ }
+ /*@ assert \valid(&d); */ ;
+ __e_acsl_delete_block((void *)(& c));
+ __e_acsl_delete_block((void *)(& d));
+ break;
+ __e_acsl_delete_block((void *)(& d));
+ __e_acsl_delete_block((void *)(& c));
+ }
+ __e_acsl_delete_block((void *)(& a));
+ return;
}
-__inline static __uint64_t __uint64_identity(__uint64_t __x)
+void label_in_switch(int value)
{
- return __x;
+ int done = 0;
+ switch (value) {
+ K: ;
+ int d = 0;
+ __e_acsl_store_block((void *)(& d),(size_t)4);
+ __e_acsl_full_init((void *)(& d));
+ {
+ int __gen_e_acsl_valid;
+ __gen_e_acsl_valid = __e_acsl_valid((void *)(& d),sizeof(int),
+ (void *)(& d),(void *)0);
+ __e_acsl_assert(__gen_e_acsl_valid,"Assertion","label_in_switch",
+ "\\valid(&d)","tests/memory/decl_in_switch.c",83);
+ }
+ /*@ assert \valid(&d); */ ;
+ L: case 0: __e_acsl_store_block_duplicate((void *)(& d),(size_t)4);
+ ;
+ int e = 1;
+ __e_acsl_store_block((void *)(& e),(size_t)4);
+ __e_acsl_full_init((void *)(& e));
+ {
+ int __gen_e_acsl_valid_2;
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& e),sizeof(int),
+ (void *)(& e),(void *)0);
+ __e_acsl_assert(__gen_e_acsl_valid_2,"Assertion","label_in_switch",
+ "\\valid(&e)","tests/memory/decl_in_switch.c",89);
+ }
+ /*@ assert \valid(&e); */ ;
+ __e_acsl_delete_block((void *)(& d));
+ __e_acsl_delete_block((void *)(& e));
+ break;
+ case 1: __e_acsl_store_block_duplicate((void *)(& d),(size_t)4);
+ __e_acsl_store_block_duplicate((void *)(& e),(size_t)4);
+ ;
+ int ff = 2;
+ __e_acsl_store_block((void *)(& ff),(size_t)4);
+ __e_acsl_full_init((void *)(& ff));
+ {
+ int __gen_e_acsl_valid_3;
+ __gen_e_acsl_valid_3 = __e_acsl_valid((void *)(& ff),sizeof(int),
+ (void *)(& ff),(void *)0);
+ __e_acsl_assert(__gen_e_acsl_valid_3,"Assertion","label_in_switch",
+ "\\valid(&ff)","tests/memory/decl_in_switch.c",93);
+ }
+ /*@ assert \valid(&ff); */ ;
+ __e_acsl_delete_block((void *)(& d));
+ __e_acsl_delete_block((void *)(& e));
+ __e_acsl_delete_block((void *)(& ff));
+ break;
+ __e_acsl_delete_block((void *)(& ff));
+ __e_acsl_delete_block((void *)(& e));
+ __e_acsl_delete_block((void *)(& d));
+ }
+ if (! done) {
+ done = 1;
+ if (value < 10) goto L; else goto K;
+ }
+ return;
}
-/*@
-predicate diffSize{L1, L2}(ℤ i) =
- \at(__e_acsl_heap_allocation_size,L1) -
- \at(__e_acsl_heap_allocation_size,L2) ≡ i;
-
-*/
-extern __attribute__((__FC_BUILTIN__)) int ( /* missing proto */ __e_acsl_memory_init)(
-int *x_0, char ***x_1, unsigned long x_2);
-
-extern __attribute__((__FC_BUILTIN__)) int ( /* missing proto */ __e_acsl_store_block)(
-void *x_0, unsigned long x_1);
-
-extern __attribute__((__FC_BUILTIN__)) int ( /* missing proto */ __e_acsl_full_init)(
-void *x_0);
-
-extern __attribute__((__FC_BUILTIN__)) int ( /* missing proto */ __e_acsl_delete_block)(
-void *x_0);
-
-extern __attribute__((__FC_BUILTIN__)) int ( /* missing proto */ __e_acsl_memory_clean)(
-void);
-
int main(int argc, char **argv)
{
int __retres;
- __e_acsl_memory_init(& argc,& argv,8UL);
- __e_acsl_memory_init(& argc,& argv,8UL);
- __e_acsl_store_block((void *)(& argc),4UL);
- {
- int *p;
- __e_acsl_store_block((void *)(& p),8UL);
- __e_acsl_store_block((void *)(& p),8UL);
- switch (argc) {
- default: ;
- __e_acsl_full_init((void *)(& p));
- __e_acsl_full_init((void *)(& p));
- p = & argc;
- break;
- }
- __e_acsl_delete_block((void *)(& p));
- __e_acsl_delete_block((void *)(& p));
- }
+ __e_acsl_memory_init(& argc,& argv,(size_t)8);
+ decl_in_switch(argc);
+ compound_decl_and_init(argc);
+ separate_decl_and_init(argc);
+ label_in_switch(argc);
__retres = 0;
__e_acsl_delete_block((void *)(& argc));
__e_acsl_memory_clean();
- __e_acsl_delete_block((void *)(& argc));
- __e_acsl_memory_clean();
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/decl_in_switch.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/decl_in_switch.res.oracle
new file mode 100644
index 00000000000..453f7b598d1
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/decl_in_switch.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/memory/decl_in_switch.c (with preprocessing)
--
GitLab