synchronize with frama-c/frama-c!1683

src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle

 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdio.h:150:[kernel] warning: Neither code nor specification for function printf, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdio.h:156:[kernel] warning: Neither code nor specification for function printf, generating default assigns from the prototype
 [e-acsl] translation done in project "e-acsl".

src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle

@@ -2,6 +2,6 @@
 [e-acsl] warning: annotating undefined function `atoi':
     the generated program may miss memory instrumentation
     if there are memory-related annotations.
-FRAMAC_SHARE/libc/stdlib.h:76:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:78:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
     Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".

src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle

@@ -15,30 +15,32 @@ tests/format/fprintf.c:24:[kernel:typing:incompatible-types-call] warning: expec
 [e-acsl] warning: annotating undefined function `fopen':
     the generated program may miss memory instrumentation
     if there are memory-related annotations.
-FRAMAC_SHARE/libc/stdio.h:146:[kernel] warning: Neither code nor specification for function fprintf, generating default assigns from the prototype
-FRAMAC_SHARE/libc/stdio.h:150:[kernel] warning: Neither code nor specification for function printf, generating default assigns from the prototype
-FRAMAC_SHARE/libc/stdio.h:152:[kernel] warning: Neither code nor specification for function snprintf, generating default assigns from the prototype
-FRAMAC_SHARE/libc/stdio.h:154:[kernel] warning: Neither code nor specification for function sprintf, generating default assigns from the prototype
-FRAMAC_SHARE/libc/stdio.h:340:[kernel] warning: Neither code nor specification for function dprintf, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdio.h:152:[kernel] warning: Neither code nor specification for function fprintf, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdio.h:156:[kernel] warning: Neither code nor specification for function printf, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdio.h:158:[kernel] warning: Neither code nor specification for function snprintf, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdio.h:160:[kernel] warning: Neither code nor specification for function sprintf, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdio.h:349:[kernel] warning: Neither code nor specification for function dprintf, generating default assigns from the prototype
 FRAMAC_SHARE/libc/sys/wait.h:60:[kernel] warning: Neither code nor specification for function waitpid, generating default assigns from the prototype
 tests/format/fprintf.c:12:[kernel] warning: Neither code nor specification for function strcpy, generating default assigns from the prototype
 tests/format/fprintf.c:13:[kernel] warning: Neither code nor specification for function mktemp, generating default assigns from the prototype
 tests/format/fprintf.c:17:[kernel] warning: Neither code nor specification for function fork, generating default assigns from the prototype
-FRAMAC_SHARE/libc/stdlib.h:413:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
-    Ignoring annotation.
 FRAMAC_SHARE/libc/stdio.h:109:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
     Ignoring annotation.
-FRAMAC_SHARE/libc/stdio.h:87:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/stdio.h:109:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+    Ignoring annotation.
+FRAMAC_SHARE/libc/stdio.h:112:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+    Ignoring annotation.
+FRAMAC_SHARE/libc/stdio.h:93:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
     Ignoring annotation.
-FRAMAC_SHARE/libc/stdio.h:89:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/stdio.h:95:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
     Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
 [value:initial-state] Values of globals at initialization
-  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
+  __fc_rand_max ∈ {32767}
   __e_acsl_init ∈ [--..--]
   stdout ∈ {{ NULL ; &S___fc_stdout[0] }}
   __fc_fopen[0..15] ∈ {0}
@@ -100,40 +102,5 @@ tests/format/signalled.h:12:[kernel] warning: Neither code nor specification for
 [value] using specification for function __e_acsl_delete_block
 tests/format/fprintf.c:18:[value] warning: Completely invalid destination for assigns clause *stream. Ignoring.
 tests/format/fprintf.c:18:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_0);
