synchronize with frama-c/frama-c!1730

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

 [e-acsl] beginning translation.
-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:157:[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/format/oracle/fprintf.res.oracle

@@ -10,11 +10,11 @@ tests/format/fprintf.c:22:[kernel:typing:incompatible-types-call] warning: expec
 [e-acsl] warning: annotating undefined function `fclose':
     the generated program may miss memory instrumentation
     if there are memory-related annotations.
-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/stdio.h:153:[kernel] warning: Neither code nor specification for function fprintf, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdio.h:157:[kernel] warning: Neither code nor specification for function printf, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdio.h:159:[kernel] warning: Neither code nor specification for function snprintf, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdio.h:161:[kernel] warning: Neither code nor specification for function sprintf, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdio.h:353:[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:15:[kernel] warning: Neither code nor specification for function fork, generating default assigns from the prototype
 FRAMAC_SHARE/libc/stdio.h:93:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.

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

@@ -15,7 +15,7 @@ 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:156:[kernel] warning: Neither code nor specification for function printf, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdio.h:157:[kernel] warning: Neither code nor specification for function printf, generating default assigns from the prototype
 FRAMAC_SHARE/libc/unistd.h:781:[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

src/plugins/e-acsl/tests/temporal/oracle/gen_t_global_init.c

@@ -83,6 +83,14 @@ void __e_acsl_globals_init(void)
   __e_acsl_full_init((void *)(& extra_lbits));
   __e_acsl_store_block((void *)(strings),(size_t)32);
   __e_acsl_full_init((void *)(& strings));
+  __e_acsl_temporal_store_nblock((void *)(& strings[0][0]),
+                                 (void *)__gen_e_acsl_literal_string_4);
+  __e_acsl_temporal_store_nblock((void *)(& strings[0][1]),
+                                 (void *)__gen_e_acsl_literal_string_3);
+  __e_acsl_temporal_store_nblock((void *)(& strings[1][0]),
+                                 (void *)__gen_e_acsl_literal_string_2);
+  __e_acsl_temporal_store_nblock((void *)(& strings[1][1]),
+                                 (void *)__gen_e_acsl_literal_string);
   __e_acsl_temporal_store_nblock((void *)(& descs2[0].desc.extra_bits),
                                  (void *)(extra_lbits));
   __e_acsl_temporal_store_nblock((void *)(& descs2[1].desc.extra_bits),
@@ -95,14 +103,6 @@ void __e_acsl_globals_init(void)
                                  (void *)(extra_lbits));
   __e_acsl_temporal_store_nblock((void *)(& l_desc.extra_bits),
                                  (void *)(extra_lbits));
-  __e_acsl_temporal_store_nblock((void *)(& strings[0][0]),
-                                 (void *)__gen_e_acsl_literal_string_4);
-  __e_acsl_temporal_store_nblock((void *)(& strings[0][1]),
-                                 (void *)__gen_e_acsl_literal_string_3);
-  __e_acsl_temporal_store_nblock((void *)(& strings[1][0]),
-                                 (void *)__gen_e_acsl_literal_string_2);
-  __e_acsl_temporal_store_nblock((void *)(& strings[1][1]),
-                                 (void *)__gen_e_acsl_literal_string);
   return;
 }