From 626669682a5fdc1f1bc61f908619f17de13dc86f Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Mon, 22 May 2017 09:00:57 +0000
Subject: [PATCH] Bugfix for t_scope testcase
---
src/plugins/e-acsl/.gitignore | 2 ++
src/plugins/e-acsl/tests/temporal/oracle/gen_t_scope.c | 6 ++----
src/plugins/e-acsl/tests/temporal/oracle/t_scope.res.oracle | 5 ++++-
src/plugins/e-acsl/tests/temporal/t_scope.c | 2 +-
4 files changed, 9 insertions(+), 6 deletions(-)
diff --git a/src/plugins/e-acsl/.gitignore b/src/plugins/e-acsl/.gitignore
index 961b1be3713..a76fdee561c 100644
--- a/src/plugins/e-acsl/.gitignore
+++ b/src/plugins/e-acsl/.gitignore
@@ -56,6 +56,7 @@
/tests/test_config
/tests/runtime/*.cm*
/tests/runtime/result/*
+/tests/temporal/result/*
/tests/no-main/result/*
/tests/full-mmodel/result/*
/tests/bts/result/*
@@ -79,3 +80,4 @@ lib/libeacsl-rtl-bittree.a
lib/libeacsl-rtl-segment.a
lib/libeacsl-rtl-bittree-dbg.a
lib/libeacsl-rtl-segment-dbg.a
+tests/csrv14/*
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_scope.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_scope.c
index c1e706f8928..bd10ab43639 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_scope.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_scope.c
@@ -98,11 +98,8 @@ int main(void)
}
else __gen_e_acsl_and_4 = 0;
__e_acsl_assert(! __gen_e_acsl_and_4,(char *)"Assertion",
- (char *)"main",(char *)"!\\valid(q)",23);
+ (char *)"main",(char *)"!\\valid(q)",24);
}
- /*@ assert Value: dangling_pointer: ¬\dangling(&q); */
- __e_acsl_initialize((void *)q,sizeof(int));
- *q = 1;
/*@ assert \valid(&j); */
{
int __gen_e_acsl_valid_5;
@@ -131,6 +128,7 @@ int main(void)
sizeof(int *));
if (__gen_e_acsl_initialized_5) {
int __gen_e_acsl_valid_6;
+ /*@ assert Value: dangling_pointer: ¬\dangling(&p); */
__gen_e_acsl_valid_6 = __e_acsl_valid((void *)p,sizeof(int),
(void *)p,(void *)(& p));
__gen_e_acsl_and_5 = __gen_e_acsl_valid_6;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_scope.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_scope.res.oracle
index 5b5f54b8ce5..6d86bdfbac7 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_scope.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_scope.res.oracle
@@ -2,4 +2,7 @@
[e-acsl] translation done in project "e-acsl".
tests/temporal/t_scope.c:10:[value] warning: locals {i} escaping the scope of a block of main through p
tests/temporal/t_scope.c:10:[value] warning: locals {i} escaping the scope of a block of main through q
-[scope:rm_asserts] removing 2 assertion(s)
+tests/temporal/t_scope.c:19:[value] warning: locals {j} escaping the scope of a block of main through p
+tests/temporal/t_scope.c:33:[value] warning: locals {a} escaping the scope of a block of main through p
+tests/temporal/t_scope.c:33:[value] warning: locals {a} escaping the scope of a block of main through q
+[scope:rm_asserts] removing 1 assertion(s)
diff --git a/src/plugins/e-acsl/tests/temporal/t_scope.c b/src/plugins/e-acsl/tests/temporal/t_scope.c
index 14435dc27e6..d023e0fb497 100644
--- a/src/plugins/e-acsl/tests/temporal/t_scope.c
+++ b/src/plugins/e-acsl/tests/temporal/t_scope.c
@@ -20,8 +20,8 @@ int main() {
p = &j;
/*@assert \valid(p); */
*p = 1;
+ /* `q` now may point to `j`, bit not necessarily */
/*@assert ! \valid(q); */
- *q = 1;
/*@assert \valid(&j); */
}
--
GitLab