From changes in the libC: fixes specification of abort and exit functions

src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c

@@ -230,6 +230,11 @@ void __gen_e_acsl_k(int x)
   return;
 }
 
+int __gen_e_acsl_h_char(int c)
+{
+  return c;
+}
+
 int __gen_e_acsl_h_short(int s)
 {
   return s;
@@ -377,9 +382,4 @@ void __gen_e_acsl_f1_7(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
   return;
 }
 
-int __gen_e_acsl_h_char(int c)
-{
-  return c;
-}
-
 

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

@@ -2,7 +2,14 @@
 [e-acsl] Warning: annotating undefined function `atoi':
   the generated program may miss memory instrumentation
   if there are memory-related annotations.
+<<<<<<< HEAD:tests/bts/oracle_ci/bts2192.res.oracle
 [e-acsl] FRAMAC_SHARE/libc/stdlib.h:78: Warning: 
+=======
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:486: Warning: 
+  E-ACSL construct `logic functions with labels' is not yet supported.
+  Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:486: Warning: 
+>>>>>>> From changes in the libC: fixes specification of abort and exit functions:tests/temporal/oracle/t_getenv.res.oracle
   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_ci/fprintf.res.oracle

@@ -46,6 +46,10 @@
 [e-acsl] FRAMAC_SHARE/libc/stdio.h:82: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdio.h:82: Warning: 
+  E-ACSL construct `@[abnormal termination case in behavior@]'
+  is not yet supported.
+  Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
 [kernel:annot:missing-spec] tests/format/fprintf.c:16: Warning: 
   Neither code nor specification for function __e_acsl_builtin_fprintf, generating default assigns from the prototype

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

@@ -189,11 +189,48 @@ void __e_acsl_globals_init(void)
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_17,sizeof("1"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_17);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_17);
+<<<<<<< HEAD:tests/format/oracle_ci/gen_fprintf.c
     __gen_e_acsl_literal_string_16 = "-%s-";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_16,
                          sizeof("-%s-"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_16);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_16);
+=======
+    __e_acsl_store_block((void *)(& __gen_e_acsl_waitpid),(size_t)1);
+    __e_acsl_full_init((void *)(& __gen_e_acsl_waitpid));
+    __e_acsl_store_block((void *)(& __gen_e_acsl_fclose),(size_t)1);
+    __e_acsl_full_init((void *)(& __gen_e_acsl_fclose));
+    __e_acsl_store_block((void *)(& __gen_e_acsl_tmpfile),(size_t)1);
+    __e_acsl_full_init((void *)(& __gen_e_acsl_tmpfile));
+    __e_acsl_store_block((void *)(& __gen_e_acsl_exit),(size_t)1);
+    __e_acsl_full_init((void *)(& __gen_e_acsl_exit));
+    __e_acsl_store_block((void *)(& signal_eval),(size_t)1);
+    __e_acsl_full_init((void *)(& signal_eval));
+    __e_acsl_store_block((void *)(& testno),(size_t)4);
+    __e_acsl_full_init((void *)(& testno));
+    __e_acsl_store_block((void *)(& __fc_fds_state),(size_t)4);
+    __e_acsl_full_init((void *)(& __fc_fds_state));
+    __e_acsl_store_block((void *)(& __fc_time),(size_t)4);
+    __e_acsl_full_init((void *)(& __fc_time));
+    __e_acsl_store_block((void *)(& __fc_p_sigaction),(size_t)8);
+    __e_acsl_full_init((void *)(& __fc_p_sigaction));
+    __e_acsl_store_block((void *)(sigaction),(size_t)2080);
+    __e_acsl_full_init((void *)(& sigaction));
+    __e_acsl_store_block((void *)(& __fc_p_fopen),(size_t)8);
+    __e_acsl_full_init((void *)(& __fc_p_fopen));
+    __e_acsl_store_block((void *)(__fc_fopen),(size_t)128);
+    __e_acsl_full_init((void *)(& __fc_fopen));
+    __e_acsl_store_block((void *)(& stdout),(size_t)8);
+    __e_acsl_full_init((void *)(& stdout));
+    __e_acsl_store_block((void *)(& __fc_p_random48_counter),(size_t)8);
+    __e_acsl_full_init((void *)(& __fc_p_random48_counter));
+    __e_acsl_store_block((void *)(random48_counter),(size_t)6);
+    __e_acsl_full_init((void *)(& random48_counter));
+    __e_acsl_store_block((void *)(& __fc_random48_init),(size_t)4);
+    __e_acsl_full_init((void *)(& __fc_random48_init));
+    __e_acsl_store_block((void *)(& __fc_rand_max),(size_t)8);
+    __e_acsl_full_init((void *)(& __fc_rand_max));
+>>>>>>> From changes in the libC: fixes specification of abort and exit functions:tests/format/oracle/gen_fprintf.c
   }
   return;
 }
@@ -504,6 +541,25 @@ int main(int argc, char const **argv)
     }
   }
   __retres = 0;
+<<<<<<< HEAD:tests/format/oracle_ci/gen_fprintf.c
+=======
+  __e_acsl_delete_block((void *)(& argv));
+  __e_acsl_delete_block((void *)(& argc));
+  __e_acsl_delete_block((void *)(& signal_eval));
+  __e_acsl_delete_block((void *)(& testno));
+  __e_acsl_delete_block((void *)(& __fc_fds_state));
+  __e_acsl_delete_block((void *)(& __fc_time));
+  __e_acsl_delete_block((void *)(& __fc_p_sigaction));
+  __e_acsl_delete_block((void *)(sigaction));
+  __e_acsl_delete_block((void *)(& __fc_p_fopen));
+  __e_acsl_delete_block((void *)(__fc_fopen));
+  __e_acsl_delete_block((void *)(& stdout));
+  __e_acsl_delete_block((void *)(& __fc_p_random48_counter));
+  __e_acsl_delete_block((void *)(random48_counter));
+  __e_acsl_delete_block((void *)(& __fc_random48_init));
+  __e_acsl_delete_block((void *)(& __fc_rand_max));
+  __e_acsl_delete_block((void *)(buf));
+>>>>>>> From changes in the libC: fixes specification of abort and exit functions:tests/format/oracle/gen_fprintf.c
   __e_acsl_delete_block((void *)(& fh));
   __e_acsl_memory_clean();
   return __retres;

src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c

@@ -276,6 +276,11 @@ void __gen_e_acsl_k(int x)
   return;
 }
 
+int __gen_e_acsl_h_char(int c)
+{
+  return c;
+}
+
 int __gen_e_acsl_h_short(int s)
 {
   return s;
@@ -471,9 +476,4 @@ void __gen_e_acsl_f1_7(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
   return;
 }
 
-int __gen_e_acsl_h_char(int c)
-{
-  return c;
-}
-