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 f1a29589830b450388bbc9714e56232c86151d43..21f967fb66daef0d1c9289d4b7585c35f903baeb 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 1dd1c9b1d48e8ee275a84a2f07bfe4df8cb2140c..a74d06267f896cd76e2657372e9f1ceac45d0549 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 c763e99a72be1e244669e2105b09add4f0b916bb..2ab5365f21ab98f99647c630ada2f743ecfe10a2 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 28e7db88f8c9d2cd4bc5d8a37b7e79cd5f384d10..5d1e68b65db9cbdae96c70f1668c9beedeb221cd 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 86a4fab89fb23cf1e47117b8cb22841586941ff3..bd5018b62592c7a2fa2720d7196ba2b8c2a5b9b1 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 3d6e2f980918ec4353688cfeb3c95fc7d8a53584..94c8b04282248450c7fdab29dc0fdc4f9946ea7e 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 4392349227f83b0201de0a667fe31c130229c9c3..afeed35f573d5fcf2ed3044515227f6a3ead7d4c 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 d0aefd40d1a060ddb49535e19480a2f7a1fc082a..25b59b742b5fa43b6938332024e4c476d69cdce8 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 5ab37c8c94175a0a1def0718b23a9857c93c0cf1..e9a738a11dc17925e073dbc9df2abc5af53f1d14 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 5ab37c8c94175a0a1def0718b23a9857c93c0cf1..e9a738a11dc17925e073dbc9df2abc5af53f1d14 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 4be0295c4878e577b1a7087712df8f70fe82cfcd..3473992e515e5b181ab14a4aa928c20b82fddba4 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 a76b277495ddd9404dc4779c788a18983f8e75c6..9c2f17ba232ba987a233b1179c6c66311cdb4d12 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 d69e644757e2c1b073a12c9f7e2f4cb0d07ec354..9548a52666388f959a1dc39d255b09c81a99a324 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 d69e644757e2c1b073a12c9f7e2f4cb0d07ec354..9548a52666388f959a1dc39d255b09c81a99a324 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: