From 8dc15b11a00791cfcd4db7bcad989ddaf64523b8 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Fri, 9 Aug 2019 16:10:53 +0200
Subject: [PATCH] [Libc] fix several specifications
---
share/libc/sys/resource.h | 26 ++++++++++++++++----------
share/libc/sys/time.h | 19 ++++++++++++++-----
share/libc/time.h | 15 +++++++++++----
share/libc/unistd.h | 2 ++
tests/libc/unistd_h.c | 13 +++++++++++++
5 files changed, 56 insertions(+), 19 deletions(-)
diff --git a/share/libc/sys/resource.h b/share/libc/sys/resource.h
index 566a0fa31e8..bcb311cb376 100644
--- a/share/libc/sys/resource.h
+++ b/share/libc/sys/resource.h
@@ -65,21 +65,27 @@ extern int getpriority(int which, id_t who);
/*@ assigns \result \from which,who,prio; */
extern int setpriority(int which, id_t who, int prio);
-/*@ assigns \result \from r;
- @ assigns rl->rlim_cur \from r;
- @ assigns rl->rlim_max \from r;
+/*@
+ requires valid_rlp: \valid(rlp);
+ assigns \result, *rlp \from resource;
*/
-extern int getrlimit(int r, struct rlimit *rl);
+extern int getrlimit(int resource, struct rlimit *rlp);
-/*@ assigns \result \from r;
- @ assigns ru->ru_utime \from r;
- @ assigns ru->ru_stime \from r;
+/*@
+ requires valid_r_usage: \valid(r_usage);
+ assigns *r_usage \from who;
+ assigns \result \from indirect:who;
+ ensures result_ok_or_error: \result == 0 || \result == -1;
*/
-extern int getrusage(int r, struct rusage *ru);
+extern int getrusage(int who, struct rusage *r_usage);
-/*@ assigns \result \from r,rl->rlim_cur,rl->rlim_max;
+/*@
+ requires valid_rlp: \valid_read(rlp);
+ assigns *rlp \from resource;
+ assigns \result \from indirect:resource, indirect:*rlp;
+ ensures result_ok_or_error: \result == 0 || \result == -1;
*/
-extern int setrlimit(int r, const struct rlimit * rl);
+extern int setrlimit(int resource, const struct rlimit *rlp);
__END_DECLS
__POP_FC_STDLIB
diff --git a/share/libc/sys/time.h b/share/libc/sys/time.h
index 426f6376887..15213f4cbb1 100644
--- a/share/libc/sys/time.h
+++ b/share/libc/sys/time.h
@@ -30,6 +30,7 @@ __BEGIN_DECLS
#include "../__fc_define_suseconds_t.h"
#include "../__fc_define_fd_set_t.h"
#include "../__fc_define_timespec.h"
+#include "../__fc_string_axiomatic.h"
struct timeval {
time_t tv_sec;
suseconds_t tv_usec;
@@ -44,7 +45,11 @@ struct timezone {
//@ ghost volatile unsigned int __fc_time __attribute__((FRAMA_C_MODEL));
//@ ghost extern int __fc_tz __attribute__((FRAMA_C_MODEL));
-/*@ assigns \result \from path[0..],times[0..1]; */
+/*@
+ requires valid_path: valid_read_string(path);
+ requires valid_times: \valid_read(times+(0..1));
+ assigns \result \from indirect:path[0..strlen(path)], indirect:times[0..1];
+*/
extern int utimes(const char *path, const struct timeval times[2]);
/*@ assigns tv->tv_sec, tv->tv_usec \from __fc_time;
@@ -83,10 +88,14 @@ extern int utimes(const char *path, const struct timeval times[2]);
@*/
extern int gettimeofday(struct timeval * restrict tv, void * restrict tz);
-/*@ assigns \result,__fc_time,__fc_tz
- @ \from tv->tv_sec, tv->tv_usec,
- @ tz->tz_dsttime, tz->tz_minuteswest;
- @*/
+/*@
+ requires valid_tv_or_null: \valid_read(tv) || tv == \null;
+ requires valid_tz_or_null: \valid_read(tz) || tz == \null;
+ assigns __fc_time, __fc_tz \from tv->tv_sec, tv->tv_usec,
+ tz->tz_dsttime, tz->tz_minuteswest;
+ assigns \result \from indirect:*tv, indirect:*tz;
+ ensures result_ok_or_error: \result == 0 || \result == -1;
+*/
extern int settimeofday(const struct timeval *tv, const struct timezone *tz);
#if (defined _POSIX_C_SOURCE && (_POSIX_C_SOURCE) >= 200112L) || \
diff --git a/share/libc/time.h b/share/libc/time.h
index 52c66700cc8..f0de06cabd8 100644
--- a/share/libc/time.h
+++ b/share/libc/time.h
@@ -86,7 +86,11 @@ extern clock_t clock(void);
/*@ assigns \result \from time1, time0; */
extern double difftime(time_t time1, time_t time0);
-/*@ assigns *timeptr, \result \from *timeptr; */
+/*@
+ requires valid_timeptr: \valid(timeptr);
+ assigns *timeptr \from *timeptr;
+ assigns \result \from indirect:*timeptr;
+ */
extern time_t mktime(struct tm *timeptr);
/*@
@@ -122,14 +126,18 @@ extern char *ctime(const time_t *timer);
struct tm __fc_time_tm;
struct tm * const __fc_p_time_tm = &__fc_time_tm;
-/*@ assigns \result \from __fc_p_time_tm;
+/*@
+ requires valid_timer: \valid_read(timer);
+ assigns \result \from __fc_p_time_tm;
assigns __fc_time_tm \from *timer;
ensures result_null_or_internal_tm:
\result == &__fc_time_tm || \result == \null ;
*/
extern struct tm *gmtime(const time_t *timer);
-/*@ assigns \result \from __fc_p_time_tm;
+/*@
+ requires valid_timer: \valid_read(timer);
+ assigns \result \from __fc_p_time_tm;
assigns __fc_time_tm \from *timer;
ensures result_null_or_internal_tm:
\result == &__fc_time_tm || \result == \null;
@@ -290,7 +298,6 @@ extern int timer_getoverrun(timer_t);
extern int timer_gettime(timer_t, struct itimerspec *);
extern int timer_settime(timer_t, int, const struct itimerspec *restrict,
struct itimerspec *restrict);
-extern void tzset(void);
extern int daylight;
extern long timezone;
diff --git a/share/libc/unistd.h b/share/libc/unistd.h
index 4a8a0455ceb..799cb03c7bd 100644
--- a/share/libc/unistd.h
+++ b/share/libc/unistd.h
@@ -985,6 +985,7 @@ extern long pathconf(char const *path, int name);
extern int pause(void);
/*@
+ requires valid_pipefd: \valid(pipefd+(0..1));
assigns pipefd[0..1] \from indirect:__fc_fds[0..];
assigns \result \from indirect:__fc_fds[0..];
ensures initialization:pipefd: \initialized(&pipefd[0..1]);
@@ -1100,6 +1101,7 @@ volatile char *__fc_p_ttyname = __fc_ttyname;
/*@
// missing: may assign to errno: EBADF, ENOTTY
+ requires valid_fildes: 0 <= fildes < __FC_MAX_OPEN_FILES;
assigns \result \from __fc_p_ttyname, indirect:fildes;
ensures result_name_or_null: \result == __fc_p_ttyname || \result == \null;
*/
diff --git a/tests/libc/unistd_h.c b/tests/libc/unistd_h.c
index b625b3b83d2..8c3104215bf 100644
--- a/tests/libc/unistd_h.c
+++ b/tests/libc/unistd_h.c
@@ -91,5 +91,18 @@ int main() {
r = chroot("/tmp");
+ if (nondet) {
+ pipe(0); // invalid fildes
+ //@ assert unreachable:\false;
+ }
+ int halfpipe;
+ if (nondet) {
+ pipe(&halfpipe); // invalid fildes
+ //@ assert unreachable:\false;
+ }
+ int pipefd[2];
+ r = pipe(pipefd);
+ //@ check ok: r == 0 || r == -1;
+
return 0;
}
--
GitLab