From 48f052b29333a2c65ba16147b82a45cf81f22a90 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Thu, 24 Mar 2022 08:01:47 +0100
Subject: [PATCH] [Libc] improve spec of read
---
share/libc/unistd.h | 16 ++++++++++++++--
tests/libc/unistd_h.c | 16 +++++++++++++---
2 files changed, 27 insertions(+), 5 deletions(-)
diff --git a/share/libc/unistd.h b/share/libc/unistd.h
index f26a5b8ed9b..4842b7958b5 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/tests/libc/unistd_h.c b/tests/libc/unistd_h.c
index 5bb417437e2..a8b8dbba169 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;
}
--
GitLab