Skip to content
Snippets Groups Projects
Commit 1beb1ffd authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

update oracles

parent 6f0bf770
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
+ 11
− 11
View file @ 1beb1ffd
......@@ -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;
......
src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
+ 1
− 1
View file @ 1beb1ffd
......@@ -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;
}
......
src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c
+ 1
− 1
View file @ 1beb1ffd
......@@ -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;
}
......
src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c
+ 65
− 62
View file @ 1beb1ffd
......@@ -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;
......
src/plugins/e-acsl/tests/runtime/oracle/gen_stmt_contract.c
+ 23
− 20
View file @ 1beb1ffd
......@@ -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; */
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment