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 1c95f09bf73480d5684cfa49940cc34453c8cdbc..4cf7ead5fe4c5ea399386f19cd2578b3b1ce6a88 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 34c9f132beba3a64708f52e4705daee7fb7a92a4..bf3ae7909b3b68131387e61208dc5f328ecf0e20 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 18295663672294403e180049e24654af482ebd96..9bbf428995a5ecd80f66ec3e83d1ab883a221022 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 3a832d675a1e42a186e5034d6a7d03154b7cb5bb..765767f1d025073d70e44ddaac3d731d8506157a 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 19dbb447c775cdf3cef0296249455486845756dc..c63be9146f50355689141c67e84aa8a5bd3673b7 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 a8284618e550daae25f90434b93e89e3e99786e9..c9c93a0901d6ad3ed35316884eb6cf6090c5896f 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 247fe7037ee8d8b4c19af56b986307549d5473f8..930d48cf15e4b7bbcf80d4af2564e9c99fc34e86 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 96325fbbbf3c10a63062b0076067e5fd1e6d8547..ace2bc58bc26deed40f0c82d6d2bf54e4365d4ea 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 a33c96cfed628a46547dc226fafaf172a6a45d8a..87d5a40951cbea3902b5532c1fa6ecea3ab9206f 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 d13ce9530e4af785dd7394dccfb56688d927f257..2326ab5b6bddfe11b47c128f6bb1b5e5b5061306 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 d9a1a7302c53451bf506f1e44ee56fdcf09c9f9f..1e978e6e597763458d73bfa271c2fbcdc23c7fff 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 57529e5daacfc80a51d916f693f84e7d15fdef13..7cffddb92f552e1957e8f4cf02fe661fd5b77ad3 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 9d0262aed46f6d6b2869db34f08acdd4d116a738..79b0b40397ed7b28352584ca5ec8a13ee719d0a6 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 5702001954cb309a157ee842d7cde3c102424758..ff7c52d67ccbab097e52ec13f8fedcfe72369ff6 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 ea5a7b2c33209a57f5432a405582b78bf96e56e4..45d5466519d6cf030ab1d1db40fa0f6daa0a3950 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 2c5a0f9da014e84b2edeeb181838a7a7970e6925..9df27b194b91e66c4de695ee4451cdc078c7fde4 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 e6143dde67e0b9a42e104d3b0b83931442bc25b5..a129b3b58e801edd9676cad89e9d9020598cc59e 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 c966edbc370fcfa9931b8543bdcca3d12deccf87..813cf4c15be5ee6856815cd37365c99e63426633 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 eaeeebc57c865f7366b0125fa9ecd8769abf7639..70cedee0a6ee9fb72b0e614d4a45301771815647 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 c4986b27502f39b78667dc392d8fcf35ccac5af0..1fe50ce6e10ebd88eff2515c39319c876f2f0e17 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 58fab9624e5211f9e3545690c86120ab90421e36..19a092a2d83bdbd6279b2825c8cd7ef4370fd5f7 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 bd50338df61de05aec784e2b28936ef4509bacce..43690a9dd32cb238190785c2661e9ff6248824c1 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}