-[value] using specification for function fopen
-tests/format/fprintf.c:21:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_1);
-[value] using specification for function __e_acsl_valid
-[value] using specification for function __e_acsl_assert
-FRAMAC_SHARE/libc/stdio.h:87:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
-[value] using specification for function fclose
-tests/format/fprintf.c:23:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_2);
-tests/format/fprintf.c:24:[value] warning: Completely invalid destination for assigns clause *stream. Ignoring.
-tests/format/fprintf.c:24:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_3);
-[value] using specification for function remove
-FRAMAC_SHARE/libc/stdio.h:70:[value] warning: no 'assigns \result \from ...' clause specified for function remove
-tests/format/fprintf.c:31:[kernel] warning: Neither code nor specification for function __e_acsl_builtin_dprintf, generating default assigns from the prototype
-[value] using specification for function __e_acsl_builtin_dprintf
-tests/format/fprintf.c:31:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_4);
-tests/format/fprintf.c:32:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_5);
-tests/format/fprintf.c:38:[kernel] warning: Neither code nor specification for function __e_acsl_builtin_sprintf, generating default assigns from the prototype
-[value] using specification for function __e_acsl_builtin_sprintf
-tests/format/fprintf.c:38:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_6);
-tests/format/fprintf.c:39:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_7);
-tests/format/fprintf.c:40:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_8);
-tests/format/fprintf.c:41:[value] warning: Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
-tests/format/fprintf.c:41:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_9);
-tests/format/fprintf.c:42:[value] warning: Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
-tests/format/fprintf.c:42:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_10);
-tests/format/fprintf.c:45:[kernel] warning: Neither code nor specification for function __e_acsl_builtin_snprintf, generating default assigns from the prototype
-[value] using specification for function __e_acsl_builtin_snprintf
-tests/format/fprintf.c:45:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_11);
-tests/format/fprintf.c:46:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_12);
-tests/format/fprintf.c:47:[value] warning: Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
-tests/format/fprintf.c:47:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_13);
-tests/format/fprintf.c:48:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_14);
-tests/format/fprintf.c:49:[value] warning: Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
-tests/format/fprintf.c:49:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_15);
-tests/format/fprintf.c:50:[value] warning: Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
-tests/format/fprintf.c:50:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_16);
-[value] using specification for function __e_acsl_memory_clean
+tests/format/fprintf.c:19:[value:alarm] warning: function __gen_e_acsl_fopen: precondition 'valid_filename' got status invalid.
 [value] done for function main

src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c

@@ -328,7 +328,6 @@ int main(int argc, char const **argv)
         int process_status_1;
         __e_acsl_store_block((void *)(& process_status_1),(size_t)4);
         waitpid(pid_1,& process_status_1,0);
-        /*@ assert Value: initialization: \initialized(&process_status_1); */
         signal_eval(process_status_1,0,__gen_e_acsl_literal_string_14);
         __e_acsl_delete_block((void *)(& process_status_1));
       }
@@ -353,7 +352,6 @@ int main(int argc, char const **argv)
         int process_status_2;
         __e_acsl_store_block((void *)(& process_status_2),(size_t)4);
         waitpid(pid_2,& process_status_2,0);
-        /*@ assert Value: initialization: \initialized(&process_status_2); */
         signal_eval(process_status_2,1,__gen_e_acsl_literal_string_15);
         __e_acsl_delete_block((void *)(& process_status_2));
       }
@@ -378,7 +376,6 @@ int main(int argc, char const **argv)
         int process_status_3;
         __e_acsl_store_block((void *)(& process_status_3),(size_t)4);
         waitpid(pid_3,& process_status_3,0);
-        /*@ assert Value: initialization: \initialized(&process_status_3); */
         signal_eval(process_status_3,1,__gen_e_acsl_literal_string_16);
         __e_acsl_delete_block((void *)(& process_status_3));
       }
@@ -403,7 +400,6 @@ int main(int argc, char const **argv)
       int process_status_4;
       __e_acsl_store_block((void *)(& process_status_4),(size_t)4);
       waitpid(pid_4,& process_status_4,0);
-      /*@ assert Value: initialization: \initialized(&process_status_4); */
       signal_eval(process_status_4,0,__gen_e_acsl_literal_string_17);
       __e_acsl_delete_block((void *)(& process_status_4));
     }
@@ -426,7 +422,6 @@ int main(int argc, char const **argv)
       int process_status_5;
       __e_acsl_store_block((void *)(& process_status_5),(size_t)4);
       waitpid(pid_5,& process_status_5,0);
-      /*@ assert Value: initialization: \initialized(&process_status_5); */
       signal_eval(process_status_5,1,__gen_e_acsl_literal_string_18);
       __e_acsl_delete_block((void *)(& process_status_5));
     }
@@ -450,7 +445,6 @@ int main(int argc, char const **argv)
       int process_status_6;
       __e_acsl_store_block((void *)(& process_status_6),(size_t)4);
       waitpid(pid_6,& process_status_6,0);
-      /*@ assert Value: initialization: \initialized(&process_status_6); */
       signal_eval(process_status_6,0,__gen_e_acsl_literal_string_21);
       __e_acsl_delete_block((void *)(& process_status_6));
     }
