From 0c5f590b3990ff078304255aa250301386588927 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Tue, 27 Jan 2015 10:11:17 +0100
Subject: [PATCH] [tests] fix oracles
---
src/plugins/e-acsl/tests/e-acsl-runtime/bts1478.c | 3 ++-
.../tests/e-acsl-runtime/oracle/bts1478.1.res.oracle | 4 ++--
.../tests/e-acsl-runtime/oracle/bts1478.res.oracle | 4 ++--
.../e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c | 10 ++++++----
.../e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c | 10 ++++++----
5 files changed, 18 insertions(+), 13 deletions(-)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1478.c b/src/plugins/e-acsl/tests/e-acsl-runtime/bts1478.c
index f36822ef19e..5270202b6e3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1478.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/bts1478.c
@@ -4,8 +4,9 @@
EXECNOW: LOG gen_bts14782.c BIN gen_bts14782.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1478.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts14782.c > /dev/null && ./gcc_test.sh bts14782
*/
-int global_i = 0;
+int global_i;
int* global_i_ptr = &global_i;
+int global_i = 0;
/*@ requires global_i == 0;
requires \valid(global_i_ptr);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.res.oracle
index 63841d478c4..646927eca20 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.res.oracle
@@ -22,9 +22,9 @@
global_i_ptr ∈ {{ &global_i }}
[value] using specification for function __store_block
[value] using specification for function __full_init
-tests/e-acsl-runtime/bts1478.c:10:[value] Function __e_acsl_loop: precondition got status valid.
tests/e-acsl-runtime/bts1478.c:11:[value] Function __e_acsl_loop: precondition got status valid.
tests/e-acsl-runtime/bts1478.c:12:[value] Function __e_acsl_loop: precondition got status valid.
+tests/e-acsl-runtime/bts1478.c:13:[value] Function __e_acsl_loop: precondition got status valid.
[value] using specification for function __gmpz_init_set_si
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_cmp
@@ -36,9 +36,9 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] using specification for function __gmpz_clear
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
-tests/e-acsl-runtime/bts1478.c:10:[value] Function loop: precondition got status valid.
tests/e-acsl-runtime/bts1478.c:11:[value] Function loop: precondition got status valid.
tests/e-acsl-runtime/bts1478.c:12:[value] Function loop: precondition got status valid.
+tests/e-acsl-runtime/bts1478.c:13:[value] Function loop: precondition got status valid.
[value] using specification for function __delete_block
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.res.oracle
index d8cdc32d4bf..819a1984571 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.res.oracle
@@ -22,16 +22,16 @@
global_i_ptr ∈ {{ &global_i }}
[value] using specification for function __store_block
[value] using specification for function __full_init
-tests/e-acsl-runtime/bts1478.c:10:[value] Function __e_acsl_loop: precondition got status valid.
tests/e-acsl-runtime/bts1478.c:11:[value] Function __e_acsl_loop: precondition got status valid.
tests/e-acsl-runtime/bts1478.c:12:[value] Function __e_acsl_loop: precondition got status valid.
+tests/e-acsl-runtime/bts1478.c:13:[value] Function __e_acsl_loop: precondition got status valid.
[value] using specification for function e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] using specification for function __valid
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-tests/e-acsl-runtime/bts1478.c:10:[value] Function loop: precondition got status valid.
tests/e-acsl-runtime/bts1478.c:11:[value] Function loop: precondition got status valid.
tests/e-acsl-runtime/bts1478.c:12:[value] Function loop: precondition got status valid.
+tests/e-acsl-runtime/bts1478.c:13:[value] Function loop: precondition got status valid.
[value] using specification for function __delete_block
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c
index ce1a2038dc8..291c1d24a82 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c
@@ -62,8 +62,10 @@ extern size_t __memory_size;
predicate diffSize{L1, L2}(ℤ i) =
\at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
*/
-int global_i = 0;
+int global_i;
+
int *global_i_ptr = & global_i;
+int global_i = 0;
/*@ requires global_i ≡ 0;
requires \valid(global_i_ptr);
requires global_i_ptr ≡ &global_i;
@@ -82,12 +84,12 @@ void __e_acsl_loop(void)
{
int __e_acsl_valid;
e_acsl_assert(global_i == 0,(char *)"Precondition",(char *)"loop",
- (char *)"global_i == 0",10);
+ (char *)"global_i == 0",11);
__e_acsl_valid = __valid((void *)global_i_ptr,sizeof(int));
e_acsl_assert(__e_acsl_valid,(char *)"Precondition",(char *)"loop",
- (char *)"\\valid(global_i_ptr)",11);
+ (char *)"\\valid(global_i_ptr)",12);
e_acsl_assert(global_i_ptr == & global_i,(char *)"Precondition",
- (char *)"loop",(char *)"global_i_ptr == &global_i",12);
+ (char *)"loop",(char *)"global_i_ptr == &global_i",13);
loop();
}
return;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c
index ef98386277d..5bfa785f3bf 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c
@@ -85,8 +85,10 @@ extern size_t __memory_size;
predicate diffSize{L1, L2}(ℤ i) =
\at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
*/
-int global_i = 0;
+int global_i;
+
int *global_i_ptr = & global_i;
+int global_i = 0;
/*@ requires global_i ≡ 0;
requires \valid(global_i_ptr);
requires global_i_ptr ≡ &global_i;
@@ -112,12 +114,12 @@ void __e_acsl_loop(void)
__e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__e_acsl_global_i),
(__mpz_struct const *)(__e_acsl));
e_acsl_assert(__e_acsl_eq == 0,(char *)"Precondition",(char *)"loop",
- (char *)"global_i == 0",10);
+ (char *)"global_i == 0",11);
__e_acsl_valid = __valid((void *)global_i_ptr,sizeof(int));
e_acsl_assert(__e_acsl_valid,(char *)"Precondition",(char *)"loop",
- (char *)"\\valid(global_i_ptr)",11);
+ (char *)"\\valid(global_i_ptr)",12);
e_acsl_assert(global_i_ptr == & global_i,(char *)"Precondition",
- (char *)"loop",(char *)"global_i_ptr == &global_i",12);
+ (char *)"loop",(char *)"global_i_ptr == &global_i",13);
__gmpz_clear(__e_acsl_global_i);
__gmpz_clear(__e_acsl);
loop();
--
GitLab