From cd684e55f27b79ec8e2df8313e335d22679d668b Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Wed, 29 Sep 2021 11:11:37 +0200
Subject: [PATCH] [eacsl] Update tests
---
.../e-acsl/tests/bts/oracle/gen_bts1307.c | 4 +-
.../tests/builtin/oracle/strcmp.res.oracle | 8 +--
.../tests/builtin/oracle/strcpy.res.oracle | 8 +--
.../tests/builtin/oracle/strlen.res.oracle | 8 +--
.../constructs/oracle/gen_function_contract.c | 12 ++--
.../e-acsl/tests/constructs/oracle/gen_rte.c | 8 +--
.../constructs/oracle/gen_stmt_contract.c | 4 +-
.../tests/examples/oracle/gen_linear_search.c | 72 +++++++++----------
.../e-acsl/tests/libc/oracle/str.res.oracle | 8 +--
.../tests/memory/oracle/gen_ctype_macros.c | 36 +++++-----
.../tests/special/oracle/gen_e-acsl-valid.c | 10 +--
11 files changed, 89 insertions(+), 89 deletions(-)
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
index 1f57c126452..3728e989aae 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
@@ -105,7 +105,6 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
__e_acsl_store_block((void *)(& Mwmin),(size_t)8);
__e_acsl_store_block((void *)(& Mtmin_in),(size_t)8);
__gen_e_acsl_contract = __e_acsl_contract_init((size_t)1);
- __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0,1);
__gen_e_acsl_valid = __e_acsl_valid((void *)Mtmin_in,sizeof(float),
(void *)Mtmin_in,
(void *)(& Mtmin_in));
@@ -120,6 +119,7 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
(void *)(& Mtmin_out));
__e_acsl_assert(__gen_e_acsl_valid_3,1,"Precondition","bar",
"\\valid(Mtmin_out)","tests/bts/bts1307.i",22);
+ __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0,1);
}
__gen_e_acsl_at_6 = Mwmin;
__gen_e_acsl_at_5 = Mtmin_in;
@@ -247,7 +247,6 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
__e_acsl_store_block((void *)(& Mwmax),(size_t)8);
__e_acsl_store_block((void *)(& Mtmax_in),(size_t)8);
__gen_e_acsl_contract = __e_acsl_contract_init((size_t)1);
- __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0,1);
__gen_e_acsl_valid = __e_acsl_valid((void *)Mtmax_in,sizeof(float),
(void *)Mtmax_in,
(void *)(& Mtmax_in));
@@ -262,6 +261,7 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
(void *)(& Mtmax_out));
__e_acsl_assert(__gen_e_acsl_valid_3,1,"Precondition","foo",
"\\valid(Mtmax_out)","tests/bts/bts1307.i",7);
+ __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0,1);
}
__gen_e_acsl_at_3 = Mwmax;
__gen_e_acsl_at_2 = Mtmax_in;
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle
index 0392f3dc598..f6d5a49bb46 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle
@@ -41,14 +41,14 @@
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:484: Warning:
E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:495: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
- is not yet supported.
- Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:484: Warning:
E-ACSL construct `logic functions or predicates with labels'
is not yet supported.
Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:495: Warning:
+ E-ACSL construct `logic functions or predicates performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:484: Warning:
Some assumes clauses could not be translated.
Ignoring complete and disjoint behaviors annotations.
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle
index 4517c470861..1ceb9a53ba6 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle
@@ -35,14 +35,14 @@
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:484: Warning:
E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:495: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
- is not yet supported.
- Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:484: Warning:
E-ACSL construct `logic functions or predicates with labels'
is not yet supported.
Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:495: Warning:
+ E-ACSL construct `logic functions or predicates performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:484: Warning:
Some assumes clauses could not be translated.
Ignoring complete and disjoint behaviors annotations.
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle
index 43114989ba5..63fab70b948 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle
@@ -38,14 +38,14 @@
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:484: Warning:
E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:495: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
- is not yet supported.
- Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:484: Warning:
E-ACSL construct `logic functions or predicates with labels'
is not yet supported.
Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:495: Warning:
+ E-ACSL construct `logic functions or predicates performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:484: Warning:
Some assumes clauses could not be translated.
Ignoring complete and disjoint behaviors annotations.
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_function_contract.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_function_contract.c
index 25c759f3ea9..e1f30089847 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_function_contract.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_function_contract.c
@@ -221,6 +221,8 @@ void __gen_e_acsl_o(void)
int __gen_e_acsl_assumes_value;
int __gen_e_acsl_active_bhvrs;
__gen_e_acsl_contract = __e_acsl_contract_init((size_t)4);
+ __e_acsl_assert(X > -1000,1,"Precondition","o","X > -1000",
+ "tests/constructs/function_contract.i",77);
__e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0,
Y < 0);
__e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)1,
@@ -229,8 +231,6 @@ void __gen_e_acsl_o(void)
Y % 2 == 1);
__e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)3,
Y % 2 == 0);
- __e_acsl_assert(X > -1000,1,"Precondition","o","X > -1000",
- "tests/constructs/function_contract.i",77);
__gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes
((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)0);
if (__gen_e_acsl_assumes_value) __e_acsl_assert(Y < 1,1,"Precondition",
@@ -342,14 +342,14 @@ void __gen_e_acsl_n(void)
{
__e_acsl_contract_t *__gen_e_acsl_contract;
__gen_e_acsl_contract = __e_acsl_contract_init((size_t)2);
- __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0,
- X == 7);
- __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)1,
- X == 5);
__e_acsl_assert(X > 0,1,"Precondition","n","X > 0",
"tests/constructs/function_contract.i",65);
__e_acsl_assert(X < 10,1,"Precondition","n","X < 10",
"tests/constructs/function_contract.i",66);
+ __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0,
+ X == 7);
+ __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)1,
+ X == 5);
n();
{
int __gen_e_acsl_assumes_value;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_rte.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_rte.c
index 46859d9e8ed..c329fa29818 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_rte.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_rte.c
@@ -55,14 +55,14 @@ void __gen_e_acsl_test(int a, int b, int c, int d, int e, int f, int g,
{
int __gen_e_acsl_assumes_value;
__gen_e_acsl_contract = __e_acsl_contract_init((size_t)1);
- __e_acsl_assert(c != 0,1,"RTE","test","division_by_zero: c != 0",
- "tests/constructs/rte.i",11);
- __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0,
- 1 % c == 1);
__e_acsl_assert(a != 0,1,"RTE","test","division_by_zero: a != 0",
"tests/constructs/rte.i",7);
__e_acsl_assert(1 % a == 1,1,"Precondition","test","1 % a == 1",
"tests/constructs/rte.i",7);
+ __e_acsl_assert(c != 0,1,"RTE","test","division_by_zero: c != 0",
+ "tests/constructs/rte.i",11);
+ __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0,
+ 1 % c == 1);
__gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes
((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)0);
if (__gen_e_acsl_assumes_value) {
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_stmt_contract.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_stmt_contract.c
index 7b81cee7b80..c547c88f2b3 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_stmt_contract.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_stmt_contract.c
@@ -144,12 +144,12 @@ int main(void)
{
int __gen_e_acsl_active_bhvrs;
__gen_e_acsl_contract_3 = __e_acsl_contract_init((size_t)2);
+ __e_acsl_assert(x > -1000,1,"Precondition","main","x > -1000",
+ "tests/constructs/stmt_contract.i",49);
__e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract_3,
(size_t)0,x >= 0);
__e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract_3,
(size_t)1,x < 0);
- __e_acsl_assert(x > -1000,1,"Precondition","main","x > -1000",
- "tests/constructs/stmt_contract.i",49);
__gen_e_acsl_active_bhvrs = __e_acsl_contract_partial_count_all_behaviors
((__e_acsl_contract_t const *)__gen_e_acsl_contract_3);
if (__gen_e_acsl_active_bhvrs != 1) {
diff --git a/src/plugins/e-acsl/tests/examples/oracle/gen_linear_search.c b/src/plugins/e-acsl/tests/examples/oracle/gen_linear_search.c
index 262fe258dc2..3223235b07b 100644
--- a/src/plugins/e-acsl/tests/examples/oracle/gen_linear_search.c
+++ b/src/plugins/e-acsl/tests/examples/oracle/gen_linear_search.c
@@ -136,13 +136,40 @@ int __gen_e_acsl_search(int elt)
__e_acsl_contract_t *__gen_e_acsl_contract;
int __retres;
{
+ int __gen_e_acsl_forall;
+ int __gen_e_acsl_i;
int __gen_e_acsl_exists;
int __gen_e_acsl_j;
- int __gen_e_acsl_forall;
- int __gen_e_acsl_j_2;
int __gen_e_acsl_forall_2;
- int __gen_e_acsl_i;
+ int __gen_e_acsl_j_2;
__gen_e_acsl_contract = __e_acsl_contract_init((size_t)2);
+ __gen_e_acsl_forall = 1;
+ __gen_e_acsl_i = 0;
+ while (1) {
+ if (__gen_e_acsl_i < 9) ; else break;
+ __e_acsl_assert((int)(__gen_e_acsl_i + 1L) < 10,1,"RTE","search",
+ "index_bound: (int)(__gen_e_acsl_i + 1) < 10",
+ "tests/examples/linear_search.i",7);
+ __e_acsl_assert(0 <= (int)(__gen_e_acsl_i + 1L),1,"RTE","search",
+ "index_bound: 0 <= (int)(__gen_e_acsl_i + 1)",
+ "tests/examples/linear_search.i",7);
+ __e_acsl_assert(__gen_e_acsl_i < 10,1,"RTE","search",
+ "index_bound: __gen_e_acsl_i < 10",
+ "tests/examples/linear_search.i",7);
+ __e_acsl_assert(0 <= __gen_e_acsl_i,1,"RTE","search",
+ "index_bound: 0 <= __gen_e_acsl_i",
+ "tests/examples/linear_search.i",7);
+ if (A[__gen_e_acsl_i] <= A[__gen_e_acsl_i + 1]) ;
+ else {
+ __gen_e_acsl_forall = 0;
+ goto e_acsl_end_loop3;
+ }
+ __gen_e_acsl_i ++;
+ }
+ e_acsl_end_loop3: ;
+ __e_acsl_assert(__gen_e_acsl_forall,1,"Precondition","search",
+ "\\forall integer i; 0 <= i < 9 ==> A[i] <= A[i + 1]",
+ "tests/examples/linear_search.i",7);
__gen_e_acsl_exists = 0;
__gen_e_acsl_j = 0;
while (1) {
@@ -156,14 +183,14 @@ int __gen_e_acsl_search(int elt)
if (! (A[__gen_e_acsl_j] == elt)) ;
else {
__gen_e_acsl_exists = 1;
- goto e_acsl_end_loop3;
+ goto e_acsl_end_loop4;
}
__gen_e_acsl_j ++;
}
- e_acsl_end_loop3: ;
+ e_acsl_end_loop4: ;
__e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0,
__gen_e_acsl_exists);
- __gen_e_acsl_forall = 1;
+ __gen_e_acsl_forall_2 = 1;
__gen_e_acsl_j_2 = 0;
while (1) {
if (__gen_e_acsl_j_2 < 10) ; else break;
@@ -174,42 +201,15 @@ int __gen_e_acsl_search(int elt)
"index_bound: 0 <= __gen_e_acsl_j_2",
"tests/examples/linear_search.i",12);
if (A[__gen_e_acsl_j_2] != elt) ;
- else {
- __gen_e_acsl_forall = 0;
- goto e_acsl_end_loop4;
- }
- __gen_e_acsl_j_2 ++;
- }
- e_acsl_end_loop4: ;
- __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)1,
- __gen_e_acsl_forall);
- __gen_e_acsl_forall_2 = 1;
- __gen_e_acsl_i = 0;
- while (1) {
- if (__gen_e_acsl_i < 9) ; else break;
- __e_acsl_assert((int)(__gen_e_acsl_i + 1L) < 10,1,"RTE","search",
- "index_bound: (int)(__gen_e_acsl_i + 1) < 10",
- "tests/examples/linear_search.i",7);
- __e_acsl_assert(0 <= (int)(__gen_e_acsl_i + 1L),1,"RTE","search",
- "index_bound: 0 <= (int)(__gen_e_acsl_i + 1)",
- "tests/examples/linear_search.i",7);
- __e_acsl_assert(__gen_e_acsl_i < 10,1,"RTE","search",
- "index_bound: __gen_e_acsl_i < 10",
- "tests/examples/linear_search.i",7);
- __e_acsl_assert(0 <= __gen_e_acsl_i,1,"RTE","search",
- "index_bound: 0 <= __gen_e_acsl_i",
- "tests/examples/linear_search.i",7);
- if (A[__gen_e_acsl_i] <= A[__gen_e_acsl_i + 1]) ;
else {
__gen_e_acsl_forall_2 = 0;
goto e_acsl_end_loop5;
}
- __gen_e_acsl_i ++;
+ __gen_e_acsl_j_2 ++;
}
e_acsl_end_loop5: ;
- __e_acsl_assert(__gen_e_acsl_forall_2,1,"Precondition","search",
- "\\forall integer i; 0 <= i < 9 ==> A[i] <= A[i + 1]",
- "tests/examples/linear_search.i",7);
+ __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)1,
+ __gen_e_acsl_forall_2);
}
__retres = search(elt);
{
diff --git a/src/plugins/e-acsl/tests/libc/oracle/str.res.oracle b/src/plugins/e-acsl/tests/libc/oracle/str.res.oracle
index 968679a56bf..b9b98bcc628 100644
--- a/src/plugins/e-acsl/tests/libc/oracle/str.res.oracle
+++ b/src/plugins/e-acsl/tests/libc/oracle/str.res.oracle
@@ -75,19 +75,19 @@
E-ACSL construct `logic functions or predicates performing read accesses'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:445: Warning:
+[e-acsl] FRAMAC_SHARE/libc/string.h:439: Warning:
E-ACSL construct `logic functions or predicates with labels'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:453: Warning:
+[e-acsl] FRAMAC_SHARE/libc/string.h:440: Warning:
E-ACSL construct `logic functions or predicates with labels'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:439: Warning:
+[e-acsl] FRAMAC_SHARE/libc/string.h:445: Warning:
E-ACSL construct `logic functions or predicates with labels'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:440: Warning:
+[e-acsl] FRAMAC_SHARE/libc/string.h:453: Warning:
E-ACSL construct `logic functions or predicates with labels'
is not yet supported.
Ignoring annotation.
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_ctype_macros.c b/src/plugins/e-acsl/tests/memory/oracle/gen_ctype_macros.c
index 14e8e659b1d..f9916ddbab1 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_ctype_macros.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_ctype_macros.c
@@ -78,34 +78,34 @@ int __gen_e_acsl_isupper(int c)
{
int __gen_e_acsl_and;
int __gen_e_acsl_or;
+ int __gen_e_acsl_and_2;
int __gen_e_acsl_or_2;
- int __gen_e_acsl_and_4;
int __gen_e_acsl_or_3;
int __gen_e_acsl_active_bhvrs;
__gen_e_acsl_contract = __e_acsl_contract_init((size_t)2);
- if (65 <= c) __gen_e_acsl_and = c <= 90; else __gen_e_acsl_and = 0;
+ if (0 <= c) __gen_e_acsl_and = c <= 255; else __gen_e_acsl_and = 0;
+ if (__gen_e_acsl_and) __gen_e_acsl_or = 1;
+ else __gen_e_acsl_or = c == -1;
+ __e_acsl_assert(__gen_e_acsl_or,1,"Precondition","isupper",
+ "c_uchar_or_eof: (0 <= c <= 255) || c == -1",
+ "FRAMAC_SHARE/libc/ctype.h",174);
+ if (65 <= c) __gen_e_acsl_and_2 = c <= 90; else __gen_e_acsl_and_2 = 0;
__e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0,
- __gen_e_acsl_and);
- if (c == -1) __gen_e_acsl_or = 1;
- else {
- int __gen_e_acsl_and_2;
- if (0 <= c) __gen_e_acsl_and_2 = c < 65; else __gen_e_acsl_and_2 = 0;
- __gen_e_acsl_or = __gen_e_acsl_and_2;
- }
- if (__gen_e_acsl_or) __gen_e_acsl_or_2 = 1;
+ __gen_e_acsl_and_2);
+ if (c == -1) __gen_e_acsl_or_2 = 1;
else {
int __gen_e_acsl_and_3;
- if (90 < c) __gen_e_acsl_and_3 = c <= 127; else __gen_e_acsl_and_3 = 0;
+ if (0 <= c) __gen_e_acsl_and_3 = c < 65; else __gen_e_acsl_and_3 = 0;
__gen_e_acsl_or_2 = __gen_e_acsl_and_3;
}
+ if (__gen_e_acsl_or_2) __gen_e_acsl_or_3 = 1;
+ else {
+ int __gen_e_acsl_and_4;
+ if (90 < c) __gen_e_acsl_and_4 = c <= 127; else __gen_e_acsl_and_4 = 0;
+ __gen_e_acsl_or_3 = __gen_e_acsl_and_4;
+ }
__e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)1,
- __gen_e_acsl_or_2);
- if (0 <= c) __gen_e_acsl_and_4 = c <= 255; else __gen_e_acsl_and_4 = 0;
- if (__gen_e_acsl_and_4) __gen_e_acsl_or_3 = 1;
- else __gen_e_acsl_or_3 = c == -1;
- __e_acsl_assert(__gen_e_acsl_or_3,1,"Precondition","isupper",
- "c_uchar_or_eof: (0 <= c <= 255) || c == -1",
- "FRAMAC_SHARE/libc/ctype.h",174);
+ __gen_e_acsl_or_3);
__gen_e_acsl_active_bhvrs = __e_acsl_contract_partial_count_all_behaviors
((__e_acsl_contract_t const *)__gen_e_acsl_contract);
__e_acsl_assert(__gen_e_acsl_active_bhvrs <= 1,1,"Precondition",
diff --git a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-valid.c b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-valid.c
index 1ec0fc0fc61..cf967bfa6fb 100644
--- a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-valid.c
+++ b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-valid.c
@@ -111,13 +111,17 @@ void __gen_e_acsl_f(int *x, int *y)
{
__e_acsl_contract_t *__gen_e_acsl_contract;
{
+ int __gen_e_acsl_valid;
int __gen_e_acsl_valid_read;
int __gen_e_acsl_valid_read_2;
- int __gen_e_acsl_valid;
int __gen_e_acsl_active_bhvrs;
__e_acsl_store_block((void *)(& y),(size_t)8);
__e_acsl_store_block((void *)(& x),(size_t)8);
__gen_e_acsl_contract = __e_acsl_contract_init((size_t)2);
+ __gen_e_acsl_valid = __e_acsl_valid((void *)y,sizeof(int),(void *)y,
+ (void *)(& y));
+ __e_acsl_assert(__gen_e_acsl_valid,1,"Precondition","f","\\valid(y)",
+ "tests/special/e-acsl-valid.c",12);
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)x,sizeof(int),
(void *)x,(void *)(& x));
__e_acsl_assert(__gen_e_acsl_valid_read,1,"RTE","f",
@@ -132,10 +136,6 @@ void __gen_e_acsl_f(int *x, int *y)
"tests/special/e-acsl-valid.c",21);
__e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)1,
*x == 0);
- __gen_e_acsl_valid = __e_acsl_valid((void *)y,sizeof(int),(void *)y,
- (void *)(& y));
- __e_acsl_assert(__gen_e_acsl_valid,1,"Precondition","f","\\valid(y)",
- "tests/special/e-acsl-valid.c",12);
__gen_e_acsl_active_bhvrs = __e_acsl_contract_partial_count_all_behaviors
((__e_acsl_contract_t const *)__gen_e_acsl_contract);
__e_acsl_assert(__gen_e_acsl_active_bhvrs >= 1,1,"Precondition","f",
--
GitLab