@@ -474,7 +468,6 @@ int main(int argc, char const **argv)
       int process_status_7;
       __e_acsl_store_block((void *)(& process_status_7),(size_t)4);
       waitpid(pid_7,& process_status_7,0);
-      /*@ assert Value: initialization: \initialized(&process_status_7); */
       signal_eval(process_status_7,0,__gen_e_acsl_literal_string_23);
       __e_acsl_delete_block((void *)(& process_status_7));
     }
@@ -498,7 +491,6 @@ int main(int argc, char const **argv)
       int process_status_8;
       __e_acsl_store_block((void *)(& process_status_8),(size_t)4);
       waitpid(pid_8,& process_status_8,0);
-      /*@ assert Value: initialization: \initialized(&process_status_8); */
       signal_eval(process_status_8,1,__gen_e_acsl_literal_string_25);
       __e_acsl_delete_block((void *)(& process_status_8));
     }
@@ -522,7 +514,6 @@ int main(int argc, char const **argv)
       int process_status_9;
       __e_acsl_store_block((void *)(& process_status_9),(size_t)4);
       waitpid(pid_9,& process_status_9,0);
-      /*@ assert Value: initialization: \initialized(&process_status_9); */
       signal_eval(process_status_9,1,__gen_e_acsl_literal_string_26);
       __e_acsl_delete_block((void *)(& process_status_9));
     }
@@ -546,7 +537,6 @@ int main(int argc, char const **argv)
       int process_status_10;
       __e_acsl_store_block((void *)(& process_status_10),(size_t)4);
       waitpid(pid_10,& process_status_10,0);
-      /*@ assert Value: initialization: \initialized(&process_status_10); */
       signal_eval(process_status_10,1,__gen_e_acsl_literal_string_27);
       __e_acsl_delete_block((void *)(& process_status_10));
     }
@@ -571,7 +561,6 @@ int main(int argc, char const **argv)
       int process_status_11;
       __e_acsl_store_block((void *)(& process_status_11),(size_t)4);
       waitpid(pid_11,& process_status_11,0);
-      /*@ assert Value: initialization: \initialized(&process_status_11); */
       signal_eval(process_status_11,0,__gen_e_acsl_literal_string_28);
       __e_acsl_delete_block((void *)(& process_status_11));
     }
@@ -596,7 +585,6 @@ int main(int argc, char const **argv)
       int process_status_12;
       __e_acsl_store_block((void *)(& process_status_12),(size_t)4);
       waitpid(pid_12,& process_status_12,0);
-      /*@ assert Value: initialization: \initialized(&process_status_12); */
       signal_eval(process_status_12,0,__gen_e_acsl_literal_string_29);
       __e_acsl_delete_block((void *)(& process_status_12));
     }
@@ -621,7 +609,6 @@ int main(int argc, char const **argv)
       int process_status_13;
       __e_acsl_store_block((void *)(& process_status_13),(size_t)4);
       waitpid(pid_13,& process_status_13,0);
-      /*@ assert Value: initialization: \initialized(&process_status_13); */
       signal_eval(process_status_13,1,__gen_e_acsl_literal_string_30);
       __e_acsl_delete_block((void *)(& process_status_13));
     }
@@ -646,7 +633,6 @@ int main(int argc, char const **argv)
       int process_status_14;
       __e_acsl_store_block((void *)(& process_status_14),(size_t)4);
       waitpid(pid_14,& process_status_14,0);
-      /*@ assert Value: initialization: \initialized(&process_status_14); */
       signal_eval(process_status_14,1,__gen_e_acsl_literal_string_31);
       __e_acsl_delete_block((void *)(& process_status_14));
     }
@@ -671,7 +657,6 @@ int main(int argc, char const **argv)
       int process_status_15;
       __e_acsl_store_block((void *)(& process_status_15),(size_t)4);
       waitpid(pid_15,& process_status_15,0);
-      /*@ assert Value: initialization: \initialized(&process_status_15); */
       signal_eval(process_status_15,1,__gen_e_acsl_literal_string_32);
       __e_acsl_delete_block((void *)(& process_status_15));
     }
@@ -696,7 +681,6 @@ int main(int argc, char const **argv)
       int process_status_16;
       __e_acsl_store_block((void *)(& process_status_16),(size_t)4);
       waitpid(pid_16,& process_status_16,0);
-      /*@ assert Value: initialization: \initialized(&process_status_16); */
       signal_eval(process_status_16,0,__gen_e_acsl_literal_string_33);
       __e_acsl_delete_block((void *)(& process_status_16));
     }

