[E-ACSL] update oracles according to printer changes

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);

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);
   }

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",

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);
     }

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; */

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; */

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);

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);
     }

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)

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)

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);

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);

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:

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: