From 3b51d7ef16a3751fbdafb3e812d20191ab85f4a3 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Tue, 25 Sep 2018 16:10:32 +0200
Subject: [PATCH] sync with frama-c/frama-c!1873
---
.../tests/format/oracle/fprintf.res.oracle | 17 +++++++--
.../e-acsl/tests/format/oracle/gen_fprintf.c | 38 ++++++++++---------
2 files changed, 34 insertions(+), 21 deletions(-)
diff --git a/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle b/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
index 93e496a3a03..f11e3e9cd19 100644
--- a/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
+++ b/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
@@ -12,6 +12,12 @@
[e-acsl] Warning: annotating undefined function `fclose':
the generated program may miss memory instrumentation
if there are memory-related annotations.
+[e-acsl] Warning: annotating undefined function `waitpid':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:87: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdio.h:94: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
@@ -73,11 +79,18 @@
[eva] using specification for function fork
[eva] using specification for function __e_acsl_builtin_fprintf
[eva] using specification for function exit
+[eva] using specification for function __e_acsl_valid
+[eva] using specification for function __e_acsl_assert
[eva] using specification for function waitpid
+[eva] using specification for function __e_acsl_initialized
+[eva:alarm] FRAMAC_SHARE/libc/sys/wait.h:93: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva] using specification for function __e_acsl_delete_block
+[eva:alarm] FRAMAC_SHARE/libc/sys/wait.h:93: Warning:
+ function __gen_e_acsl_waitpid, behavior stat_loc_non_null: postcondition 'initialization,stat_loc_init_on_success' got status unknown.
[eva:alarm] tests/format/fprintf.c:15: Warning:
accessing uninitialized left-value. assert \initialized(&process_status);
[eva] using specification for function __e_acsl_builtin_printf
-[eva] using specification for function __e_acsl_delete_block
[eva] tests/format/fprintf.c:16: Warning:
Completely invalid destination for assigns clause *stream. Ignoring.
[eva:alarm] tests/format/fprintf.c:16: Warning:
@@ -85,8 +98,6 @@
[eva] using specification for function tmpfile
[eva:alarm] tests/format/fprintf.c:19: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_1);
-[eva] using specification for function __e_acsl_valid
-[eva] using specification for function __e_acsl_assert
[eva:alarm] FRAMAC_SHARE/libc/stdio.h:94: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva] using specification for function fclose
diff --git a/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c b/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
index 09448857900..5f67fe8ac43 100644
--- a/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
+++ b/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
@@ -191,6 +191,8 @@ void __e_acsl_globals_init(void)
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_17,sizeof("-%s-"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_17);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_17);
+ __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);
@@ -238,7 +240,7 @@ int main(int argc, char const **argv)
else {
int process_status;
__e_acsl_store_block((void *)(& process_status),(size_t)4);
- waitpid(pid,& process_status,0);
+ __gen_e_acsl_waitpid(pid,& process_status,0);
/*@ assert Eva: initialization: \initialized(&process_status); */
signal_eval(process_status,0,__gen_e_acsl_literal_string_8);
__e_acsl_delete_block((void *)(& process_status));
@@ -256,7 +258,7 @@ int main(int argc, char const **argv)
else {
int process_status_0;
__e_acsl_store_block((void *)(& process_status_0),(size_t)4);
- waitpid(pid_0,& process_status_0,0);
+ __gen_e_acsl_waitpid(pid_0,& process_status_0,0);
/*@ assert Eva: initialization: \initialized(&process_status_0); */
signal_eval(process_status_0,1,__gen_e_acsl_literal_string_9);
__e_acsl_delete_block((void *)(& process_status_0));
@@ -279,7 +281,7 @@ int main(int argc, char const **argv)
else {
int process_status_1;
__e_acsl_store_block((void *)(& process_status_1),(size_t)4);
- waitpid(pid_1,& process_status_1,0);
+ __gen_e_acsl_waitpid(pid_1,& process_status_1,0);
/*@ assert Eva: initialization: \initialized(&process_status_1); */
signal_eval(process_status_1,0,__gen_e_acsl_literal_string_12);
__e_acsl_delete_block((void *)(& process_status_1));
@@ -299,7 +301,7 @@ int main(int argc, char const **argv)
else {
int process_status_2;
__e_acsl_store_block((void *)(& process_status_2),(size_t)4);
- waitpid(pid_2,& process_status_2,0);
+ __gen_e_acsl_waitpid(pid_2,& process_status_2,0);
/*@ assert Eva: initialization: \initialized(&process_status_2); */
signal_eval(process_status_2,1,__gen_e_acsl_literal_string_13);
__e_acsl_delete_block((void *)(& process_status_2));
@@ -319,7 +321,7 @@ int main(int argc, char const **argv)
else {
int process_status_3;
__e_acsl_store_block((void *)(& process_status_3),(size_t)4);
- waitpid(pid_3,& process_status_3,0);
+ __gen_e_acsl_waitpid(pid_3,& process_status_3,0);
/*@ assert Eva: initialization: \initialized(&process_status_3); */
signal_eval(process_status_3,1,__gen_e_acsl_literal_string_14);
__e_acsl_delete_block((void *)(& process_status_3));
@@ -338,7 +340,7 @@ int main(int argc, char const **argv)
else {
int process_status_4;
__e_acsl_store_block((void *)(& process_status_4),(size_t)4);
- waitpid(pid_4,& process_status_4,0);
+ __gen_e_acsl_waitpid(pid_4,& process_status_4,0);
/*@ assert Eva: initialization: \initialized(&process_status_4); */
signal_eval(process_status_4,0,__gen_e_acsl_literal_string_15);
__e_acsl_delete_block((void *)(& process_status_4));
@@ -356,7 +358,7 @@ int main(int argc, char const **argv)
else {
int process_status_5;
__e_acsl_store_block((void *)(& process_status_5),(size_t)4);
- waitpid(pid_5,& process_status_5,0);
+ __gen_e_acsl_waitpid(pid_5,& process_status_5,0);
/*@ assert Eva: initialization: \initialized(&process_status_5); */
signal_eval(process_status_5,1,__gen_e_acsl_literal_string_16);
__e_acsl_delete_block((void *)(& process_status_5));
@@ -375,7 +377,7 @@ int main(int argc, char const **argv)
else {
int process_status_6;
__e_acsl_store_block((void *)(& process_status_6),(size_t)4);
- waitpid(pid_6,& process_status_6,0);
+ __gen_e_acsl_waitpid(pid_6,& process_status_6,0);
/*@ assert Eva: initialization: \initialized(&process_status_6); */
signal_eval(process_status_6,0,__gen_e_acsl_literal_string_19);
__e_acsl_delete_block((void *)(& process_status_6));
@@ -394,7 +396,7 @@ int main(int argc, char const **argv)
else {
int process_status_7;
__e_acsl_store_block((void *)(& process_status_7),(size_t)4);
- waitpid(pid_7,& process_status_7,0);
+ __gen_e_acsl_waitpid(pid_7,& process_status_7,0);
/*@ assert Eva: initialization: \initialized(&process_status_7); */
signal_eval(process_status_7,0,__gen_e_acsl_literal_string_21);
__e_acsl_delete_block((void *)(& process_status_7));
@@ -413,7 +415,7 @@ int main(int argc, char const **argv)
else {
int process_status_8;
__e_acsl_store_block((void *)(& process_status_8),(size_t)4);
- waitpid(pid_8,& process_status_8,0);
+ __gen_e_acsl_waitpid(pid_8,& process_status_8,0);
/*@ assert Eva: initialization: \initialized(&process_status_8); */
signal_eval(process_status_8,1,__gen_e_acsl_literal_string_23);
__e_acsl_delete_block((void *)(& process_status_8));
@@ -432,7 +434,7 @@ int main(int argc, char const **argv)
else {
int process_status_9;
__e_acsl_store_block((void *)(& process_status_9),(size_t)4);
- waitpid(pid_9,& process_status_9,0);
+ __gen_e_acsl_waitpid(pid_9,& process_status_9,0);
/*@ assert Eva: initialization: \initialized(&process_status_9); */
signal_eval(process_status_9,1,__gen_e_acsl_literal_string_24);
__e_acsl_delete_block((void *)(& process_status_9));
@@ -451,7 +453,7 @@ int main(int argc, char const **argv)
else {
int process_status_10;
__e_acsl_store_block((void *)(& process_status_10),(size_t)4);
- waitpid(pid_10,& process_status_10,0);
+ __gen_e_acsl_waitpid(pid_10,& process_status_10,0);
/*@ assert Eva: initialization: \initialized(&process_status_10); */
signal_eval(process_status_10,1,__gen_e_acsl_literal_string_25);
__e_acsl_delete_block((void *)(& process_status_10));
@@ -471,7 +473,7 @@ int main(int argc, char const **argv)
else {
int process_status_11;
__e_acsl_store_block((void *)(& process_status_11),(size_t)4);
- waitpid(pid_11,& process_status_11,0);
+ __gen_e_acsl_waitpid(pid_11,& process_status_11,0);
/*@ assert Eva: initialization: \initialized(&process_status_11); */
signal_eval(process_status_11,0,__gen_e_acsl_literal_string_26);
__e_acsl_delete_block((void *)(& process_status_11));
@@ -491,7 +493,7 @@ int main(int argc, char const **argv)
else {
int process_status_12;
__e_acsl_store_block((void *)(& process_status_12),(size_t)4);
- waitpid(pid_12,& process_status_12,0);
+ __gen_e_acsl_waitpid(pid_12,& process_status_12,0);
/*@ assert Eva: initialization: \initialized(&process_status_12); */
signal_eval(process_status_12,0,__gen_e_acsl_literal_string_27);
__e_acsl_delete_block((void *)(& process_status_12));
@@ -511,7 +513,7 @@ int main(int argc, char const **argv)
else {
int process_status_13;
__e_acsl_store_block((void *)(& process_status_13),(size_t)4);
- waitpid(pid_13,& process_status_13,0);
+ __gen_e_acsl_waitpid(pid_13,& process_status_13,0);
/*@ assert Eva: initialization: \initialized(&process_status_13); */
signal_eval(process_status_13,1,__gen_e_acsl_literal_string_28);
__e_acsl_delete_block((void *)(& process_status_13));
@@ -531,7 +533,7 @@ int main(int argc, char const **argv)
else {
int process_status_14;
__e_acsl_store_block((void *)(& process_status_14),(size_t)4);
- waitpid(pid_14,& process_status_14,0);
+ __gen_e_acsl_waitpid(pid_14,& process_status_14,0);
/*@ assert Eva: initialization: \initialized(&process_status_14); */
signal_eval(process_status_14,1,__gen_e_acsl_literal_string_29);
__e_acsl_delete_block((void *)(& process_status_14));
@@ -551,7 +553,7 @@ int main(int argc, char const **argv)
else {
int process_status_15;
__e_acsl_store_block((void *)(& process_status_15),(size_t)4);
- waitpid(pid_15,& process_status_15,0);
+ __gen_e_acsl_waitpid(pid_15,& process_status_15,0);
/*@ assert Eva: initialization: \initialized(&process_status_15); */
signal_eval(process_status_15,1,__gen_e_acsl_literal_string_30);
__e_acsl_delete_block((void *)(& process_status_15));
@@ -571,7 +573,7 @@ int main(int argc, char const **argv)
else {
int process_status_16;
__e_acsl_store_block((void *)(& process_status_16),(size_t)4);
- waitpid(pid_16,& process_status_16,0);
+ __gen_e_acsl_waitpid(pid_16,& process_status_16,0);
/*@ assert Eva: initialization: \initialized(&process_status_16); */
signal_eval(process_status_16,0,__gen_e_acsl_literal_string_31);
__e_acsl_delete_block((void *)(& process_status_16));
--
GitLab