From 29bd6ccb10ddf39e79584c4b7c8ff40388f619d5 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 21 Jun 2013 06:55:12 +0000
Subject: [PATCH] [E-ACSL] update oracles according to printer changes
---
.../tests/e-acsl-runtime/oracle/gen_bts1324.c | 4 ++--
.../tests/e-acsl-runtime/oracle/gen_bts13242.c | 4 ++--
.../tests/e-acsl-runtime/oracle/gen_bts1390.c | 8 ++++----
.../tests/e-acsl-runtime/oracle/gen_bts13902.c | 8 ++++----
.../e-acsl-runtime/oracle/gen_labeled_stmt.c | 2 +-
.../e-acsl-runtime/oracle/gen_labeled_stmt2.c | 2 +-
.../e-acsl-runtime/oracle/gen_linear_search.c | 8 ++++----
.../e-acsl-runtime/oracle/gen_linear_search2.c | 8 ++++----
.../tests/e-acsl-runtime/oracle/gen_longlong.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_longlong2.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_quantif.c | 16 ++++++++--------
.../tests/e-acsl-runtime/oracle/gen_quantif2.c | 16 ++++++++--------
.../oracle/gen_valid_in_contract.c | 2 +-
.../oracle/gen_valid_in_contract2.c | 2 +-
14 files changed, 42 insertions(+), 42 deletions(-)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c
index f1a29589830..21f967fb66d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c
@@ -75,7 +75,7 @@ int sorted(int *t, int n)
b ++;
}
__retres = 1;
- return_label: /* internal */ return __retres;
+ return_label: return __retres;
}
/*@ behavior yes:
@@ -115,7 +115,7 @@ int __e_acsl_sorted(int *t, int n)
}
__e_acsl_i ++;
}
- e_acsl_end_loop1: /* internal */ ;
+ e_acsl_end_loop1: ;
__e_acsl_at = __e_acsl_forall;
}
__retres = sorted(t,n);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c
index 1dd1c9b1d48..a74d06267f8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c
@@ -130,7 +130,7 @@ int sorted(int *t, int n)
b ++;
}
__retres = 1;
- return_label: /* internal */ return __retres;
+ return_label: return __retres;
}
/*@ behavior yes:
@@ -211,7 +211,7 @@ int __e_acsl_sorted(int *t, int n)
__gmpz_clear(__e_acsl_add_2);
}
}
- e_acsl_end_loop1: /* internal */ ;
+ e_acsl_end_loop1: ;
__e_acsl_at = __e_acsl_forall;
__gmpz_clear(__e_acsl_i);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c
index c763e99a72b..2ab5365f21a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c
@@ -92,7 +92,7 @@ void *memchr(void const *buf, int c, size_t n)
}
__full_init((void *)(& __retres));
__retres = (void *)0;
- return_label: /* internal */
+ return_label:
__delete_block((void *)(& buf));
__delete_block((void *)(& s));
__delete_block((void *)(& __retres));
@@ -141,7 +141,7 @@ void *__e_acsl_memchr(void const *buf, int c, size_t n)
}
__e_acsl_k ++;
}
- e_acsl_end_loop3: /* internal */ ;
+ e_acsl_end_loop3: ;
__e_acsl_at_4 = __e_acsl_forall_2;
}
__e_acsl_at_3 = c;
@@ -169,7 +169,7 @@ void *__e_acsl_memchr(void const *buf, int c, size_t n)
}
__e_acsl_i ++;
}
- e_acsl_end_loop1: /* internal */ ;
+ e_acsl_end_loop1: ;
__e_acsl_at = __e_acsl_exists;
}
__retres = memchr(buf,c,n);
@@ -204,7 +204,7 @@ void *__e_acsl_memchr(void const *buf, int c, size_t n)
}
__e_acsl_j ++;
}
- e_acsl_end_loop2: /* internal */ ;
+ e_acsl_end_loop2: ;
__e_acsl_implies = __e_acsl_forall;
}
e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",(char *)"memchr",
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c
index 28e7db88f8c..5d1e68b65db 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c
@@ -147,7 +147,7 @@ void *memchr(void const *buf, int c, size_t n)
}
__full_init((void *)(& __retres));
__retres = (void *)0;
- return_label: /* internal */
+ return_label:
__delete_block((void *)(& buf));
__delete_block((void *)(& s));
__delete_block((void *)(& __retres));
@@ -226,7 +226,7 @@ void *__e_acsl_memchr(void const *buf, int c, size_t n)
__gmpz_clear(__e_acsl_add_3);
}
}
- e_acsl_end_loop3: /* internal */ ;
+ e_acsl_end_loop3: ;
__e_acsl_at_4 = __e_acsl_forall_2;
__gmpz_clear(__e_acsl_k);
}
@@ -285,7 +285,7 @@ void *__e_acsl_memchr(void const *buf, int c, size_t n)
__gmpz_clear(__e_acsl_add);
}
}
- e_acsl_end_loop1: /* internal */ ;
+ e_acsl_end_loop1: ;
__e_acsl_at = __e_acsl_exists;
__gmpz_clear(__e_acsl_i);
}
@@ -348,7 +348,7 @@ void *__e_acsl_memchr(void const *buf, int c, size_t n)
__gmpz_clear(__e_acsl_add_2);
}
}
- e_acsl_end_loop2: /* internal */ ;
+ e_acsl_end_loop2: ;
__e_acsl_implies = __e_acsl_forall;
__gmpz_clear(__e_acsl_j);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt.c
index 86a4fab89fb..bd5018b6259 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt.c
@@ -64,7 +64,7 @@ int __e_acsl_main(void)
goto return_label;
}
__retres = 0;
- return_label: /* internal */ return __retres;
+ return_label: return __retres;
}
/*@ ensures X ≡ 3; */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt2.c
index 3d6e2f98091..94c8b042822 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt2.c
@@ -115,7 +115,7 @@ int __e_acsl_main(void)
goto return_label;
}
__retres = 0;
- return_label: /* internal */ return __retres;
+ return_label: return __retres;
}
/*@ ensures X ≡ 3; */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
index 4392349227f..afeed35f573 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
@@ -68,7 +68,7 @@ int search(int elt)
k ++;
}
__retres = 0;
- return_label: /* internal */ return __retres;
+ return_label: return __retres;
}
/*@ requires ∀ ℤ i; 0 ≤ i ∧ i < 9 ⇒ A[i] ≤ A[i+1];
@@ -108,7 +108,7 @@ int __e_acsl_search(int elt)
}
__e_acsl_i ++;
}
- e_acsl_end_loop1: /* internal */ ;
+ e_acsl_end_loop1: ;
e_acsl_assert(__e_acsl_forall,(char *)"Precondition",(char *)"search",
(char *)"\\forall integer i; 0 <= i && i < 9 ==> A[i] <= A[i+1]",
9);
@@ -130,7 +130,7 @@ int __e_acsl_search(int elt)
}
__e_acsl_j_2 ++;
}
- e_acsl_end_loop3: /* internal */ ;
+ e_acsl_end_loop3: ;
__e_acsl_at_2 = __e_acsl_forall_2;
}
{
@@ -151,7 +151,7 @@ int __e_acsl_search(int elt)
}
__e_acsl_j ++;
}
- e_acsl_end_loop2: /* internal */ ;
+ e_acsl_end_loop2: ;
__e_acsl_at = __e_acsl_exists;
}
__retres = search(elt);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search2.c
index d0aefd40d1a..25b59b742b5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search2.c
@@ -117,7 +117,7 @@ int search(int elt)
k ++;
}
__retres = 0;
- return_label: /* internal */ return __retres;
+ return_label: return __retres;
}
/*@ requires ∀ ℤ i; 0 ≤ i ∧ i < 9 ⇒ A[i] ≤ A[i+1];
@@ -196,7 +196,7 @@ int __e_acsl_search(int elt)
__gmpz_clear(__e_acsl_add_2);
}
}
- e_acsl_end_loop1: /* internal */ ;
+ e_acsl_end_loop1: ;
e_acsl_assert(__e_acsl_forall,(char *)"Precondition",(char *)"search",
(char *)"\\forall integer i; 0 <= i && i < 9 ==> A[i] <= A[i+1]",
9);
@@ -252,7 +252,7 @@ int __e_acsl_search(int elt)
__gmpz_clear(__e_acsl_add_4);
}
}
- e_acsl_end_loop3: /* internal */ ;
+ e_acsl_end_loop3: ;
__e_acsl_at_2 = __e_acsl_forall_2;
__gmpz_clear(__e_acsl_j_3);
}
@@ -307,7 +307,7 @@ int __e_acsl_search(int elt)
__gmpz_clear(__e_acsl_add_3);
}
}
- e_acsl_end_loop2: /* internal */ ;
+ e_acsl_end_loop2: ;
__e_acsl_at = __e_acsl_exists;
__gmpz_clear(__e_acsl_j);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong.c
index 5ab37c8c941..e9a738a11dc 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong.c
@@ -126,7 +126,7 @@ unsigned long long my_pow(unsigned int x, unsigned int n)
goto return_label;
}
__retres = (unsigned long long)(x * (unsigned int)tmp);
- return_label: /* internal */ return __retres;
+ return_label: return __retres;
}
int main(void)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong2.c
index 5ab37c8c941..e9a738a11dc 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong2.c
@@ -126,7 +126,7 @@ unsigned long long my_pow(unsigned int x, unsigned int n)
goto return_label;
}
__retres = (unsigned long long)(x * (unsigned int)tmp);
- return_label: /* internal */ return __retres;
+ return_label: return __retres;
}
int main(void)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif.c
index 4be0295c487..3473992e515 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif.c
@@ -59,7 +59,7 @@ int main(void)
}
__e_acsl_x ++;
}
- e_acsl_end_loop1: /* internal */ ;
+ e_acsl_end_loop1: ;
e_acsl_assert(__e_acsl_forall,(char *)"Assertion",(char *)"main",
(char *)"\\forall integer x; 0 <= x && x <= 1 ==> x == 0 || x == 1",
11);
@@ -79,7 +79,7 @@ int main(void)
}
__e_acsl_x_2 ++;
}
- e_acsl_end_loop2: /* internal */ ;
+ e_acsl_end_loop2: ;
e_acsl_assert(__e_acsl_forall_2,(char *)"Assertion",(char *)"main",
(char *)"\\forall integer x; 0 < x && x <= 1 ==> x == 1",
12);
@@ -99,7 +99,7 @@ int main(void)
}
__e_acsl_x_3 ++;
}
- e_acsl_end_loop3: /* internal */ ;
+ e_acsl_end_loop3: ;
e_acsl_assert(__e_acsl_forall_3,(char *)"Assertion",(char *)"main",
(char *)"\\forall integer x; 0 < x && x < 1 ==> \\false",
13);
@@ -119,7 +119,7 @@ int main(void)
}
__e_acsl_x_4 ++;
}
- e_acsl_end_loop4: /* internal */ ;
+ e_acsl_end_loop4: ;
e_acsl_assert(__e_acsl_forall_4,(char *)"Assertion",(char *)"main",
(char *)"\\forall integer x; 0 <= x && x < 1 ==> x == 0",
14);
@@ -155,7 +155,7 @@ int main(void)
}
__e_acsl_x_5 ++;
}
- e_acsl_end_loop5: /* internal */ ;
+ e_acsl_end_loop5: ;
e_acsl_assert(__e_acsl_forall_5,(char *)"Assertion",(char *)"main",
(char *)"\\forall integer x, integer y, integer z;\n ((0 <= x && x < 2) && (0 <= y && y < 5)) && (0 <= z && z <= y) ==>\n x+z <= y+1",
18);
@@ -175,7 +175,7 @@ int main(void)
}
__e_acsl_x_6 ++;
}
- e_acsl_end_loop6: /* internal */ ;
+ e_acsl_end_loop6: ;
e_acsl_assert(__e_acsl_exists,(char *)"Assertion",(char *)"main",
(char *)"\\exists int x; (0 <= x && x < 10) && x == 5",23);
}
@@ -208,7 +208,7 @@ int main(void)
}
__e_acsl_y_2 ++;
}
- e_acsl_end_loop7: /* internal */ ;
+ e_acsl_end_loop7: ;
__e_acsl_implies = __e_acsl_exists_2;
}
if (__e_acsl_implies) ;
@@ -219,7 +219,7 @@ int main(void)
}
__e_acsl_x_7 ++;
}
- e_acsl_end_loop8: /* internal */ ;
+ e_acsl_end_loop8: ;
e_acsl_assert(__e_acsl_forall_6,(char *)"Assertion",(char *)"main",
(char *)"\\forall int x;\n 0 <= x && x < 10 ==>\n (x%2 == 0 ==> (\\exists integer y; (0 <= y && y <= x/2) && x == 2*y))",
27);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif2.c
index a76b277495d..9c2f17ba232 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif2.c
@@ -172,7 +172,7 @@ int main(void)
__gmpz_clear(__e_acsl_add);
}
}
- e_acsl_end_loop1: /* internal */ ;
+ e_acsl_end_loop1: ;
e_acsl_assert(__e_acsl_forall,(char *)"Assertion",(char *)"main",
(char *)"\\forall integer x; 0 <= x && x <= 1 ==> x == 0 || x == 1",
11);
@@ -233,7 +233,7 @@ int main(void)
__gmpz_clear(__e_acsl_add_3);
}
}
- e_acsl_end_loop2: /* internal */ ;
+ e_acsl_end_loop2: ;
e_acsl_assert(__e_acsl_forall_2,(char *)"Assertion",(char *)"main",
(char *)"\\forall integer x; 0 < x && x <= 1 ==> x == 1",
12);
@@ -286,7 +286,7 @@ int main(void)
__gmpz_clear(__e_acsl_add_5);
}
}
- e_acsl_end_loop3: /* internal */ ;
+ e_acsl_end_loop3: ;
e_acsl_assert(__e_acsl_forall_3,(char *)"Assertion",(char *)"main",
(char *)"\\forall integer x; 0 < x && x < 1 ==> \\false",
13);
@@ -339,7 +339,7 @@ int main(void)
__gmpz_clear(__e_acsl_add_6);
}
}
- e_acsl_end_loop4: /* internal */ ;
+ e_acsl_end_loop4: ;
e_acsl_assert(__e_acsl_forall_4,(char *)"Assertion",(char *)"main",
(char *)"\\forall integer x; 0 <= x && x < 1 ==> x == 0",
14);
@@ -463,7 +463,7 @@ int main(void)
__gmpz_clear(__e_acsl_add_11);
}
}
- e_acsl_end_loop5: /* internal */ ;
+ e_acsl_end_loop5: ;
e_acsl_assert(__e_acsl_forall_5,(char *)"Assertion",(char *)"main",
(char *)"\\forall integer x, integer y, integer z;\n ((0 <= x && x < 2) && (0 <= y && y < 5)) && (0 <= z && z <= y) ==>\n x+z <= y+1",
18);
@@ -518,7 +518,7 @@ int main(void)
__gmpz_clear(__e_acsl_add_12);
}
}
- e_acsl_end_loop6: /* internal */ ;
+ e_acsl_end_loop6: ;
e_acsl_assert(__e_acsl_exists,(char *)"Assertion",(char *)"main",
(char *)"\\exists int x; (0 <= x && x < 10) && x == 5",23);
__gmpz_clear(__e_acsl_x_6);
@@ -637,7 +637,7 @@ int main(void)
__gmpz_clear(__e_acsl_add_13);
}
}
- e_acsl_end_loop7: /* internal */ ;
+ e_acsl_end_loop7: ;
__e_acsl_implies = __e_acsl_exists_2;
__gmpz_clear(__e_acsl_y_2);
}
@@ -662,7 +662,7 @@ int main(void)
__gmpz_clear(__e_acsl_add_14);
}
}
- e_acsl_end_loop8: /* internal */ ;
+ e_acsl_end_loop8: ;
e_acsl_assert(__e_acsl_forall_6,(char *)"Assertion",(char *)"main",
(char *)"\\forall int x;\n 0 <= x && x < 10 ==>\n (x%2 == 0 ==> (\\exists integer y; (0 <= y && y <= x/2) && x == 2*y))",
27);
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 d69e644757e..9548a526663 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
@@ -85,7 +85,7 @@ struct list *f(struct list *l)
goto return_label;
}
__retres = (struct list *)((void *)0);
- return_label: /* internal */ return __retres;
+ return_label: return __retres;
}
/*@ behavior B1:
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 d69e644757e..9548a526663 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
@@ -85,7 +85,7 @@ struct list *f(struct list *l)
goto return_label;
}
__retres = (struct list *)((void *)0);
- return_label: /* internal */ return __retres;
+ return_label: return __retres;
}
/*@ behavior B1:
--
GitLab