From f2ce5c291f67f92d6a9ca33bba3e834cab3171d1 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Mon, 8 Jan 2018 11:05:13 +0100
Subject: [PATCH] fix crash when translating a postcondition that generates
local variables
---
src/plugins/e-acsl/doc/Changelog | 4 +-
.../tests/runtime/oracle/gen_stmt_contract.c | 49 ++++++++++---------
.../e-acsl/tests/runtime/stmt_contract.i | 4 +-
src/plugins/e-acsl/visit.ml | 5 +-
4 files changed, 37 insertions(+), 25 deletions(-)
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index f1ab26ee2ef..61763b17e73 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -19,10 +19,12 @@
# configure configure
###############################################################################
+-* E-ACSL [2018/01/08] Fix a crash when translating a postcondition
+ that should generate a local variable (bts #2339).
-* e-acsl-gcc [2017/11/28] Several files may be given to e-acsl-gcc.sh
(as specified).
-* E-ACSL [2017/11/27] Fix 'segmentation fault' of the generated monitor
- whenever the main as a precondition depending on the memory
+ whenever the main has a precondition depending on the memory
model.
-* E-ACSL [2017/11/27] Restore behavior of option -e-acsl-valid broken
since Phosphorus (included).
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_stmt_contract.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_stmt_contract.c
index 69110b0e12a..f93322eba9c 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_stmt_contract.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_stmt_contract.c
@@ -13,27 +13,32 @@ int main(void)
(char *)"x == 1",8);
}
/*@ ensures x ≡ 2;
- ensures y ≡ 2; */
+ ensures y ≡ 2;
+ ensures x ≡ 2 ∧ y ≡ 2; */
{
+ int __gen_e_acsl_and;
x = 2;
__e_acsl_assert(x == 2,(char *)"Postcondition",(char *)"main",
(char *)"x == 2",11);
__e_acsl_assert(y == 2,(char *)"Postcondition",(char *)"main",
(char *)"y == 2",12);
+ if (x == 2) __gen_e_acsl_and = y == 2; else __gen_e_acsl_and = 0;
+ __e_acsl_assert(__gen_e_acsl_and,(char *)"Postcondition",(char *)"main",
+ (char *)"x == 2 && y == 2",13);
}
/*@ requires x ≡ 2; */
{
__e_acsl_assert(x == 2,(char *)"Precondition",(char *)"main",
- (char *)"x == 2",15);
+ (char *)"x == 2",17);
x ++;
}
/*@ requires x ≡ 3;
requires y ≡ 2; */
{
__e_acsl_assert(x == 3,(char *)"Precondition",(char *)"main",
- (char *)"x == 3",18);
+ (char *)"x == 3",20);
__e_acsl_assert(y == 2,(char *)"Precondition",(char *)"main",
- (char *)"y == 2",19);
+ (char *)"y == 2",21);
x += y;
}
/*@ behavior b1:
@@ -47,16 +52,16 @@ int main(void)
*/
{
__e_acsl_assert(x == 5,(char *)"Precondition",(char *)"main",
- (char *)"x == 5",23);
+ (char *)"x == 5",25);
__e_acsl_assert(x == 3L + y,(char *)"Precondition",(char *)"main",
- (char *)"x == 3 + y",26);
+ (char *)"x == 3 + y",28);
__e_acsl_assert(y == 2,(char *)"Precondition",(char *)"main",
- (char *)"y == 2",27);
+ (char *)"y == 2",29);
x = 3;
__e_acsl_assert(x == 3,(char *)"Postcondition",(char *)"main",
- (char *)"x == 3",24);
+ (char *)"x == 3",26);
__e_acsl_assert(x == y + 1L,(char *)"Postcondition",(char *)"main",
- (char *)"x == y + 1",28);
+ (char *)"x == y + 1",30);
}
/*@ behavior b1:
assumes x ≡ 1;
@@ -71,37 +76,37 @@ int main(void)
{
{
int __gen_e_acsl_implies;
- int __gen_e_acsl_and;
- int __gen_e_acsl_implies_2;
int __gen_e_acsl_and_2;
+ int __gen_e_acsl_implies_2;
+ int __gen_e_acsl_and_3;
int __gen_e_acsl_implies_3;
if (! (x == 1)) __gen_e_acsl_implies = 1;
else __gen_e_acsl_implies = x == 0;
__e_acsl_assert(__gen_e_acsl_implies,(char *)"Precondition",
- (char *)"main",(char *)"x == 1 ==> x == 0",33);
- if (x == 3) __gen_e_acsl_and = y == 2; else __gen_e_acsl_and = 0;
- if (! __gen_e_acsl_and) __gen_e_acsl_implies_2 = 1;
+ (char *)"main",(char *)"x == 1 ==> x == 0",35);
+ if (x == 3) __gen_e_acsl_and_2 = y == 2; else __gen_e_acsl_and_2 = 0;
+ if (! __gen_e_acsl_and_2) __gen_e_acsl_implies_2 = 1;
else __gen_e_acsl_implies_2 = x == 3;
__e_acsl_assert(__gen_e_acsl_implies_2,(char *)"Precondition",
(char *)"main",(char *)"x == 3 && y == 2 ==> x == 3",
- 37);
- if (x == 3) __gen_e_acsl_and_2 = y == 2; else __gen_e_acsl_and_2 = 0;
- if (! __gen_e_acsl_and_2) __gen_e_acsl_implies_3 = 1;
+ 39);
+ if (x == 3) __gen_e_acsl_and_3 = y == 2; else __gen_e_acsl_and_3 = 0;
+ if (! __gen_e_acsl_and_3) __gen_e_acsl_implies_3 = 1;
else __gen_e_acsl_implies_3 = x + (long)y == 5L;
__e_acsl_assert(__gen_e_acsl_implies_3,(char *)"Precondition",
(char *)"main",
- (char *)"x == 3 && y == 2 ==> x + y == 5",38);
+ (char *)"x == 3 && y == 2 ==> x + y == 5",40);
}
x += y;
}
/*@ requires x ≡ 5; */
{
__e_acsl_assert(x == 5,(char *)"Precondition",(char *)"main",
- (char *)"x == 5",41);
+ (char *)"x == 5",43);
/*@ requires y ≡ 2; */
{
__e_acsl_assert(y == 2,(char *)"Precondition",(char *)"main",
- (char *)"y == 2",42);
+ (char *)"y == 2",44);
x += y;
}
}
@@ -109,11 +114,11 @@ int main(void)
ensures x ≡ 7; */
{
__e_acsl_assert(x == 7,(char *)"Precondition",(char *)"main",
- (char *)"x == 7",45);
+ (char *)"x == 7",47);
__retres = 0;
goto return_label;
__e_acsl_assert(x == 7,(char *)"Postcondition",(char *)"main",
- (char *)"x == 7",46);
+ (char *)"x == 7",48);
}
return_label: return __retres;
}
diff --git a/src/plugins/e-acsl/tests/runtime/stmt_contract.i b/src/plugins/e-acsl/tests/runtime/stmt_contract.i
index 8634ee26980..3d105913ded 100644
--- a/src/plugins/e-acsl/tests/runtime/stmt_contract.i
+++ b/src/plugins/e-acsl/tests/runtime/stmt_contract.i
@@ -9,7 +9,9 @@ int main(void) {
x = 1;
// several ensures
/*@ ensures x == 2;
- @ ensures y == 2; */
+ @ ensures y == 2;
+ @ ensures x == 2 && y == 2; // generate local variables: see BTS #2339
+ @*/
x = 2;
// one requires
/*@ requires x == 2; */
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 6e8131899b5..f0365cb55e4 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -702,7 +702,10 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
~global_clear:false
Env.Before
in
- let post_block = Cil.transient_block post_block in
+ let post_block =
+ if post_block.blocals = [] then Cil.transient_block post_block
+ else post_block
+ in
Misc.mk_block prj new_stmt post_block, env
end else
stmt, env
--
GitLab