From 331cfad5b2697aae484b185ce10384e3e24f5a0b Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Tue, 8 Dec 2015 13:23:58 +0100
Subject: [PATCH] Update several test oracles as per Frama-C code generation
changes.
---
src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c | 4 ++--
src/plugins/e-acsl/tests/bts/oracle/gen_bts13992.c | 4 ++--
.../e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c | 2 +-
.../tests/e-acsl-runtime/oracle/linear_search.0.res.oracle | 5 ++---
.../tests/e-acsl-runtime/oracle/linear_search.1.res.oracle | 4 ++--
.../e-acsl/tests/e-acsl-runtime/oracle/loop.1.res.oracle | 2 +-
7 files changed, 11 insertions(+), 12 deletions(-)
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
index 871363e9725..11363caf14f 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
@@ -8,8 +8,8 @@ typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
typedef unsigned int size_t;
struct spongeStateStruct {
- unsigned char __attribute__((__aligned__(32))) state[200] ;
- unsigned char __attribute__((__aligned__(32))) dataQueue[192] ;
+ unsigned char __attribute__((__aligned__(32))) state[1600 / 8] ;
+ unsigned char __attribute__((__aligned__(32))) dataQueue[1536 / 8] ;
unsigned int bitsInQueue ;
} __attribute__((__aligned__(32)));
typedef struct spongeStateStruct spongeState;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13992.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13992.c
index a348cbfc041..85b487196c3 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13992.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13992.c
@@ -8,8 +8,8 @@ typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
typedef unsigned int size_t;
struct spongeStateStruct {
- unsigned char __attribute__((__aligned__(32))) state[200] ;
- unsigned char __attribute__((__aligned__(32))) dataQueue[192] ;
+ unsigned char __attribute__((__aligned__(32))) state[1600 / 8] ;
+ unsigned char __attribute__((__aligned__(32))) dataQueue[1536 / 8] ;
unsigned int bitsInQueue ;
} __attribute__((__aligned__(32)));
typedef struct spongeStateStruct spongeState;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c
index a6fe60a1e27..b012a7b28ff 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c
@@ -150,7 +150,7 @@ int main(void)
struct list *l;
__store_block((void *)(& l),4U);
__full_init((void *)(& l));
- l = (struct list *)((void *)0);
+ l = (struct list *)0;
__full_init((void *)(& l));
l = add(l,4);
__full_init((void *)(& l));
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c
index a6fe60a1e27..b012a7b28ff 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c
@@ -150,7 +150,7 @@ int main(void)
struct list *l;
__store_block((void *)(& l),4U);
__full_init((void *)(& l));
- l = (struct list *)((void *)0);
+ l = (struct list *)0;
__full_init((void *)(& l));
l = add(l,4);
__full_init((void *)(& l));
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 b3277552b85..bc5af2b6f63 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
@@ -24,11 +24,10 @@ tests/e-acsl-runtime/linear_search.i:20:[value] entering loop for the first time
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 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:12:[value] Function search, behavior 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: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: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 d769c2b730b..e143e1fd124 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,10 +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 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:12:[value] Function search, behavior 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: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: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/loop.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.1.res.oracle
index 71aa24d07a4..fd67dfecc92 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.1.res.oracle
@@ -18,8 +18,8 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition g
[value] using specification for function __gmpz_clear
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: 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 invalid.
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status invalid.
tests/e-acsl-runtime/loop.i:10:[value] Loop invariant got status valid.
tests/e-acsl-runtime/loop.i:17:[value] Loop invariant got status valid.
[value] using specification for function __gmpz_init
--
GitLab