diff --git a/share/libc/unistd.h b/share/libc/unistd.h
index f26a5b8ed9b284074e578891a1bd46a8c3d6d20b..4842b7958b5be55538779d46fb59be49aad8e092 100644
--- a/share/libc/unistd.h
+++ b/share/libc/unistd.h
@@ -1009,8 +1009,20 @@ extern ssize_t pwrite(int, const void *, size_t, off_t);
assigns __fc_fds[fd] \from __fc_fds[fd];
assigns \result, *((char *)buf+(0..count-1))
\from indirect:__fc_fds[fd], indirect:count;
- ensures result_error_or_read_length: 0 <= \result <= count || \result == -1;
- ensures initialization:buf: \initialized(((char*)buf)+(0..\result-1));
+ behavior full_read:
+ assumes nondet_small_count: Frama_C_entropy_source && count <= SSIZE_MAX;
+ ensures res_full: \result == count;
+ ensures res_init:initialization: \initialized(((char*)buf)+(0..count-1));
+ behavior large_read_implementation_defined:
+ assumes nondet_large_count: Frama_C_entropy_source && count > SSIZE_MAX;
+ ensures res_init:initialization: \initialized(((char*)buf)+(0..count-1));
+ behavior partial_or_error:
+ assumes nondet: !Frama_C_entropy_source;
+ ensures result_error_or_read_length: -1 <= \result < count;
+ ensures initialization:buf: \initialized(((char*)buf)+(0..\result-1));
+ //note: for \result == -1, the above range is empty, as intended
+ disjoint behaviors;
+ complete behaviors;
*/
extern ssize_t read(int fd, void *buf, size_t count);
diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c b/src/plugins/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c
index ee89abb7fcb4c4457d8d139441afbf78d105cc07..40f13a6bb2b9b8efb37e49b2c6b0a42f3f1fcb91 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c
+++ b/src/plugins/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c
@@ -750,7 +750,7 @@ int __gen_e_acsl_usleep(useconds_t usec)
__gen_e_acsl_assert_data.pred_txt = "\\result == 0 || \\result == -1";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/unistd.h";
__gen_e_acsl_assert_data.fct = "usleep";
- __gen_e_acsl_assert_data.line = 1133;
+ __gen_e_acsl_assert_data.line = 1145;
__gen_e_acsl_assert_data.name = "result_ok_or_error";
__e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_debug.c b/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_debug.c
index 015865844d25becb116a1fef1bd8cfbc986dabe0..4f732c743cec300b6b732d4bc173a952ba3ed750 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_debug.c
+++ b/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_debug.c
@@ -432,7 +432,7 @@ int __gen_e_acsl_usleep(useconds_t usec)
__gen_e_acsl_assert_data.pred_txt = "\\result == 0 || \\result == -1";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/unistd.h";
__gen_e_acsl_assert_data.fct = "usleep";
- __gen_e_acsl_assert_data.line = 1133;
+ __gen_e_acsl_assert_data.line = 1145;
__gen_e_acsl_assert_data.name = "result_ok_or_error";
__e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/parallel_threads.res.oracle b/src/plugins/e-acsl/tests/concurrency/oracle/parallel_threads.res.oracle
index e2c36e496bfdfe3bfea42a54de5cd5d7e96cc934..7ea32d04a840db852dfa49087dfe4c53929d64ae 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/parallel_threads.res.oracle
+++ b/src/plugins/e-acsl/tests/concurrency/oracle/parallel_threads.res.oracle
@@ -35,7 +35,7 @@
[e-acsl] Warning: annotating undefined function `usleep':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-[e-acsl] FRAMAC_SHARE/libc/unistd.h:1130: Warning:
+[e-acsl] FRAMAC_SHARE/libc/unistd.h:1142: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:505: Warning:
@@ -166,6 +166,6 @@
[eva:alarm] FRAMAC_SHARE/libc/pthread.h:316: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/unistd.h:1133: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/unistd.h:1145: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/threads_debug.res.oracle b/src/plugins/e-acsl/tests/concurrency/oracle/threads_debug.res.oracle
index e2c36e496bfdfe3bfea42a54de5cd5d7e96cc934..7ea32d04a840db852dfa49087dfe4c53929d64ae 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/threads_debug.res.oracle
+++ b/src/plugins/e-acsl/tests/concurrency/oracle/threads_debug.res.oracle
@@ -35,7 +35,7 @@
[e-acsl] Warning: annotating undefined function `usleep':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-[e-acsl] FRAMAC_SHARE/libc/unistd.h:1130: Warning:
+[e-acsl] FRAMAC_SHARE/libc/unistd.h:1142: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:505: Warning:
@@ -166,6 +166,6 @@
[eva:alarm] FRAMAC_SHARE/libc/pthread.h:316: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/unistd.h:1133: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/unistd.h:1145: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
diff --git a/src/plugins/value/engine/transfer_logic.ml b/src/plugins/value/engine/transfer_logic.ml
index 634021c6eccb088daea3311546445e8d09afb663..74a8d6d679985101272a63334dc9c6a1bb24a24e 100644
--- a/src/plugins/value/engine/transfer_logic.ml
+++ b/src/plugins/value/engine/transfer_logic.ml
@@ -359,7 +359,7 @@ module Make
| Postcondition (PostLeaf | PostUseSpec) -> true
| _ -> false)
&& pr.pred_content <> Pfalse then
- Self.warning ~once:true ~source
+ Self.warning ~once:true ~source ~wkey:Self.wkey_ensures_false
"@[%a:@ this postcondition@ evaluates to@ false@ in this@ context.\
@ If it is valid,@ either@ a precondition@ was not@ verified@ \
for this@ call%t,@ or some assigns/from@ clauses@ are \
diff --git a/src/plugins/value/self.ml b/src/plugins/value/self.ml
index 84e12b63e791fbc0c4193ff32bc6ca8113e8fdfe..430ed2dfde6c190fe6d58c1fca3c4af01cadfcf1 100644
--- a/src/plugins/value/self.ml
+++ b/src/plugins/value/self.ml
@@ -132,3 +132,4 @@ let wkey_invalid_assigns = register_warn_category "invalid-assigns"
let () = set_warn_status wkey_invalid_assigns Log.Wfeedback
let wkey_experimental = register_warn_category "experimental"
let wkey_unknown_size = register_warn_category "unknown-size"
+let wkey_ensures_false = register_warn_category "ensures-false"
diff --git a/src/plugins/value/self.mli b/src/plugins/value/self.mli
index f975ab4db65c66f3a491aedc74f8b647f0c675b5..97b25ff341643a3f700ffffb5f2fe9a0ab4a8ddb 100644
--- a/src/plugins/value/self.mli
+++ b/src/plugins/value/self.mli
@@ -77,3 +77,4 @@ val wkey_signed_overflow : warn_category
val wkey_invalid_assigns : warn_category
val wkey_experimental : warn_category
val wkey_unknown_size : warn_category
+val wkey_ensures_false : warn_category
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 6ba53d2036b480268f8f925ee06e00879500715d..eb9d4cd87ec5c6171e6fb573668971226b2196c1 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -3222,17 +3222,42 @@ extern int pipe(int pipefd[2]);
/*@ requires valid_fd: 0 ≤ fd < 1024;
requires buf_has_room: \valid((char *)buf + (0 .. count - 1));
- ensures
- result_error_or_read_length:
- (0 ≤ \result ≤ \old(count)) ∨ \result ≡ -1;
- ensures
- initialization: buf:
- \initialized((char *)\old(buf) + (0 .. \result - 1));
assigns __fc_fds[fd], \result, *((char *)buf + (0 .. count - 1));
assigns __fc_fds[fd] \from __fc_fds[fd];
assigns \result \from (indirect: __fc_fds[fd]), (indirect: count);
assigns *((char *)buf + (0 .. count - 1))
\from (indirect: __fc_fds[fd]), (indirect: count);
+
+ behavior full_read:
+ assumes
+ nondet_small_count:
+ Frama_C_entropy_source ≢ 0 ∧ count ≤ 2147483647;
+ ensures res_full: \result ≡ \old(count);
+ ensures
+ res_init: initialization:
+ \initialized((char *)\old(buf) + (0 .. \old(count) - 1));
+
+ behavior large_read_implementation_defined:
+ assumes
+ nondet_large_count:
+ Frama_C_entropy_source ≢ 0 ∧ count > 2147483647;
+ ensures
+ res_init: initialization:
+ \initialized((char *)\old(buf) + (0 .. \old(count) - 1));
+
+ behavior partial_or_error:
+ assumes nondet: Frama_C_entropy_source ≡ 0;
+ ensures result_error_or_read_length: -1 ≤ \result < \old(count);
+ ensures
+ initialization: buf:
+ \initialized((char *)\old(buf) + (0 .. \result - 1));
+
+ complete behaviors partial_or_error,
+ large_read_implementation_defined,
+ full_read;
+ disjoint behaviors partial_or_error,
+ large_read_implementation_defined,
+ full_read;
*/
extern ssize_t read(int fd, void *buf, size_t count);
diff --git a/tests/libc/oracle/socket.0.res.oracle b/tests/libc/oracle/socket.0.res.oracle
index 4acfb213c4bf47fc7efa2270fb213a80678388ba..99635468b5f16ccf760bd70d5fed0ea3c85f3cd9 100644
--- a/tests/libc/oracle/socket.0.res.oracle
+++ b/tests/libc/oracle/socket.0.res.oracle
@@ -50,6 +50,8 @@
[eva] using specification for function read
[eva] socket.c:61: function read: precondition 'valid_fd' got status valid.
[eva] socket.c:61: function read: precondition 'buf_has_room' got status valid.
+[eva] socket.c:61:
+ function read, behavior large_read_implementation_defined: assumes got status invalid; behavior not evaluated.
[eva] Done for function read
[eva] computing for function printf_va_1 <- test_read <- main.
Called from socket.c:62.
@@ -173,6 +175,8 @@
Called from socket.c:115.
[eva] socket.c:115: function read: precondition 'valid_fd' got status valid.
[eva] socket.c:115: function read: precondition 'buf_has_room' got status valid.
+[eva] socket.c:115:
+ function read, behavior large_read_implementation_defined: assumes got status invalid; behavior not evaluated.
[eva] Done for function read
[eva] computing for function write <- test_server_echo <- main.
Called from socket.c:117.
diff --git a/tests/libc/oracle/socket.1.res.oracle b/tests/libc/oracle/socket.1.res.oracle
index 0b2bd9c09e3acafc53c4fcdc3283110c241bc1c4..8f908c607936382b0b3797665fb94079fd895b78 100644
--- a/tests/libc/oracle/socket.1.res.oracle
+++ b/tests/libc/oracle/socket.1.res.oracle
@@ -50,6 +50,8 @@
[eva] using specification for function read
[eva] socket.c:61: function read: precondition 'valid_fd' got status valid.
[eva] socket.c:61: function read: precondition 'buf_has_room' got status valid.
+[eva] socket.c:61:
+ function read, behavior large_read_implementation_defined: assumes got status invalid; behavior not evaluated.
[eva] Done for function read
[eva] computing for function printf_va_1 <- test_read <- main.
Called from socket.c:62.
@@ -173,6 +175,8 @@
Called from socket.c:115.
[eva] socket.c:115: function read: precondition 'valid_fd' got status valid.
[eva] socket.c:115: function read: precondition 'buf_has_room' got status valid.
+[eva] socket.c:115:
+ function read, behavior large_read_implementation_defined: assumes got status invalid; behavior not evaluated.
[eva] Done for function read
[eva] computing for function write <- test_server_echo <- main.
Called from socket.c:117.
diff --git a/tests/libc/oracle/unistd_h.0.res.oracle b/tests/libc/oracle/unistd_h.0.res.oracle
index 2c6070858f6f0ab0c1849eab3272d2ddba7fc3be..69911d84a7244a5f0a797b6dfe46824a5ca3c93b 100644
--- a/tests/libc/oracle/unistd_h.0.res.oracle
+++ b/tests/libc/oracle/unistd_h.0.res.oracle
@@ -11,6 +11,7 @@
\return(isatty) == 0 (auto)
\return(lseek) == -1 (auto)
\return(pipe) == 0 (auto)
+ \return(read) == -1, 32 (auto)
\return(setegid) == 0 (auto)
\return(seteuid) == 0 (auto)
\return(setgid) == 0 (auto)
@@ -564,6 +565,53 @@
Called from unistd_h.c:107.
[eva] Done for function sleep
[eva] unistd_h.c:108: assertion got status valid.
+[eva] computing for function read <- main.
+ Called from unistd_h.c:111.
+[eva] using specification for function read
+[eva] unistd_h.c:111: function read: precondition 'valid_fd' got status valid.
+[eva] unistd_h.c:111:
+ function read: precondition 'buf_has_room' got status valid.
+[eva] Done for function read
+[eva] computing for function read <- main.
+ Called from unistd_h.c:111.
+[eva] Done for function read
+[eva] unistd_h.c:113: assertion got status valid.
+[eva] computing for function read <- main.
+ Called from unistd_h.c:117.
+[eva] unistd_h.c:117: function read: precondition 'valid_fd' got status valid.
+[eva] unistd_h.c:117:
+ function read: precondition 'buf_has_room' got status valid.
+[eva] Done for function read
+[eva] computing for function read <- main.
+ Called from unistd_h.c:117.
+[eva] Done for function read
+[eva] computing for function read <- main.
+ Called from unistd_h.c:118.
+[eva] unistd_h.c:118: function read: precondition 'valid_fd' got status valid.
+[eva] unistd_h.c:118:
+ function read: precondition 'buf_has_room' got status valid.
+[eva] Done for function read
+[eva] computing for function read <- main.
+ Called from unistd_h.c:118.
+[eva] Done for function read
+[eva] computing for function read <- main.
+ Called from unistd_h.c:118.
+[eva] Done for function read
+[eva] computing for function read <- main.
+ Called from unistd_h.c:118.
+[eva] Done for function read
+[eva] computing for function read <- main.
+ Called from unistd_h.c:118.
+[eva] Done for function read
+[eva] computing for function read <- main.
+ Called from unistd_h.c:118.
+[eva] Done for function read
+[eva] computing for function read <- main.
+ Called from unistd_h.c:118.
+[eva] Done for function read
+[eva] computing for function read <- main.
+ Called from unistd_h.c:118.
+[eva] Done for function read
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -591,4 +639,6 @@
halfpipe ∈ UNINITIALIZED
pipefd[0..1] ∈ [0..1023] or UNINITIALIZED
unslept ∈ [0..42]
+ buf[0..4294967294] ∈ [--..--] or UNINITIALIZED
+ rread ∈ [--..--]
__retres ∈ {0; 1}
diff --git a/tests/libc/oracle/unistd_h.1.res.oracle b/tests/libc/oracle/unistd_h.1.res.oracle
index 31219df8042f56171d9fabbbe9c30c8662d4ab4b..85607de98dd75b610ec922e97d6186922ef614cc 100644
--- a/tests/libc/oracle/unistd_h.1.res.oracle
+++ b/tests/libc/oracle/unistd_h.1.res.oracle
@@ -11,6 +11,7 @@
\return(isatty) == 0 (auto)
\return(lseek) == -1 (auto)
\return(pipe) == 0 (auto)
+ \return(read) == -1, 32 (auto)
\return(setegid) == 0 (auto)
\return(seteuid) == 0 (auto)
\return(setgid) == 0 (auto)
@@ -564,6 +565,53 @@
Called from unistd_h.c:107.
[eva] Done for function sleep
[eva] unistd_h.c:108: assertion got status valid.
+[eva] computing for function read <- main.
+ Called from unistd_h.c:111.
+[eva] using specification for function read
+[eva] unistd_h.c:111: function read: precondition 'valid_fd' got status valid.
+[eva] unistd_h.c:111:
+ function read: precondition 'buf_has_room' got status valid.
+[eva] Done for function read
+[eva] computing for function read <- main.
+ Called from unistd_h.c:111.
+[eva] Done for function read
+[eva] unistd_h.c:113: assertion got status valid.
+[eva] computing for function read <- main.
+ Called from unistd_h.c:117.
+[eva] unistd_h.c:117: function read: precondition 'valid_fd' got status valid.
+[eva] unistd_h.c:117:
+ function read: precondition 'buf_has_room' got status valid.
+[eva] Done for function read
+[eva] computing for function read <- main.
+ Called from unistd_h.c:117.
+[eva] Done for function read
+[eva] computing for function read <- main.
+ Called from unistd_h.c:118.
+[eva] unistd_h.c:118: function read: precondition 'valid_fd' got status valid.
+[eva] unistd_h.c:118:
+ function read: precondition 'buf_has_room' got status valid.
+[eva] Done for function read
+[eva] computing for function read <- main.
+ Called from unistd_h.c:118.
+[eva] Done for function read
+[eva] computing for function read <- main.
+ Called from unistd_h.c:118.
+[eva] Done for function read
+[eva] computing for function read <- main.
+ Called from unistd_h.c:118.
+[eva] Done for function read
+[eva] computing for function read <- main.
+ Called from unistd_h.c:118.
+[eva] Done for function read
+[eva] computing for function read <- main.
+ Called from unistd_h.c:118.
+[eva] Done for function read
+[eva] computing for function read <- main.
+ Called from unistd_h.c:118.
+[eva] Done for function read
+[eva] computing for function read <- main.
+ Called from unistd_h.c:118.
+[eva] Done for function read
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -591,4 +639,6 @@
halfpipe ∈ UNINITIALIZED
pipefd[0..1] ∈ [0..1023] or UNINITIALIZED
unslept ∈ [0..42]
+ buf[0..4294967294] ∈ [--..--] or UNINITIALIZED
+ rread ∈ [--..--]
__retres ∈ {0; 1}
diff --git a/tests/libc/unistd_h.c b/tests/libc/unistd_h.c
index 5bb417437e2cf0245e3cc735ab6b8f0b288cef99..a8b8dbba169df6fe6632a2f50137619af62162b1 100644
--- a/tests/libc/unistd_h.c
+++ b/tests/libc/unistd_h.c
@@ -1,11 +1,11 @@
/*run.config
- STDOPT: #"-eva-slevel 12" #"-eva-split-return auto"
- STDOPT: #"-variadic-no-translation" #"-eva-slevel 12" #"-eva-split-return auto"
+ STDOPT: #"-machdep x86_32 -eva-slevel 12" #"-eva-split-return auto"
+ STDOPT: #"-machdep x86_32 -variadic-no-translation" #"-eva-slevel 12" #"-eva-split-return auto"
*/
#define _GNU_SOURCE
#define _XOPEN_SOURCE 600
#include <unistd.h>
-
+#include <stdint.h>
volatile int nondet;
int main() {
@@ -107,5 +107,15 @@ int main() {
int unslept = sleep(42);
//@ assert 0 <= unslept <= 42;
+ char buf[SIZE_MAX];
+ ssize_t rread = read(fd, buf, 32);
+ if (rread == 32) {
+ //@ assert \initialized(buf+(0..31));
+ }
+ if (rread == -1)
+ // In x86-32, SSIZE_MAX < SIZE_MAX, so we check for issues
+ rread = read(fd, buf, SSIZE_MAX);
+ rread = read(fd, buf, SIZE_MAX);
+
return 0;
}
diff --git a/tests/misc/oracle/audit-out.json b/tests/misc/oracle/audit-out.json
index 346565cf549acdf98e4eec25060052a867e100ba..a8b104f9be78dc2ab732dd1655dcd1da30bfa25c 100644
--- a/tests/misc/oracle/audit-out.json
+++ b/tests/misc/oracle/audit-out.json
@@ -38,9 +38,9 @@
"warning-categories": {
"enabled": [
"*", "alarm", "builtins", "builtins:missing-spec",
- "builtins:override", "experimental", "libc", "libc:unsupported-spec",
- "locals-escaping", "loop-unroll", "malloc", "malloc:imprecise",
- "signed-overflow", "taint", "unknown-size"
+ "builtins:override", "ensures-false", "experimental", "libc",
+ "libc:unsupported-spec", "locals-escaping", "loop-unroll", "malloc",
+ "malloc:imprecise", "signed-overflow", "taint", "unknown-size"
],
"disabled": [
"garbled-mix", "invalid-assigns", "loop-unroll:auto",
diff --git a/tests/value/oracle/initialized.res.oracle b/tests/value/oracle/initialized.res.oracle
index 0553f68805ce659b5e8311f2399b6261a5293705..28313721c94409af21b570e0a043955e260d67e3 100644
--- a/tests/value/oracle/initialized.res.oracle
+++ b/tests/value/oracle/initialized.res.oracle
@@ -183,7 +183,7 @@
[eva] computing for function wrong_assigns <- g5 <- main.
Called from initialized.c:127.
[eva] using specification for function wrong_assigns
-[eva] initialized.c:114: Warning:
+[eva:ensures-false] initialized.c:114: Warning:
function wrong_assigns: this postcondition evaluates to false in this
context. If it is valid, either a precondition was not verified for this
call, or some assigns/from clauses are incomplete (or incorrect).
diff --git a/tests/value/oracle/narrow_behaviors.res.oracle b/tests/value/oracle/narrow_behaviors.res.oracle
index c43c26d146781e1eef682d6fd32f623f008a80a3..32fe99abc39f02de30c9f3480ff73dc9abb0f8f7 100644
--- a/tests/value/oracle/narrow_behaviors.res.oracle
+++ b/tests/value/oracle/narrow_behaviors.res.oracle
@@ -105,7 +105,7 @@
function f2, behavior a: assumes got status invalid; behavior not evaluated.
[eva] narrow_behaviors.i:63:
function f2, behavior d: assumes got status invalid; behavior not evaluated.
-[eva] narrow_behaviors.i:43: Warning:
+[eva:ensures-false] narrow_behaviors.i:43: Warning:
function f2, behavior c: this postcondition evaluates to false in this
context. If it is valid, either a precondition was not verified for this
call, or some assigns/from clauses are incomplete (or incorrect).
diff --git a/tests/value/oracle/postcond_leaf.res.oracle b/tests/value/oracle/postcond_leaf.res.oracle
index 0bc230cfbc6bff000ac6d050b6ca3051b54ae5d7..c1b3280dc1fa594d2aa5c84a5c614c21717f71d9 100644
--- a/tests/value/oracle/postcond_leaf.res.oracle
+++ b/tests/value/oracle/postcond_leaf.res.oracle
@@ -8,24 +8,24 @@
[kernel] postcond_leaf.c:109: Warning:
No code nor implicit assigns clause for function f1, generating default assigns from the prototype
[eva] using specification for function f1
-[eva] postcond_leaf.c:21: Warning:
+[eva:ensures-false] postcond_leaf.c:21: Warning:
function f1: this postcondition evaluates to false in this context.
If it is valid, either a precondition was not verified for this call,
or some assigns/from clauses are incomplete (or incorrect).
[eva] using specification for function f2
-[eva] postcond_leaf.c:28: Warning:
+[eva:ensures-false] postcond_leaf.c:28: Warning:
function f2, behavior b: this postcondition evaluates to false in this
context. If it is valid, either a precondition was not verified for this
call, or some assigns/from clauses are incomplete (or incorrect).
[eva] using specification for function f3
[eva] using specification for function f4
[eva] using specification for function g1
-[eva] postcond_leaf.c:46: Warning:
+[eva:ensures-false] postcond_leaf.c:46: Warning:
function g1: this postcondition evaluates to false in this context.
If it is valid, either a precondition was not verified for this call,
or some assigns/from clauses are incomplete (or incorrect).
[eva] using specification for function g2
-[eva] postcond_leaf.c:55: Warning:
+[eva:ensures-false] postcond_leaf.c:55: Warning:
function g2, behavior b: this postcondition evaluates to false in this
context. If it is valid, either a precondition was not verified for this
call, or some assigns/from clauses are incomplete (or incorrect).