[e-acsl] tests compatible with strange behavior of gcc 4.6 (linking order)

[e-acsl] all tests are now executed with gcc
[e-acsl] fix bug with integer division and modulo
[e-acsl] untested support of most logic labels
[e-acsl]

src/plugins/e-acsl/TODO

 à traiter avant la 1ère release:
 - quantifications sans exentension de syntaxe
 - \return
-- \old et \at
 
 ########
 # CODE #
@@ -20,11 +19,15 @@
 - constante entière longue: utiliser la représentation sous forme de string et 
   rechercher la base appropriée.
 - introduire feature wishes Bernard (voir mail du 9 juin)
+- arithmetic overflows
 
 #########
 # TESTS #
 #########
 
+- plus de tests de divisions et modulos entières
+- exécuter rte
+- testing logic labels
 - tester plusieurs fonctions contenant des annotations
 - améliorer test "integer_constant.i" quand bug fixed #745
 - test sizeof.i devraient être plus précis quand logic_typing plus précis

src/plugins/e-acsl/env.ml

@@ -215,6 +215,24 @@ let pop_and_get env stmt ~global_clear where =
 
 let get_generated_variables env = List.rev env.new_global_vars
 
+let stmt_of_label env = function
+  | StmtLabel { contents = stmt } -> stmt
+  | LogicLabel(_, label) when label = "Here" -> 
+    (match env.visitor#current_stmt with
+    | None -> Misc.not_yet "label \"Here\" in function contract"
+    | Some s -> s)
+  | LogicLabel(_, label) when label = "Old" || label = "Pre" -> 
+    (try 
+       Kernel_function.find_first_stmt (Extlib.the env.visitor#current_kf)
+     with Kernel_function.No_Statement ->
+       Misc.not_yet (Format.sprintf "label %S in function without code" label))
+  | LogicLabel(_, label) when label = "Post" -> 
+    (try
+       Kernel_function.find_return (Extlib.the env.visitor#current_kf)
+     with Kernel_function.No_Statement ->
+       Misc.not_yet "label \"Post\" in function without code")
+  | LogicLabel(_, _label) -> assert false
+
 (*
 Local Variables:
 compile-command: "make"

src/plugins/e-acsl/env.mli

@@ -78,6 +78,8 @@ val get_generated_variables: t -> varinfo list
 
 val get_visitor: t -> Visitor.generic_frama_c_visitor
 
+val stmt_of_label: t -> logic_label -> stmt
+
 (*
 Local Variables:
 compile-command: "make"

src/plugins/e-acsl/share/e-acsl/e_acsl_gmp.h

@@ -70,13 +70,13 @@ extern void mpz_mul(mpz_t z1, const mpz_t z2, const mpz_t z3);
   @ requires \valid(z2);
   @ requires \valid(z3);
   @ assigns *z1; */
-extern void mpz_cdiv_q(mpz_t z1, const mpz_t z2, const mpz_t z3);
+extern void mpz_tdiv_q(mpz_t z1, const mpz_t z2, const mpz_t z3);
 
 /*@ requires \valid(z1);
   @ requires \valid(z2);
   @ requires \valid(z3);
   @ assigns *z1; */
-extern void mpz_mod(mpz_t z1, const mpz_t z2, const mpz_t z3);
+extern void mpz_tdiv_r(mpz_t z1, const mpz_t z2, const mpz_t z3);
 
 // coercions to C int
 

src/plugins/e-acsl/tests/e-acsl-runtime/arith.i

 /* run.config
    COMMENT: arithmetic operations
    COMMENT: add the last assertion when fixing BTS #751
-   EXECNOW: LOG gen_arith.c BIN gen_arith.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/arith.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_arith.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_arith.out -lgmp ./tests/e-acsl-runtime/result/gen_arith.c
+   EXECNOW: LOG gen_arith.c BIN gen_arith.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/arith.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_arith.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_arith.out ./tests/e-acsl-runtime/result/gen_arith.c -lgmp && ./tests/e-acsl-runtime/result/gen_arith.out
 */
 
 int main(void) {

src/plugins/e-acsl/tests/e-acsl-runtime/array.i

 /* run.config
    COMMENT: arrays
-   EXECNOW: LOG gen_array.c BIN gen_array.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/array.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_array.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_array.out -lgmp ./tests/e-acsl-runtime/result/gen_array.c && ./tests/e-acsl-runtime/result/gen_array.out
+   EXECNOW: LOG gen_array.c BIN gen_array.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/array.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_array.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_array.out ./tests/e-acsl-runtime/result/gen_array.c -lgmp && ./tests/e-acsl-runtime/result/gen_array.out
 */
 
 int T1[3],T2[4];

src/plugins/e-acsl/tests/e-acsl-runtime/at.i

 /* run.config
    COMMENT: \at
-   EXECNOW: LOG gen_at.c BIN gen_at.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/at.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_at.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_at.out -lgmp ./tests/e-acsl-runtime/result/gen_at.c && ./tests/e-acsl-runtime/result/gen_at.out
+   EXECNOW: LOG gen_at.c BIN gen_at.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/at.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_at.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_at.out ./tests/e-acsl-runtime/result/gen_at.c -lgmp && ./tests/e-acsl-runtime/result/gen_at.out
 */
 
 int main(void) {
@@ -10,6 +10,7 @@ int main(void) {
   x = 0;
  L: /*@ assert x == 0; */ x = 1;
   x = 2;
+
   /*@ assert \at(x,L) == 0; */
   /*@ assert \at(x+1,L) == 1; */
   /*@ assert \at(x,L)+1 == 1; */

src/plugins/e-acsl/tests/e-acsl-runtime/cast.i

 /* run.config
    COMMENT: cast
-   EXECNOW: LOG gen_cast.c BIN gen_cast.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/cast.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_cast.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_cast.out -lgmp ./tests/e-acsl-runtime/result/gen_cast.c && ./tests/e-acsl-runtime/result/gen_cast.out
+   EXECNOW: LOG gen_cast.c BIN gen_cast.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/cast.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_cast.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_cast.out ./tests/e-acsl-runtime/result/gen_cast.c -lgmp && ./tests/e-acsl-runtime/result/gen_cast.out
 */
 
 int main(void) {

src/plugins/e-acsl/tests/e-acsl-runtime/comparison.i

 /* run.config
    COMMENT: comparison operators
-   EXECNOW: LOG gen_comparison.c BIN gen_comparison.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/comparison.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_comparison.c > /dev/null &&  gcc -o ./tests/e-acsl-runtime/result/gen_comparison.out -lgmp ./tests/e-acsl-runtime/result/gen_comparison.c && ./tests/e-acsl-runtime/result/gen_comparison.out
+   EXECNOW: LOG gen_comparison.c BIN gen_comparison.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/comparison.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_comparison.c > /dev/null &&  gcc -o ./tests/e-acsl-runtime/result/gen_comparison.out ./tests/e-acsl-runtime/result/gen_comparison.c -lgmp && ./tests/e-acsl-runtime/result/gen_comparison.out
 */
 
 int main(void) {

src/plugins/e-acsl/tests/e-acsl-runtime/function_contract.i

 /* run.config
    COMMENT: function contract
-   EXECNOW: LOG gen_function_contract.c BIN gen_function_contract.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/function_contract.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_function_contract.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_function_contract.out -lgmp ./tests/e-acsl-runtime/result/gen_function_contract.c && ./tests/e-acsl-runtime/result/gen_function_contract.out
+   EXECNOW: LOG gen_function_contract.c BIN gen_function_contract.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/function_contract.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_function_contract.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_function_contract.out ./tests/e-acsl-runtime/result/gen_function_contract.c -lgmp && ./tests/e-acsl-runtime/result/gen_function_contract.out
 */
 
 int X = 0, Y = 2;

src/plugins/e-acsl/tests/e-acsl-runtime/integer_constant.i

 /* run.config
    COMMENT: integer constant + a stmt after the assertion
    COMMENT: waiting for fixing BTS #745
-   EXECNOW: LOG gen_integer_constant.c BIN gen_integer_constant.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/integer_constant.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_integer_constant.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_integer_constant.out -lgmp ./tests/e-acsl-runtime/result/gen_integer_constant.c && ./tests/e-acsl-runtime/result/gen_integer_constant.out
+   EXECNOW: LOG gen_integer_constant.c BIN gen_integer_constant.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/integer_constant.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_integer_constant.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_integer_constant.out ./tests/e-acsl-runtime/result/gen_integer_constant.c -lgmp && ./tests/e-acsl-runtime/result/gen_integer_constant.out
 */
 int main(void) {
   int x;

src/plugins/e-acsl/tests/e-acsl-runtime/lazy.i

 /* run.config
    COMMENT: predicate using lazy operators
-   EXECNOW: LOG gen_lazy.c BIN gen_lazy.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/lazy.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_lazy.c > /dev/null &&  gcc -o ./tests/e-acsl-runtime/result/gen_lazy.out -lgmp ./tests/e-acsl-runtime/result/gen_lazy.c 2> /dev/null && ./tests/e-acsl-runtime/result/gen_lazy.out
+   EXECNOW: LOG gen_lazy.c BIN gen_lazy.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/lazy.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_lazy.c > /dev/null &&  gcc -o ./tests/e-acsl-runtime/result/gen_lazy.out ./tests/e-acsl-runtime/result/gen_lazy.c -lgmp 2> /dev/null && ./tests/e-acsl-runtime/result/gen_lazy.out
 */
 
 int main(void) {

src/plugins/e-acsl/tests/e-acsl-runtime/nested_code_annot.i

 /* run.config
    COMMENT: structured stmt with several code annotations inside
-   EXECNOW: LOG gen_nested_code_annot.c BIN gen_nested_code_annot.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/nested_code_annot.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_nested_code_annot.c > /dev/null &&  gcc -o ./tests/e-acsl-runtime/result/gen_nested_code_annot.out -lgmp ./tests/e-acsl-runtime/result/gen_nested_code_annot.c && ./tests/e-acsl-runtime/result/gen_nested_code_annot.out
+   EXECNOW: LOG gen_nested_code_annot.c BIN gen_nested_code_annot.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/nested_code_annot.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_nested_code_annot.c > /dev/null &&  gcc -o ./tests/e-acsl-runtime/result/gen_nested_code_annot.out ./tests/e-acsl-runtime/result/gen_nested_code_annot.c -lgmp && ./tests/e-acsl-runtime/result/gen_nested_code_annot.out
 */
 
 int main(void) {

src/plugins/e-acsl/tests/e-acsl-runtime/null.i

 /* run.config
    COMMENT: assert \null == 0
-   EXECNOW: LOG gen_null.c BIN gen_null.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/null.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_null.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_null.out -lgmp ./tests/e-acsl-runtime/result/gen_null.c && ./tests/e-acsl-runtime/result/gen_null.out
+   EXECNOW: LOG gen_null.c BIN gen_null.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/null.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_null.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_null.out ./tests/e-acsl-runtime/result/gen_null.c -lgmp && ./tests/e-acsl-runtime/result/gen_null.out
 */
 
 int main(void) {

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle

@@ -8,12 +8,12 @@ tests/e-acsl-runtime/array.i:14:[e-acsl] warning: missing guard for ensuring tha
 [value] Values of globals at initialization
         T1[0..2] ∈ {0}
         T2[0..3] ∈ {0}
-PROJECT_FILE.i:136:[value] entering loop for the first time
-PROJECT_FILE.i:136:[value] assigning non deterministic value for the first time
-PROJECT_FILE.i:139:[value] entering loop for the first time
-PROJECT_FILE.i:142:[value] Assertion got status unknown.
+PROJECT_FILE.i:138:[value] entering loop for the first time
+PROJECT_FILE.i:142:[value] assigning non deterministic value for the first time
+PROJECT_FILE.i:147:[value] entering loop for the first time
+PROJECT_FILE.i:154:[value] Assertion got status unknown.
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:143.
+        Called from PROJECT_FILE.i:155.
 [value] computing for function printf <- e_acsl_fail <- main.
         Called from PROJECT_FILE.i:129.
 [value] Done for function printf
@@ -23,9 +23,9 @@ PROJECT_FILE.i:119:[value] Function exit: postcondition got status invalid.
 [value] Done for function exit
 [value] Recording results for e_acsl_fail
 [value] Done for function e_acsl_fail
-PROJECT_FILE.i:145:[value] Assertion got status unknown.
+PROJECT_FILE.i:157:[value] Assertion got status unknown.
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:146.
+        Called from PROJECT_FILE.i:158.
 [value] computing for function printf <- e_acsl_fail <- main.
         Called from PROJECT_FILE.i:129.
 [value] Done for function printf
@@ -64,10 +64,20 @@ int T2[4];
 int main(void)
 {
   int __retres;
-  { int i; i = 0; while (1) { if (! (i < 3)) { break; } T1[i] = i; i ++; } }
+  { int i;
+    i = 0;
+    while (1) {
+      if (! (i < 3)) { break; }
+      T1[i] = i;
+      i ++; } }
   
-  { int i_0; i_0 = 0;
-    while (1) { if (! (i_0 < 4)) { break; } T2[i_0] = 2 * i_0; i_0 ++; }
+  {
+    int i_0;
+    i_0 = 0;
+    while (1) {
+      if (! (i_0 < 4)) { break; }
+      T2[i_0] = 2 * i_0;
+      i_0 ++; }
   }
   
   /*@ assert T1[0] ≡ T2[0]; */ ;

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle

@@ -3,50 +3,50 @@
 [value] Initial state computed
 [value] Values of globals at initialization
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:142.
+        Called from PROJECT_FILE.i:145.
 PROJECT_FILE.i:33:[value] Function mpz_init_set_si: postcondition got status valid.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:142.
+        Called from PROJECT_FILE.i:146.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <- main.
-        Called from PROJECT_FILE.i:143.
+        Called from PROJECT_FILE.i:147.
 PROJECT_FILE.i:21:[value] Function mpz_init: postcondition got status valid.
 [value] Done for function mpz_init
 [value] computing for function mpz_add <- main.
-        Called from PROJECT_FILE.i:143.
+        Called from PROJECT_FILE.i:148.
 PROJECT_FILE.i:64:[value] Function mpz_add: precondition got status valid.
 PROJECT_FILE.i:65:[value] Function mpz_add: precondition got status valid.
 PROJECT_FILE.i:66:[value] Function mpz_add: precondition got status valid.
 [value] Done for function mpz_add
 [value] computing for function mpz_init_set <- main.
-        Called from PROJECT_FILE.i:144.
+        Called from PROJECT_FILE.i:149.
 PROJECT_FILE.i:25:[value] Function mpz_init_set: postcondition got status valid.
 [value] Done for function mpz_init_set
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:144.
+        Called from PROJECT_FILE.i:150.
 PROJECT_FILE.i:43:[value] Function mpz_clear: precondition got status valid.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:145.
+        Called from PROJECT_FILE.i:151.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:145.
+        Called from PROJECT_FILE.i:152.
 [value] Done for function mpz_clear
-PROJECT_FILE.i:149:[value] Assertion got status valid.
+PROJECT_FILE.i:156:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:151.
+        Called from PROJECT_FILE.i:161.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:151.
+        Called from PROJECT_FILE.i:162.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_cmp <- main.
-        Called from PROJECT_FILE.i:152.
+        Called from PROJECT_FILE.i:163.
 PROJECT_FILE.i:49:[value] Function mpz_cmp: precondition got status valid.
 PROJECT_FILE.i:50:[value] Function mpz_cmp: precondition got status valid.
 [value] Done for function mpz_cmp
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:153.
+        Called from PROJECT_FILE.i:164.
 [value] computing for function printf <- e_acsl_fail <- main.
         Called from PROJECT_FILE.i:129.
 [value] Done for function printf
@@ -57,23 +57,23 @@ PROJECT_FILE.i:119:[value] Function exit: postcondition got status invalid.
 [value] Recording results for e_acsl_fail
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:153.
+        Called from PROJECT_FILE.i:165.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:154.
+        Called from PROJECT_FILE.i:166.
 [value] Done for function mpz_clear
-PROJECT_FILE.i:159:[value] Assertion got status unknown.
+PROJECT_FILE.i:172:[value] Assertion got status unknown.
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:161.
+        Called from PROJECT_FILE.i:177.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:161.
+        Called from PROJECT_FILE.i:178.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_cmp <- main.
-        Called from PROJECT_FILE.i:162.
+        Called from PROJECT_FILE.i:179.
 [value] Done for function mpz_cmp
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:163.
+        Called from PROJECT_FILE.i:180.
 [value] computing for function printf <- e_acsl_fail <- main.
         Called from PROJECT_FILE.i:129.
 [value] Done for function printf
@@ -83,20 +83,20 @@ PROJECT_FILE.i:159:[value] Assertion got status unknown.
 [value] Recording results for e_acsl_fail
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:164.
+        Called from PROJECT_FILE.i:181.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:164.
+        Called from PROJECT_FILE.i:182.
 [value] Done for function mpz_clear
-PROJECT_FILE.i:167:[value] Assertion got status unknown.
+PROJECT_FILE.i:186:[value] Assertion got status unknown.
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:168.
+        Called from PROJECT_FILE.i:190.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_cmp <- main.
-        Called from PROJECT_FILE.i:169.
+        Called from PROJECT_FILE.i:191.
 [value] Done for function mpz_cmp
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:170.
+        Called from PROJECT_FILE.i:192.
 [value] computing for function printf <- e_acsl_fail <- main.
         Called from PROJECT_FILE.i:129.
 [value] Done for function printf
@@ -106,26 +106,26 @@ PROJECT_FILE.i:167:[value] Assertion got status unknown.
 [value] Recording results for e_acsl_fail
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:171.
+        Called from PROJECT_FILE.i:193.
 [value] Done for function mpz_clear
-PROJECT_FILE.i:174:[value] Assertion got status unknown.
+PROJECT_FILE.i:197:[value] Assertion got status unknown.
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:176.
+        Called from PROJECT_FILE.i:203.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:176.
+        Called from PROJECT_FILE.i:204.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <- main.
-        Called from PROJECT_FILE.i:177.
+        Called from PROJECT_FILE.i:205.
 [value] Done for function mpz_init
 [value] computing for function mpz_add <- main.
-        Called from PROJECT_FILE.i:177.
+        Called from PROJECT_FILE.i:206.
 [value] Done for function mpz_add
 [value] computing for function mpz_cmp <- main.
-        Called from PROJECT_FILE.i:178.
+        Called from PROJECT_FILE.i:207.
 [value] Done for function mpz_cmp
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:179.
+        Called from PROJECT_FILE.i:208.
 [value] computing for function printf <- e_acsl_fail <- main.
         Called from PROJECT_FILE.i:129.
 [value] Done for function printf
@@ -135,16 +135,16 @@ PROJECT_FILE.i:174:[value] Assertion got status unknown.
 [value] Recording results for e_acsl_fail
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:180.
+        Called from PROJECT_FILE.i:209.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:180.
+        Called from PROJECT_FILE.i:210.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:180.
+        Called from PROJECT_FILE.i:211.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:184.
+        Called from PROJECT_FILE.i:216.
 [value] Done for function mpz_clear
 [value] Recording results for main
 [value] done for function main
@@ -214,7 +214,10 @@ int main(void)
   int e_acsl_14;
   x = 0;
   L: e_acsl_14 = x;
-  { mpz_t e_acsl_8; mpz_t e_acsl_9; mpz_t e_acsl_10;
+  {
+    mpz_t e_acsl_8;
+    mpz_t e_acsl_9;
+    mpz_t e_acsl_10;
     mpz_init_set_si((__mpz_struct *)(e_acsl_8),(long)x);
     mpz_init_set_si((__mpz_struct *)(e_acsl_9),(long)1);
     mpz_init((__mpz_struct *)(e_acsl_10));
@@ -229,7 +232,10 @@ int main(void)
   
   e_acsl_4 = x;
   /*@ assert x ≡ 0; */ ;
-  { mpz_t e_acsl_1; mpz_t e_acsl_2; int e_acsl_3;
+  {
+    mpz_t e_acsl_1;
+    mpz_t e_acsl_2;
+    int e_acsl_3;
     mpz_init_set_si((__mpz_struct *)(e_acsl_1),(long)x);
     mpz_init_set_si((__mpz_struct *)(e_acsl_2),(long)0);
     e_acsl_3 = mpz_cmp((__mpz_struct const *)(e_acsl_1),
@@ -242,7 +248,10 @@ int main(void)
   x = 1;
   x = 2;
   /*@ assert \at(x,L) ≡ 0; */ ;
-  { mpz_t e_acsl_5; mpz_t e_acsl_6; int e_acsl_7;
+  {
+    mpz_t e_acsl_5;
+    mpz_t e_acsl_6;
+    int e_acsl_7;
     mpz_init_set_si((__mpz_struct *)(e_acsl_5),(long)e_acsl_4);
     mpz_init_set_si((__mpz_struct *)(e_acsl_6),(long)0);
     e_acsl_7 = mpz_cmp((__mpz_struct const *)(e_acsl_5),
@@ -253,7 +262,9 @@ int main(void)
   }
   
   /*@ assert \at(x+1,L) ≡ 1; */ ;
-  { mpz_t e_acsl_12; int e_acsl_13;
+  {
+    mpz_t e_acsl_12;
+    int e_acsl_13;
     mpz_init_set_si((__mpz_struct *)(e_acsl_12),(long)1);
     e_acsl_13 = mpz_cmp((__mpz_struct const *)(e_acsl_11),
                         (__mpz_struct const *)(e_acsl_12));
@@ -262,7 +273,11 @@ int main(void)
   }
   
   /*@ assert \at(x,L)+1 ≡ 1; */ ;
-  { mpz_t e_acsl_15; mpz_t e_acsl_16; mpz_t e_acsl_17; int e_acsl_18;
+  {
+    mpz_t e_acsl_15;
+    mpz_t e_acsl_16;
+    mpz_t e_acsl_17;
+    int e_acsl_18;
     mpz_init_set_si((__mpz_struct *)(e_acsl_15),(long)e_acsl_14);
     mpz_init_set_si((__mpz_struct *)(e_acsl_16),(long)1);
     mpz_init((__mpz_struct *)(e_acsl_17));

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle

@@ -6,15 +6,15 @@ tests/e-acsl-runtime/cast.i:18:[e-acsl] warning: missing guard for ensuring that
 [value] Values of globals at initialization
 PROJECT_FILE.i:138:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_str <- main.
-        Called from PROJECT_FILE.i:140.
+        Called from PROJECT_FILE.i:142.
 PROJECT_FILE.i:37:[value] Function mpz_init_set_str: postcondition got status valid.
 [value] Done for function mpz_init_set_str
 [value] computing for function mpz_get_si <- main.
-        Called from PROJECT_FILE.i:141.
+        Called from PROJECT_FILE.i:143.
 PROJECT_FILE.i:96:[value] Function mpz_get_si: precondition got status valid.
 [value] Done for function mpz_get_si
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:142.
+        Called from PROJECT_FILE.i:144.
 [value] computing for function printf <- e_acsl_fail <- main.
         Called from PROJECT_FILE.i:129.
 [value] Done for function printf
@@ -25,19 +25,19 @@ PROJECT_FILE.i:119:[value] Function exit: postcondition got status invalid.
 [value] Recording results for e_acsl_fail
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:143.
+        Called from PROJECT_FILE.i:145.
 PROJECT_FILE.i:43:[value] Function mpz_clear: precondition got status valid.
 [value] Done for function mpz_clear
-PROJECT_FILE.i:146:[value] Assertion got status valid.
+PROJECT_FILE.i:149:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_str <- main.
-        Called from PROJECT_FILE.i:148.
+        Called from PROJECT_FILE.i:153.
 [value] Done for function mpz_init_set_str
 [value] computing for function mpz_get_ui <- main.
-        Called from PROJECT_FILE.i:149.
+        Called from PROJECT_FILE.i:154.
 PROJECT_FILE.i:100:[value] Function mpz_get_ui: precondition got status valid.
 [value] Done for function mpz_get_ui
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:151.
+        Called from PROJECT_FILE.i:156.
 [value] computing for function printf <- e_acsl_fail <- main.
         Called from PROJECT_FILE.i:129.
 [value] Done for function printf
@@ -47,7 +47,7 @@ PROJECT_FILE.i:100:[value] Function mpz_get_ui: precondition got status valid.
 [value] Recording results for e_acsl_fail
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:152.
+        Called from PROJECT_FILE.i:158.
 [value] Done for function mpz_clear
 [value] Recording results for main
 [value] done for function main
@@ -100,21 +100,27 @@ int main(void)
   x = (long)0;
   y = 0;
   /*@ assert y ≢ (int)0xfffffffffffffff; */ ;
-  { mpz_t e_acsl_1; int e_acsl_2;
+  {
+    mpz_t e_acsl_1;
+    int e_acsl_2;
     mpz_init_set_str((__mpz_struct *)(e_acsl_1),"1152921504606846975",10);
     e_acsl_2 = (int)mpz_get_si((__mpz_struct const *)(e_acsl_1));
     if (! (y != e_acsl_2)) {
       e_acsl_fail((char *)"(y != (int)0xfffffffffffffff)");
-    } mpz_clear((__mpz_struct *)(e_acsl_1));
+    }
+    mpz_clear((__mpz_struct *)(e_acsl_1));
   }
   
   /*@ assert (unsigned int)y ≢ (unsigned int)0xfffffffffffffff; */ ;
-  { mpz_t e_acsl_3; unsigned int e_acsl_4;
+  {
+    mpz_t e_acsl_3;
+    unsigned int e_acsl_4;
     mpz_init_set_str((__mpz_struct *)(e_acsl_3),"1152921504606846975",10);
     e_acsl_4 = (unsigned int)mpz_get_ui((__mpz_struct const *)(e_acsl_3));
     if (! ((unsigned int)y != e_acsl_4)) {
       e_acsl_fail((char *)"((unsigned int)y != (unsigned int)0xfffffffffffffff)");
-    } mpz_clear((__mpz_struct *)(e_acsl_3));
+    }
+    mpz_clear((__mpz_struct *)(e_acsl_3));
   }
   
   __retres = 0;

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle

@@ -6,19 +6,19 @@ PROJECT_FILE.i:139:[value] Assertion got status valid.
 PROJECT_FILE.i:142:[value] Assertion got status valid.
 PROJECT_FILE.i:145:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:147.
+        Called from PROJECT_FILE.i:150.
 PROJECT_FILE.i:33:[value] Function mpz_init_set_si: postcondition got status valid.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:147.
+        Called from PROJECT_FILE.i:151.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_cmp <- main.
-        Called from PROJECT_FILE.i:148.
+        Called from PROJECT_FILE.i:152.
 PROJECT_FILE.i:49:[value] Function mpz_cmp: precondition got status valid.
 PROJECT_FILE.i:50:[value] Function mpz_cmp: precondition got status valid.
 [value] Done for function mpz_cmp
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:149.
+        Called from PROJECT_FILE.i:153.
 [value] computing for function printf <- e_acsl_fail <- main.
         Called from PROJECT_FILE.i:129.
 [value] Done for function printf
@@ -29,24 +29,24 @@ PROJECT_FILE.i:119:[value] Function exit: postcondition got status invalid.
 [value] Recording results for e_acsl_fail
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:149.
+        Called from PROJECT_FILE.i:154.
 PROJECT_FILE.i:43:[value] Function mpz_clear: precondition got status valid.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:150.
+        Called from PROJECT_FILE.i:155.
 [value] Done for function mpz_clear
-PROJECT_FILE.i:153:[value] Assertion got status valid.
+PROJECT_FILE.i:159:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:155.
+        Called from PROJECT_FILE.i:164.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:155.
+        Called from PROJECT_FILE.i:165.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_cmp <- main.
-        Called from PROJECT_FILE.i:156.
+        Called from PROJECT_FILE.i:166.
 [value] Done for function mpz_cmp
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:157.
+        Called from PROJECT_FILE.i:167.
 [value] computing for function printf <- e_acsl_fail <- main.
         Called from PROJECT_FILE.i:129.
 [value] Done for function printf
@@ -56,40 +56,40 @@ PROJECT_FILE.i:153:[value] Assertion got status valid.
 [value] Recording results for e_acsl_fail
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:157.
+        Called from PROJECT_FILE.i:168.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:158.
+        Called from PROJECT_FILE.i:169.
 [value] Done for function mpz_clear
-PROJECT_FILE.i:162:[value] Assertion got status valid.
-PROJECT_FILE.i:165:[value] Assertion got status unknown.
-PROJECT_FILE.i:168:[value] Assertion got status valid.
-PROJECT_FILE.i:171:[value] Assertion got status valid.
 PROJECT_FILE.i:174:[value] Assertion got status valid.
-PROJECT_FILE.i:177:[value] Assertion got status valid.
+PROJECT_FILE.i:177:[value] Assertion got status unknown.
 PROJECT_FILE.i:180:[value] Assertion got status valid.
 PROJECT_FILE.i:183:[value] Assertion got status valid.
 PROJECT_FILE.i:186:[value] Assertion got status valid.
+PROJECT_FILE.i:189:[value] Assertion got status valid.
+PROJECT_FILE.i:192:[value] Assertion got status valid.
+PROJECT_FILE.i:195:[value] Assertion got status valid.
+PROJECT_FILE.i:198:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:188.
+        Called from PROJECT_FILE.i:204.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <- main.
-        Called from PROJECT_FILE.i:188.
+        Called from PROJECT_FILE.i:205.
 PROJECT_FILE.i:21:[value] Function mpz_init: postcondition got status valid.
 [value] Done for function mpz_init
 [value] computing for function mpz_neg <- main.
-        Called from PROJECT_FILE.i:189.
+        Called from PROJECT_FILE.i:206.
 PROJECT_FILE.i:59:[value] Function mpz_neg: precondition got status valid.
 PROJECT_FILE.i:60:[value] Function mpz_neg: precondition got status valid.
 [value] Done for function mpz_neg
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:189.
+        Called from PROJECT_FILE.i:207.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_cmp <- main.
-        Called from PROJECT_FILE.i:190.
+        Called from PROJECT_FILE.i:208.
 [value] Done for function mpz_cmp
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:191.
+        Called from PROJECT_FILE.i:209.
 [value] computing for function printf <- e_acsl_fail <- main.
         Called from PROJECT_FILE.i:129.
 [value] Done for function printf
@@ -99,32 +99,32 @@ PROJECT_FILE.i:60:[value] Function mpz_neg: precondition got status valid.
 [value] Recording results for e_acsl_fail
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:191.
+        Called from PROJECT_FILE.i:210.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:192.
+        Called from PROJECT_FILE.i:211.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:192.
+        Called from PROJECT_FILE.i:212.
 [value] Done for function mpz_clear
-PROJECT_FILE.i:195:[value] Assertion got status valid.
+PROJECT_FILE.i:216:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:197.
+        Called from PROJECT_FILE.i:222.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:197.
+        Called from PROJECT_FILE.i:223.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <- main.
-        Called from PROJECT_FILE.i:198.
+        Called from PROJECT_FILE.i:224.
 [value] Done for function mpz_init
 [value] computing for function mpz_neg <- main.
-        Called from PROJECT_FILE.i:198.
+        Called from PROJECT_FILE.i:225.
 [value] Done for function mpz_neg
 [value] computing for function mpz_cmp <- main.
-        Called from PROJECT_FILE.i:199.
+        Called from PROJECT_FILE.i:226.
 [value] Done for function mpz_cmp
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:200.
+        Called from PROJECT_FILE.i:227.
 [value] computing for function printf <- e_acsl_fail <- main.
         Called from PROJECT_FILE.i:129.
 [value] Done for function printf
@@ -134,32 +134,32 @@ PROJECT_FILE.i:195:[value] Assertion got status valid.
 [value] Recording results for e_acsl_fail
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:201.
+        Called from PROJECT_FILE.i:228.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:201.
+        Called from PROJECT_FILE.i:229.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:201.
+        Called from PROJECT_FILE.i:230.
 [value] Done for function mpz_clear
-PROJECT_FILE.i:204:[value] Assertion got status valid.
+PROJECT_FILE.i:234:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:206.
+        Called from PROJECT_FILE.i:240.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <- main.
-        Called from PROJECT_FILE.i:206.
+        Called from PROJECT_FILE.i:241.
 [value] Done for function mpz_init
 [value] computing for function mpz_neg <- main.
-        Called from PROJECT_FILE.i:207.
+        Called from PROJECT_FILE.i:242.
 [value] Done for function mpz_neg
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:207.
+        Called from PROJECT_FILE.i:243.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_cmp <- main.
-        Called from PROJECT_FILE.i:208.
+        Called from PROJECT_FILE.i:244.
 [value] Done for function mpz_cmp
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:209.
+        Called from PROJECT_FILE.i:245.
 [value] computing for function printf <- e_acsl_fail <- main.
         Called from PROJECT_FILE.i:129.
 [value] Done for function printf
@@ -169,32 +169,32 @@ PROJECT_FILE.i:204:[value] Assertion got status valid.
 [value] Recording results for e_acsl_fail
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:210.
+        Called from PROJECT_FILE.i:246.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:210.
+        Called from PROJECT_FILE.i:247.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:210.
+        Called from PROJECT_FILE.i:248.
 [value] Done for function mpz_clear
-PROJECT_FILE.i:213:[value] Assertion got status valid.
+PROJECT_FILE.i:252:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:215.
+        Called from PROJECT_FILE.i:258.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:215.
+        Called from PROJECT_FILE.i:259.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <- main.
-        Called from PROJECT_FILE.i:216.
+        Called from PROJECT_FILE.i:260.
 [value] Done for function mpz_init
 [value] computing for function mpz_neg <- main.
-        Called from PROJECT_FILE.i:216.
+        Called from PROJECT_FILE.i:261.
 [value] Done for function mpz_neg
 [value] computing for function mpz_cmp <- main.
-        Called from PROJECT_FILE.i:217.
+        Called from PROJECT_FILE.i:262.
 [value] Done for function mpz_cmp
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:218.
+        Called from PROJECT_FILE.i:263.
 [value] computing for function printf <- e_acsl_fail <- main.
         Called from PROJECT_FILE.i:129.
 [value] Done for function printf
@@ -204,29 +204,29 @@ PROJECT_FILE.i:213:[value] Assertion got status valid.
 [value] Recording results for e_acsl_fail
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:219.
+        Called from PROJECT_FILE.i:264.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:219.
+        Called from PROJECT_FILE.i:265.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:219.
+        Called from PROJECT_FILE.i:266.
 [value] Done for function mpz_clear
-PROJECT_FILE.i:222:[value] Assertion got status valid.
+PROJECT_FILE.i:270:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:224.
+        Called from PROJECT_FILE.i:275.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <- main.
-        Called from PROJECT_FILE.i:224.
+        Called from PROJECT_FILE.i:276.
 [value] Done for function mpz_init
 [value] computing for function mpz_neg <- main.
-        Called from PROJECT_FILE.i:225.
+        Called from PROJECT_FILE.i:277.
 [value] Done for function mpz_neg
 [value] computing for function mpz_cmp <- main.
-        Called from PROJECT_FILE.i:226.
+        Called from PROJECT_FILE.i:278.
 [value] Done for function mpz_cmp
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:227.
+        Called from PROJECT_FILE.i:279.
 [value] computing for function printf <- e_acsl_fail <- main.
         Called from PROJECT_FILE.i:129.
 [value] Done for function printf
@@ -236,29 +236,29 @@ PROJECT_FILE.i:222:[value] Assertion got status valid.
 [value] Recording results for e_acsl_fail
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:228.
+        Called from PROJECT_FILE.i:280.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:228.
+        Called from PROJECT_FILE.i:281.
 [value] Done for function mpz_clear
-PROJECT_FILE.i:231:[value] Assertion got status valid.
+PROJECT_FILE.i:285:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:233.
+        Called from PROJECT_FILE.i:291.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:233.
+        Called from PROJECT_FILE.i:292.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <- main.
-        Called from PROJECT_FILE.i:234.
+        Called from PROJECT_FILE.i:293.
 [value] Done for function mpz_init
 [value] computing for function mpz_neg <- main.
-        Called from PROJECT_FILE.i:234.
+        Called from PROJECT_FILE.i:294.
 [value] Done for function mpz_neg
 [value] computing for function mpz_cmp <- main.
-        Called from PROJECT_FILE.i:235.
+        Called from PROJECT_FILE.i:295.
 [value] Done for function mpz_cmp
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:236.
+        Called from PROJECT_FILE.i:296.
 [value] computing for function printf <- e_acsl_fail <- main.
         Called from PROJECT_FILE.i:129.
 [value] Done for function printf
@@ -268,13 +268,13 @@ PROJECT_FILE.i:231:[value] Assertion got status valid.
 [value] Recording results for e_acsl_fail
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:237.
+        Called from PROJECT_FILE.i:297.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:237.
+        Called from PROJECT_FILE.i:298.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:237.
+        Called from PROJECT_FILE.i:299.
 [value] Done for function mpz_clear
 [value] Recording results for main
 [value] done for function main
@@ -340,7 +340,10 @@ int main(void)
   /*@ assert y > x; */ ;
   if (! (y > x)) { e_acsl_fail((char *)"(y > x)"); }
   /*@ assert x ≤ 0; */ ;
-  { mpz_t e_acsl_1; mpz_t e_acsl_2; int e_acsl_3;
+  {
+    mpz_t e_acsl_1;
+    mpz_t e_acsl_2;
+    int e_acsl_3;
     mpz_init_set_si((__mpz_struct *)(e_acsl_1),(long)x);
     mpz_init_set_si((__mpz_struct *)(e_acsl_2),(long)0);
     e_acsl_3 = mpz_cmp((__mpz_struct const *)(e_acsl_1),
@@ -351,7 +354,10 @@ int main(void)
   }
   
   /*@ assert y ≥ 1; */ ;
-  { mpz_t e_acsl_4; mpz_t e_acsl_5; int e_acsl_6;
+  {
+    mpz_t e_acsl_4;
+    mpz_t e_acsl_5;
+    int e_acsl_6;
     mpz_init_set_si((__mpz_struct *)(e_acsl_4),(long)y);
     mpz_init_set_si((__mpz_struct *)(e_acsl_5),(long)1);
     e_acsl_6 = mpz_cmp((__mpz_struct const *)(e_acsl_4),
@@ -380,7 +386,11 @@ int main(void)
   /*@ assert 1 ≢ 2; */ ;
   if (! (1 != 2)) { e_acsl_fail((char *)"(1 != 2)"); }
   /*@ assert -5 < 18; */ ;
-  { mpz_t e_acsl_7; mpz_t e_acsl_8; mpz_t e_acsl_9; int e_acsl_10;
+  {
+    mpz_t e_acsl_7;
+    mpz_t e_acsl_8;
+    mpz_t e_acsl_9;
+    int e_acsl_10;
     mpz_init_set_si((__mpz_struct *)(e_acsl_7),(long)5);
     mpz_init((__mpz_struct *)(e_acsl_8));
     mpz_neg((__mpz_struct *)(e_acsl_8),(__mpz_struct const *)(e_acsl_7));
@@ -394,7 +404,11 @@ int main(void)
   }
   
   /*@ assert 32 > -3; */ ;
-  { mpz_t e_acsl_11; mpz_t e_acsl_12; mpz_t e_acsl_13; int e_acsl_14;
+  {
+    mpz_t e_acsl_11;
+    mpz_t e_acsl_12;
+    mpz_t e_acsl_13;
+    int e_acsl_14;
     mpz_init_set_si((__mpz_struct *)(e_acsl_11),(long)32);
     mpz_init_set_si((__mpz_struct *)(e_acsl_12),(long)3);
     mpz_init((__mpz_struct *)(e_acsl_13));
@@ -408,7 +422,11 @@ int main(void)
   }
   
   /*@ assert -12 ≤ 13; */ ;
-  { mpz_t e_acsl_15; mpz_t e_acsl_16; mpz_t e_acsl_17; int e_acsl_18;
+  {
+    mpz_t e_acsl_15;
+    mpz_t e_acsl_16;
+    mpz_t e_acsl_17;
+    int e_acsl_18;
     mpz_init_set_si((__mpz_struct *)(e_acsl_15),(long)12);
     mpz_init((__mpz_struct *)(e_acsl_16));
     mpz_neg((__mpz_struct *)(e_acsl_16),(__mpz_struct const *)(e_acsl_15));
@@ -422,7 +440,11 @@ int main(void)
   }
   
   /*@ assert 123 ≥ -12; */ ;
-  { mpz_t e_acsl_19; mpz_t e_acsl_20; mpz_t e_acsl_21; int e_acsl_22;
+  {
+    mpz_t e_acsl_19;
+    mpz_t e_acsl_20;
+    mpz_t e_acsl_21;
+    int e_acsl_22;
     mpz_init_set_si((__mpz_struct *)(e_acsl_19),(long)123);
     mpz_init_set_si((__mpz_struct *)(e_acsl_20),(long)12);
     mpz_init((__mpz_struct *)(e_acsl_21));
@@ -436,7 +458,10 @@ int main(void)
   }
   
   /*@ assert -0xff ≡ -0xff; */ ;
-  { mpz_t e_acsl_23; mpz_t e_acsl_24; int e_acsl_25;
+  {
+    mpz_t e_acsl_23;
+    mpz_t e_acsl_24;
+    int e_acsl_25;
     mpz_init_set_si((__mpz_struct *)(e_acsl_23),(long)0xff);
     mpz_init((__mpz_struct *)(e_acsl_24));
     mpz_neg((__mpz_struct *)(e_acsl_24),(__mpz_struct const *)(e_acsl_23));
@@ -448,7 +473,11 @@ int main(void)
   }
   
   /*@ assert 1 ≢ -2; */ ;
-  { mpz_t e_acsl_26; mpz_t e_acsl_27; mpz_t e_acsl_28; int e_acsl_29;
+  {
+    mpz_t e_acsl_26;
+    mpz_t e_acsl_27;
+    mpz_t e_acsl_28;
+    int e_acsl_29;
     mpz_init_set_si((__mpz_struct *)(e_acsl_26),(long)1);
     mpz_init_set_si((__mpz_struct *)(e_acsl_27),(long)2);
     mpz_init((__mpz_struct *)(e_acsl_28));

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle

@@ -27,7 +27,9 @@ int main(void)
   int __retres;
   int x;
   x = 0;
-  if (x) { /*@ assert \false; */ ; e_acsl_fail((char *)"(\\false)"); }
+  if (x) {
+    /*@ assert \false; */ ;
+    e_acsl_fail((char *)"(\\false)"); }
   __retres = 0;
   return (__retres);
 }