From 439b922063f7205741e09c88cc98334911a0d902 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <Patrick.Baudin@cea.fr>
Date: Fri, 26 Jul 2019 17:18:35 +0200
Subject: [PATCH] From changes in the libC: fixes specification of abort and
exit functions
---
.../tests/arith/oracle_ci/gen_functions.c | 10 ++--
.../tests/bts/oracle_ci/bts2192.res.oracle | 7 +++
.../tests/format/oracle_ci/fprintf.res.oracle | 4 ++
.../tests/format/oracle_ci/gen_fprintf.c | 56 +++++++++++++++++++
.../tests/gmp-only/oracle_ci/gen_functions.c | 10 ++--
5 files changed, 77 insertions(+), 10 deletions(-)
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c
index 7863ef08ac2..5137def7dd4 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c
+++ b/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;
-}
-
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/bts2192.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts2192.res.oracle
index f96be2395e6..02e753058cf 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/bts2192.res.oracle
+++ b/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".
diff --git a/src/plugins/e-acsl/tests/format/oracle_ci/fprintf.res.oracle b/src/plugins/e-acsl/tests/format/oracle_ci/fprintf.res.oracle
index e7f38920c95..24f1f2d50e2 100644
--- a/src/plugins/e-acsl/tests/format/oracle_ci/fprintf.res.oracle
+++ b/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
diff --git a/src/plugins/e-acsl/tests/format/oracle_ci/gen_fprintf.c b/src/plugins/e-acsl/tests/format/oracle_ci/gen_fprintf.c
index 493d424dacf..e103fd6397f 100644
--- a/src/plugins/e-acsl/tests/format/oracle_ci/gen_fprintf.c
+++ b/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;
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c
index 7cf1bcc8904..bae23e804b7 100644
--- a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c
+++ b/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;
-}
-
--
GitLab