src/plugins/e-acsl/tests/format/oracle/printf.res.oracle

@@ -15,46 +15,46 @@ tests/format/printf.c:88:[kernel] warning: Floating-point constant 0.2 is not re
 [e-acsl] warning: annotating undefined function `strcpy':
     the generated program may miss memory instrumentation
     if there are memory-related annotations.
-FRAMAC_SHARE/libc/stdio.h:150:[kernel] warning: Neither code nor specification for function printf, generating default assigns from the prototype
-FRAMAC_SHARE/libc/unistd.h:785:[kernel] warning: Neither code nor specification for function fork, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdio.h:156:[kernel] warning: Neither code nor specification for function printf, generating default assigns from the prototype
+FRAMAC_SHARE/libc/unistd.h:780:[kernel] warning: Neither code nor specification for function fork, generating default assigns from the prototype
 FRAMAC_SHARE/libc/sys/wait.h:60:[kernel] warning: Neither code nor specification for function waitpid, generating default assigns from the prototype
 :0:[kernel] warning: Neither code nor specification for function __fc_vla_free, generating default assigns from the prototype
 :0:[kernel] warning: Neither code nor specification for function __fc_vla_alloc, generating default assigns from the prototype
-FRAMAC_SHARE/libc/string.h:309:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+FRAMAC_SHARE/libc/string.h:317:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
     Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:310:[e-acsl] warning: E-ACSL construct `trange' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:312:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:312:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/string.h:318:[e-acsl] warning: E-ACSL construct `trange' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/string.h:320:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/string.h:320:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
     Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:315:[e-acsl] warning: E-ACSL construct `logic function returning an integer' is not yet supported.
+FRAMAC_SHARE/libc/string.h:323:[e-acsl] warning: E-ACSL construct `logic function returning an integer' is not yet supported.
     Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:140:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+FRAMAC_SHARE/libc/string.h:143:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
     Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:153:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/string.h:157:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
     Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:143:[e-acsl] warning: E-ACSL construct `user-defined logic type' is not yet supported.
+FRAMAC_SHARE/libc/string.h:146:[e-acsl] warning: E-ACSL construct `user-defined logic type' is not yet supported.
     Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:143:[e-acsl] warning: E-ACSL construct `user-defined logic type' is not yet supported.
+FRAMAC_SHARE/libc/string.h:146:[e-acsl] warning: E-ACSL construct `user-defined logic type' is not yet supported.
     Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:150:[e-acsl] warning: E-ACSL construct `user-defined logic type' is not yet supported.
+FRAMAC_SHARE/libc/string.h:153:[e-acsl] warning: E-ACSL construct `user-defined logic type' is not yet supported.
     Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:108:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+FRAMAC_SHARE/libc/string.h:111:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
     Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:108:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/string.h:111:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
     Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:110:[e-acsl] warning: E-ACSL construct `logic function returning an integer' is not yet supported.
+FRAMAC_SHARE/libc/string.h:113:[e-acsl] warning: E-ACSL construct `logic function returning an integer' is not yet supported.
     Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:110:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/string.h:113:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
     Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:415:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:406:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
     Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
 [value:initial-state] Values of globals at initialization
-  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
+  __fc_rand_max ∈ {32767}
   __e_acsl_init ∈ [--..--]
   __fc_fopen[0..15] ∈ {0}
   __fc_p_fopen ∈ {{ &__fc_fopen[0] }}

src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.0.res.oracle

@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value:initial-state] Values of globals at initialization
-  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
+  __fc_rand_max ∈ {32767}
   __e_acsl_init ∈ [--..--]
   __fc_fopen[0..15] ∈ {0}
   __fc_p_fopen ∈ {{ &__fc_fopen[0] }}

src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.1.res.oracle

@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value:initial-state] Values of globals at initialization
-  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
+  __fc_rand_max ∈ {32767}
   __e_acsl_init ∈ [--..--]
   __fc_fopen[0..15] ∈ {0}
   __fc_p_fopen ∈ {{ &__fc_fopen[0] }}

src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle

@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value:initial-state] Values of globals at initialization
-  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
+  __fc_rand_max ∈ {32767}
   __e_acsl_init ∈ [--..--]
   __fc_fopen[0..15] ∈ {0}
   __fc_p_fopen ∈ {{ &__fc_fopen[0] }}

src/plugins/e-acsl/tests/gmp/oracle/arith.1.res.oracle

