From 1beb1ffd8ad21aa64ae0053219c40e16350d6f50 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 27 Mar 2017 12:43:39 +0200
Subject: [PATCH] update oracles
---
.../e-acsl/tests/bts/oracle/gen_bts1307.c | 22 +--
.../e-acsl/tests/bts/oracle/gen_bts1478.c | 2 +-
.../runtime/oracle/gen_function_contract.c | 2 +-
.../tests/runtime/oracle/gen_linear_search.c | 127 +++++++++---------
.../tests/runtime/oracle/gen_stmt_contract.c | 43 +++---
5 files changed, 101 insertions(+), 95 deletions(-)
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
index 5717cea6648..caa221c7af4 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
@@ -135,14 +135,14 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
(void *)(& Mtmin_out));
__e_acsl_assert(__gen_e_acsl_valid_3,(char *)"Precondition",
(char *)"bar",(char *)"\\valid(Mtmin_out)",19);
- __gen_e_acsl_at_6 = Mwmin;
- __gen_e_acsl_at_5 = Mtmin_in;
- __gen_e_acsl_at_4 = Mwmin;
- __gen_e_acsl_at_3 = Mtmin_in;
- __gen_e_acsl_at_2 = Mtmin_in;
- __gen_e_acsl_at = Mtmin_out;
- bar(Mtmin_in,Mwmin,Mtmin_out);
}
+ __gen_e_acsl_at_6 = Mwmin;
+ __gen_e_acsl_at_5 = Mtmin_in;
+ __gen_e_acsl_at_4 = Mwmin;
+ __gen_e_acsl_at_3 = Mtmin_in;
+ __gen_e_acsl_at_2 = Mtmin_in;
+ __gen_e_acsl_at = Mtmin_out;
+ bar(Mtmin_in,Mwmin,Mtmin_out);
{
int __gen_e_acsl_valid_read;
int __gen_e_acsl_valid_read_2;
@@ -248,11 +248,11 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
(void *)(& Mtmax_out));
__e_acsl_assert(__gen_e_acsl_valid_3,(char *)"Precondition",
(char *)"foo",(char *)"\\valid(Mtmax_out)",7);
- __gen_e_acsl_at_3 = Mwmax;
- __gen_e_acsl_at_2 = Mtmax_in;
- __gen_e_acsl_at = Mtmax_out;
- foo(Mtmax_in,Mwmax,Mtmax_out);
}
+ __gen_e_acsl_at_3 = Mwmax;
+ __gen_e_acsl_at_2 = Mtmax_in;
+ __gen_e_acsl_at = Mtmax_out;
+ foo(Mtmax_in,Mwmax,Mtmax_out);
{
int __gen_e_acsl_valid_read;
int __gen_e_acsl_valid_read_2;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
index 6e3a6dfa88e..d7ada2c7115 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
@@ -36,8 +36,8 @@ void __gen_e_acsl_loop(void)
(char *)"\\valid(global_i_ptr)",10);
__e_acsl_assert(global_i_ptr == & global_i,(char *)"Precondition",
(char *)"loop",(char *)"global_i_ptr == &global_i",11);
- loop();
}
+ loop();
return;
}
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c
index 7b7b067ff37..d2f07efc1d2 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c
@@ -316,8 +316,8 @@ void __gen_e_acsl_k(void)
else __gen_e_acsl_implies_3 = X + (long)Y == 5L;
__e_acsl_assert(__gen_e_acsl_implies_3,(char *)"Precondition",
(char *)"k",(char *)"X == 3 && Y == 2 ==> X + Y == 5",43);
- k();
}
+ k();
return;
}
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c
index aad0f8d74ae..6fd208997af 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c
@@ -29,31 +29,34 @@ int search(int elt)
int k;
k = 0;
{
- int __gen_e_acsl_forall;
- int __gen_e_acsl_i;
- int __gen_e_acsl_and;
- __gen_e_acsl_forall = 1;
- __gen_e_acsl_i = 0;
- while (1) {
- if (__gen_e_acsl_i < k) ; else break;
- __e_acsl_assert(__gen_e_acsl_i < 10,(char *)"RTE",(char *)"search",
- (char *)"index_bound: __gen_e_acsl_i < 10",18);
- __e_acsl_assert(0 <= __gen_e_acsl_i,(char *)"RTE",(char *)"search",
- (char *)"index_bound: 0 <= __gen_e_acsl_i",18);
- if (A[__gen_e_acsl_i] < elt) ;
- else {
- __gen_e_acsl_forall = 0;
- goto e_acsl_end_loop1;
+ {
+ int __gen_e_acsl_forall;
+ int __gen_e_acsl_i;
+ int __gen_e_acsl_and;
+ __gen_e_acsl_forall = 1;
+ __gen_e_acsl_i = 0;
+ while (1) {
+ if (__gen_e_acsl_i < k) ; else break;
+ __e_acsl_assert(__gen_e_acsl_i < 10,(char *)"RTE",(char *)"search",
+ (char *)"index_bound: __gen_e_acsl_i < 10",18);
+ __e_acsl_assert(0 <= __gen_e_acsl_i,(char *)"RTE",(char *)"search",
+ (char *)"index_bound: 0 <= __gen_e_acsl_i",18);
+ if (A[__gen_e_acsl_i] < elt) ;
+ else {
+ __gen_e_acsl_forall = 0;
+ goto e_acsl_end_loop1;
+ }
+ __gen_e_acsl_i ++;
}
- __gen_e_acsl_i ++;
+ e_acsl_end_loop1: ;
+ __e_acsl_assert(__gen_e_acsl_forall,(char *)"Invariant",
+ (char *)"search",
+ (char *)"\\forall integer i; 0 <= i < k ==> A[i] < elt",
+ 18);
+ if (0 <= k) __gen_e_acsl_and = k <= 10; else __gen_e_acsl_and = 0;
+ __e_acsl_assert(__gen_e_acsl_and,(char *)"Invariant",(char *)"search",
+ (char *)"0 <= k <= 10",17);
}
- e_acsl_end_loop1: ;
- __e_acsl_assert(__gen_e_acsl_forall,(char *)"Invariant",(char *)"search",
- (char *)"\\forall integer i; 0 <= i < k ==> A[i] < elt",
- 18);
- if (0 <= k) __gen_e_acsl_and = k <= 10; else __gen_e_acsl_and = 0;
- __e_acsl_assert(__gen_e_acsl_and,(char *)"Invariant",(char *)"search",
- (char *)"0 <= k <= 10",17);
/*@ loop invariant 0 ≤ k ≤ 10;
loop invariant ∀ ℤ i; 0 ≤ i < k ⇒ A[i] < elt;
*/
@@ -174,50 +177,50 @@ int __gen_e_acsl_search(int elt)
(char *)"search",
(char *)"\\forall integer i; 0 <= i < 9 ==> A[i] <= A[i + 1]",
7);
- {
- int __gen_e_acsl_forall_2;
- int __gen_e_acsl_j_2;
- __gen_e_acsl_forall_2 = 1;
- __gen_e_acsl_j_2 = 0;
- while (1) {
- if (__gen_e_acsl_j_2 < 10) ; else break;
- __e_acsl_assert(__gen_e_acsl_j_2 < 10,(char *)"RTE",(char *)"search",
- (char *)"index_bound: __gen_e_acsl_j_2 < 10",12);
- __e_acsl_assert(0 <= __gen_e_acsl_j_2,(char *)"RTE",(char *)"search",
- (char *)"index_bound: 0 <= __gen_e_acsl_j_2",12);
- if (A[__gen_e_acsl_j_2] != elt) ;
- else {
- __gen_e_acsl_forall_2 = 0;
- goto e_acsl_end_loop5;
- }
- __gen_e_acsl_j_2 ++;
+ }
+ {
+ int __gen_e_acsl_forall_2;
+ int __gen_e_acsl_j_2;
+ __gen_e_acsl_forall_2 = 1;
+ __gen_e_acsl_j_2 = 0;
+ while (1) {
+ if (__gen_e_acsl_j_2 < 10) ; else break;
+ __e_acsl_assert(__gen_e_acsl_j_2 < 10,(char *)"RTE",(char *)"search",
+ (char *)"index_bound: __gen_e_acsl_j_2 < 10",12);
+ __e_acsl_assert(0 <= __gen_e_acsl_j_2,(char *)"RTE",(char *)"search",
+ (char *)"index_bound: 0 <= __gen_e_acsl_j_2",12);
+ if (A[__gen_e_acsl_j_2] != elt) ;
+ else {
+ __gen_e_acsl_forall_2 = 0;
+ goto e_acsl_end_loop5;
}
- e_acsl_end_loop5: ;
- __gen_e_acsl_at_2 = __gen_e_acsl_forall_2;
+ __gen_e_acsl_j_2 ++;
}
- {
- int __gen_e_acsl_exists;
- int __gen_e_acsl_j;
- __gen_e_acsl_exists = 0;
- __gen_e_acsl_j = 0;
- while (1) {
- if (__gen_e_acsl_j < 10) ; else break;
- __e_acsl_assert(__gen_e_acsl_j < 10,(char *)"RTE",(char *)"search",
- (char *)"index_bound: __gen_e_acsl_j < 10",9);
- __e_acsl_assert(0 <= __gen_e_acsl_j,(char *)"RTE",(char *)"search",
- (char *)"index_bound: 0 <= __gen_e_acsl_j",9);
- if (! (A[__gen_e_acsl_j] == elt)) ;
- else {
- __gen_e_acsl_exists = 1;
- goto e_acsl_end_loop4;
- }
- __gen_e_acsl_j ++;
+ e_acsl_end_loop5: ;
+ __gen_e_acsl_at_2 = __gen_e_acsl_forall_2;
+ }
+ {
+ int __gen_e_acsl_exists;
+ int __gen_e_acsl_j;
+ __gen_e_acsl_exists = 0;
+ __gen_e_acsl_j = 0;
+ while (1) {
+ if (__gen_e_acsl_j < 10) ; else break;
+ __e_acsl_assert(__gen_e_acsl_j < 10,(char *)"RTE",(char *)"search",
+ (char *)"index_bound: __gen_e_acsl_j < 10",9);
+ __e_acsl_assert(0 <= __gen_e_acsl_j,(char *)"RTE",(char *)"search",
+ (char *)"index_bound: 0 <= __gen_e_acsl_j",9);
+ if (! (A[__gen_e_acsl_j] == elt)) ;
+ else {
+ __gen_e_acsl_exists = 1;
+ goto e_acsl_end_loop4;
}
- e_acsl_end_loop4: ;
- __gen_e_acsl_at = __gen_e_acsl_exists;
+ __gen_e_acsl_j ++;
}
- __retres = search(elt);
+ e_acsl_end_loop4: ;
+ __gen_e_acsl_at = __gen_e_acsl_exists;
}
+ __retres = search(elt);
{
int __gen_e_acsl_implies;
int __gen_e_acsl_implies_2;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_stmt_contract.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_stmt_contract.c
index 876d034eec1..106da5a5841 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_stmt_contract.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_stmt_contract.c
@@ -68,26 +68,29 @@ int main(void)
requires x + y ≡ 5;
*/
{
- int __gen_e_acsl_implies;
- int __gen_e_acsl_and;
- int __gen_e_acsl_implies_2;
- int __gen_e_acsl_and_2;
- int __gen_e_acsl_implies_3;
- if (! (x == 1)) __gen_e_acsl_implies = 1;
- else __gen_e_acsl_implies = x == 0;
- __e_acsl_assert(__gen_e_acsl_implies,(char *)"Precondition",
- (char *)"main",(char *)"x == 1 ==> x == 0",33);
- if (x == 3) __gen_e_acsl_and = y == 2; else __gen_e_acsl_and = 0;
- if (! __gen_e_acsl_and) __gen_e_acsl_implies_2 = 1;
- else __gen_e_acsl_implies_2 = x == 3;
- __e_acsl_assert(__gen_e_acsl_implies_2,(char *)"Precondition",
- (char *)"main",(char *)"x == 3 && y == 2 ==> x == 3",37);
- if (x == 3) __gen_e_acsl_and_2 = y == 2; else __gen_e_acsl_and_2 = 0;
- if (! __gen_e_acsl_and_2) __gen_e_acsl_implies_3 = 1;
- else __gen_e_acsl_implies_3 = x + (long)y == 5L;
- __e_acsl_assert(__gen_e_acsl_implies_3,(char *)"Precondition",
- (char *)"main",(char *)"x == 3 && y == 2 ==> x + y == 5",
- 38);
+ {
+ int __gen_e_acsl_implies;
+ int __gen_e_acsl_and;
+ int __gen_e_acsl_implies_2;
+ int __gen_e_acsl_and_2;
+ int __gen_e_acsl_implies_3;
+ if (! (x == 1)) __gen_e_acsl_implies = 1;
+ else __gen_e_acsl_implies = x == 0;
+ __e_acsl_assert(__gen_e_acsl_implies,(char *)"Precondition",
+ (char *)"main",(char *)"x == 1 ==> x == 0",33);
+ if (x == 3) __gen_e_acsl_and = y == 2; else __gen_e_acsl_and = 0;
+ if (! __gen_e_acsl_and) __gen_e_acsl_implies_2 = 1;
+ else __gen_e_acsl_implies_2 = x == 3;
+ __e_acsl_assert(__gen_e_acsl_implies_2,(char *)"Precondition",
+ (char *)"main",(char *)"x == 3 && y == 2 ==> x == 3",
+ 37);
+ if (x == 3) __gen_e_acsl_and_2 = y == 2; else __gen_e_acsl_and_2 = 0;
+ if (! __gen_e_acsl_and_2) __gen_e_acsl_implies_3 = 1;
+ else __gen_e_acsl_implies_3 = x + (long)y == 5L;
+ __e_acsl_assert(__gen_e_acsl_implies_3,(char *)"Precondition",
+ (char *)"main",
+ (char *)"x == 3 && y == 2 ==> x + y == 5",38);
+ }
x += y;
}
/*@ requires x ≡ 5; */
--
GitLab