From 060c37784652c118dd30861a3fd3b1330aa23761 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Mon, 24 Jan 2022 15:12:06 +0100
Subject: [PATCH] [eacsl] Update tests oracles
---
.../e-acsl/tests/arith/oracle/at.res.oracle | 2 +-
.../e-acsl/tests/arith/oracle/gen_at.c | 38 +++++++++----------
.../tests/bts/bts1386_complex_flowgraph.c | 4 ++
.../oracle/gen_bts1386_complex_flowgraph.c | 21 ++++++----
.../e-acsl/tests/bts/oracle/gen_bts1390.c | 10 ++---
.../e-acsl/tests/bts/oracle/gen_bts1717.c | 8 ++--
.../e-acsl/tests/bts/oracle/gen_bts1718.c | 8 ++--
.../e-acsl/tests/bts/oracle/gen_bts1740.c | 2 +-
.../tests/bts/oracle/gen_issue-eacsl-105.c | 2 +-
.../tests/bts/oracle/gen_issue-eacsl-91.c | 9 ++---
.../concurrency/oracle/gen_parallel_threads.c | 14 +++----
.../constructs/oracle/gen_labeled_stmt.c | 8 ++--
.../memory/oracle/decl_in_switch.res.oracle | 24 ++++++++++++
.../tests/memory/oracle/gen_bypassed_var.c | 3 +-
.../tests/memory/oracle/gen_decl_in_switch.c | 16 +++++---
.../tests/memory/oracle/gen_early_exit.c | 6 +--
.../e-acsl/tests/memory/oracle/gen_goto.c | 6 +--
.../memory/oracle/gen_valid_in_contract.c | 8 ++--
.../tests/temporal/oracle/gen_t_labels.c | 6 ++-
.../tests/temporal/oracle/gen_t_while.c | 3 +-
20 files changed, 113 insertions(+), 85 deletions(-)
diff --git a/src/plugins/e-acsl/tests/arith/oracle/at.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/at.res.oracle
index 95c57008f70..f3865d1f2f0 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/at.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/at.res.oracle
@@ -21,7 +21,7 @@
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
[eva:alarm] at.i:29: Warning: assertion got status unknown.
-[eva:alarm] at.i:31: Warning: assertion got status unknown.
[eva:alarm] at.i:31: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
+[eva:alarm] at.i:31: Warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_at.c b/src/plugins/e-acsl/tests/arith/oracle/gen_at.c
index fd8b7c2323e..066ff02534b 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_at.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_at.c
@@ -181,26 +181,25 @@ void g(int *p, int *q)
{
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
- "\\at(*(p + \\at(*q,__invalid_label)),L2)",
- 0,__gen_e_acsl_at_2);
+ "\\at(*(p + \\at(*q,L1)),L2)",0,
+ __gen_e_acsl_at_2);
__gen_e_acsl_assert_data.blocking = 1;
__gen_e_acsl_assert_data.kind = "Assertion";
- __gen_e_acsl_assert_data.pred_txt = "\\at(*(p + \\at(*q,__invalid_label)),L2) == 2";
+ __gen_e_acsl_assert_data.pred_txt = "\\at(*(p + \\at(*q,L1)),L2) == 2";
__gen_e_acsl_assert_data.file = "at.i";
__gen_e_acsl_assert_data.fct = "g";
__gen_e_acsl_assert_data.line = 29;
__e_acsl_assert(__gen_e_acsl_at_2 == 2,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
}
- /*@ assert \at(*(p + \at(*q,__invalid_label)),L2) == 2; */ ;
+ /*@ assert \at(*(p + \at(*q,L1)),L2) == 2; */ ;
L3:
- /*@ assert \at(*(p + \at(*q,__invalid_label)),Here) == 2; */
{
int __gen_e_acsl_valid_read_4;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_4 =
{.values = (void *)0};
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_4,
- "*(p + \\at(*q,__invalid_label))",0,
+ "*(p + \\at(*q,L1))",0,
*(p + __gen_e_acsl_at_3));
__e_acsl_assert_data_t __gen_e_acsl_assert_data_6 =
{.values = (void *)0};
@@ -222,7 +221,7 @@ void g(int *p, int *q)
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_6);
__gen_e_acsl_assert_data_4.blocking = 1;
__gen_e_acsl_assert_data_4.kind = "Assertion";
- __gen_e_acsl_assert_data_4.pred_txt = "\\at(*(p + \\at(*q,__invalid_label)),Here) == 2";
+ __gen_e_acsl_assert_data_4.pred_txt = "\\at(*(p + \\at(*q,L1)),Here) == 2";
__gen_e_acsl_assert_data_4.file = "at.i";
__gen_e_acsl_assert_data_4.fct = "g";
__gen_e_acsl_assert_data_4.line = 31;
@@ -230,6 +229,7 @@ void g(int *p, int *q)
& __gen_e_acsl_assert_data_4);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
}
+ /*@ assert \at(*(p + \at(*q,L1)),Here) == 2; */ ;
__e_acsl_delete_block((void *)(& q));
__e_acsl_delete_block((void *)(& p));
return;
@@ -259,7 +259,6 @@ int main(void)
__e_acsl_full_init((void *)(& x));
x = __gen_e_acsl_h(0);
L:
- /*@ assert x == 0; */
{
__gen_e_acsl_at_3 = (long)x;
__gen_e_acsl_at_2 = x + 1L;
@@ -277,6 +276,7 @@ int main(void)
__e_acsl_assert(x == 0,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
}
+ /*@ assert x == 0; */ ;
}
__e_acsl_full_init((void *)(& x));
x = 1;
@@ -286,43 +286,41 @@ int main(void)
{
__e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
{.values = (void *)0};
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,
- "\\at(x,__invalid_label)",0,__gen_e_acsl_at);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,"\\at(x,L)",0,
+ __gen_e_acsl_at);
__gen_e_acsl_assert_data_2.blocking = 1;
__gen_e_acsl_assert_data_2.kind = "Assertion";
- __gen_e_acsl_assert_data_2.pred_txt = "\\at(x,__invalid_label) == 0";
+ __gen_e_acsl_assert_data_2.pred_txt = "\\at(x,L) == 0";
__gen_e_acsl_assert_data_2.file = "at.i";
__gen_e_acsl_assert_data_2.fct = "main";
__gen_e_acsl_assert_data_2.line = 54;
__e_acsl_assert(__gen_e_acsl_at == 0,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
}
- /*@ assert \at(x,__invalid_label) == 0; */ ;
+ /*@ assert \at(x,L) == 0; */ ;
{
__e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
{.values = (void *)0};
__e_acsl_assert_register_long(& __gen_e_acsl_assert_data_3,
- "\\at(x + 1,__invalid_label)",0,
- __gen_e_acsl_at_2);
+ "\\at(x + 1,L)",0,__gen_e_acsl_at_2);
__gen_e_acsl_assert_data_3.blocking = 1;
__gen_e_acsl_assert_data_3.kind = "Assertion";
- __gen_e_acsl_assert_data_3.pred_txt = "\\at(x + 1,__invalid_label) == 1";
+ __gen_e_acsl_assert_data_3.pred_txt = "\\at(x + 1,L) == 1";
__gen_e_acsl_assert_data_3.file = "at.i";
__gen_e_acsl_assert_data_3.fct = "main";
__gen_e_acsl_assert_data_3.line = 55;
__e_acsl_assert(__gen_e_acsl_at_2 == 1L,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
}
- /*@ assert \at(x + 1,__invalid_label) == 1; */ ;
+ /*@ assert \at(x + 1,L) == 1; */ ;
{
__e_acsl_assert_data_t __gen_e_acsl_assert_data_4 =
{.values = (void *)0};
- __e_acsl_assert_register_long(& __gen_e_acsl_assert_data_4,
- "\\at(x,__invalid_label)",0,
+ __e_acsl_assert_register_long(& __gen_e_acsl_assert_data_4,"\\at(x,L)",0,
__gen_e_acsl_at_3);
__gen_e_acsl_assert_data_4.blocking = 1;
__gen_e_acsl_assert_data_4.kind = "Assertion";
- __gen_e_acsl_assert_data_4.pred_txt = "\\at(x,__invalid_label) + 1 == 1";
+ __gen_e_acsl_assert_data_4.pred_txt = "\\at(x,L) + 1 == 1";
__gen_e_acsl_assert_data_4.file = "at.i";
__gen_e_acsl_assert_data_4.fct = "main";
__gen_e_acsl_assert_data_4.line = 56;
@@ -330,7 +328,7 @@ int main(void)
& __gen_e_acsl_assert_data_4);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
}
- /*@ assert \at(x,__invalid_label) + 1 == 1; */ ;
+ /*@ assert \at(x,L) + 1 == 1; */ ;
g(t,& x);
__retres = 0;
__e_acsl_delete_block((void *)(t));
diff --git a/src/plugins/e-acsl/tests/bts/bts1386_complex_flowgraph.c b/src/plugins/e-acsl/tests/bts/bts1386_complex_flowgraph.c
index 11a259f7b28..6dd76f26cdf 100644
--- a/src/plugins/e-acsl/tests/bts/bts1386_complex_flowgraph.c
+++ b/src/plugins/e-acsl/tests/bts/bts1386_complex_flowgraph.c
@@ -1,3 +1,7 @@
+/* run.config
+ STDOPT: #"-eva-slevel 5"
+*/
+
/* MDH WCET BENCHMARK SUITE. File version $Id: duff.c,v 1.4 2005/12/21 09:43:07 jgn Exp $ */
/*----------------------------------------------------------------------
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1386_complex_flowgraph.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1386_complex_flowgraph.c
index 7a3999163b8..0082fd03200 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1386_complex_flowgraph.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1386_complex_flowgraph.c
@@ -57,7 +57,8 @@ void duffcopy(char *to, char *from, int count)
from ++;
__e_acsl_initialize((void *)tmp,sizeof(char));
*tmp = *tmp_0;
- case 7: __e_acsl_store_block_duplicate((void *)(& tmp),(size_t)8);
+ 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);
@@ -81,7 +82,8 @@ void duffcopy(char *to, char *from, int count)
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);
+ 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);
@@ -105,7 +107,8 @@ void duffcopy(char *to, char *from, int count)
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);
+ 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);
@@ -129,7 +132,8 @@ void duffcopy(char *to, char *from, int count)
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);
+ 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);
@@ -153,7 +157,8 @@ void duffcopy(char *to, char *from, int count)
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);
+ 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);
@@ -177,7 +182,8 @@ void duffcopy(char *to, char *from, int count)
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);
+ 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);
@@ -201,7 +207,8 @@ void duffcopy(char *to, char *from, int count)
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);
+ 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);
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
index aa0f1053640..710fec08e42 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
@@ -49,12 +49,10 @@ void *memchr(void const *buf, int c, size_t n)
__e_acsl_full_init((void *)(& __retres));
__retres = (void *)0;
return_label:
- {
- __e_acsl_delete_block((void *)(& buf));
- __e_acsl_delete_block((void *)(& s));
- __e_acsl_delete_block((void *)(& __retres));
- return __retres;
- }
+ __e_acsl_delete_block((void *)(& buf));
+ __e_acsl_delete_block((void *)(& s));
+ __e_acsl_delete_block((void *)(& __retres));
+ return __retres;
}
/*@ behavior exists:
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
index 6c169fa3ba0..6479ce65549 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
@@ -19,7 +19,6 @@ int main(void)
__e_acsl_full_init((void *)(& a));
goto lbl_1;
lbl_2:
- /*@ assert \valid(p); */
{
int __gen_e_acsl_initialized;
int __gen_e_acsl_and;
@@ -54,12 +53,11 @@ int main(void)
__e_acsl_assert(__gen_e_acsl_and,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
}
+ /*@ assert \valid(p); */ ;
__retres = 0;
goto return_label;
- lbl_1: {
- __e_acsl_full_init((void *)(& p));
- p = & a;
- }
+ lbl_1: __e_acsl_full_init((void *)(& p));
+ p = & a;
goto lbl_2;
return_label:
{
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
index 4e20f15d53e..23f2cb2d589 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
@@ -19,7 +19,6 @@ int main(void)
__e_acsl_full_init((void *)(& a));
goto lbl_1;
lbl_2:
- /*@ assert \valid(p); */
{
int __gen_e_acsl_initialized;
int __gen_e_acsl_and;
@@ -54,12 +53,11 @@ int main(void)
__e_acsl_assert(__gen_e_acsl_and,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
}
+ /*@ assert \valid(p); */ ;
__retres = 0;
goto return_label;
- lbl_1: {
- __e_acsl_full_init((void *)(& p));
- p = & a;
- }
+ lbl_1: __e_acsl_full_init((void *)(& p));
+ p = & a;
goto lbl_2;
return_label:
{
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c
index 535feb4a46f..b233499a490 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c
@@ -62,7 +62,6 @@ int main(void)
__e_acsl_delete_block((void *)(& a));
}
L:
- /*@ assert !\valid(p); */
{
int __gen_e_acsl_initialized_2;
int __gen_e_acsl_and_2;
@@ -100,6 +99,7 @@ int main(void)
__e_acsl_assert(! __gen_e_acsl_and_2,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
}
+ /*@ assert !\valid(p); */ ;
__retres = 0;
__e_acsl_delete_block((void *)(& p));
__e_acsl_memory_clean();
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-105.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-105.c
index 7005fdef05a..34d4bc63358 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-105.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-105.c
@@ -16,7 +16,6 @@ int f(void)
__e_acsl_full_init((void *)(& a));
goto lbl_1;
lbl_2:
- /*@ assert \valid(&a); */
{
int __gen_e_acsl_valid;
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
@@ -37,6 +36,7 @@ int f(void)
__e_acsl_assert(__gen_e_acsl_valid,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
}
+ /*@ assert \valid(&a); */ ;
__retres = 0;
goto return_label;
lbl_1: goto lbl_2;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-91.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-91.c
index 3f28748da01..40c85c745e4 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-91.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-91.c
@@ -17,7 +17,8 @@ char b(void)
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);
+ case 0:
+ __e_acsl_store_block_duplicate((void *)(& c),(size_t)4);
__e_acsl_delete_block((void *)(& c));
goto d;
int tmp = c;
@@ -26,10 +27,8 @@ char b(void)
__e_acsl_delete_block((void *)(& tmp));
__e_acsl_delete_block((void *)(& c));
}
- d: {
- __e_acsl_full_init((void *)(& __retres));
- __retres = (char)2;
- }
+ d: __e_acsl_full_init((void *)(& __retres));
+ __retres = (char)2;
__e_acsl_delete_block((void *)(& __retres));
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c b/src/plugins/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c
index 0883dc14bc1..f9f9cc90b23 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c
+++ b/src/plugins/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c
@@ -454,14 +454,12 @@ void *read_value(void *arg)
__e_acsl_delete_block((void *)(& idx));
}
return_label:
- {
- __e_acsl_delete_block((void *)(& arg));
- __e_acsl_delete_block((void *)(& tmp_1));
- __e_acsl_delete_block((void *)(& tmp_0));
- __e_acsl_delete_block((void *)(& tmp));
- __e_acsl_delete_block((void *)(& __retres));
- return __retres;
- }
+ __e_acsl_delete_block((void *)(& arg));
+ __e_acsl_delete_block((void *)(& tmp_1));
+ __e_acsl_delete_block((void *)(& tmp_0));
+ __e_acsl_delete_block((void *)(& tmp));
+ __e_acsl_delete_block((void *)(& __retres));
+ return __retres;
}
/*@ requires
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_labeled_stmt.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_labeled_stmt.c
index 5562e5d3d84..ffe68532b72 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_labeled_stmt.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_labeled_stmt.c
@@ -17,7 +17,6 @@ int __gen_e_acsl_main(void)
int __retres;
goto L1;
L1:
- /*@ assert X == 0; */
{
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data,"X",0,X);
@@ -30,11 +29,10 @@ int __gen_e_acsl_main(void)
__e_acsl_assert(X == 0,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
}
+ /*@ assert X == 0; */ ;
X = 1;
goto L2;
L2:
- /*@ requires X == 1;
- ensures X == 2; */
{
{
__e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
@@ -48,8 +46,10 @@ int __gen_e_acsl_main(void)
__gen_e_acsl_assert_data_2.line = 13;
__e_acsl_assert(X == 1,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
- X = 2;
}
+ /*@ requires X == 1;
+ ensures X == 2; */
+ X = 2;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
{.values = (void *)0};
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,"X",0,X);
diff --git a/src/plugins/e-acsl/tests/memory/oracle/decl_in_switch.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/decl_in_switch.res.oracle
index 727a00d39c6..f57964d77a4 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/decl_in_switch.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/decl_in_switch.res.oracle
@@ -12,12 +12,36 @@
[eva:alarm] decl_in_switch.c:30: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
+[eva:alarm] decl_in_switch.c:35: Warning:
+ function __e_acsl_assert_register_ulong: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
+[eva:alarm] decl_in_switch.c:35: Warning:
+ function __e_acsl_assert_register_int: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
[eva:alarm] decl_in_switch.c:45: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
[eva:alarm] decl_in_switch.c:45: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
+[eva:alarm] decl_in_switch.c:55: Warning:
+ function __e_acsl_assert_register_ulong: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
+[eva:alarm] decl_in_switch.c:55: Warning:
+ function __e_acsl_assert_register_int: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
+[eva:alarm] decl_in_switch.c:61: Warning:
+ function __e_acsl_assert_register_ulong: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
+[eva:alarm] decl_in_switch.c:61: Warning:
+ function __e_acsl_assert_register_int: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
+[eva:alarm] decl_in_switch.c:84: Warning:
+ function __e_acsl_assert_register_ulong: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
+[eva:alarm] decl_in_switch.c:84: Warning:
+ function __e_acsl_assert_register_int: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
[eva:alarm] decl_in_switch.c:74: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_bypassed_var.c b/src/plugins/e-acsl/tests/memory/oracle/gen_bypassed_var.c
index 1c6b6223e6c..9db991fcd5f 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_bypassed_var.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_bypassed_var.c
@@ -16,7 +16,8 @@ int main(int argc, char const **argv)
{
int *p;
__e_acsl_store_block((void *)(& p),(size_t)8);
- L: __e_acsl_store_block_duplicate((void *)(& p),(size_t)8);
+ L:
+ __e_acsl_store_block_duplicate((void *)(& p),(size_t)8);
__e_acsl_full_init((void *)(& p));
p = & argc;
{
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_decl_in_switch.c b/src/plugins/e-acsl/tests/memory/oracle/gen_decl_in_switch.c
index 24f47f9ec9c..0d716b69a95 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_decl_in_switch.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_decl_in_switch.c
@@ -14,7 +14,8 @@ void decl_in_switch(int value)
switch (value) {
int *p;
__e_acsl_store_block((void *)(& p),(size_t)8);
- default: __e_acsl_store_block_duplicate((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));
@@ -104,7 +105,7 @@ void compound_decl_and_init(int value)
__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));
@@ -196,7 +197,8 @@ void separate_decl_and_init(int value)
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
}
/*@ assert \valid(&b); */ ;
- case 0: __e_acsl_store_block_duplicate((void *)(& c),(size_t)4);
+ 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));
@@ -226,7 +228,8 @@ void separate_decl_and_init(int value)
__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);
+ 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));
@@ -294,7 +297,7 @@ void label_in_switch(int value)
}
/*@ 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));
@@ -323,7 +326,8 @@ void label_in_switch(int value)
__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);
+ 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;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_early_exit.c b/src/plugins/e-acsl/tests/memory/oracle/gen_early_exit.c
index c2b9a420914..f7356a6d34e 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_early_exit.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_early_exit.c
@@ -61,7 +61,6 @@ int goto_bts(void)
__e_acsl_delete_block((void *)(& a));
}
L:
- /*@ assert !\valid(p); */
{
int __gen_e_acsl_initialized_2;
int __gen_e_acsl_and_2;
@@ -99,6 +98,7 @@ int goto_bts(void)
__e_acsl_assert(! __gen_e_acsl_and_2,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
}
+ /*@ assert !\valid(p); */ ;
__retres = 0;
__e_acsl_delete_block((void *)(& p));
return __retres;
@@ -146,7 +146,6 @@ int goto_valid(void)
}
}
FIRST:
- /*@ assert \valid(p); */
{
int __gen_e_acsl_initialized;
int __gen_e_acsl_and;
@@ -183,6 +182,7 @@ int goto_valid(void)
__e_acsl_assert(__gen_e_acsl_and,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
}
+ /*@ assert \valid(p); */ ;
{
int __gen_e_acsl_initialized_2;
int __gen_e_acsl_and_2;
@@ -268,7 +268,6 @@ int goto_valid(void)
__e_acsl_delete_block((void *)(& a1));
}
SECOND:
- /*@ assert !\valid(p); */
{
int __gen_e_acsl_initialized_4;
int __gen_e_acsl_and_4;
@@ -305,6 +304,7 @@ int goto_valid(void)
__e_acsl_assert(! __gen_e_acsl_and_4,& __gen_e_acsl_assert_data_4);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
}
+ /*@ assert !\valid(p); */ ;
{
int __gen_e_acsl_initialized_5;
int __gen_e_acsl_and_5;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_goto.c b/src/plugins/e-acsl/tests/memory/oracle/gen_goto.c
index 86288462093..43911e961b2 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_goto.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_goto.c
@@ -34,10 +34,8 @@ int main(void)
__e_acsl_globals_init();
__e_acsl_store_block((void *)(& b),(size_t)8);
goto _LOR;
- _LOR: {
- __e_acsl_full_init((void *)(& b));
- b = & a;
- }
+ _LOR: __e_acsl_full_init((void *)(& b));
+ b = & a;
if (a) goto _LOR;
{
int __gen_e_acsl_initialized;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_valid_in_contract.c b/src/plugins/e-acsl/tests/memory/oracle/gen_valid_in_contract.c
index 07956350652..3f991258a7a 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_valid_in_contract.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_valid_in_contract.c
@@ -41,11 +41,9 @@ struct list *f(struct list *l)
__e_acsl_full_init((void *)(& __retres));
__retres = (struct list *)0;
return_label:
- {
- __e_acsl_delete_block((void *)(& l));
- __e_acsl_delete_block((void *)(& __retres));
- return __retres;
- }
+ __e_acsl_delete_block((void *)(& l));
+ __e_acsl_delete_block((void *)(& __retres));
+ return __retres;
}
int main(void)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_labels.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_labels.c
index e47fdc487dc..75e427d2eea 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_labels.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_labels.c
@@ -49,7 +49,8 @@ int main(int argc, char const **argv)
__e_acsl_temporal_store_nblock((void *)(& q),(void *)(& b));
__e_acsl_store_block((void *)(& q),(size_t)8);
__e_acsl_full_init((void *)(& q));
- LAB: __e_acsl_temporal_reset_parameters();
+ LAB:
+ __e_acsl_temporal_reset_parameters();
__e_acsl_temporal_reset_return();
__e_acsl_temporal_save_nreferent_parameter((void *)(& p),0U);
__e_acsl_temporal_save_nreferent_parameter((void *)(& q),1U);
@@ -118,8 +119,9 @@ int main(int argc, char const **argv)
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
}
/*@ assert \valid(p) && \valid(q); */ ;
+ LAB2:
__e_acsl_full_init((void *)(& q));
- LAB2: __e_acsl_temporal_store_nreferent((void *)(& q),(void *)(& p));
+ __e_acsl_temporal_store_nreferent((void *)(& q),(void *)(& p));
q = p;
{
int __gen_e_acsl_initialized_3;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_while.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_while.c
index 650797a31e1..5a074dd5307 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_while.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_while.c
@@ -108,7 +108,8 @@ int main(void)
}
/*@ assert !\valid(q); */ ;
__retres = 0;
- return_label: __e_acsl_store_block_duplicate((void *)(& q),(size_t)8);
+ return_label:
+ __e_acsl_store_block_duplicate((void *)(& q),(size_t)8);
__e_acsl_delete_block((void *)(& q));
__e_acsl_delete_block((void *)(arr));
__e_acsl_memory_clean();
--
GitLab