@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value:initial-state] Values of globals at initialization
-  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
+  __fc_rand_max ∈ {32767}
   __e_acsl_init ∈ [--..--]
   __fc_fopen[0..15] ∈ {0}
   __fc_p_fopen ∈ {{ &__fc_fopen[0] }}

src/plugins/e-acsl/tests/gmp/oracle/array.0.res.oracle

@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value:initial-state] Values of globals at initialization
-  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
+  __fc_rand_max ∈ {32767}
   __e_acsl_init ∈ [--..--]
   __fc_fopen[0..15] ∈ {0}
   __fc_p_fopen ∈ {{ &__fc_fopen[0] }}

src/plugins/e-acsl/tests/gmp/oracle/array.1.res.oracle

@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value:initial-state] Values of globals at initialization
-  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
+  __fc_rand_max ∈ {32767}
   __e_acsl_init ∈ [--..--]
   __fc_fopen[0..15] ∈ {0}
   __fc_p_fopen ∈ {{ &__fc_fopen[0] }}

src/plugins/e-acsl/tests/gmp/oracle/at.0.res.oracle

@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value:initial-state] Values of globals at initialization
-  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
+  __fc_rand_max ∈ {32767}
   __e_acsl_init ∈ [--..--]
   __fc_fopen[0..15] ∈ {0}
   __fc_p_fopen ∈ {{ &__fc_fopen[0] }}

src/plugins/e-acsl/tests/gmp/oracle/at.1.res.oracle

@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value:initial-state] Values of globals at initialization
-  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
+  __fc_rand_max ∈ {32767}
   __e_acsl_init ∈ [--..--]
   __fc_fopen[0..15] ∈ {0}
   __fc_p_fopen ∈ {{ &__fc_fopen[0] }}

src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle

@@ -6,8 +6,8 @@ tests/gmp/cast.i:23:[e-acsl] warning: approximating a real number by a float
 [value] Computing initial state
 [value] Initial state computed
 [value:initial-state] Values of globals at initialization
-  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
+  __fc_rand_max ∈ {32767}
   __e_acsl_init ∈ [--..--]
   __fc_fopen[0..15] ∈ {0}
   __fc_p_fopen ∈ {{ &__fc_fopen[0] }}

src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle

@@ -6,8 +6,8 @@ tests/gmp/cast.i:23:[e-acsl] warning: approximating a real number by a float
 [value] Computing initial state
 [value] Initial state computed
 [value:initial-state] Values of globals at initialization
-  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
+  __fc_rand_max ∈ {32767}
   __e_acsl_init ∈ [--..--]
   __fc_fopen[0..15] ∈ {0}
   __fc_p_fopen ∈ {{ &__fc_fopen[0] }}

src/plugins/e-acsl/tests/gmp/oracle/comparison.0.res.oracle

@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value:initial-state] Values of globals at initialization
-  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
+  __fc_rand_max ∈ {32767}
   __e_acsl_init ∈ [--..--]
   __fc_fopen[0..15] ∈ {0}
   __fc_p_fopen ∈ {{ &__fc_fopen[0] }}

src/plugins/e-acsl/tests/gmp/oracle/comparison.1.res.oracle

@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value:initial-state] Values of globals at initialization
-  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
+  __fc_rand_max ∈ {32767}
   __e_acsl_init ∈ [--..--]
   __fc_fopen[0..15] ∈ {0}
   __fc_p_fopen ∈ {{ &__fc_fopen[0] }}

src/plugins/e-acsl/tests/gmp/oracle/integer_constant.0.res.oracle

@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value:initial-state] Values of globals at initialization
-  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
+  __fc_rand_max ∈ {32767}
   __e_acsl_init ∈ [--..--]
   __fc_fopen[0..15] ∈ {0}
   __fc_p_fopen ∈ {{ &__fc_fopen[0] }}

src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.res.oracle

@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value:initial-state] Values of globals at initialization
-  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
+  __fc_rand_max ∈ {32767}
   __e_acsl_init ∈ [--..--]
   __fc_fopen[0..15] ∈ {0}
   __fc_p_fopen ∈ {{ &__fc_fopen[0] }}

src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle

@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value:initial-state] Values of globals at initialization
-  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
+  __fc_rand_max ∈ {32767}
   __e_acsl_init ∈ [--..--]
   __fc_fopen[0..15] ∈ {0}
   __fc_p_fopen ∈ {{ &__fc_fopen[0] }}