diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 6c71048d8f6dd78d2e941a4f0017c0d9449d9873..0cd3328d7a8dfbfa86be0b67c528bebe08236174 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -25,6 +25,9 @@
Plugin E-ACSL <next-release>
############################
+-* E-ACSL [2021-09-29] Fix translation order of the default behavior's
+ requires clauses. They are now translated before the evaluation
+ of the assumes clauses of the other behaviors.
-* E-ACSL [2021-09-13] Fix unsound reuse of previously typed recursive
functions (frama-c/e-acsl#177)
- E-ACSL [2021-08-03] Correct monitoring of code depending on libc
diff --git a/src/plugins/e-acsl/src/code_generator/contract.ml b/src/plugins/e-acsl/src/code_generator/contract.ml
index 126fa5a0c6be126c6606db65bdf826e1dcaf4736..82b54f9910c67a00c8af4bf77f3664c1391f0198 100644
--- a/src/plugins/e-acsl/src/code_generator/contract.ml
+++ b/src/plugins/e-acsl/src/code_generator/contract.ml
@@ -322,27 +322,37 @@ let fold_left_handle_error_with_args f (env, acc) l =
(env, acc)
l
-(** Insert requires check for the given contract in the environment *)
-let check_requires kf kinstr env contract =
+(** Insert requires check for the default behavior of the given contract in the
+ environment. *)
+let check_default_requires kf kinstr env contract =
+ let default_behavior =
+ Cil.find_default_behavior contract.spec
+ in
+ match default_behavior with
+ | Some b ->
+ fold_left_handle_error
+ (fun env ip_requires ->
+ if !must_translate_ppt_ref
+ (Property.ip_of_requires kf kinstr b ip_requires) then
+ let tp_requires = ip_requires.ip_content in
+ let loc = tp_requires.tp_statement.pred_loc in
+ Cil.CurrentLoc.set loc;
+ Translate.translate_predicate kf env tp_requires
+ else
+ env)
+ env
+ b.b_requires
+ | None -> env
+
+(** Insert requires check for the behaviors other than the default behavior of
+ the given contract in the environment *)
+let check_other_requires kf kinstr env contract =
let get_or_create_assumes_var =
mk_get_or_create_var kf Cil.intType "assumes_value"
in
let do_behavior env b =
if Cil.is_default_behavior b then
- fold_left_handle_error
- (fun env ip_requires ->
- if !must_translate_ppt_ref
- (Property.ip_of_requires kf kinstr b ip_requires) then
- (* If translating the default behavior, directly translate the
- predicate *)
- let tp_requires = ip_requires.ip_content in
- let loc = tp_requires.tp_statement.pred_loc in
- Cil.CurrentLoc.set loc;
- Translate.translate_predicate kf env tp_requires
- else
- env)
- env
- b.b_requires
+ env
else
(* Compute the assumes predicate for pretty-printing *)
let assumes = assumes_predicate env b.b_assumes in
@@ -763,9 +773,18 @@ let translate_preconditions kf kinstr env contract =
let env = Env.set_annotation_kind env Smart_stmt.Precondition in
let env = Env.push_contract env contract in
let env = init kf env contract in
+ (* Start with translating the requires predicate of the default behavior. *)
+ let env =
+ Env.handle_error
+ (fun env -> check_default_requires kf kinstr env contract)
+ env
+ in
+ (* Then setup the assumes clauses of the contract. *)
let env = setup_assumes kf env contract in
+ (* And finally translate the requires predicates of the rest of the behaviors,
+ skipping over the default behavior. *)
let do_it env =
- let env = check_requires kf kinstr env contract in
+ let env = check_other_requires kf kinstr env contract in
let env = check_complete_and_disjoint kf kinstr env contract in
env
in
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 1f57c1264523dccaf72db598e93285e3c4e267f4..3728e989aae62e7ec981e79fa5898e0524b17a2f 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 0392f3dc598187fa8dd9a29f3302874460d66773..f6d5a49bb4668f287960d7a34c241cda92310917 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 4517c4708613ca9fc534b644d640fc8f364aa812..1ceb9a53ba6c92b671944c932ca575728419a8e4 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 43114989ba56ee774a674dda286fce60781c1600..63fab70b9482fd6e1cf972c850956812b2008ff3 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 25c759f3ea90c05e3333efb2506a5c2cd92ca811..e1f30089847a12fbd35fbf233d86154766a2b8c8 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 46859d9e8ed08d0815cc9c57a674096b5e838124..c329fa2981878b3f2d4ef2d0ebc0f6d680c54b56 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 7b81cee7b804ad1fc0f0fd9f8e285ce744ec26c3..c547c88f2b3786ffc97a2844b28de2e5b0b85715 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 262fe258dc2fa6b5bf8ab516b18ab188b5c87f7e..3223235b07b31a8e2c509a8a17ba1ff8017a516f 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 968679a56bfa6d106020403e352f258ad6d52820..b9b98bcc628913f1dea52d98fb97c33115ee181c 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 14e8e659b1d09100f4d4c310c8b0cb1b661848e7..f9916ddbab122006517ed7aa326b5f5075428cfb 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 1ec0fc0fc6106d101670dd1cc3607cf5902d581a..cf967bfa6fb56894ae6236270ff14523ae6d1469 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",