From f96a98ca28c244a8b7daf9ed00436acd250e73ff Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Tue, 31 Aug 2021 17:17:52 +0200
Subject: [PATCH] update test oracles
---
.../e-acsl/tests/builtin/oracle/gen_strcat.c | 6 ++--
.../e-acsl/tests/builtin/oracle/gen_strcmp.c | 6 ++--
.../e-acsl/tests/builtin/oracle/gen_strcpy.c | 6 ++--
.../e-acsl/tests/builtin/oracle/gen_strlen.c | 6 ++--
.../tests/builtin/oracle/strcat.res.oracle | 4 +--
.../tests/builtin/oracle/strcmp.res.oracle | 4 +--
.../tests/builtin/oracle/strcpy.res.oracle | 4 +--
.../tests/builtin/oracle/strlen.res.oracle | 4 +--
.../tests/format/oracle/fprintf.res.oracle | 4 +--
.../e-acsl/tests/format/oracle/gen_fprintf.c | 6 ++--
.../e-acsl/tests/format/oracle/gen_printf.c | 6 ++--
.../tests/format/oracle/printf.res.oracle | 4 +--
.../tests/known/oracle/fcntl.res.oracle | 6 ++--
.../tests/known/oracle/open.res.oracle | 6 ++--
.../tests/known/oracle/open_wrong.res.oracle | 6 ++--
.../tests/known/oracle/openat.res.oracle | 6 ++--
.../tests/known/oracle/printf.res.oracle | 1 -
.../oracle/printf_wrong_arity.res.oracle | 1 -
tests/libc/oracle/fc_libc.0.res.oracle | 29 +++++++++----------
tests/libc/oracle/fc_libc.1.res.oracle | 4 ---
tests/libc/oracle/fc_libc.2.res.oracle | 2 ++
tests/libc/oracle/sys_types.res.oracle | 6 +---
22 files changed, 59 insertions(+), 68 deletions(-)
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
index 1c95f09bf73..4cf7ead5fe4 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
@@ -728,7 +728,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__gen_e_acsl_assert_data.pred_txt = "stat_loc_non_null: valid_stat_loc: \\valid(stat_loc)";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/sys/wait.h";
__gen_e_acsl_assert_data.fct = "waitpid";
- __gen_e_acsl_assert_data.line = 92;
+ __gen_e_acsl_assert_data.line = 95;
__e_acsl_assert(__gen_e_acsl_valid,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
}
@@ -755,7 +755,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__gen_e_acsl_assert_data_2.pred_txt = "result_ok_or_error: \\result == -1 || \\result >= 0";
__gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/sys/wait.h";
__gen_e_acsl_assert_data_2.fct = "waitpid";
- __gen_e_acsl_assert_data_2.line = 84;
+ __gen_e_acsl_assert_data_2.line = 87;
__e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
@@ -788,7 +788,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__gen_e_acsl_assert_data_3.pred_txt = "initialization: stat_loc_init_on_success:\n \\result >= 0 && \\old(stat_loc) != \\null ==> \\initialized(\\old(stat_loc))";
__gen_e_acsl_assert_data_3.file = "FRAMAC_SHARE/libc/sys/wait.h";
__gen_e_acsl_assert_data_3.fct = "waitpid";
- __gen_e_acsl_assert_data_3.line = 86;
+ __gen_e_acsl_assert_data_3.line = 89;
__e_acsl_assert(__gen_e_acsl_implies,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
__e_acsl_contract_clean(__gen_e_acsl_contract);
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
index 34c9f132beb..bf3ae7909b3 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
@@ -268,7 +268,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__gen_e_acsl_assert_data.pred_txt = "stat_loc_non_null: valid_stat_loc: \\valid(stat_loc)";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/sys/wait.h";
__gen_e_acsl_assert_data.fct = "waitpid";
- __gen_e_acsl_assert_data.line = 92;
+ __gen_e_acsl_assert_data.line = 95;
__e_acsl_assert(__gen_e_acsl_valid,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
}
@@ -295,7 +295,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__gen_e_acsl_assert_data_2.pred_txt = "result_ok_or_error: \\result == -1 || \\result >= 0";
__gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/sys/wait.h";
__gen_e_acsl_assert_data_2.fct = "waitpid";
- __gen_e_acsl_assert_data_2.line = 84;
+ __gen_e_acsl_assert_data_2.line = 87;
__e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
@@ -328,7 +328,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__gen_e_acsl_assert_data_3.pred_txt = "initialization: stat_loc_init_on_success:\n \\result >= 0 && \\old(stat_loc) != \\null ==> \\initialized(\\old(stat_loc))";
__gen_e_acsl_assert_data_3.file = "FRAMAC_SHARE/libc/sys/wait.h";
__gen_e_acsl_assert_data_3.fct = "waitpid";
- __gen_e_acsl_assert_data_3.line = 86;
+ __gen_e_acsl_assert_data_3.line = 89;
__e_acsl_assert(__gen_e_acsl_implies,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
__e_acsl_contract_clean(__gen_e_acsl_contract);
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
index 18295663672..9bbf428995a 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
@@ -702,7 +702,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__gen_e_acsl_assert_data.pred_txt = "stat_loc_non_null: valid_stat_loc: \\valid(stat_loc)";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/sys/wait.h";
__gen_e_acsl_assert_data.fct = "waitpid";
- __gen_e_acsl_assert_data.line = 92;
+ __gen_e_acsl_assert_data.line = 95;
__e_acsl_assert(__gen_e_acsl_valid,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
}
@@ -729,7 +729,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__gen_e_acsl_assert_data_2.pred_txt = "result_ok_or_error: \\result == -1 || \\result >= 0";
__gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/sys/wait.h";
__gen_e_acsl_assert_data_2.fct = "waitpid";
- __gen_e_acsl_assert_data_2.line = 84;
+ __gen_e_acsl_assert_data_2.line = 87;
__e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
@@ -762,7 +762,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__gen_e_acsl_assert_data_3.pred_txt = "initialization: stat_loc_init_on_success:\n \\result >= 0 && \\old(stat_loc) != \\null ==> \\initialized(\\old(stat_loc))";
__gen_e_acsl_assert_data_3.file = "FRAMAC_SHARE/libc/sys/wait.h";
__gen_e_acsl_assert_data_3.fct = "waitpid";
- __gen_e_acsl_assert_data_3.line = 86;
+ __gen_e_acsl_assert_data_3.line = 89;
__e_acsl_assert(__gen_e_acsl_implies,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
__e_acsl_contract_clean(__gen_e_acsl_contract);
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
index 3a832d675a1..765767f1d02 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
@@ -242,7 +242,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__gen_e_acsl_assert_data.pred_txt = "stat_loc_non_null: valid_stat_loc: \\valid(stat_loc)";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/sys/wait.h";
__gen_e_acsl_assert_data.fct = "waitpid";
- __gen_e_acsl_assert_data.line = 92;
+ __gen_e_acsl_assert_data.line = 95;
__e_acsl_assert(__gen_e_acsl_valid,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
}
@@ -269,7 +269,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__gen_e_acsl_assert_data_2.pred_txt = "result_ok_or_error: \\result == -1 || \\result >= 0";
__gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/sys/wait.h";
__gen_e_acsl_assert_data_2.fct = "waitpid";
- __gen_e_acsl_assert_data_2.line = 84;
+ __gen_e_acsl_assert_data_2.line = 87;
__e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
@@ -302,7 +302,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__gen_e_acsl_assert_data_3.pred_txt = "initialization: stat_loc_init_on_success:\n \\result >= 0 && \\old(stat_loc) != \\null ==> \\initialized(\\old(stat_loc))";
__gen_e_acsl_assert_data_3.file = "FRAMAC_SHARE/libc/sys/wait.h";
__gen_e_acsl_assert_data_3.fct = "waitpid";
- __gen_e_acsl_assert_data_3.line = 86;
+ __gen_e_acsl_assert_data_3.line = 89;
__e_acsl_assert(__gen_e_acsl_implies,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
__e_acsl_contract_clean(__gen_e_acsl_contract);
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle
index 19dbb447c77..c63be9146f5 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle
@@ -11,10 +11,10 @@
[e-acsl] FRAMAC_SHARE/libc/unistd.h:843: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:79: Warning:
+[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:82: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:86: Warning:
+[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:89: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:470: Warning:
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle
index a8284618e55..c9c93a0901d 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle
@@ -44,10 +44,10 @@
[e-acsl] FRAMAC_SHARE/libc/unistd.h:843: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:79: Warning:
+[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:82: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:86: Warning:
+[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:89: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:470: Warning:
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle
index 247fe7037ee..930d48cf15e 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle
@@ -39,10 +39,10 @@
[e-acsl] FRAMAC_SHARE/libc/unistd.h:843: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:79: Warning:
+[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:82: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:86: Warning:
+[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:89: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:470: Warning:
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle
index 96325fbbbf3..ace2bc58bc2 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle
@@ -42,10 +42,10 @@
[e-acsl] FRAMAC_SHARE/libc/unistd.h:843: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:79: Warning:
+[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:82: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:86: Warning:
+[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:89: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:470: Warning:
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 a33c96cfed6..87d5a40951c 100644
--- a/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
+++ b/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
@@ -17,10 +17,10 @@
[e-acsl] FRAMAC_SHARE/libc/unistd.h:843: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:79: Warning:
+[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:82: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:86: Warning:
+[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:89: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:470: Warning:
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 d13ce9530e4..2326ab5b6bd 100644
--- a/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
+++ b/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
@@ -182,7 +182,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__gen_e_acsl_assert_data.pred_txt = "stat_loc_non_null: valid_stat_loc: \\valid(stat_loc)";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/sys/wait.h";
__gen_e_acsl_assert_data.fct = "waitpid";
- __gen_e_acsl_assert_data.line = 92;
+ __gen_e_acsl_assert_data.line = 95;
__e_acsl_assert(__gen_e_acsl_valid,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
}
@@ -209,7 +209,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__gen_e_acsl_assert_data_2.pred_txt = "result_ok_or_error: \\result == -1 || \\result >= 0";
__gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/sys/wait.h";
__gen_e_acsl_assert_data_2.fct = "waitpid";
- __gen_e_acsl_assert_data_2.line = 84;
+ __gen_e_acsl_assert_data_2.line = 87;
__e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
@@ -242,7 +242,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__gen_e_acsl_assert_data_3.pred_txt = "initialization: stat_loc_init_on_success:\n \\result >= 0 && \\old(stat_loc) != \\null ==> \\initialized(\\old(stat_loc))";
__gen_e_acsl_assert_data_3.file = "FRAMAC_SHARE/libc/sys/wait.h";
__gen_e_acsl_assert_data_3.fct = "waitpid";
- __gen_e_acsl_assert_data_3.line = 86;
+ __gen_e_acsl_assert_data_3.line = 89;
__e_acsl_assert(__gen_e_acsl_implies,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
__e_acsl_contract_clean(__gen_e_acsl_contract);
diff --git a/src/plugins/e-acsl/tests/format/oracle/gen_printf.c b/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
index d9a1a7302c5..1e978e6e597 100644
--- a/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
+++ b/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
@@ -1071,7 +1071,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__gen_e_acsl_assert_data.pred_txt = "stat_loc_non_null: valid_stat_loc: \\valid(stat_loc)";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/sys/wait.h";
__gen_e_acsl_assert_data.fct = "waitpid";
- __gen_e_acsl_assert_data.line = 92;
+ __gen_e_acsl_assert_data.line = 95;
__e_acsl_assert(__gen_e_acsl_valid,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
}
@@ -1098,7 +1098,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__gen_e_acsl_assert_data_2.pred_txt = "result_ok_or_error: \\result == -1 || \\result >= 0";
__gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/sys/wait.h";
__gen_e_acsl_assert_data_2.fct = "waitpid";
- __gen_e_acsl_assert_data_2.line = 84;
+ __gen_e_acsl_assert_data_2.line = 87;
__e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
@@ -1131,7 +1131,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
__gen_e_acsl_assert_data_3.pred_txt = "initialization: stat_loc_init_on_success:\n \\result >= 0 && \\old(stat_loc) != \\null ==> \\initialized(\\old(stat_loc))";
__gen_e_acsl_assert_data_3.file = "FRAMAC_SHARE/libc/sys/wait.h";
__gen_e_acsl_assert_data_3.fct = "waitpid";
- __gen_e_acsl_assert_data_3.line = 86;
+ __gen_e_acsl_assert_data_3.line = 89;
__e_acsl_assert(__gen_e_acsl_implies,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
__e_acsl_contract_clean(__gen_e_acsl_contract);
diff --git a/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle b/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
index 57529e5daac..7cffddb92f5 100644
--- a/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
+++ b/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
@@ -80,10 +80,10 @@
[e-acsl] FRAMAC_SHARE/libc/unistd.h:843: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:79: Warning:
+[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:82: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:86: Warning:
+[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:89: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:470: Warning:
diff --git a/src/plugins/variadic/tests/known/oracle/fcntl.res.oracle b/src/plugins/variadic/tests/known/oracle/fcntl.res.oracle
index 9d0262aed46..79b0b40397e 100644
--- a/src/plugins/variadic/tests/known/oracle/fcntl.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/fcntl.res.oracle
@@ -1,7 +1,7 @@
-[variadic] FRAMAC_SHARE/libc/fcntl.h:118:
+[variadic] FRAMAC_SHARE/libc/fcntl.h:121:
Declaration of variadic function fcntl.
-[variadic] FRAMAC_SHARE/libc/fcntl.h:121: Declaration of variadic function open.
-[variadic] FRAMAC_SHARE/libc/fcntl.h:128:
+[variadic] FRAMAC_SHARE/libc/fcntl.h:124: Declaration of variadic function open.
+[variadic] FRAMAC_SHARE/libc/fcntl.h:131:
Declaration of variadic function openat.
[variadic] fcntl.c:8:
Translating call to the specialized version fcntl(int, int).
diff --git a/src/plugins/variadic/tests/known/oracle/open.res.oracle b/src/plugins/variadic/tests/known/oracle/open.res.oracle
index 5702001954c..ff7c52d67cc 100644
--- a/src/plugins/variadic/tests/known/oracle/open.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/open.res.oracle
@@ -1,7 +1,7 @@
-[variadic] FRAMAC_SHARE/libc/fcntl.h:118:
+[variadic] FRAMAC_SHARE/libc/fcntl.h:121:
Declaration of variadic function fcntl.
-[variadic] FRAMAC_SHARE/libc/fcntl.h:121: Declaration of variadic function open.
-[variadic] FRAMAC_SHARE/libc/fcntl.h:128:
+[variadic] FRAMAC_SHARE/libc/fcntl.h:124: Declaration of variadic function open.
+[variadic] FRAMAC_SHARE/libc/fcntl.h:131:
Declaration of variadic function openat.
[variadic] open.c:7:
Translating call to the specialized version open(char const *, int, mode_t).
diff --git a/src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle b/src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle
index ea5a7b2c332..45d5466519d 100644
--- a/src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle
@@ -1,7 +1,7 @@
-[variadic] FRAMAC_SHARE/libc/fcntl.h:118:
+[variadic] FRAMAC_SHARE/libc/fcntl.h:121:
Declaration of variadic function fcntl.
-[variadic] FRAMAC_SHARE/libc/fcntl.h:121: Declaration of variadic function open.
-[variadic] FRAMAC_SHARE/libc/fcntl.h:128:
+[variadic] FRAMAC_SHARE/libc/fcntl.h:124: Declaration of variadic function open.
+[variadic] FRAMAC_SHARE/libc/fcntl.h:131:
Declaration of variadic function openat.
[variadic] open_wrong.c:13: Warning:
No matching prototype found for this call to open.
diff --git a/src/plugins/variadic/tests/known/oracle/openat.res.oracle b/src/plugins/variadic/tests/known/oracle/openat.res.oracle
index 2c5a0f9da01..9df27b194b9 100644
--- a/src/plugins/variadic/tests/known/oracle/openat.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/openat.res.oracle
@@ -1,7 +1,7 @@
-[variadic] FRAMAC_SHARE/libc/fcntl.h:118:
+[variadic] FRAMAC_SHARE/libc/fcntl.h:121:
Declaration of variadic function fcntl.
-[variadic] FRAMAC_SHARE/libc/fcntl.h:121: Declaration of variadic function open.
-[variadic] FRAMAC_SHARE/libc/fcntl.h:128:
+[variadic] FRAMAC_SHARE/libc/fcntl.h:124: Declaration of variadic function open.
+[variadic] FRAMAC_SHARE/libc/fcntl.h:131:
Declaration of variadic function openat.
[variadic] openat.c:8:
Translating call to the specialized version openat(int, char const *, int, mode_t).
diff --git a/src/plugins/variadic/tests/known/oracle/printf.res.oracle b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
index e6143dde67e..a129b3b58e8 100644
--- a/src/plugins/variadic/tests/known/oracle/printf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
@@ -170,7 +170,6 @@
#include "stdlib.h"
#include "string.h"
#include "strings.h"
-#include "sys/types.h"
#include "time.h"
#include "wchar.h"
/*@ requires valid_read_string(format);
diff --git a/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle
index c966edbc370..813cf4c15be 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle
@@ -47,7 +47,6 @@
#include "stdio.c"
#include "stdio.h"
#include "stdlib.h"
-#include "sys/types.h"
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index eaeeebc57c8..70cedee0a6e 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -4,10 +4,10 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] fc_libc.c:167: assertion got status valid.
-[eva] fc_libc.c:168: assertion got status valid.
[eva] fc_libc.c:169: assertion got status valid.
[eva] fc_libc.c:170: assertion got status valid.
+[eva] fc_libc.c:171: assertion got status valid.
+[eva] fc_libc.c:172: assertion got status valid.
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -64,7 +64,7 @@
wcslen (3 calls); wcsncat (0 call); wcsncpy (0 call); wmemcpy (1 call);
wmemset (0 call);
- Specified-only functions (428)
+ Specified-only functions (427)
==============================
FD_CLR (0 call); FD_ISSET (0 call); FD_SET (0 call); FD_ZERO (0 call);
Frama_C_int_interval (0 call); Frama_C_long_interval (0 call);
@@ -141,17 +141,16 @@
log (0 call); log10 (0 call); log10f (0 call); log10l (0 call);
log2 (0 call); log2f (0 call); log2l (0 call); logf (0 call); logl (0 call);
longjmp (0 call); lrand48 (0 call); lseek (0 call); lstat (0 call);
- makedev (0 call); malloc (13 calls); mblen (0 call); mbstowcs (0 call);
- mbtowc (0 call); mkdir (0 call); mkfifo (0 call); mknod (0 call);
- mkstemp (0 call); mktime (0 call); mrand48 (0 call); nan (0 call);
- nanf (0 call); nanl (0 call); nanosleep (0 call); nrand48 (0 call);
- ntohl (0 call); ntohs (0 call); open (0 call); openat (0 call);
- opendir (0 call); openlog (0 call); pathconf (0 call); pclose (0 call);
- perror (0 call); pipe (0 call); poll (0 call); popen (0 call); pow (0 call);
- powf (0 call); pthread_cond_broadcast (0 call);
- pthread_cond_destroy (0 call); pthread_cond_init (0 call);
- pthread_cond_wait (0 call); pthread_create (0 call);
- pthread_getname_np (0 call); pthread_join (0 call);
+ malloc (13 calls); mblen (0 call); mbstowcs (0 call); mbtowc (0 call);
+ mkdir (0 call); mkfifo (0 call); mknod (0 call); mkstemp (0 call);
+ mktime (0 call); mrand48 (0 call); nan (0 call); nanf (0 call);
+ nanl (0 call); nanosleep (0 call); nrand48 (0 call); ntohl (0 call);
+ ntohs (0 call); open (0 call); openat (0 call); opendir (0 call);
+ openlog (0 call); pathconf (0 call); pclose (0 call); perror (0 call);
+ pipe (0 call); poll (0 call); popen (0 call); pow (0 call); powf (0 call);
+ pthread_cond_broadcast (0 call); pthread_cond_destroy (0 call);
+ pthread_cond_init (0 call); pthread_cond_wait (0 call);
+ pthread_create (0 call); pthread_getname_np (0 call); pthread_join (0 call);
pthread_mutex_destroy (0 call); pthread_mutex_init (0 call);
pthread_mutex_lock (0 call); pthread_mutex_unlock (0 call);
pthread_mutexattr_destroy (0 call); pthread_mutexattr_init (0 call);
@@ -222,7 +221,7 @@
Goto = 118
Assignment = 717
Exit point = 128
- Function = 557
+ Function = 556
Function call = 165
Pointer dereferencing = 350
Cyclomatic complexity = 435
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index c4986b27502..1fe50ce6e10 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -6698,10 +6698,6 @@ ssize_t getline(char **lineptr, size_t *n, FILE *stream);
int asprintf(char **strp, char const *fmt, void * const *__va_params);
-/*@ assigns \result;
- assigns \result \from maj, min; */
-extern dev_t makedev(int maj, int min);
-
FILE __fc_initial_stdout =
{.__fc_FILE_id = (unsigned int)1, .__fc_FILE_data = 0U};
FILE *__fc_stdout = & __fc_initial_stdout;
diff --git a/tests/libc/oracle/fc_libc.2.res.oracle b/tests/libc/oracle/fc_libc.2.res.oracle
index 58fab9624e5..19a092a2d83 100644
--- a/tests/libc/oracle/fc_libc.2.res.oracle
+++ b/tests/libc/oracle/fc_libc.2.res.oracle
@@ -15,6 +15,7 @@
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_intptr_t.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_iovec.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_key_t.h (with preprocessing)
+[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_locale_t.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_max_open_files.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_mode_t.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_nlink_t.h (with preprocessing)
@@ -70,6 +71,7 @@ skipping FRAMAC_SHARE/libc/complex.h
[kernel] Parsing FRAMAC_SHARE/libc/ifaddrs.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/inttypes.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/iso646.h (with preprocessing)
+[kernel] Parsing FRAMAC_SHARE/libc/langinfo.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/libgen.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/limits.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/locale.h (with preprocessing)
diff --git a/tests/libc/oracle/sys_types.res.oracle b/tests/libc/oracle/sys_types.res.oracle
index bd50338df61..43690a9dd32 100644
--- a/tests/libc/oracle/sys_types.res.oracle
+++ b/tests/libc/oracle/sys_types.res.oracle
@@ -4,13 +4,9 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] computing for function makedev <- main.
- Called from sys_types.c:4.
-[eva] using specification for function makedev
-[eva] Done for function makedev
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
- dev ∈ [--..--]
+ dev ∈ {298}
__retres ∈ {0}
--
GitLab