From 9f0b656ae6d9988fd1cf2c46a2398f1cb9fb288c Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 25 Apr 2013 05:34:21 +0000
Subject: [PATCH] [E-ACSL] dataflow optimisation: ignore duplicated function
contract
---
src/plugins/e-acsl/TODO | 5 ++---
src/plugins/e-acsl/pre_analysis.ml | 2 +-
.../tests/e-acsl-runtime/oracle/bts1324.1.res.oracle | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c | 6 +-----
.../e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c | 6 +-----
.../e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c | 8 --------
.../e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c | 8 --------
.../e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c | 1 -
.../e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c | 1 -
.../tests/e-acsl-runtime/oracle/gen_valid_in_contract.c | 6 +-----
.../tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c | 6 +-----
.../e-acsl-runtime/oracle/valid_in_contract.1.res.oracle | 2 +-
.../e-acsl-runtime/oracle/valid_in_contract.res.oracle | 2 +-
14 files changed, 11 insertions(+), 46 deletions(-)
diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index 505eb087adc..c0b61d74d73 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -25,14 +25,13 @@
(voir test result.i, cas -e-acsl-gmp-only)
- générer les delete des globals dans une fonction séparée, comme pour les init.
- variadic functions are not yet duplicated
-- generate guard for \offset & co (\offset(p) must ensures that p is valid)
-- improve computation of the initial state of the dataflow analysis
+- generate guard for \offset, \block_length and \base_addr
+ (\offset(p) must ensures that p is valid)
- don't generate code for properties with status valid_under_hyp when we know
that the hyp will be generated
- use value analysis whenever possible instead of our own imprecise analysis
- use checked assigns whenever possible in the analysis
checked property = valid property or property for which code will be generated
-- fix \offset, \block_length and \base_addr
- RTE avec du code GMP
##############
diff --git a/src/plugins/e-acsl/pre_analysis.ml b/src/plugins/e-acsl/pre_analysis.ml
index 8a01e0e4370..b0e13ff81d6 100644
--- a/src/plugins/e-acsl/pre_analysis.ml
+++ b/src/plugins/e-acsl/pre_analysis.ml
@@ -285,7 +285,7 @@ module rec Transfer
(fun state ->
let state = Env.default_varinfos state in
let state =
- if is_first || is_last then
+ if (is_first || is_last) && Misc.is_generated_kf kf then
Annotations.fold_behaviors
(fun _ bhv s ->
let handle_annot test f s =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle
index 81e304bee51..701e70d1ec9 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle
@@ -48,10 +48,10 @@ share/e-acsl/e_acsl_gmp.h:185:[value] Function __gmpz_get_ui: precondition got s
tests/e-acsl-runtime/bts1324.i:8:[kernel] warning: out of bounds read. assert \valid_read(t+__e_acsl_2);
tests/e-acsl-runtime/bts1324.i:8:[kernel] warning: out of bounds read. assert \valid_read(t+__e_acsl_i_2);
tests/e-acsl-runtime/bts1324.i:15:[value] entering loop for the first time
-[value] using specification for function __delete_block
tests/e-acsl-runtime/bts1324.i:9:[value] Function sorted, behavior yes: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
[value] using specification for function e_acsl_assert
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+[value] using specification for function __delete_block
tests/e-acsl-runtime/bts1324.i:9:[value] Function __e_acsl_sorted, behavior yes: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/bts1324.i:25:[value] Assertion got status valid.
[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle
index a4a9ff1b0db..3f65dd22867 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle
@@ -22,9 +22,9 @@
[value] using specification for function e_acsl_assert
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
tests/e-acsl-runtime/bts1324.i:15:[value] entering loop for the first time
-[value] using specification for function __delete_block
tests/e-acsl-runtime/bts1324.i:9:[value] Function sorted, behavior yes: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
+[value] using specification for function __delete_block
tests/e-acsl-runtime/bts1324.i:9:[value] Function __e_acsl_sorted, behavior yes: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/bts1324.i:25:[value] Assertion got status valid.
[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c
index 5d1ddfc9fb5..1421ddbabe9 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c
@@ -64,8 +64,6 @@ int sorted(int *t, int n)
{
int __retres;
int b;
- __store_block((void *)(& t),4U);
- __full_init((void *)(& t));
b = 1;
if (n <= 1) {
__retres = 1;
@@ -80,9 +78,7 @@ int sorted(int *t, int n)
b ++;
}
__retres = 1;
- return_label: /* internal */
- __delete_block((void *)(& t));
- return __retres;
+ return_label: /* internal */ return __retres;
}
/*@ behavior yes:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c
index 2b3a02ae35b..990bc56bd1b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c
@@ -119,8 +119,6 @@ int sorted(int *t, int n)
{
int __retres;
int b;
- __store_block((void *)(& t),4U);
- __full_init((void *)(& t));
b = 1;
if (n <= 1) {
__retres = 1;
@@ -135,9 +133,7 @@ int sorted(int *t, int n)
b ++;
}
__retres = 1;
- return_label: /* internal */
- __delete_block((void *)(& t));
- return __retres;
+ return_label: /* internal */ return __retres;
}
/*@ behavior yes:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c
index 6b73631e322..eed220126b0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c
@@ -74,29 +74,21 @@ void *memchr(void const *buf, int c, size_t n)
void *__retres;
int i;
char *s;
- __store_block((void *)(& s),4U);
- __store_block((void *)(& __retres),4U);
__store_block((void *)(& buf),4U);
__full_init((void *)(& buf));
- __full_init((void *)(& s));
s = (char *)buf;
i = 0;
while ((size_t)i < n) {
if ((int)*s == c) {
- __full_init((void *)(& __retres));
__retres = (void *)s;
goto return_label;
}
- __full_init((void *)(& s));
s ++;
i ++;
}
- __full_init((void *)(& __retres));
__retres = (void *)0;
return_label: /* internal */
__delete_block((void *)(& buf));
- __delete_block((void *)(& s));
- __delete_block((void *)(& __retres));
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c
index b20cf19b813..29aaa98132f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c
@@ -129,29 +129,21 @@ void *memchr(void const *buf, int c, size_t n)
void *__retres;
int i;
char *s;
- __store_block((void *)(& s),4U);
- __store_block((void *)(& __retres),4U);
__store_block((void *)(& buf),4U);
__full_init((void *)(& buf));
- __full_init((void *)(& s));
s = (char *)buf;
i = 0;
while ((size_t)i < n) {
if ((int)*s == c) {
- __full_init((void *)(& __retres));
__retres = (void *)s;
goto return_label;
}
- __full_init((void *)(& s));
s ++;
i ++;
}
- __full_init((void *)(& __retres));
__retres = (void *)0;
return_label: /* internal */
__delete_block((void *)(& buf));
- __delete_block((void *)(& s));
- __delete_block((void *)(& __retres));
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
index 3ec6a39d6ed..aaf10d25d9a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
@@ -186,7 +186,6 @@ int *f(int *x)
e_acsl_assert(! __e_acsl_and,(char *)"Assertion",(char *)"f",
(char *)"!\\valid(y)",19);
}
- __full_init((void *)(& y));
y = x;
/*@ assert \valid(x); */
{
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c
index 3ec6a39d6ed..aaf10d25d9a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c
@@ -186,7 +186,6 @@ int *f(int *x)
e_acsl_assert(! __e_acsl_and,(char *)"Assertion",(char *)"f",
(char *)"!\\valid(y)",19);
}
- __full_init((void *)(& y));
y = x;
/*@ assert \valid(x); */
{
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
index 359dfcc485c..9f2f6dba7d3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
@@ -79,8 +79,6 @@ predicate diffSize{L1, L2}(ℤ i) =
struct list *f(struct list *l)
{
struct list *__retres;
- __store_block((void *)(& l),4U);
- __full_init((void *)(& l));
if (l == (void *)0) {
__retres = l;
goto return_label;
@@ -90,9 +88,7 @@ struct list *f(struct list *l)
goto return_label;
}
__retres = (struct list *)((void *)0);
- return_label: /* internal */
- __delete_block((void *)(& l));
- return __retres;
+ return_label: /* internal */ return __retres;
}
/*@ behavior B1:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c
index 359dfcc485c..9f2f6dba7d3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c
@@ -79,8 +79,6 @@ predicate diffSize{L1, L2}(ℤ i) =
struct list *f(struct list *l)
{
struct list *__retres;
- __store_block((void *)(& l),4U);
- __full_init((void *)(& l));
if (l == (void *)0) {
__retres = l;
goto return_label;
@@ -90,9 +88,7 @@ struct list *f(struct list *l)
goto return_label;
}
__retres = (struct list *)((void *)0);
- return_label: /* internal */
- __delete_block((void *)(& l));
- return __retres;
+ return_label: /* internal */ return __retres;
}
/*@ behavior B1:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle
index 4dc384ce71d..23998488d26 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle
@@ -27,10 +27,10 @@ share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status
tests/e-acsl-runtime/valid_in_contract.c:21:[kernel] warning: out of bounds read. assert \valid_read(&l->next);
tests/e-acsl-runtime/valid_in_contract.c:21:[value] all evaluations are invalid for function call argument
(void *)l->next
-[value] using specification for function __delete_block
tests/e-acsl-runtime/valid_in_contract.c:18:[value] Function f, behavior B1: postcondition got status valid.
tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function f, behavior B2: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
+[value] using specification for function __delete_block
tests/e-acsl-runtime/valid_in_contract.c:18:[value] Function __e_acsl_f, behavior B1: postcondition got status valid.
tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function __e_acsl_f, behavior B2: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle
index 4dc384ce71d..23998488d26 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle
@@ -27,10 +27,10 @@ share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status
tests/e-acsl-runtime/valid_in_contract.c:21:[kernel] warning: out of bounds read. assert \valid_read(&l->next);
tests/e-acsl-runtime/valid_in_contract.c:21:[value] all evaluations are invalid for function call argument
(void *)l->next
-[value] using specification for function __delete_block
tests/e-acsl-runtime/valid_in_contract.c:18:[value] Function f, behavior B1: postcondition got status valid.
tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function f, behavior B2: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
+[value] using specification for function __delete_block
tests/e-acsl-runtime/valid_in_contract.c:18:[value] Function __e_acsl_f, behavior B1: postcondition got status valid.
tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function __e_acsl_f, behavior B2: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
--
GitLab