From 4555659e60ae99a6ff6345249faf0e342f6c96d4 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 6 Nov 2015 19:09:13 +0100
Subject: [PATCH] [tests] update tests wrt kernel changes
---
src/plugins/e-acsl/tests/e-acsl-runtime/linear_search.i | 2 +-
.../tests/e-acsl-runtime/oracle/gen_valid_in_contract.c | 8 ++++----
.../tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c | 8 ++++----
.../e-acsl-runtime/oracle/linear_search.0.res.oracle | 6 ++++--
.../e-acsl-runtime/oracle/linear_search.1.res.oracle | 6 ++++--
5 files changed, 17 insertions(+), 13 deletions(-)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/linear_search.i b/src/plugins/e-acsl/tests/e-acsl-runtime/linear_search.i
index 4f72855791d..f0324f6405d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/linear_search.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/linear_search.i
@@ -1,5 +1,5 @@
/* run.config
- COMMENT: linear search (example of the SAC'13 article)
+ COMMENT: linear search (example from the SAC'13 article)
EXECNOW: LOG gen_linear_search.c BIN gen_linear_search.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/linear_search.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_linear_search.c > /dev/null && ./gcc_runtime.sh linear_search
EXECNOW: LOG gen_linear_search2.c BIN gen_linear_search2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/linear_search.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_linear_search2.c > /dev/null && ./gcc_runtime.sh linear_search2
*/
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 45a24b77ddd..6b59fc96e3c 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
@@ -98,18 +98,18 @@ struct list *f(struct list *l)
struct list *__retres;
__store_block((void *)(& __retres),4U);
__store_block((void *)(& l),4U);
- if (l == (void *)0) {
+ if (l == (struct list *)0) {
__full_init((void *)(& __retres));
__retres = l;
goto return_label;
}
- if (l->next == (void *)0) {
+ if (l->next == (struct list *)0) {
__full_init((void *)(& __retres));
__retres = l;
goto return_label;
}
__full_init((void *)(& __retres));
- __retres = (struct list *)((void *)0);
+ __retres = (struct list *)0;
return_label:
__delete_block((void *)(& l));
__delete_block((void *)(& __retres));
@@ -187,7 +187,7 @@ struct list *__e_acsl_f(struct list *l)
int main(void)
{
int __retres;
- __e_acsl_f((struct list *)((void *)0));
+ __e_acsl_f((struct list *)0);
__retres = 0;
__e_acsl_memory_clean();
return __retres;
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 45a24b77ddd..6b59fc96e3c 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
@@ -98,18 +98,18 @@ struct list *f(struct list *l)
struct list *__retres;
__store_block((void *)(& __retres),4U);
__store_block((void *)(& l),4U);
- if (l == (void *)0) {
+ if (l == (struct list *)0) {
__full_init((void *)(& __retres));
__retres = l;
goto return_label;
}
- if (l->next == (void *)0) {
+ if (l->next == (struct list *)0) {
__full_init((void *)(& __retres));
__retres = l;
goto return_label;
}
__full_init((void *)(& __retres));
- __retres = (struct list *)((void *)0);
+ __retres = (struct list *)0;
return_label:
__delete_block((void *)(& l));
__delete_block((void *)(& __retres));
@@ -187,7 +187,7 @@ struct list *__e_acsl_f(struct list *l)
int main(void)
{
int __retres;
- __e_acsl_f((struct list *)((void *)0));
+ __e_acsl_f((struct list *)0);
__retres = 0;
__e_acsl_memory_clean();
return __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.0.res.oracle
index 6000f8fb4f8..b3277552b85 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.0.res.oracle
@@ -25,8 +25,10 @@ tests/e-acsl-runtime/linear_search.i:19:[value] Loop invariant got status valid.
tests/e-acsl-runtime/linear_search.i:20:[value] Loop invariant got status unknown.
tests/e-acsl-runtime/linear_search.i:21:[value] entering loop for the first time
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status invalid.
-tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/linear_search.i:12:[value] Function __e_acsl_search, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/linear_search.i:15:[value] Function __e_acsl_search, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/linear_search.i:33:[value] Assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
index ed5739d6aa1..d769c2b730b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
@@ -47,8 +47,10 @@ tests/e-acsl-runtime/linear_search.i:19:[value] Loop invariant got status valid.
tests/e-acsl-runtime/linear_search.i:20:[value] Loop invariant got status unknown.
tests/e-acsl-runtime/linear_search.i:21:[value] entering loop for the first time
tests/e-acsl-runtime/linear_search.i:20:[kernel] warning: accessing out of bounds index [0..4294967295]. assert __e_acsl_i_4 < 10;
-tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/linear_search.i:12:[value] Function __e_acsl_search, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/linear_search.i:15:[value] Function __e_acsl_search, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/linear_search.i:33:[value] Assertion got status unknown.
--
GitLab