diff --git a/share/libc/__fc_machdep.h b/share/libc/__fc_machdep.h
index f6f2d7e9a6d71c73f7cc7a786e0f77a6190bce45..55db3e0093ebd50630f313f57cb9a533a9646d1b 100644
--- a/share/libc/__fc_machdep.h
+++ b/share/libc/__fc_machdep.h
@@ -99,6 +99,10 @@
/* POSIX */
#define __SSIZE_T int
#define __SSIZE_MAX __FC_INT_MAX
+/* stdio.h */
+#ifndef __FC_L_tmpnam
+#define __FC_L_tmpnam 1024
+#endif
/* stdint.h */
#define __FC_PTRDIFF_MIN __FC_INT_MIN
#define __FC_PTRDIFF_MAX __FC_INT_MAX
@@ -195,6 +199,10 @@
/* POSIX */
#define __SSIZE_T signed long
#define __SSIZE_MAX __FC_LONG_MAX
+/* stdio.h */
+#ifndef __FC_L_tmpnam
+#define __FC_L_tmpnam 1024
+#endif
/* stdint.h */
#define __FC_PTRDIFF_MIN __FC_LONG_MIN
#define __FC_PTRDIFF_MAX __FC_LONG_MAX
@@ -293,6 +301,10 @@
/* POSIX */
#define __SSIZE_T signed long
#define __SSIZE_MAX __FC_LONG_MAX
+/* stdio.h */
+#ifndef __FC_L_tmpnam
+#define __FC_L_tmpnam 1024
+#endif
/* stdint.h */
#define __FC_PTRDIFF_MIN __FC_LONG_MIN
#define __FC_PTRDIFF_MAX __FC_LONG_MAX
@@ -388,6 +400,10 @@
/* POSIX */
#define __SSIZE_T int
#define __SSIZE_MAX __FC_INT_MAX
+/* stdio.h */
+#ifndef __FC_L_tmpnam
+#define __FC_L_tmpnam 1024
+#endif
/* stdint.h */
#define __FC_PTRDIFF_MIN __FC_INT_MIN
#define __FC_PTRDIFF_MAX __FC_INT_MAX
@@ -558,6 +574,10 @@
/* POSIX */
#define __SSIZE_T signed long long
+/* stdio.h */
+#ifndef __FC_L_tmpnam
+#define __FC_L_tmpnam 20
+#endif
/* stdint.h */
#define __FC_WCHAR_MIN 0
#define __FC_WCHAR_MAX __FC_USHRT_MAX
diff --git a/share/libc/__fc_string_axiomatic.h b/share/libc/__fc_string_axiomatic.h
index a89a527466eacc4412932d441b23dbfbb3817c69..efd4b09bc698630ed51de4c0ae6bdece653e5e11 100644
--- a/share/libc/__fc_string_axiomatic.h
+++ b/share/libc/__fc_string_axiomatic.h
@@ -171,6 +171,21 @@ __BEGIN_DECLS
@ }
@*/
+/*@ axiomatic WMemChr {
+ @ logic 𔹠wmemchr{L}(wchar_t *s, wchar_t c, ℤ n)
+ @ reads s[0..n - 1];
+ @ // Returns [true] iff wide char array [s] contains wide character [c]
+ @
+ @ logic ℤ wmemchr_off{L}(wchar_t *s, wchar_t c, ℤ n)
+ @ reads s[0..n - 1];
+ @ // Returns the offset at which [c] appears in [s].
+ @
+ @ axiom wmemchr_def{L}:
+ @ \forall wchar_t *s; \forall wchar_t c; \forall ℤ n;
+ @ wmemchr(s,c,n) <==> \exists int i; 0 <= i < n && s[i] == c;
+ @ }
+ @*/
+
/*@ axiomatic WcsLen {
@ logic ℤ wcslen{L}(wchar_t *s)
@ reads s[0..];
diff --git a/share/libc/stdio.h b/share/libc/stdio.h
index 9c27119c016ce7fced52dde77b279b8f1db2630b..b571cce1e3e1386dc938692203cfff6d8edc9787 100644
--- a/share/libc/stdio.h
+++ b/share/libc/stdio.h
@@ -44,6 +44,9 @@ __PUSH_FC_STDLIB
#define BUFSIZ __FC_BUFSIZ
#define FOPEN_MAX __FC_FOPEN_MAX
#define FILENAME_MAX __FC_FILENAME_MAX
+#ifndef __FC_L_tmpnam
+#error machdep should have defined __FC_L_tmpnam!
+#endif
#define L_tmpnam __FC_L_tmpnam
#include "__fc_define_seek_macros.h"
@@ -67,10 +70,22 @@ extern FILE * __fc_stdout;
non-interferent between them.
*/
-/*@ assigns \nothing; */
+/*@ // missing: assigns 'filesystem' \from filename[0..];
+ // missing: assigns errno one of several possible values
+ requires valid_filename: valid_read_string(filename);
+ assigns \result \from indirect:filename[0..strlen(filename)];
+ ensures result_ok_or_error: \result == 0 || \result == -1;
+*/
extern int remove(const char *filename);
-/*@ assigns \nothing; */
+/*@ // missing: assigns 'filesystem' \from old_name[0..], new_name[0..];
+ // missing: assigns errno one of 21 different possible values
+ requires valid_old_name: valid_read_string(old_name);
+ requires valid_new_name: valid_read_string(new_name);
+ assigns \result \from indirect:old_name[0..strlen(old_name)],
+ indirect:new_name[0..strlen(new_name)];
+ ensures result_ok_or_error: \result == 0 || \result == -1;
+*/
extern int rename(const char *old_name, const char *new_name);
FILE __fc_fopen[__FC_FOPEN_MAX];
@@ -83,33 +98,59 @@ FILE* const __fc_p_fopen = __fc_fopen;
*/
extern FILE *tmpfile(void);
+char __fc_tmpnam[L_tmpnam];
+char * const __fc_p_tmpnam = __fc_tmpnam;
+
/*@
- assigns \result \from s[..];
- assigns s[..] \from \nothing;
- // TODO: more precise behaviors from ISO C 7.19.4.4
+ // Note: the tmpnam example in POSIX uses an array of size L_tmpnam+1
+ // missing: assigns __fc_p_tmpnam[0..L_tmpnam] \from 'PRNG and internal state'
+ // missing: if called more than TMP_MAX, behavior is implementation-defined
+ requires valid_s_or_null: s == \null || \valid(s+(0 .. L_tmpnam));
+ assigns __fc_p_tmpnam[0 .. L_tmpnam] \from __fc_p_tmpnam[0 .. L_tmpnam],
+ indirect:s;
+ assigns s[0 .. L_tmpnam] \from indirect:s, __fc_p_tmpnam[0 .. L_tmpnam];
+ assigns \result \from s, __fc_p_tmpnam;
+ ensures result_string_or_null: \result == \null || \result == s ||
+ \result == __fc_p_tmpnam;
*/
extern char *tmpnam(char *s);
/*@
+ // missing: assigns errno
requires valid_stream: \valid(stream);
- assigns \result \from stream, stream->__fc_FILE_id;
+ assigns \result \from indirect:stream, indirect:*stream;
ensures result_zero_or_EOF: \result == 0 || \result == EOF;
- // TODO: more precise behaviors from ISO C 7.19.4.1
*/
extern int fclose(FILE *stream);
/*@
+ // missing: assigns errno
requires null_or_valid_stream: stream == \null || \valid_read(stream);
- assigns \result \from stream, stream->__fc_FILE_id;
ensures result_zero_or_EOF: \result == 0 || \result == EOF;
- // TODO: more precise behaviors from ISO C 7.19.5.2
+ assigns \result
+ \from indirect:*stream, indirect:__fc_fopen[0 .. __FC_FOPEN_MAX-1];
+ assigns *stream, __fc_fopen[0 .. __FC_FOPEN_MAX-1]
+ \from indirect:stream, *stream,
+ __fc_fopen[0 .. __FC_FOPEN_MAX-1]; // may flush ALL open streams
+ behavior flush_all:
+ assumes all_streams: stream == \null;
+ assigns __fc_fopen[0 .. __FC_FOPEN_MAX-1]
+ \from __fc_fopen[0 .. __FC_FOPEN_MAX-1]; // flush ALL open streams
+ assigns \result \from indirect:__fc_fopen[0 .. __FC_FOPEN_MAX-1];
+ behavior flush_stream:
+ assumes single_stream: stream != \null;
+ assigns *stream \from *stream;
+ assigns \result \from indirect:*stream;
+ complete behaviors;
+ disjoint behaviors;
*/
extern int fflush(FILE *stream);
/*@
requires valid_filename: valid_read_string(filename);
requires valid_mode: valid_read_string(mode);
- assigns \result \from indirect:filename[..], indirect:mode[..], __fc_p_fopen;
+ assigns \result \from indirect:filename[0..strlen(filename)],
+ indirect:mode[0..strlen(mode)], __fc_p_fopen;
ensures result_null_or_valid_fd:
\result==\null || (\subset(\result,&__fc_fopen[0 .. __FC_FOPEN_MAX-1])) ;
*/
@@ -118,8 +159,9 @@ extern FILE *fopen(const char * restrict filename,
/*@
requires valid_mode: valid_read_string(mode);
- assigns \result, __fc_fopen[fd] \from indirect:fd, indirect:mode[0..],
- indirect:__fc_fopen[fd], __fc_p_fopen;
+ assigns \result, __fc_fopen[fd] \from indirect:fd,
+ indirect:mode[0..strlen(mode)],
+ indirect:__fc_fopen[fd], __fc_p_fopen;
ensures result_null_or_valid_fd:
\result == \null || (\subset(\result,&__fc_fopen[0 .. __FC_FOPEN_MAX-1])) ;
*/
@@ -222,55 +264,97 @@ extern int fgetc(FILE *stream);
/*@
requires valid_stream: \valid(stream);
- assigns s[0..size] \from indirect:size, indirect:*stream;
+ requires room_s: \valid(s+(0..size-1));
+ assigns s[0..size-1] \from indirect:size, indirect:*stream;
assigns \result \from s, indirect:size, indirect:*stream;
ensures result_null_or_same: \result == \null || \result == s;
+ ensures initialization:at_least_one:\result != \null ==> \initialized(&s[0]);
+ // the return value does not tell how many characters were written,
+ // so we can only ensure the first one was initialized
ensures terminated_string_on_success:
\result != \null ==> valid_string(s);
*/
extern char *fgets(char * restrict s, int size,
FILE * restrict stream);
-/*@ assigns *stream ; */
+/*@
+ requires valid_stream: \valid(stream);
+ assigns *stream \from c, *stream;
+ assigns \result \from indirect:*stream;
+*/
extern int fputc(int c, FILE *stream);
-/*@ assigns *stream \from s[..]; */
+/*@
+ requires valid_string_s: valid_read_string(s);
+ assigns *stream \from s[0..strlen(s)], *stream;
+ assigns \result \from indirect:s[0..strlen(s)], indirect:*stream;
+*/
extern int fputs(const char * restrict s,
FILE * restrict stream);
-/*@ assigns \result,*stream \from *stream; */
+/*@
+ requires valid_stream: \valid(stream);
+ assigns \result, *stream \from *stream;
+*/
extern int getc(FILE *stream);
-/*@ assigns \result \from *__fc_stdin ; */
+/*@
+ assigns \result, *__fc_stdin \from *__fc_stdin;
+*/
extern int getchar(void);
+// Number of characters that will read by gets()
+/*@
+ axiomatic GetsLength {
+ logic size_t gets_length{L} reads *__fc_stdin;
+ }
+*/
+
/*@
- assigns s[..] \from *__fc_stdin ;
- assigns \result \from s, __fc_stdin;
+ requires room_s: \valid(s+(0..gets_length));
+ assigns s[0..gets_length] \from *__fc_stdin ;
+ assigns \result \from s, *__fc_stdin;
+ assigns *__fc_stdin \from *__fc_stdin;
ensures result_null_or_same: \result == s || \result == \null;
*/
extern char *gets(char *s);
-/*@ assigns *stream \from c; */
+/*@
+ requires valid_stream: \valid(stream);
+ assigns *stream \from c, *stream;
+ assigns \result \from indirect:*stream;
+*/
extern int putc(int c, FILE *stream);
-/*@ assigns *__fc_stdout \from c; */
+/*@
+ assigns *__fc_stdout \from c, *__fc_stdout;
+ assigns \result \from indirect:*__fc_stdout;
+*/
extern int putchar(int c);
-/*@ assigns *__fc_stdout \from s[..]; */
+/*@
+ requires valid_string_s: valid_read_string(s);
+ assigns *__fc_stdout \from s[0..strlen(s)], *__fc_stdout;
+ assigns \result \from indirect:s[0..strlen(s)], indirect:*__fc_stdout;
+*/
extern int puts(const char *s);
-/*@ assigns *stream \from c; */
+/*@
+ requires valid_stream: \valid(stream);
+ assigns *stream \from indirect:c;
+ assigns \result \from indirect:c, indirect:*stream;
+ ensures result_ok_or_error: \result == c || \result == EOF;
+*/
extern int ungetc(int c, FILE *stream);
/*@
requires valid_ptr_block: \valid(((char*)ptr)+(0..(nmemb*size)-1));
requires valid_stream: \valid(stream);
- assigns *(((char*)ptr)+(0..(nmemb*size)-1)) \from size, nmemb, *stream;
- assigns \result \from size, *stream;
+ assigns *(((char*)ptr)+(0..(nmemb*size)-1)), *stream
+ \from indirect:size, indirect:nmemb, indirect:*stream;
+ assigns \result \from size, indirect:*stream;
ensures size_read: \result <= nmemb;
ensures initialization: \initialized(((char*)ptr)+(0..(\result*size)-1));
- //TODO: specify precise fields from struct FILE
*/
extern size_t fread(void * restrict ptr,
size_t size, size_t nmemb,
@@ -279,15 +363,20 @@ extern size_t fread(void * restrict ptr,
/*@
requires valid_ptr_block: \valid_read(((char*)ptr)+(0..(nmemb*size)-1));
requires valid_stream: \valid(stream);
- assigns *stream, \result \from *(((char*)ptr)+(0..(nmemb*size)-1));
+ assigns *stream, \result \from indirect:*(((char*)ptr)+(0..(nmemb*size)-1));
ensures size_written: \result <= nmemb;
- //TODO: specify precise fields from struct FILE
*/
extern size_t fwrite(const void * restrict ptr,
size_t size, size_t nmemb,
FILE * restrict stream);
-/*@ assigns *pos \from *stream ; */
+/*@
+ requires valid_stream: \valid(stream);
+ requires valid_pos: \valid(pos);
+ requires initialization:pos: \initialized(pos);
+ assigns *pos \from indirect:*stream;
+ assigns \result \from indirect:*stream;
+ */
extern int fgetpos(FILE * restrict stream,
fpos_t * restrict pos);
@@ -300,7 +389,12 @@ extern int fgetpos(FILE * restrict stream,
*/
extern int fseek(FILE *stream, long int offset, int whence);
-/*@ assigns *stream \from *pos; */
+/*@
+ requires valid_stream: \valid(stream);
+ requires valid_pos: \valid_read(pos);
+ requires initialization:pos: \initialized(pos);
+ assigns *stream \from *pos;
+*/
extern int fsetpos(FILE *stream, const fpos_t *pos);
/*@
@@ -311,50 +405,108 @@ extern int fsetpos(FILE *stream, const fpos_t *pos);
*/
extern long int ftell(FILE *stream);
-/*@ assigns *stream \from \nothing; */
+/*@
+ requires valid_stream: \valid(stream);
+ assigns *stream \from \nothing;
+ */
extern void rewind(FILE *stream);
-/*@ assigns *stream \from \nothing; */
+/*@
+ requires valid_stream: \valid(stream);
+ assigns *stream \from \nothing;
+ */
extern void clearerr(FILE *stream);
-/*@ assigns \result \from *stream ;*/
+/*@
+ requires valid_stream: \valid(stream);
+ assigns \result \from indirect:*stream;
+*/
extern int feof(FILE *stream);
-/*@ assigns \result \from *stream ;*/
+/*@
+ requires valid_stream: \valid(stream);
+ assigns \result \from indirect:*stream;
+*/
extern int fileno(FILE *stream);
-/*@ assigns *stream \from \nothing ;*/
+/*@
+ requires valid_stream: \valid(stream);
+ assigns *stream \from \nothing;
+*/
extern void flockfile(FILE *stream);
-/*@ assigns *stream \from \nothing ;*/
+/*@
+ requires valid_stream: \valid(stream);
+ assigns *stream \from \nothing;
+*/
extern void funlockfile(FILE *stream);
-/*@ assigns \result,*stream \from \nothing ;*/
+/*@
+ requires valid_stream: \valid(stream);
+ assigns \result,*stream \from \nothing;
+*/
extern int ftrylockfile(FILE *stream);
-/*@ assigns \result \from *stream ;*/
+/*@
+ requires valid_stream: \valid(stream);
+ assigns \result \from indirect:*stream;
+*/
extern int ferror(FILE *stream);
-/*@ assigns __fc_stdout \from __fc_errno, s[..]; */
+/*@
+ requires valid_string_s: valid_read_string(s);
+ assigns __fc_stdout \from __fc_errno, s[0..strlen(s)];
+ */
extern void perror(const char *s);
-/*@ assigns \result,*stream \from *stream; */
+/*@
+ requires valid_stream: \valid(stream);
+ assigns \result,*stream \from *stream;
+*/
extern int getc_unlocked(FILE *stream);
-/*@ assigns \result \from *__fc_stdin ; */
+
+/*@
+ assigns \result \from *__fc_stdin;
+ */
extern int getchar_unlocked(void);
-/*@ assigns *stream \from c; */
+
+/*@
+ requires valid_stream: \valid(stream);
+ assigns *stream \from c;
+ assigns \result \from indirect:*stream;
+*/
extern int putc_unlocked(int c, FILE *stream);
-/*@ assigns *__fc_stdout \from c; */
+
+/*@
+ assigns *__fc_stdout \from c;
+ assigns \result \from indirect:*__fc_stdout;
+ */
extern int putchar_unlocked(int c);
-/*@ assigns *stream \from \nothing; */
+/*@
+ requires valid_stream: \valid(stream);
+ assigns *stream \from \nothing;
+*/
extern void clearerr_unlocked(FILE *stream);
-/*@ assigns \result \from *stream ;*/
+
+/*@
+ requires valid_stream: \valid(stream);
+ assigns \result \from indirect:*stream;
+*/
extern int feof_unlocked(FILE *stream);
-/*@ assigns \result \from *stream ;*/
+
+/*@
+ requires valid_stream: \valid(stream);
+ assigns \result \from indirect:*stream;
+*/
extern int ferror_unlocked(FILE *stream);
-/*@ assigns \result \from *stream ;*/
+
+/*@
+ requires valid_stream: \valid(stream);
+ assigns \result \from indirect:*stream;
+*/
extern int fileno_unlocked(FILE *stream);
+
extern int fflush_unlocked(FILE *stream);
extern int fgetc_unlocked(FILE *stream);
extern int fputc_unlocked(int c, FILE *stream);
diff --git a/share/libc/sys/resource.h b/share/libc/sys/resource.h
index 566a0fa31e89d69517d1abc749a81056d01f6c07..bcb311cb3768d2207524d2a27044ed02e2196fd7 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 426f637688704543ab931b8ea5d48424d621bdaf..afeb1fb4af0c87f6b6dd097c375672b22c38bb90 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,12 @@ 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_or_null: \valid_read(times+(0..1)) || times == \null;
+ assigns \result \from indirect:path[0..strlen(path)],
+ indirect:times, 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 +89,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 52c66700cc80c3df73b708b8f6a302a30b2d6877..f0de06cabd85307aa0dad4d05dd7122bae3dc630 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 4a8a0455ceb36a581255d0a30a29e4f94a198aba..799cb03c7bdddae9766726300f8c301453cbd31c 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/share/libc/wchar.h b/share/libc/wchar.h
index ff7e863ad8de1e7b5cf5c657bfe7f17d873ceadd..fb07265633362a1736cde59aac0f3f83d1bf365d 100644
--- a/share/libc/wchar.h
+++ b/share/libc/wchar.h
@@ -41,6 +41,8 @@ __PUSH_FC_STDLIB
// ISO C requires the tag 'struct tm' (as declared in <time.h>) to be declared.
#include "time.h"
+#include "string.h"
+
__BEGIN_DECLS
#ifndef WEOF
@@ -48,16 +50,35 @@ __BEGIN_DECLS
#endif
/*@
+ requires valid:
+ valid_read_or_empty((char*)s, (size_t)(sizeof(wchar_t)*n))
+ || \valid_read(((unsigned char*)s)+(0..wmemchr_off(s,c,n)));
+ @ requires initialization:
+ \initialized(s+(0..n - 1))
+ || \initialized(s+(0..wmemchr_off(s,c,n)));
+ @ requires danglingness:
+ non_escaping(s, (size_t)(sizeof(wchar_t)*n))
+ || non_escaping(s, (size_t)(sizeof(wchar_t)*(wmemchr_off(s,c,n)+1)));
assigns \result \from s, indirect:s[0 .. n-1], indirect:c, indirect:n;
ensures result_null_or_inside_s:
\result == \null || \subset (\result, s+(0 .. n-1));
*/
extern wchar_t * wmemchr(const wchar_t *s, wchar_t c, size_t n);
-/*@ assigns \result \from indirect:s1[0 .. n-1], indirect:s2[0 .. n-1], indirect:n; */
+/*@
+ requires valid_s1: valid_read_or_empty(s1, (size_t)(sizeof(wchar_t)*n));
+ requires valid_s2: valid_read_or_empty(s2, (size_t)(sizeof(wchar_t)*n));
+ requires initialization:s1: \initialized(s1+(0..n-1));
+ requires initialization:s2: \initialized(s2+(0..n-1));
+ requires danglingness:s1: non_escaping(s1, (size_t)(sizeof(wchar_t)*n));
+ requires danglingness:s2: non_escaping(s2, (size_t)(sizeof(wchar_t)*n));
+ assigns \result \from indirect:s1[0 .. n-1], indirect:s2[0 .. n-1], indirect:n;
+*/
extern int wmemcmp(const wchar_t *s1, const wchar_t *s2, size_t n);
/*@
+ requires valid_dest: valid_or_empty(dest, (size_t)(sizeof(wchar_t)*n));
+ requires valid_src: valid_read_or_empty(src, (size_t)(sizeof(wchar_t)*n));
requires separation:dest:src: \separated(dest+(0 .. n-1), src+(0 .. n-1));
assigns dest[0 .. n-1] \from src[0 .. n-1], indirect:src, indirect:n;
assigns \result \from dest;
@@ -66,6 +87,8 @@ extern int wmemcmp(const wchar_t *s1, const wchar_t *s2, size_t n);
extern wchar_t * wmemcpy(wchar_t *restrict dest, const wchar_t *restrict src, size_t n);
/*@
+ requires valid_src: \valid_read(src+(0..n-1));
+ requires valid_dest: \valid(dest+(0..n-1));
assigns dest[0 .. n-1] \from src[0 .. n-1], indirect:src, indirect:n;
assigns \result \from dest;
ensures result_ptr: \result == dest;
@@ -73,6 +96,7 @@ extern wchar_t * wmemcpy(wchar_t *restrict dest, const wchar_t *restrict src, si
extern wchar_t * wmemmove(wchar_t *dest, const wchar_t *src, size_t n);
/*@
+ requires valid_wcs: \valid(wcs+(0..n-1));
assigns wcs[0 .. n-1] \from wc, indirect:n;
assigns \result \from wcs;
ensures result_ptr: \result == wcs;
@@ -82,6 +106,10 @@ extern wchar_t * wmemmove(wchar_t *dest, const wchar_t *src, size_t n);
extern wchar_t * wmemset(wchar_t *wcs, wchar_t wc, size_t n);
/*@
+ requires valid_wstring_src: valid_read_wstring(src);
+ requires valid_wstring_dest: valid_wstring(dest);
+ requires room_for_concatenation: \valid(dest+(wcslen(dest)..wcslen(dest)+wcslen(src)));
+ requires separation:\separated(dest+(0..wcslen(dest)+wcslen(src)),src+(0..wcslen(src)));
assigns dest[0 .. ] \from dest[0 .. ], indirect:dest, src[0 .. ], indirect:src;
assigns \result \from dest;
ensures result_ptr: \result == dest;
@@ -96,21 +124,36 @@ extern wchar_t * wcscat(wchar_t *restrict dest, const wchar_t *restrict src);
*/
extern wchar_t * wcschr(const wchar_t *wcs, wchar_t wc);
-/*@ assigns \result \from indirect:s1[0 .. ], indirect:s2[0 .. ]; */
+/*@
+ requires valid_wstring_s1: valid_read_wstring(s1); // over-strong
+ requires valid_wstring_s2: valid_read_wstring(s2); // over-strong
+ assigns \result \from indirect:s1[0 .. ], indirect:s2[0 .. ];
+*/
extern int wcscmp(const wchar_t *s1, const wchar_t *s2);
/*@
- assigns dest[0 .. ] \from src[0 .. ], indirect:src, dest[0 .. ], indirect:dest;
+ requires valid_wstring_src: valid_read_wstring(src);
+ requires room_wstring: \valid(dest+(0 .. wcslen(src)));
+ requires separation:\separated(dest+(0..wcslen(src)),src+(0..wcslen(src)));
+ assigns dest[0 .. wcslen(src)] \from src[0 .. wcslen(src)], indirect:src;
assigns \result \from dest;
ensures result_ptr: \result == dest;
*/
extern wchar_t * wcscpy(wchar_t *restrict dest, const wchar_t *restrict src);
-/*@ assigns \result \from indirect:wcs[0 .. ], indirect:accept[0 .. ]; */
+/*@
+ requires valid_wstring_wcs: valid_read_wstring(wcs);
+ requires valid_wstring_accept: valid_read_wstring(accept);
+ assigns \result \from indirect:wcs[0 .. ], indirect:accept[0 .. ];
+ */
extern size_t wcscspn(const wchar_t *wcs, const wchar_t *accept);
// wcslcat is a BSD extension (non-C99, non-POSIX)
/*@
+ requires valid_nwstring_src: valid_read_nwstring(src, n);
+ requires valid_wstring_dest: valid_wstring(dest);
+ requires room_for_concatenation: \valid(dest+(wcslen(dest)..wcslen(dest)+\min(wcslen(src), n)));
+ requires separation:\separated(dest+(0..wcslen(dest)+wcslen(src)),src+(0..wcslen(src)));
assigns dest[0 .. ] \from dest[0 .. ], indirect:dest, src[0 .. n-1], indirect:src, indirect:n;
assigns \result \from indirect:dest[0 .. ], indirect:src[0 .. n-1], indirect:n;
*/
@@ -118,6 +161,8 @@ extern size_t wcslcat(wchar_t *restrict dest, const wchar_t *restrict src, size_
// wcslcpy is a BSD extension (non-C99, non-POSIX)
/*@
+ requires valid_wstring_src: valid_read_wstring(src);
+ requires room_nwstring: \valid(dest+(0 .. n));
requires separation:dest:src: \separated(dest+(0 .. n-1), src+(0 .. n-1));
assigns dest[0 .. n-1] \from src[0 .. n-1], indirect:src, indirect:n;
assigns \result \from indirect:dest[0 .. n-1], indirect:dest,
@@ -125,29 +170,45 @@ extern size_t wcslcat(wchar_t *restrict dest, const wchar_t *restrict src, size_
*/
extern size_t wcslcpy(wchar_t *dest, const wchar_t *src, size_t n);
-/*@ requires valid_string_s: valid_read_wstring(s);
- assigns \result \from indirect:s[0 .. ]; */
+/*@
+ requires valid_string_s: valid_read_wstring(s);
+ assigns \result \from indirect:s[0 .. wcslen(s)];
+ ensures result_is_length: \result == wcslen(s);
+ */
extern size_t wcslen(const wchar_t *s);
/*@
+ requires valid_nwstring_src: valid_read_nwstring(src, n);
+ requires valid_wstring_dest: valid_wstring(dest);
+ requires room_for_concatenation: \valid(dest+(wcslen(dest)..wcslen(dest)+\min(wcslen(src), n)));
+ requires separation:\separated(dest+(0..wcslen(dest)+wcslen(src)),src+(0..wcslen(src)));
assigns dest[0 .. ] \from dest[0 .. ], indirect:dest, src[0 .. n-1], indirect:src, indirect:n;
assigns \result \from dest;
ensures result_ptr: \result == dest;
*/
extern wchar_t * wcsncat(wchar_t *restrict dest, const wchar_t *restrict src, size_t n);
-/*@ assigns \result \from indirect:s1[0 .. n-1], indirect:s2[0 .. n-1], indirect:n; */
+/*@
+ requires valid_wstring_s1: valid_read_wstring(s1); // over-strong
+ requires valid_wstring_s2: valid_read_wstring(s2); // over-strong
+ assigns \result \from indirect:s1[0 .. n-1], indirect:s2[0 .. n-1], indirect:n;
+*/
extern int wcsncmp(const wchar_t *s1, const wchar_t *s2, size_t n);
/*@
+ requires valid_wstring_src: valid_read_wstring(src);
+ requires room_nwstring: \valid(dest+(0 .. n-1));
requires separation:dest:src: \separated(dest+(0 .. n-1), src+(0 .. n-1));
assigns dest[0 .. n-1] \from src[0 .. n-1], indirect:src, indirect:n;
assigns \result \from dest;
ensures result_ptr: \result == dest;
+ ensures initialization: \initialized(dest+(0 .. n-1));
*/
extern wchar_t * wcsncpy(wchar_t *restrict dest, const wchar_t *restrict src, size_t n);
/*@
+ requires valid_wstring_wcs: valid_read_wstring(wcs);
+ requires valid_wstring_accept: valid_read_wstring(accept);
assigns \result \from wcs, indirect:wcs[0 .. ], indirect:accept[0 .. ];
ensures result_null_or_inside_wcs:
\result == \null || \subset (\result, wcs+(0 .. ));
@@ -155,16 +216,24 @@ extern wchar_t * wcsncpy(wchar_t *restrict dest, const wchar_t *restrict src, si
extern wchar_t * wcspbrk(const wchar_t *wcs, const wchar_t *accept);
/*@
- assigns \result \from wcs, indirect:wcs[0 .. ], indirect:wc;
+ requires valid_wstring_wcs: valid_read_wstring(wcs);
+ assigns \result \from wcs, indirect:wcs[0 .. wcslen(wcs)], indirect:wc;
ensures result_null_or_inside_wcs:
\result == \null || \subset (\result, wcs+(0 .. ));
*/
extern wchar_t * wcsrchr(const wchar_t *wcs, wchar_t wc);
-/*@ assigns \result \from indirect:wcs[0 .. ], indirect:accept[0 .. ]; */
+/*@
+ requires valid_wstring_wcs: valid_read_wstring(wcs);
+ requires valid_wstring_accept: valid_read_wstring(accept);
+ assigns \result \from indirect:wcs[0 .. wcslen(wcs)],
+ indirect:accept[0 .. wcslen(accept)];
+*/
extern size_t wcsspn(const wchar_t *wcs, const wchar_t *accept);
/*@
+ requires valid_wstring_haystack: valid_read_wstring(haystack);
+ requires valid_wstring_needle: valid_read_wstring(needle);
assigns \result \from haystack, indirect:haystack[0 .. ], indirect:needle[0 .. ];
ensures result_null_or_inside_haystack:
\result == \null || \subset (\result, haystack+(0 .. ));
@@ -172,8 +241,9 @@ extern size_t wcsspn(const wchar_t *wcs, const wchar_t *accept);
extern wchar_t * wcsstr(const wchar_t *haystack, const wchar_t *needle);
/*@
+ requires room_nwstring: \valid(ws+(0..n-1));
requires valid_stream: \valid(stream);
- assigns ws[0..n] \from indirect:n, indirect:*stream;
+ assigns ws[0..n-1] \from indirect:n, indirect:*stream;
assigns \result \from ws, indirect:n, indirect:*stream;
ensures result_null_or_same: \result == \null || \result == ws;
ensures terminated_string_on_success:
diff --git a/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle b/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle
index 832567d64f6290b9c371111691b52b65e7c1926c..ebb217fac029c7ecff4322210ffa55295ce48b7d 100644
--- a/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle
+++ b/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle
@@ -1,18 +1,18 @@
-[variadic] FRAMAC_SHARE/libc/stdio.h:165:
+[variadic] FRAMAC_SHARE/libc/stdio.h:207:
Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167:
+[variadic] FRAMAC_SHARE/libc/stdio.h:209:
Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169:
+[variadic] FRAMAC_SHARE/libc/stdio.h:211:
Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170:
+[variadic] FRAMAC_SHARE/libc/stdio.h:212:
Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171:
+[variadic] FRAMAC_SHARE/libc/stdio.h:213:
Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173:
+[variadic] FRAMAC_SHARE/libc/stdio.h:215:
Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175:
+[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369:
+[variadic] FRAMAC_SHARE/libc/stdio.h:521:
Declaration of variadic function dprintf.
[variadic] tests/erroneous/printf.c:8: Warning: Multiple usage of flag '-'.
[variadic] tests/erroneous/printf.c:8: Warning:
diff --git a/src/plugins/variadic/tests/known/oracle/printf.res.oracle b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
index 95d6cf5297f29e539893f37b6ec3b2469440b761..83d6f21822edc4f5972f9e493f12f9c4aac08a1d 100644
--- a/src/plugins/variadic/tests/known/oracle/printf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
@@ -1,30 +1,30 @@
-[variadic] FRAMAC_SHARE/libc/wchar.h:195:
+[variadic] FRAMAC_SHARE/libc/wchar.h:265:
Declaration of variadic function fwprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:197:
+[variadic] FRAMAC_SHARE/libc/wchar.h:267:
Declaration of variadic function swprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:199:
+[variadic] FRAMAC_SHARE/libc/wchar.h:269:
Declaration of variadic function wprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:202:
+[variadic] FRAMAC_SHARE/libc/wchar.h:272:
Declaration of variadic function wscanf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:204:
+[variadic] FRAMAC_SHARE/libc/wchar.h:274:
Declaration of variadic function fwscanf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:206:
+[variadic] FRAMAC_SHARE/libc/wchar.h:276:
Declaration of variadic function swscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:165:
+[variadic] FRAMAC_SHARE/libc/stdio.h:207:
Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167:
+[variadic] FRAMAC_SHARE/libc/stdio.h:209:
Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169:
+[variadic] FRAMAC_SHARE/libc/stdio.h:211:
Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170:
+[variadic] FRAMAC_SHARE/libc/stdio.h:212:
Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171:
+[variadic] FRAMAC_SHARE/libc/stdio.h:213:
Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173:
+[variadic] FRAMAC_SHARE/libc/stdio.h:215:
Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175:
+[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369:
+[variadic] FRAMAC_SHARE/libc/stdio.h:521:
Declaration of variadic function dprintf.
[variadic] tests/known/printf.c:37:
Translating call to printf to a call to the specialized version printf_va_1.
@@ -162,6 +162,8 @@
#include "stdio.c"
#include "stdio.h"
#include "stdlib.h"
+#include "string.h"
+#include "strings.h"
#include "time.h"
#include "wchar.h"
/*@ requires valid_read_string(format);
diff --git a/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
index 25e8c3610196c5963f1c9e911eb1e8f829319bfe..ec9df06d3ed29feb21b4fef6d0321d049ac1d8aa 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
@@ -1,18 +1,18 @@
-[variadic] FRAMAC_SHARE/libc/stdio.h:165:
+[variadic] FRAMAC_SHARE/libc/stdio.h:207:
Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167:
+[variadic] FRAMAC_SHARE/libc/stdio.h:209:
Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169:
+[variadic] FRAMAC_SHARE/libc/stdio.h:211:
Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170:
+[variadic] FRAMAC_SHARE/libc/stdio.h:212:
Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171:
+[variadic] FRAMAC_SHARE/libc/stdio.h:213:
Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173:
+[variadic] FRAMAC_SHARE/libc/stdio.h:215:
Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175:
+[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369:
+[variadic] FRAMAC_SHARE/libc/stdio.h:521:
Declaration of variadic function dprintf.
[variadic] tests/known/printf_garbled_mix.c:8:
Variadic builtin Frama_C_show_each_nb_printed left untransformed.
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 d322a92f77e082966e1f3ba31a4096c403113f6b..f04220bcfaad7d57eea618f3fd406d3c3bf88e24 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
@@ -1,18 +1,18 @@
-[variadic] FRAMAC_SHARE/libc/stdio.h:165:
+[variadic] FRAMAC_SHARE/libc/stdio.h:207:
Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167:
+[variadic] FRAMAC_SHARE/libc/stdio.h:209:
Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169:
+[variadic] FRAMAC_SHARE/libc/stdio.h:211:
Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170:
+[variadic] FRAMAC_SHARE/libc/stdio.h:212:
Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171:
+[variadic] FRAMAC_SHARE/libc/stdio.h:213:
Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173:
+[variadic] FRAMAC_SHARE/libc/stdio.h:215:
Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175:
+[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369:
+[variadic] FRAMAC_SHARE/libc/stdio.h:521:
Declaration of variadic function dprintf.
[variadic] tests/known/printf_wrong_arity.c:8:
Translating call to printf to a call to the specialized version printf_va_1.
diff --git a/src/plugins/variadic/tests/known/oracle/printf_wrong_pointers.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_wrong_pointers.res.oracle
index 12097cda98fa628de6c3431143db25fd7544f16c..48af02448ee3c902d99e1bbda933bbb555bba0aa 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_wrong_pointers.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_wrong_pointers.res.oracle
@@ -1,18 +1,18 @@
-[variadic] FRAMAC_SHARE/libc/stdio.h:165:
+[variadic] FRAMAC_SHARE/libc/stdio.h:207:
Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167:
+[variadic] FRAMAC_SHARE/libc/stdio.h:209:
Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169:
+[variadic] FRAMAC_SHARE/libc/stdio.h:211:
Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170:
+[variadic] FRAMAC_SHARE/libc/stdio.h:212:
Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171:
+[variadic] FRAMAC_SHARE/libc/stdio.h:213:
Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173:
+[variadic] FRAMAC_SHARE/libc/stdio.h:215:
Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175:
+[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369:
+[variadic] FRAMAC_SHARE/libc/stdio.h:521:
Declaration of variadic function dprintf.
[variadic] tests/known/printf_wrong_pointers.c:14:
Translating call to printf to a call to the specialized version printf_va_1.
diff --git a/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle
index 40db9d7dbbf143e9c8ced207fd7ac8ac2ebe8d23..b720645e9345e20e4a5ecb05b2d3e6d7bd35b43f 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle
@@ -1,18 +1,18 @@
-[variadic] FRAMAC_SHARE/libc/stdio.h:165:
+[variadic] FRAMAC_SHARE/libc/stdio.h:207:
Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167:
+[variadic] FRAMAC_SHARE/libc/stdio.h:209:
Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169:
+[variadic] FRAMAC_SHARE/libc/stdio.h:211:
Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170:
+[variadic] FRAMAC_SHARE/libc/stdio.h:212:
Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171:
+[variadic] FRAMAC_SHARE/libc/stdio.h:213:
Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173:
+[variadic] FRAMAC_SHARE/libc/stdio.h:215:
Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175:
+[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369:
+[variadic] FRAMAC_SHARE/libc/stdio.h:521:
Declaration of variadic function dprintf.
[variadic] tests/known/printf_wrong_types.c:18:
Translating call to printf to a call to the specialized version printf_va_1.
@@ -410,21 +410,21 @@ int main(void)
}
-[variadic] FRAMAC_SHARE/libc/stdio.h:165:
+[variadic] FRAMAC_SHARE/libc/stdio.h:207:
Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167:
+[variadic] FRAMAC_SHARE/libc/stdio.h:209:
Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169:
+[variadic] FRAMAC_SHARE/libc/stdio.h:211:
Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170:
+[variadic] FRAMAC_SHARE/libc/stdio.h:212:
Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171:
+[variadic] FRAMAC_SHARE/libc/stdio.h:213:
Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173:
+[variadic] FRAMAC_SHARE/libc/stdio.h:215:
Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175:
+[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369:
+[variadic] FRAMAC_SHARE/libc/stdio.h:521:
Declaration of variadic function dprintf.
[variadic] tests/known/printf_wrong_types.c:18:
Translating call to printf to a call to the specialized version printf_va_1.
diff --git a/src/plugins/variadic/tests/known/oracle/scanf.res.oracle b/src/plugins/variadic/tests/known/oracle/scanf.res.oracle
index 22a8fdf1bb42bb62dcd300c2b8a68f3e8d281426..cd8ae9652f370cfb52d0d3cde3e03835ed894acf 100644
--- a/src/plugins/variadic/tests/known/oracle/scanf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/scanf.res.oracle
@@ -1,18 +1,18 @@
-[variadic] FRAMAC_SHARE/libc/stdio.h:165:
+[variadic] FRAMAC_SHARE/libc/stdio.h:207:
Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167:
+[variadic] FRAMAC_SHARE/libc/stdio.h:209:
Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169:
+[variadic] FRAMAC_SHARE/libc/stdio.h:211:
Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170:
+[variadic] FRAMAC_SHARE/libc/stdio.h:212:
Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171:
+[variadic] FRAMAC_SHARE/libc/stdio.h:213:
Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173:
+[variadic] FRAMAC_SHARE/libc/stdio.h:215:
Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175:
+[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369:
+[variadic] FRAMAC_SHARE/libc/stdio.h:521:
Declaration of variadic function dprintf.
[variadic] tests/known/scanf.c:7:
Translating call to scanf to a call to the specialized version scanf_va_1.
diff --git a/src/plugins/variadic/tests/known/oracle/scanf_loop.res.oracle b/src/plugins/variadic/tests/known/oracle/scanf_loop.res.oracle
index 0a7a3cb2f389a34ab022bcfa82d62fb3908882ef..db959e60948ec7b6831aea0217bbe8f926e20e25 100644
--- a/src/plugins/variadic/tests/known/oracle/scanf_loop.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/scanf_loop.res.oracle
@@ -1,18 +1,18 @@
-[variadic] FRAMAC_SHARE/libc/stdio.h:165:
+[variadic] FRAMAC_SHARE/libc/stdio.h:207:
Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167:
+[variadic] FRAMAC_SHARE/libc/stdio.h:209:
Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169:
+[variadic] FRAMAC_SHARE/libc/stdio.h:211:
Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170:
+[variadic] FRAMAC_SHARE/libc/stdio.h:212:
Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171:
+[variadic] FRAMAC_SHARE/libc/stdio.h:213:
Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173:
+[variadic] FRAMAC_SHARE/libc/stdio.h:215:
Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175:
+[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369:
+[variadic] FRAMAC_SHARE/libc/stdio.h:521:
Declaration of variadic function dprintf.
[variadic] tests/known/scanf_loop.c:6:
Translating call to scanf to a call to the specialized version scanf_va_1.
diff --git a/src/plugins/variadic/tests/known/oracle/scanf_wrong.res.oracle b/src/plugins/variadic/tests/known/oracle/scanf_wrong.res.oracle
index 0ad1522b6520cd7aa591efda0f9f72657c9162b1..b468aea8acafdcac55a9e2c8f2df1e0152df8ea3 100644
--- a/src/plugins/variadic/tests/known/oracle/scanf_wrong.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/scanf_wrong.res.oracle
@@ -1,18 +1,18 @@
-[variadic] FRAMAC_SHARE/libc/stdio.h:165:
+[variadic] FRAMAC_SHARE/libc/stdio.h:207:
Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167:
+[variadic] FRAMAC_SHARE/libc/stdio.h:209:
Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169:
+[variadic] FRAMAC_SHARE/libc/stdio.h:211:
Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170:
+[variadic] FRAMAC_SHARE/libc/stdio.h:212:
Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171:
+[variadic] FRAMAC_SHARE/libc/stdio.h:213:
Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173:
+[variadic] FRAMAC_SHARE/libc/stdio.h:215:
Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175:
+[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369:
+[variadic] FRAMAC_SHARE/libc/stdio.h:521:
Declaration of variadic function dprintf.
[variadic] tests/known/scanf_wrong.c:8:
Translating call to scanf to a call to the specialized version scanf_va_1.
diff --git a/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle b/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle
index cf8814488a75dd118d8e8abac81f3bab09ad9baa..2b2dd3e7684dc91bc32669a14ae8cb0c8bfb8435 100644
--- a/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle
@@ -1,18 +1,18 @@
-[variadic] FRAMAC_SHARE/libc/stdio.h:165:
+[variadic] FRAMAC_SHARE/libc/stdio.h:207:
Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167:
+[variadic] FRAMAC_SHARE/libc/stdio.h:209:
Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169:
+[variadic] FRAMAC_SHARE/libc/stdio.h:211:
Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170:
+[variadic] FRAMAC_SHARE/libc/stdio.h:212:
Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171:
+[variadic] FRAMAC_SHARE/libc/stdio.h:213:
Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173:
+[variadic] FRAMAC_SHARE/libc/stdio.h:215:
Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175:
+[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369:
+[variadic] FRAMAC_SHARE/libc/stdio.h:521:
Declaration of variadic function dprintf.
[variadic] tests/known/snprintf.c:12:
Translating call to snprintf to a call to the specialized version snprintf_va_1.
diff --git a/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle b/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle
index 41f785ff02c2f035754f6d27cb48445c435a0f04..0cacefc0330324049f21defc8287bd88133d15c7 100644
--- a/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle
@@ -1,18 +1,18 @@
-[variadic] FRAMAC_SHARE/libc/stdio.h:165:
+[variadic] FRAMAC_SHARE/libc/stdio.h:207:
Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167:
+[variadic] FRAMAC_SHARE/libc/stdio.h:209:
Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169:
+[variadic] FRAMAC_SHARE/libc/stdio.h:211:
Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170:
+[variadic] FRAMAC_SHARE/libc/stdio.h:212:
Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171:
+[variadic] FRAMAC_SHARE/libc/stdio.h:213:
Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173:
+[variadic] FRAMAC_SHARE/libc/stdio.h:215:
Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175:
+[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369:
+[variadic] FRAMAC_SHARE/libc/stdio.h:521:
Declaration of variadic function dprintf.
[variadic] tests/known/stdio_print.c:9: Warning:
Call to function fprintf with non-static format argument:
diff --git a/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle b/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle
index 23148c803852e714e6e6460bbb3584c014a6662f..671f5bf3f3583974376171a38a07521abc4f5cca 100644
--- a/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle
@@ -1,18 +1,18 @@
-[variadic] FRAMAC_SHARE/libc/stdio.h:165:
+[variadic] FRAMAC_SHARE/libc/stdio.h:207:
Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167:
+[variadic] FRAMAC_SHARE/libc/stdio.h:209:
Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169:
+[variadic] FRAMAC_SHARE/libc/stdio.h:211:
Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170:
+[variadic] FRAMAC_SHARE/libc/stdio.h:212:
Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171:
+[variadic] FRAMAC_SHARE/libc/stdio.h:213:
Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173:
+[variadic] FRAMAC_SHARE/libc/stdio.h:215:
Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175:
+[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369:
+[variadic] FRAMAC_SHARE/libc/stdio.h:521:
Declaration of variadic function dprintf.
[variadic] tests/known/stdio_scan.c:10: Warning:
Call to function fscanf with non-static format argument:
diff --git a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle b/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
index f4694f2f3632e5e0d4fdbcdf9ef2ef527a077e69..79025ff0d26ed6ef5e13f3c3ab32bf758d978cae 100644
--- a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
@@ -1,30 +1,30 @@
-[variadic] FRAMAC_SHARE/libc/wchar.h:195:
+[variadic] FRAMAC_SHARE/libc/wchar.h:265:
Declaration of variadic function fwprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:197:
+[variadic] FRAMAC_SHARE/libc/wchar.h:267:
Declaration of variadic function swprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:199:
+[variadic] FRAMAC_SHARE/libc/wchar.h:269:
Declaration of variadic function wprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:202:
+[variadic] FRAMAC_SHARE/libc/wchar.h:272:
Declaration of variadic function wscanf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:204:
+[variadic] FRAMAC_SHARE/libc/wchar.h:274:
Declaration of variadic function fwscanf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:206:
+[variadic] FRAMAC_SHARE/libc/wchar.h:276:
Declaration of variadic function swscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:165:
+[variadic] FRAMAC_SHARE/libc/stdio.h:207:
Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167:
+[variadic] FRAMAC_SHARE/libc/stdio.h:209:
Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169:
+[variadic] FRAMAC_SHARE/libc/stdio.h:211:
Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170:
+[variadic] FRAMAC_SHARE/libc/stdio.h:212:
Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171:
+[variadic] FRAMAC_SHARE/libc/stdio.h:213:
Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173:
+[variadic] FRAMAC_SHARE/libc/stdio.h:215:
Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175:
+[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369:
+[variadic] FRAMAC_SHARE/libc/stdio.h:521:
Declaration of variadic function dprintf.
[variadic] tests/known/swprintf.c:12:
Translating call to swprintf to a call to the specialized version swprintf_va_1.
@@ -57,6 +57,8 @@
#include "signal.h"
#include "stdarg.h"
#include "stdio.h"
+#include "string.h"
+#include "strings.h"
#include "time.h"
#include "wchar.h"
int volatile nondet;
diff --git a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle b/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
index a5376947d85456fcb47acfbcc4979db23dd1eb7a..0e93065e23f4b5b463c55d01b9ba31a7d3e0f759 100644
--- a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
@@ -1,30 +1,30 @@
-[variadic] FRAMAC_SHARE/libc/wchar.h:195:
+[variadic] FRAMAC_SHARE/libc/wchar.h:265:
Declaration of variadic function fwprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:197:
+[variadic] FRAMAC_SHARE/libc/wchar.h:267:
Declaration of variadic function swprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:199:
+[variadic] FRAMAC_SHARE/libc/wchar.h:269:
Declaration of variadic function wprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:202:
+[variadic] FRAMAC_SHARE/libc/wchar.h:272:
Declaration of variadic function wscanf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:204:
+[variadic] FRAMAC_SHARE/libc/wchar.h:274:
Declaration of variadic function fwscanf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:206:
+[variadic] FRAMAC_SHARE/libc/wchar.h:276:
Declaration of variadic function swscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:165:
+[variadic] FRAMAC_SHARE/libc/stdio.h:207:
Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167:
+[variadic] FRAMAC_SHARE/libc/stdio.h:209:
Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169:
+[variadic] FRAMAC_SHARE/libc/stdio.h:211:
Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170:
+[variadic] FRAMAC_SHARE/libc/stdio.h:212:
Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171:
+[variadic] FRAMAC_SHARE/libc/stdio.h:213:
Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173:
+[variadic] FRAMAC_SHARE/libc/stdio.h:215:
Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175:
+[variadic] FRAMAC_SHARE/libc/stdio.h:217:
Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369:
+[variadic] FRAMAC_SHARE/libc/stdio.h:521:
Declaration of variadic function dprintf.
[variadic] tests/known/wchar.c:11:
Translating call to wprintf to a call to the specialized version wprintf_va_1.
@@ -86,6 +86,8 @@
#include "signal.h"
#include "stdarg.h"
#include "stdio.h"
+#include "string.h"
+#include "strings.h"
#include "time.h"
#include "wchar.h"
/*@ requires valid_read_wstring(format);
diff --git a/tests/builtins/oracle/linked_list.0.res.oracle b/tests/builtins/oracle/linked_list.0.res.oracle
index a720cea4364ad8be5ec34cc894fc4c0c6c6b63a0..7edb0dc61aa38f4ca9fa5dd58d0b5404bc3a30ec 100644
--- a/tests/builtins/oracle/linked_list.0.res.oracle
+++ b/tests/builtins/oracle/linked_list.0.res.oracle
@@ -15,6 +15,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..2047] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
@@ -55,6 +57,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..2047] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
@@ -91,6 +95,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..2047] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
@@ -130,6 +136,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..2047] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
@@ -168,6 +176,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..2047] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
@@ -210,6 +220,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..2047] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
@@ -250,6 +262,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..2047] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
@@ -294,6 +308,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..2047] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
@@ -336,6 +352,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..2047] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
@@ -382,6 +400,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..2047] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
@@ -426,6 +446,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..2047] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
@@ -474,6 +496,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..2047] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
@@ -765,6 +789,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..2047] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
@@ -1058,6 +1084,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..2047] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
diff --git a/tests/builtins/oracle/linked_list.1.res.oracle b/tests/builtins/oracle/linked_list.1.res.oracle
index 67b3d10651f9e9d8f7d950db2f0cc401ee64c0bf..58a095a29ca9923f3349863a3f663a973737095e 100644
--- a/tests/builtins/oracle/linked_list.1.res.oracle
+++ b/tests/builtins/oracle/linked_list.1.res.oracle
@@ -15,6 +15,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -55,6 +57,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -91,6 +95,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -130,6 +136,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -168,6 +176,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -210,6 +220,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -250,6 +262,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -294,6 +308,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -336,6 +352,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -382,6 +400,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -427,6 +447,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -476,6 +498,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -519,6 +543,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -560,6 +586,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
diff --git a/tests/builtins/oracle/linked_list.2.res.oracle b/tests/builtins/oracle/linked_list.2.res.oracle
index 4687366532f8f130442769db11f45930b3d4ec6e..b893ef1a658089db5f2be138b4391460dc1624ea 100644
--- a/tests/builtins/oracle/linked_list.2.res.oracle
+++ b/tests/builtins/oracle/linked_list.2.res.oracle
@@ -15,6 +15,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -55,6 +57,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -90,6 +94,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -129,6 +135,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -167,6 +175,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -209,6 +219,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -249,6 +261,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -293,6 +307,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -335,6 +351,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -381,6 +399,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -425,6 +445,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -473,6 +495,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -519,6 +543,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -569,6 +595,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -617,6 +645,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -669,6 +699,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -719,6 +751,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -773,6 +807,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -825,6 +861,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
@@ -881,6 +919,8 @@
__fc_stdout ∈ {{ &__fc_initial_stdout }}
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
__fc_heap_status ∈ [--..--]
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {0x7FFF}
diff --git a/tests/builtins/oracle/memcpy.res.oracle b/tests/builtins/oracle/memcpy.res.oracle
index 630d2219ba4794e3763ba8e70b88cedb13ad48b3..9deb0bc5e01c04aaea0bbf5178f55316e8f09166 100644
--- a/tests/builtins/oracle/memcpy.res.oracle
+++ b/tests/builtins/oracle/memcpy.res.oracle
@@ -1055,6 +1055,8 @@
Unverifiable but considered Valid.
[ Extern ] Axiom 'wcsncmp_zero'
Unverifiable but considered Valid.
+[ Extern ] Axiom 'wmemchr_def'
+ Unverifiable but considered Valid.
[ Valid ] Axiomatic 'MemChr'
by Frama-C kernel.
[ Valid ] Axiomatic 'MemCmp'
@@ -1069,6 +1071,8 @@
by Frama-C kernel.
[ Valid ] Axiomatic 'StrNCmp'
by Frama-C kernel.
+[ Valid ] Axiomatic 'WMemChr'
+ by Frama-C kernel.
[ Valid ] Axiomatic 'WcsChr'
by Frama-C kernel.
[ Valid ] Axiomatic 'WcsCmp'
@@ -2216,9 +2220,9 @@
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
- 161 Completely validated
- 238 Considered valid
+ 162 Completely validated
+ 239 Considered valid
29 To be validated
4 Alarms emitted
- 432 Total
+ 434 Total
--------------------------------------------------------------------------------
diff --git a/tests/builtins/oracle/wcslen.res.oracle b/tests/builtins/oracle/wcslen.res.oracle
index 95f2548751afd2e5be3566ba103027f089417ec5..f5a97cc85744af051d76551bd0250596ac7f074f 100644
--- a/tests/builtins/oracle/wcslen.res.oracle
+++ b/tests/builtins/oracle/wcslen.res.oracle
@@ -618,7 +618,7 @@
[inout] Inputs for function misc:
Frama_C_entropy_source; static_str; zero_str; tab_str[0..11];
unterminated_string[0..11]; nondet; L"Hello World\n"[bits 0 to 415];
- L"abc\000\000\000abc"[bits 0 to 319]; L""; L"a"[bits 0 to 63];
+ L"abc\000\000\000abc"[bits 0 to 127]; L""; L"a"[bits 0 to 63];
L"aa"[bits 0 to 95]; L"aaa"[bits 0 to 127]; L"aaaa"[bits 0 to 159];
L"aaaaa"[bits 0 to 191]; L"aaaaaa"[bits 0 to 223];
L"aaaaaaaaa"[bits 0 to 319]; L"aaaaaaaaaa"[bits 0 to 351];
@@ -662,7 +662,7 @@
[inout] Inputs for function main:
Frama_C_entropy_source; static_str; zero_str; tab_str[0..11];
unterminated_string[0..11]; nondet; L"Hello World\n"[bits 0 to 415];
- L"abc\000\000\000abc"[bits 0 to 319]; L""; L"a"[bits 0 to 63];
+ L"abc\000\000\000abc"[bits 0 to 127]; L""; L"a"[bits 0 to 63];
L"aa"[bits 0 to 95]; L"aaa"[bits 0 to 127]; L"aaaa"[bits 0 to 159];
L"aaaaa"[bits 0 to 191]; L"aaaaaa"[bits 0 to 223];
L"aaaaaaaaa"[bits 0 to 319]; L"aaaaaaaaaa"[bits 0 to 351];
diff --git a/tests/idct/oracle/ieee_1180_1990.res.oracle b/tests/idct/oracle/ieee_1180_1990.res.oracle
index 56319e5d1845473862f9cb775b4515dc3ab93f09..1b12533c9f8de027acbe4871855f4d283b89627f 100644
--- a/tests/idct/oracle/ieee_1180_1990.res.oracle
+++ b/tests/idct/oracle/ieee_1180_1990.res.oracle
@@ -1223,6 +1223,12 @@
[ Extern ] Axiom 'wcsncmp_zero'
axiom wcsncmp_zero
Unverifiable but considered Valid.
+[ Extern ] Axiom 'wmemchr_def'
+ axiom wmemchr_def
+ Unverifiable but considered Valid.
+[ Valid ] Axiomatic 'GetsLength'
+ axiomatic GetsLength
+ by Frama-C kernel.
[ Valid ] Axiomatic 'MemChr'
axiomatic MemChr
by Frama-C kernel.
@@ -1244,6 +1250,9 @@
[ Valid ] Axiomatic 'StrNCmp'
axiomatic StrNCmp
by Frama-C kernel.
+[ Valid ] Axiomatic 'WMemChr'
+ axiomatic WMemChr
+ by Frama-C kernel.
[ Valid ] Axiomatic 'WcsChr'
axiomatic WcsChr
by Frama-C kernel.
@@ -1267,9 +1276,16 @@
--- Properties of Function 'remove'
--------------------------------------------------------------------------------
+[ Extern ] Post-condition 'result_ok_or_error'
+ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1
+ Unverifiable but considered Valid.
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 76)
+ assigns \result
+ \from (indirect: *(filename + (0 .. strlen{Old}(filename))));
+ Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
by Frama-C kernel.
@@ -1278,9 +1294,17 @@
--- Properties of Function 'rename'
--------------------------------------------------------------------------------
+[ Extern ] Post-condition 'result_ok_or_error'
+ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1
+ Unverifiable but considered Valid.
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 85)
+ assigns \result
+ \from (indirect: *(old_name + (0 .. strlen{Old}(old_name)))),
+ (indirect: *(new_name + (0 .. strlen{Old}(new_name))));
+ Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
by Frama-C kernel.
@@ -1298,7 +1322,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 80)
+[ Extern ] Froms (file share/libc/stdio.h, line 95)
assigns \result \from __fc_p_fopen;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1309,14 +1333,26 @@
--- Properties of Function 'tmpnam'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 87)
- assigns \result, *(s + (..));
+[ Extern ] Post-condition 'result_string_or_null'
+ ensures
+ result_string_or_null:
+ \result ≡ \null ∨ \result ≡ \old(s) ∨
+ \result ≡ __fc_p_tmpnam
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/stdio.h, line 109)
+ assigns *(__fc_p_tmpnam + (0 .. 2048)), *(s + (0 .. 2048)),
+ \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 87)
- assigns \result \from *(s + (..));
+[ Extern ] Froms (file share/libc/stdio.h, line 109)
+ assigns *(__fc_p_tmpnam + (0 .. 2048))
+ \from *(__fc_p_tmpnam + (0 .. 2048)), (indirect: s);
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 88)
- assigns *(s + (..)) \from \nothing;
+[ Extern ] Froms (file share/libc/stdio.h, line 111)
+ assigns *(s + (0 .. 2048))
+ \from (indirect: s), *(__fc_p_tmpnam + (0 .. 2048));
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 112)
+ assigns \result \from s, __fc_p_tmpnam;
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
@@ -1332,8 +1368,8 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 95)
- assigns \result \from stream, stream->__fc_FILE_id;
+[ Extern ] Froms (file share/libc/stdio.h, line 121)
+ assigns \result \from (indirect: stream), (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
@@ -1346,15 +1382,48 @@
[ Extern ] Post-condition 'result_zero_or_EOF'
ensures result_zero_or_EOF: \result ≡ 0 ∨ \result ≡ -1
Unverifiable but considered Valid.
-[ Extern ] Assigns nothing
- assigns \nothing;
+[ Extern ] Assigns (file share/libc/stdio.h, line 130)
+ assigns \result, *stream, __fc_fopen[0 .. 16 - 1];
+ Unverifiable but considered Valid.
+[ Extern ] Assigns for 'flush_all' (file share/libc/stdio.h, line 137)
+ assigns __fc_fopen[0 .. 16 - 1], \result;
+ Unverifiable but considered Valid.
+[ Extern ] Assigns for 'flush_stream' (file share/libc/stdio.h, line 142)
+ assigns *stream, \result;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 130)
+ assigns \result
+ \from (indirect: *stream), (indirect: __fc_fopen[0 .. 16 - 1]);
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 103)
- assigns \result \from stream, stream->__fc_FILE_id;
+[ Extern ] Froms (file share/libc/stdio.h, line 132)
+ assigns *stream
+ \from (indirect: stream), *stream, __fc_fopen[0 .. 16 - 1];
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 132)
+ assigns __fc_fopen[0 .. 16 - 1]
+ \from (indirect: stream), *stream, __fc_fopen[0 .. 16 - 1];
+ Unverifiable but considered Valid.
+[ Extern ] Froms for 'flush_all' (file share/libc/stdio.h, line 137)
+ assigns __fc_fopen[0 .. 16 - 1] \from __fc_fopen[0 .. 16 - 1];
+ Unverifiable but considered Valid.
+[ Extern ] Froms for 'flush_all' (file share/libc/stdio.h, line 139)
+ assigns \result \from (indirect: __fc_fopen[0 .. 16 - 1]);
+ Unverifiable but considered Valid.
+[ Extern ] Froms for 'flush_stream' (file share/libc/stdio.h, line 142)
+ assigns *stream \from *stream;
+ Unverifiable but considered Valid.
+[ Extern ] Froms for 'flush_stream' (file share/libc/stdio.h, line 143)
+ assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
by Frama-C kernel.
+[ Valid ] Behavior 'flush_all'
+ behavior flush_all
+ by Frama-C kernel.
+[ Valid ] Behavior 'flush_stream'
+ behavior flush_stream
+ by Frama-C kernel.
--------------------------------------------------------------------------------
--- Properties of Function 'fopen'
@@ -1369,10 +1438,11 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 112)
+[ Extern ] Froms (file share/libc/stdio.h, line 152)
assigns \result
- \from (indirect: *(filename + (..))),
- (indirect: *(mode + (..))), __fc_p_fopen;
+ \from (indirect: *(filename + (0 .. strlen{Old}(filename)))),
+ (indirect: *(mode + (0 .. strlen{Old}(mode)))),
+ __fc_p_fopen;
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
@@ -1388,17 +1458,19 @@
\result ≡ \null ∨
\subset(\result, &__fc_fopen[0 .. 16 - 1])
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 121)
+[ Extern ] Assigns (file share/libc/stdio.h, line 162)
assigns \result, __fc_fopen[fd];
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 121)
+[ Extern ] Froms (file share/libc/stdio.h, line 162)
assigns \result
- \from (indirect: fd), (indirect: *(mode + (0 ..))),
+ \from (indirect: fd),
+ (indirect: *(mode + (0 .. strlen{Old}(mode)))),
(indirect: __fc_fopen[fd]), __fc_p_fopen;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 121)
+[ Extern ] Froms (file share/libc/stdio.h, line 162)
assigns __fc_fopen[fd]
- \from (indirect: fd), (indirect: *(mode + (0 ..))),
+ \from (indirect: fd),
+ (indirect: *(mode + (0 .. strlen{Old}(mode)))),
(indirect: __fc_fopen[fd]), __fc_p_fopen;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1417,16 +1489,16 @@
[ Extern ] Post-condition 'stream_opened'
ensures stream_opened: *\old(stream) ∈ __fc_fopen[0 .. 16 - 1]
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 132)
+[ Extern ] Assigns (file share/libc/stdio.h, line 174)
assigns \result, *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 132)
+[ Extern ] Froms (file share/libc/stdio.h, line 174)
assigns \result
\from (indirect: *(filename + (..))),
(indirect: *(mode + (..))), __fc_p_fopen,
(indirect: stream);
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 134)
+[ Extern ] Froms (file share/libc/stdio.h, line 176)
assigns *stream
\from (indirect: *(filename + (..))),
(indirect: *(mode + (..))), __fc_p_fopen,
@@ -1440,10 +1512,10 @@
--- Properties of Function 'setbuf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 145)
+[ Extern ] Assigns (file share/libc/stdio.h, line 187)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 145)
+[ Extern ] Froms (file share/libc/stdio.h, line 187)
assigns *stream \from buf;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1454,10 +1526,10 @@
--- Properties of Function 'setvbuf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 149)
+[ Extern ] Assigns (file share/libc/stdio.h, line 191)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 149)
+[ Extern ] Froms (file share/libc/stdio.h, line 191)
assigns *stream \from buf, mode, size;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1468,10 +1540,10 @@
--- Properties of Function 'vfprintf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 178)
+[ Extern ] Assigns (file share/libc/stdio.h, line 220)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 178)
+[ Extern ] Froms (file share/libc/stdio.h, line 220)
assigns *stream \from *(format + (..)), arg;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1482,10 +1554,10 @@
--- Properties of Function 'vfscanf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 183)
+[ Extern ] Assigns (file share/libc/stdio.h, line 225)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 183)
+[ Extern ] Froms (file share/libc/stdio.h, line 225)
assigns *stream \from *(format + (..)), *stream;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1496,10 +1568,10 @@
--- Properties of Function 'vprintf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 189)
+[ Extern ] Assigns (file share/libc/stdio.h, line 231)
assigns *__fc_stdout;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 189)
+[ Extern ] Froms (file share/libc/stdio.h, line 231)
assigns *__fc_stdout \from arg;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1510,10 +1582,10 @@
--- Properties of Function 'vscanf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 193)
+[ Extern ] Assigns (file share/libc/stdio.h, line 235)
assigns *__fc_stdin;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 193)
+[ Extern ] Froms (file share/libc/stdio.h, line 235)
assigns *__fc_stdin \from *(format + (..));
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1524,10 +1596,10 @@
--- Properties of Function 'vsnprintf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 198)
+[ Extern ] Assigns (file share/libc/stdio.h, line 240)
assigns *(s + (0 .. n - 1));
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 198)
+[ Extern ] Froms (file share/libc/stdio.h, line 240)
assigns *(s + (0 .. n - 1)) \from *(format + (..)), arg;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1538,10 +1610,10 @@
--- Properties of Function 'vsprintf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 204)
+[ Extern ] Assigns (file share/libc/stdio.h, line 246)
assigns *(s + (0 ..));
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 204)
+[ Extern ] Froms (file share/libc/stdio.h, line 246)
assigns *(s + (0 ..)) \from *(format + (..)), arg;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1556,13 +1628,13 @@
ensures
result_uchar_or_eof: (0 ≤ \result ≤ 255) ∨ \result ≡ -1
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 217)
+[ Extern ] Assigns (file share/libc/stdio.h, line 259)
assigns *stream, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 217)
+[ Extern ] Froms (file share/libc/stdio.h, line 259)
assigns *stream \from *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 218)
+[ Extern ] Froms (file share/libc/stdio.h, line 260)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1577,19 +1649,24 @@
ensures
result_null_or_same: \result ≡ \null ∨ \result ≡ \old(s)
Unverifiable but considered Valid.
+[ Extern ] Post-condition 'initialization,at_least_one'
+ ensures
+ initialization: at_least_one:
+ \result ≢ \null ⇒ \initialized(\old(s) + 0)
+ Unverifiable but considered Valid.
[ Extern ] Post-condition 'terminated_string_on_success'
ensures
terminated_string_on_success:
\result ≢ \null ⇒ valid_string(\old(s))
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 225)
- assigns *(s + (0 .. size)), \result;
+[ Extern ] Assigns (file share/libc/stdio.h, line 268)
+ assigns *(s + (0 .. size - 1)), \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 225)
- assigns *(s + (0 .. size))
+[ Extern ] Froms (file share/libc/stdio.h, line 268)
+ assigns *(s + (0 .. size - 1))
\from (indirect: size), (indirect: *stream);
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 226)
+[ Extern ] Froms (file share/libc/stdio.h, line 269)
assigns \result \from s, (indirect: size), (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1600,8 +1677,14 @@
--- Properties of Function 'fputc'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 234)
- assigns *stream;
+[ Extern ] Assigns (file share/libc/stdio.h, line 282)
+ assigns *stream, \result;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 282)
+ assigns *stream \from c, *stream;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 283)
+ assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
@@ -1611,11 +1694,16 @@
--- Properties of Function 'fputs'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 237)
- assigns *stream;
+[ Extern ] Assigns (file share/libc/stdio.h, line 289)
+ assigns *stream, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 237)
- assigns *stream \from *(s + (..));
+[ Extern ] Froms (file share/libc/stdio.h, line 289)
+ assigns *stream \from *(s + (0 .. strlen{Old}(s))), *stream;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 290)
+ assigns \result
+ \from (indirect: *(s + (0 .. strlen{Old}(s)))),
+ (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
@@ -1625,13 +1713,13 @@
--- Properties of Function 'getc'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 241)
+[ Extern ] Assigns (file share/libc/stdio.h, line 297)
assigns \result, *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 241)
+[ Extern ] Froms (file share/libc/stdio.h, line 297)
assigns \result \from *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 241)
+[ Extern ] Froms (file share/libc/stdio.h, line 297)
assigns *stream \from *stream;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1642,12 +1730,15 @@
--- Properties of Function 'getchar'
--------------------------------------------------------------------------------
-[ Extern ] Assigns nothing
- assigns \nothing;
+[ Extern ] Assigns (file share/libc/stdio.h, line 302)
+ assigns \result, *__fc_stdin;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 244)
+[ Extern ] Froms (file share/libc/stdio.h, line 302)
assigns \result \from *__fc_stdin;
Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 302)
+ assigns *__fc_stdin \from *__fc_stdin;
+ Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
by Frama-C kernel.
@@ -1660,14 +1751,17 @@
ensures
result_null_or_same: \result ≡ \old(s) ∨ \result ≡ \null
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 248)
- assigns *(s + (..)), \result;
+[ Extern ] Assigns (file share/libc/stdio.h, line 315)
+ assigns *(s + (0 .. gets_length{Old})), \result, *__fc_stdin;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 315)
+ assigns *(s + (0 .. gets_length{Old})) \from *__fc_stdin;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 248)
- assigns *(s + (..)) \from *__fc_stdin;
+[ Extern ] Froms (file share/libc/stdio.h, line 316)
+ assigns \result \from s, *__fc_stdin;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 249)
- assigns \result \from s, __fc_stdin;
+[ Extern ] Froms (file share/libc/stdio.h, line 317)
+ assigns *__fc_stdin \from *__fc_stdin;
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
@@ -1677,11 +1771,14 @@
--- Properties of Function 'putc'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 254)
- assigns *stream;
+[ Extern ] Assigns (file share/libc/stdio.h, line 324)
+ assigns *stream, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 254)
- assigns *stream \from c;
+[ Extern ] Froms (file share/libc/stdio.h, line 324)
+ assigns *stream \from c, *stream;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 325)
+ assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
@@ -1691,11 +1788,14 @@
--- Properties of Function 'putchar'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 257)
- assigns *__fc_stdout;
+[ Extern ] Assigns (file share/libc/stdio.h, line 330)
+ assigns *__fc_stdout, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 257)
- assigns *__fc_stdout \from c;
+[ Extern ] Froms (file share/libc/stdio.h, line 330)
+ assigns *__fc_stdout \from c, *__fc_stdout;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 331)
+ assigns \result \from (indirect: *__fc_stdout);
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
@@ -1705,11 +1805,17 @@
--- Properties of Function 'puts'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 260)
- assigns *__fc_stdout;
+[ Extern ] Assigns (file share/libc/stdio.h, line 337)
+ assigns *__fc_stdout, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 260)
- assigns *__fc_stdout \from *(s + (..));
+[ Extern ] Froms (file share/libc/stdio.h, line 337)
+ assigns *__fc_stdout
+ \from *(s + (0 .. strlen{Old}(s))), *__fc_stdout;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 338)
+ assigns \result
+ \from (indirect: *(s + (0 .. strlen{Old}(s)))),
+ (indirect: *__fc_stdout);
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
@@ -1719,11 +1825,18 @@
--- Properties of Function 'ungetc'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 263)
- assigns *stream;
+[ Extern ] Post-condition 'result_ok_or_error'
+ ensures
+ result_ok_or_error: \result ≡ \old(c) ∨ \result ≡ -1
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 263)
- assigns *stream \from c;
+[ Extern ] Assigns (file share/libc/stdio.h, line 344)
+ assigns *stream, \result;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 344)
+ assigns *stream \from (indirect: c);
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 345)
+ assigns \result \from (indirect: c), (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
@@ -1742,15 +1855,20 @@
\initialized((char *)\old(ptr) +
(0 .. \result * \old(size) - 1))
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 269)
- assigns *((char *)ptr + (0 .. nmemb * size - 1)), \result;
+[ Extern ] Assigns (file share/libc/stdio.h, line 353)
+ assigns *((char *)ptr + (0 .. nmemb * size - 1)), *stream,
+ \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 269)
+[ Extern ] Froms (file share/libc/stdio.h, line 353)
assigns *((char *)ptr + (0 .. nmemb * size - 1))
- \from size, nmemb, *stream;
+ \from (indirect: size), (indirect: nmemb), (indirect: *stream);
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 270)
- assigns \result \from size, *stream;
+[ Extern ] Froms (file share/libc/stdio.h, line 353)
+ assigns *stream
+ \from (indirect: size), (indirect: nmemb), (indirect: *stream);
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 355)
+ assigns \result \from size, (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
@@ -1763,14 +1881,16 @@
[ Extern ] Post-condition 'size_written'
ensures size_written: \result ≤ \old(nmemb)
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 282)
+[ Extern ] Assigns (file share/libc/stdio.h, line 366)
assigns *stream, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 282)
- assigns *stream \from *((char *)ptr + (0 .. nmemb * size - 1));
+[ Extern ] Froms (file share/libc/stdio.h, line 366)
+ assigns *stream
+ \from (indirect: *((char *)ptr + (0 .. nmemb * size - 1)));
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 282)
- assigns \result \from *((char *)ptr + (0 .. nmemb * size - 1));
+[ Extern ] Froms (file share/libc/stdio.h, line 366)
+ assigns \result
+ \from (indirect: *((char *)ptr + (0 .. nmemb * size - 1)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
@@ -1780,11 +1900,14 @@
--- Properties of Function 'fgetpos'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 290)
- assigns *pos;
+[ Extern ] Assigns (file share/libc/stdio.h, line 377)
+ assigns *pos, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 290)
- assigns *pos \from *stream;
+[ Extern ] Froms (file share/libc/stdio.h, line 377)
+ assigns *pos \from (indirect: *stream);
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 378)
+ assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
@@ -1794,19 +1917,19 @@
--- Properties of Function 'fseek'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 297)
+[ Extern ] Assigns (file share/libc/stdio.h, line 386)
assigns *stream, \result, __fc_errno;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 297)
+[ Extern ] Froms (file share/libc/stdio.h, line 386)
assigns *stream
\from *stream, (indirect: offset), (indirect: whence);
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 298)
+[ Extern ] Froms (file share/libc/stdio.h, line 387)
assigns \result
\from (indirect: *stream), (indirect: offset),
(indirect: whence);
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 298)
+[ Extern ] Froms (file share/libc/stdio.h, line 387)
assigns __fc_errno
\from (indirect: *stream), (indirect: offset),
(indirect: whence);
@@ -1819,10 +1942,10 @@
--- Properties of Function 'fsetpos'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 303)
+[ Extern ] Assigns (file share/libc/stdio.h, line 396)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 303)
+[ Extern ] Froms (file share/libc/stdio.h, line 396)
assigns *stream \from *pos;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1839,13 +1962,13 @@
\result ≡ -1 ∨
(\result ≥ 0 ∧ __fc_errno ≡ \old(__fc_errno))
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 308)
+[ Extern ] Assigns (file share/libc/stdio.h, line 402)
assigns \result, __fc_errno;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 308)
+[ Extern ] Froms (file share/libc/stdio.h, line 402)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 308)
+[ Extern ] Froms (file share/libc/stdio.h, line 402)
assigns __fc_errno \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1856,10 +1979,10 @@
--- Properties of Function 'rewind'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 314)
+[ Extern ] Assigns (file share/libc/stdio.h, line 410)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 314)
+[ Extern ] Froms (file share/libc/stdio.h, line 410)
assigns *stream \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1870,10 +1993,10 @@
--- Properties of Function 'clearerr'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 317)
+[ Extern ] Assigns (file share/libc/stdio.h, line 416)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 317)
+[ Extern ] Froms (file share/libc/stdio.h, line 416)
assigns *stream \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1887,8 +2010,8 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 320)
- assigns \result \from *stream;
+[ Extern ] Froms (file share/libc/stdio.h, line 422)
+ assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
@@ -1901,8 +2024,8 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 323)
- assigns \result \from *stream;
+[ Extern ] Froms (file share/libc/stdio.h, line 428)
+ assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
@@ -1912,10 +2035,10 @@
--- Properties of Function 'flockfile'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 326)
+[ Extern ] Assigns (file share/libc/stdio.h, line 434)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 326)
+[ Extern ] Froms (file share/libc/stdio.h, line 434)
assigns *stream \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1926,10 +2049,10 @@
--- Properties of Function 'funlockfile'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 329)
+[ Extern ] Assigns (file share/libc/stdio.h, line 440)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 329)
+[ Extern ] Froms (file share/libc/stdio.h, line 440)
assigns *stream \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1940,13 +2063,13 @@
--- Properties of Function 'ftrylockfile'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 332)
+[ Extern ] Assigns (file share/libc/stdio.h, line 446)
assigns \result, *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 332)
+[ Extern ] Froms (file share/libc/stdio.h, line 446)
assigns \result \from \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 332)
+[ Extern ] Froms (file share/libc/stdio.h, line 446)
assigns *stream \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -1960,8 +2083,8 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 335)
- assigns \result \from *stream;
+[ Extern ] Froms (file share/libc/stdio.h, line 452)
+ assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
@@ -1971,11 +2094,12 @@
--- Properties of Function 'perror'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 338)
+[ Extern ] Assigns (file share/libc/stdio.h, line 458)
assigns __fc_stdout;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 338)
- assigns __fc_stdout \from __fc_errno, *(s + (..));
+[ Extern ] Froms (file share/libc/stdio.h, line 458)
+ assigns __fc_stdout
+ \from __fc_errno, *(s + (0 .. strlen{Old}(s)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
@@ -1985,13 +2109,13 @@
--- Properties of Function 'getc_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 341)
+[ Extern ] Assigns (file share/libc/stdio.h, line 464)
assigns \result, *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 341)
+[ Extern ] Froms (file share/libc/stdio.h, line 464)
assigns \result \from *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 341)
+[ Extern ] Froms (file share/libc/stdio.h, line 464)
assigns *stream \from *stream;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2005,7 +2129,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 343)
+[ Extern ] Froms (file share/libc/stdio.h, line 469)
assigns \result \from *__fc_stdin;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2016,12 +2140,15 @@
--- Properties of Function 'putc_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 345)
- assigns *stream;
+[ Extern ] Assigns (file share/libc/stdio.h, line 475)
+ assigns *stream, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 345)
+[ Extern ] Froms (file share/libc/stdio.h, line 475)
assigns *stream \from c;
Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 476)
+ assigns \result \from (indirect: *stream);
+ Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
by Frama-C kernel.
@@ -2030,12 +2157,15 @@
--- Properties of Function 'putchar_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 347)
- assigns *__fc_stdout;
+[ Extern ] Assigns (file share/libc/stdio.h, line 481)
+ assigns *__fc_stdout, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 347)
+[ Extern ] Froms (file share/libc/stdio.h, line 481)
assigns *__fc_stdout \from c;
Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 482)
+ assigns \result \from (indirect: *__fc_stdout);
+ Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
by Frama-C kernel.
@@ -2044,10 +2174,10 @@
--- Properties of Function 'clearerr_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 350)
+[ Extern ] Assigns (file share/libc/stdio.h, line 488)
assigns *stream;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 350)
+[ Extern ] Froms (file share/libc/stdio.h, line 488)
assigns *stream \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2061,8 +2191,8 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 352)
- assigns \result \from *stream;
+[ Extern ] Froms (file share/libc/stdio.h, line 494)
+ assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
@@ -2075,8 +2205,8 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 354)
- assigns \result \from *stream;
+[ Extern ] Froms (file share/libc/stdio.h, line 500)
+ assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
@@ -2089,8 +2219,8 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 356)
- assigns \result \from *stream;
+[ Extern ] Froms (file share/libc/stdio.h, line 506)
+ assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
@@ -2107,14 +2237,14 @@
(\subset(\result, &__fc_fopen[0 .. 16 - 1]) ∧
is_open_pipe(\result))
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 381)
+[ Extern ] Assigns (file share/libc/stdio.h, line 533)
assigns \result, __fc_fopen[0 ..];
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 381)
+[ Extern ] Froms (file share/libc/stdio.h, line 533)
assigns \result
\from (indirect: *command), (indirect: *type), __fc_p_fopen;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 383)
+[ Extern ] Froms (file share/libc/stdio.h, line 535)
assigns __fc_fopen[0 ..]
\from (indirect: *command), (indirect: *type), __fc_fopen[0 ..];
Unverifiable but considered Valid.
@@ -2132,7 +2262,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 395)
+[ Extern ] Froms (file share/libc/stdio.h, line 547)
assigns \result \from (indirect: *stream);
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3922,9 +4052,9 @@
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
- 175 Completely validated
+ 179 Completely validated
16 Locally validated
- 454 Considered valid
+ 484 Considered valid
56 To be validated
- 701 Total
+ 735 Total
--------------------------------------------------------------------------------
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index e8cb83c5ada4c1850d6cd7cd3708da2ec16145dc..8554a5a2d796a49cecbaea8e86f5ded905a0e92f 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -172,7 +172,7 @@
==============
Sloc = 1083
Decision point = 204
- Global variables = 68
+ Global variables = 70
If = 195
Loop = 43
Goto = 89
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index b85450e07ee183420637f89e3cd128f4c31ce19d..ed172048f4c391e586f81f1d78820d16d0d48d97 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -1308,6 +1308,23 @@ axiomatic StrChr {
}
*/
/*@
+axiomatic WMemChr {
+ logic 𔹠wmemchr{L}(wchar_t *s, wchar_t c, ℤ n)
+ reads *(s + (0 .. n - 1));
+
+ logic ℤ wmemchr_off{L}(wchar_t *s, wchar_t c, ℤ n)
+ reads *(s + (0 .. n - 1));
+
+ axiom wmemchr_def{L}:
+ ∀ wchar_t *s;
+ ∀ int c;
+ ∀ ℤ n;
+ wmemchr(s, c, n) ≡ \true ⇔
+ (∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
+
+ }
+ */
+/*@
axiomatic WcsLen {
logic ℤ wcslen{L}(wchar_t *s)
reads *(s + (0 ..));
@@ -1643,7 +1660,8 @@ extern off_t lseek(int fd, off_t offset, int whence);
*/
extern long pathconf(char const *path, int name);
-/*@ ensures initialization: pipefd: \initialized(\old(pipefd) + (0 .. 1));
+/*@ requires valid_pipefd: \valid(pipefd + (0 .. 1));
+ ensures initialization: pipefd: \initialized(\old(pipefd) + (0 .. 1));
ensures valid_fd0: 0 ≤ *(\old(pipefd) + 0) < 1024;
ensures valid_fd1: 0 ≤ *(\old(pipefd) + 1) < 1024;
ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
@@ -1727,7 +1745,8 @@ extern long sysconf(int name);
extern char volatile __fc_ttyname[32];
char volatile *__fc_p_ttyname = __fc_ttyname;
-/*@ ensures
+/*@ requires valid_fildes: 0 ≤ fildes < 1024;
+ ensures
result_name_or_null: \result ≡ __fc_p_ttyname ∨ \result ≡ \null;
assigns \result;
assigns \result \from __fc_p_ttyname, (indirect: fildes);
@@ -4448,10 +4467,22 @@ FILE *__fc_stdin;
FILE *__fc_stdout;
-/*@ assigns \nothing; */
+/*@ requires valid_filename: valid_read_string(filename);
+ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+ assigns \result;
+ assigns \result
+ \from (indirect: *(filename + (0 .. strlen{Old}(filename))));
+ */
extern int remove(char const *filename);
-/*@ assigns \nothing; */
+/*@ requires valid_old_name: valid_read_string(old_name);
+ requires valid_new_name: valid_read_string(new_name);
+ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+ assigns \result;
+ assigns \result
+ \from (indirect: *(old_name + (0 .. strlen{Old}(old_name)))),
+ (indirect: *(new_name + (0 .. strlen{Old}(new_name))));
+ */
extern int rename(char const *old_name, char const *new_name);
FILE __fc_fopen[16];
@@ -4464,23 +4495,53 @@ FILE * const __fc_p_fopen = __fc_fopen;
*/
extern FILE *tmpfile(void);
-/*@ assigns \result, *(s + (..));
- assigns \result \from *(s + (..));
- assigns *(s + (..)) \from \nothing;
+char __fc_tmpnam[2048];
+char * const __fc_p_tmpnam = __fc_tmpnam;
+/*@ requires valid_s_or_null: s ≡ \null ∨ \valid(s + (0 .. 2048));
+ ensures
+ result_string_or_null:
+ \result ≡ \null ∨ \result ≡ \old(s) ∨
+ \result ≡ __fc_p_tmpnam;
+ assigns *(__fc_p_tmpnam + (0 .. 2048)), *(s + (0 .. 2048)), \result;
+ assigns *(__fc_p_tmpnam + (0 .. 2048))
+ \from *(__fc_p_tmpnam + (0 .. 2048)), (indirect: s);
+ assigns *(s + (0 .. 2048))
+ \from (indirect: s), *(__fc_p_tmpnam + (0 .. 2048));
+ assigns \result \from s, __fc_p_tmpnam;
*/
extern char *tmpnam(char *s);
/*@ requires valid_stream: \valid(stream);
ensures result_zero_or_EOF: \result ≡ 0 ∨ \result ≡ -1;
assigns \result;
- assigns \result \from stream, stream->__fc_FILE_id;
+ assigns \result \from (indirect: stream), (indirect: *stream);
*/
extern int fclose(FILE *stream);
/*@ requires null_or_valid_stream: stream ≡ \null ∨ \valid_read(stream);
ensures result_zero_or_EOF: \result ≡ 0 ∨ \result ≡ -1;
- assigns \result;
- assigns \result \from stream, stream->__fc_FILE_id;
+ assigns \result, *stream, __fc_fopen[0 .. 16 - 1];
+ assigns \result
+ \from (indirect: *stream), (indirect: __fc_fopen[0 .. 16 - 1]);
+ assigns *stream
+ \from (indirect: stream), *stream, __fc_fopen[0 .. 16 - 1];
+ assigns __fc_fopen[0 .. 16 - 1]
+ \from (indirect: stream), *stream, __fc_fopen[0 .. 16 - 1];
+
+ behavior flush_all:
+ assumes all_streams: stream ≡ \null;
+ assigns __fc_fopen[0 .. 16 - 1], \result;
+ assigns __fc_fopen[0 .. 16 - 1] \from __fc_fopen[0 .. 16 - 1];
+ assigns \result \from (indirect: __fc_fopen[0 .. 16 - 1]);
+
+ behavior flush_stream:
+ assumes single_stream: stream ≢ \null;
+ assigns *stream, \result;
+ assigns *stream \from *stream;
+ assigns \result \from (indirect: *stream);
+
+ complete behaviors flush_stream, flush_all;
+ disjoint behaviors flush_stream, flush_all;
*/
extern int fflush(FILE *stream);
@@ -4491,8 +4552,8 @@ extern int fflush(FILE *stream);
\result ≡ \null ∨ \subset(\result, &__fc_fopen[0 .. 16 - 1]);
assigns \result;
assigns \result
- \from (indirect: *(filename + (..))), (indirect: *(mode + (..))),
- __fc_p_fopen;
+ \from (indirect: *(filename + (0 .. strlen{Old}(filename)))),
+ (indirect: *(mode + (0 .. strlen{Old}(mode)))), __fc_p_fopen;
*/
extern FILE *fopen(char const * __restrict filename,
char const * __restrict mode);
@@ -4503,10 +4564,10 @@ extern FILE *fopen(char const * __restrict filename,
\result ≡ \null ∨ \subset(\result, &__fc_fopen[0 .. 16 - 1]);
assigns \result, __fc_fopen[fd];
assigns \result
- \from (indirect: fd), (indirect: *(mode + (0 ..))),
+ \from (indirect: fd), (indirect: *(mode + (0 .. strlen{Old}(mode)))),
(indirect: __fc_fopen[fd]), __fc_p_fopen;
assigns __fc_fopen[fd]
- \from (indirect: fd), (indirect: *(mode + (0 ..))),
+ \from (indirect: fd), (indirect: *(mode + (0 .. strlen{Old}(mode)))),
(indirect: __fc_fopen[fd]), __fc_p_fopen;
*/
extern FILE *fdopen(int fd, char const *mode);
@@ -4583,54 +4644,93 @@ extern int vsprintf(char * __restrict s, char const * __restrict format,
extern int fgetc(FILE *stream);
/*@ requires valid_stream: \valid(stream);
+ requires room_s: \valid(s + (0 .. size - 1));
ensures result_null_or_same: \result ≡ \null ∨ \result ≡ \old(s);
+ ensures
+ initialization: at_least_one:
+ \result ≢ \null ⇒ \initialized(\old(s) + 0);
ensures
terminated_string_on_success:
\result ≢ \null ⇒ valid_string(\old(s));
- assigns *(s + (0 .. size)), \result;
- assigns *(s + (0 .. size)) \from (indirect: size), (indirect: *stream);
+ assigns *(s + (0 .. size - 1)), \result;
+ assigns *(s + (0 .. size - 1))
+ \from (indirect: size), (indirect: *stream);
assigns \result \from s, (indirect: size), (indirect: *stream);
*/
extern char *fgets(char * __restrict s, int size, FILE * __restrict stream);
-/*@ assigns *stream; */
+/*@ requires valid_stream: \valid(stream);
+ assigns *stream, \result;
+ assigns *stream \from c, *stream;
+ assigns \result \from (indirect: *stream);
+ */
extern int fputc(int c, FILE *stream);
-/*@ assigns *stream;
- assigns *stream \from *(s + (..)); */
+/*@ requires valid_string_s: valid_read_string(s);
+ assigns *stream, \result;
+ assigns *stream \from *(s + (0 .. strlen{Old}(s))), *stream;
+ assigns \result
+ \from (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: *stream);
+ */
extern int fputs(char const * __restrict s, FILE * __restrict stream);
-/*@ assigns \result, *stream;
+/*@ requires valid_stream: \valid(stream);
+ assigns \result, *stream;
assigns \result \from *stream;
assigns *stream \from *stream;
*/
extern int getc(FILE *stream);
-/*@ assigns \result;
- assigns \result \from *__fc_stdin; */
+/*@ assigns \result, *__fc_stdin;
+ assigns \result \from *__fc_stdin;
+ assigns *__fc_stdin \from *__fc_stdin;
+ */
extern int getchar(void);
-/*@ ensures result_null_or_same: \result ≡ \old(s) ∨ \result ≡ \null;
- assigns *(s + (..)), \result;
- assigns *(s + (..)) \from *__fc_stdin;
- assigns \result \from s, __fc_stdin;
+/*@ axiomatic GetsLength {
+ logic size_t gets_length{L}
+ reads *__fc_stdin;
+
+ }
+
+*/
+/*@ requires room_s: \valid(s + (0 .. gets_length));
+ ensures result_null_or_same: \result ≡ \old(s) ∨ \result ≡ \null;
+ assigns *(s + (0 .. gets_length{Old})), \result, *__fc_stdin;
+ assigns *(s + (0 .. gets_length{Old})) \from *__fc_stdin;
+ assigns \result \from s, *__fc_stdin;
+ assigns *__fc_stdin \from *__fc_stdin;
*/
extern char *gets(char *s);
-/*@ assigns *stream;
- assigns *stream \from c; */
+/*@ requires valid_stream: \valid(stream);
+ assigns *stream, \result;
+ assigns *stream \from c, *stream;
+ assigns \result \from (indirect: *stream);
+ */
extern int putc(int c, FILE *stream);
-/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from c; */
+/*@ assigns *__fc_stdout, \result;
+ assigns *__fc_stdout \from c, *__fc_stdout;
+ assigns \result \from (indirect: *__fc_stdout);
+ */
extern int putchar(int c);
-/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(s + (..)); */
+/*@ requires valid_string_s: valid_read_string(s);
+ assigns *__fc_stdout, \result;
+ assigns *__fc_stdout \from *(s + (0 .. strlen{Old}(s))), *__fc_stdout;
+ assigns \result
+ \from (indirect: *(s + (0 .. strlen{Old}(s)))),
+ (indirect: *__fc_stdout);
+ */
extern int puts(char const *s);
-/*@ assigns *stream;
- assigns *stream \from c; */
+/*@ requires valid_stream: \valid(stream);
+ ensures result_ok_or_error: \result ≡ \old(c) ∨ \result ≡ -1;
+ assigns *stream, \result;
+ assigns *stream \from (indirect: c);
+ assigns \result \from (indirect: c), (indirect: *stream);
+ */
extern int ungetc(int c, FILE *stream);
/*@ requires valid_ptr_block: \valid((char *)ptr + (0 .. nmemb * size - 1));
@@ -4639,10 +4739,12 @@ extern int ungetc(int c, FILE *stream);
ensures
initialization:
\initialized((char *)\old(ptr) + (0 .. \result * \old(size) - 1));
- assigns *((char *)ptr + (0 .. nmemb * size - 1)), \result;
+ assigns *((char *)ptr + (0 .. nmemb * size - 1)), *stream, \result;
assigns *((char *)ptr + (0 .. nmemb * size - 1))
- \from size, nmemb, *stream;
- assigns \result \from size, *stream;
+ \from (indirect: size), (indirect: nmemb), (indirect: *stream);
+ assigns *stream
+ \from (indirect: size), (indirect: nmemb), (indirect: *stream);
+ assigns \result \from size, (indirect: *stream);
*/
extern size_t fread(void * __restrict ptr, size_t size, size_t nmemb,
FILE * __restrict stream);
@@ -4652,14 +4754,21 @@ extern size_t fread(void * __restrict ptr, size_t size, size_t nmemb,
requires valid_stream: \valid(stream);
ensures size_written: \result ≤ \old(nmemb);
assigns *stream, \result;
- assigns *stream \from *((char *)ptr + (0 .. nmemb * size - 1));
- assigns \result \from *((char *)ptr + (0 .. nmemb * size - 1));
+ assigns *stream
+ \from (indirect: *((char *)ptr + (0 .. nmemb * size - 1)));
+ assigns \result
+ \from (indirect: *((char *)ptr + (0 .. nmemb * size - 1)));
*/
extern size_t fwrite(void const * __restrict ptr, size_t size, size_t nmemb,
FILE * __restrict stream);
-/*@ assigns *pos;
- assigns *pos \from *stream; */
+/*@ requires valid_stream: \valid(stream);
+ requires valid_pos: \valid(pos);
+ requires initialization: pos: \initialized(pos);
+ assigns *pos, \result;
+ assigns *pos \from (indirect: *stream);
+ assigns \result \from (indirect: *stream);
+ */
extern int fgetpos(FILE * __restrict stream, fpos_t * __restrict pos);
/*@ requires valid_stream: \valid(stream);
@@ -4673,8 +4782,12 @@ extern int fgetpos(FILE * __restrict stream, fpos_t * __restrict pos);
*/
extern int fseek(FILE *stream, long offset, int whence);
-/*@ assigns *stream;
- assigns *stream \from *pos; */
+/*@ requires valid_stream: \valid(stream);
+ requires valid_pos: \valid_read(pos);
+ requires initialization: pos: \initialized(pos);
+ assigns *stream;
+ assigns *stream \from *pos;
+ */
extern int fsetpos(FILE *stream, fpos_t const *pos);
/*@ requires valid_stream: \valid(stream);
@@ -4688,46 +4801,63 @@ extern int fsetpos(FILE *stream, fpos_t const *pos);
*/
extern long ftell(FILE *stream);
-/*@ assigns *stream;
- assigns *stream \from \nothing; */
+/*@ requires valid_stream: \valid(stream);
+ assigns *stream;
+ assigns *stream \from \nothing;
+ */
extern void rewind(FILE *stream);
-/*@ assigns *stream;
- assigns *stream \from \nothing; */
+/*@ requires valid_stream: \valid(stream);
+ assigns *stream;
+ assigns *stream \from \nothing;
+ */
extern void clearerr(FILE *stream);
-/*@ assigns \result;
- assigns \result \from *stream; */
+/*@ requires valid_stream: \valid(stream);
+ assigns \result;
+ assigns \result \from (indirect: *stream);
+ */
extern int feof(FILE *stream);
-/*@ assigns \result;
- assigns \result \from *stream; */
+/*@ requires valid_stream: \valid(stream);
+ assigns \result;
+ assigns \result \from (indirect: *stream);
+ */
extern int fileno(FILE *stream);
-/*@ assigns *stream;
- assigns *stream \from \nothing; */
+/*@ requires valid_stream: \valid(stream);
+ assigns *stream;
+ assigns *stream \from \nothing;
+ */
extern void flockfile(FILE *stream);
-/*@ assigns *stream;
- assigns *stream \from \nothing; */
+/*@ requires valid_stream: \valid(stream);
+ assigns *stream;
+ assigns *stream \from \nothing;
+ */
extern void funlockfile(FILE *stream);
-/*@ assigns \result, *stream;
+/*@ requires valid_stream: \valid(stream);
+ assigns \result, *stream;
assigns \result \from \nothing;
assigns *stream \from \nothing;
*/
extern int ftrylockfile(FILE *stream);
-/*@ assigns \result;
- assigns \result \from *stream; */
+/*@ requires valid_stream: \valid(stream);
+ assigns \result;
+ assigns \result \from (indirect: *stream);
+ */
extern int ferror(FILE *stream);
-/*@ assigns __fc_stdout;
- assigns __fc_stdout \from __fc_errno, *(s + (..));
+/*@ requires valid_string_s: valid_read_string(s);
+ assigns __fc_stdout;
+ assigns __fc_stdout \from __fc_errno, *(s + (0 .. strlen{Old}(s)));
*/
extern void perror(char const *s);
-/*@ assigns \result, *stream;
+/*@ requires valid_stream: \valid(stream);
+ assigns \result, *stream;
assigns \result \from *stream;
assigns *stream \from *stream;
*/
@@ -4737,28 +4867,41 @@ extern int getc_unlocked(FILE *stream);
assigns \result \from *__fc_stdin; */
extern int getchar_unlocked(void);
-/*@ assigns *stream;
- assigns *stream \from c; */
+/*@ requires valid_stream: \valid(stream);
+ assigns *stream, \result;
+ assigns *stream \from c;
+ assigns \result \from (indirect: *stream);
+ */
extern int putc_unlocked(int c, FILE *stream);
-/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from c; */
+/*@ assigns *__fc_stdout, \result;
+ assigns *__fc_stdout \from c;
+ assigns \result \from (indirect: *__fc_stdout);
+ */
extern int putchar_unlocked(int c);
-/*@ assigns *stream;
- assigns *stream \from \nothing; */
+/*@ requires valid_stream: \valid(stream);
+ assigns *stream;
+ assigns *stream \from \nothing;
+ */
extern void clearerr_unlocked(FILE *stream);
-/*@ assigns \result;
- assigns \result \from *stream; */
+/*@ requires valid_stream: \valid(stream);
+ assigns \result;
+ assigns \result \from (indirect: *stream);
+ */
extern int feof_unlocked(FILE *stream);
-/*@ assigns \result;
- assigns \result \from *stream; */
+/*@ requires valid_stream: \valid(stream);
+ assigns \result;
+ assigns \result \from (indirect: *stream);
+ */
extern int ferror_unlocked(FILE *stream);
-/*@ assigns \result;
- assigns \result \from *stream; */
+/*@ requires valid_stream: \valid(stream);
+ assigns \result;
+ assigns \result \from (indirect: *stream);
+ */
extern int fileno_unlocked(FILE *stream);
/*@ axiomatic pipe_streams {
@@ -6082,9 +6225,10 @@ extern clock_t clock(void);
assigns \result \from time1, time0; */
extern double difftime(time_t time1, time_t time0);
-/*@ assigns *timeptr, \result;
+/*@ requires valid_timeptr: \valid(timeptr);
+ assigns *timeptr, \result;
assigns *timeptr \from *timeptr;
- assigns \result \from *timeptr;
+ assigns \result \from (indirect: *timeptr);
*/
extern time_t mktime(struct tm *timeptr);
@@ -6126,7 +6270,8 @@ extern char *ctime(time_t const *timer);
struct tm __fc_time_tm;
struct tm * const __fc_p_time_tm = & __fc_time_tm;
-/*@ ensures
+/*@ requires valid_timer: \valid_read(timer);
+ ensures
result_null_or_internal_tm:
\result ≡ &__fc_time_tm ∨ \result ≡ \null;
assigns \result, __fc_time_tm;
@@ -6135,7 +6280,8 @@ struct tm * const __fc_p_time_tm = & __fc_time_tm;
*/
extern struct tm *gmtime(time_t const *timer);
-/*@ ensures
+/*@ requires valid_timer: \valid_read(timer);
+ ensures
result_null_or_internal_tm:
\result ≡ &__fc_time_tm ∨ \result ≡ \null;
assigns \result, __fc_time_tm;
@@ -6312,8 +6458,6 @@ extern int clock_nanosleep(clockid_t clock_id, int flags,
*/
extern int nanosleep(struct timespec const *rqtp, struct timespec *rmtp);
-extern void tzset(void);
-
extern char *tzname[2];
/*@ assigns *(tzname[0 .. 1] + (0 ..));
@@ -6321,7 +6465,21 @@ extern char *tzname[2];
*/
extern void tzset(void);
-/*@ ensures
+/*@ requires
+ valid:
+ valid_read_or_empty((void *)s, (unsigned int)(sizeof(wchar_t) * n)) ∨
+ \valid_read((unsigned char *)s + (0 .. wmemchr_off(s, c, n)));
+ requires
+ initialization:
+ \initialized(s + (0 .. n - 1)) ∨
+ \initialized(s + (0 .. wmemchr_off(s, c, n)));
+ requires
+ danglingness:
+ non_escaping((void *)s, (unsigned int)(sizeof(wchar_t) * n)) ∨
+ non_escaping((void *)s,
+ (unsigned int)(sizeof(wchar_t) *
+ (wmemchr_off(s, c, n) + 1)));
+ ensures
result_null_or_inside_s:
\result ≡ \null ∨ \subset(\result, \old(s) + (0 .. \old(n) - 1));
assigns \result;
@@ -6330,7 +6488,21 @@ extern void tzset(void);
*/
extern wchar_t *wmemchr(wchar_t const *s, wchar_t c, size_t n);
-/*@ assigns \result;
+/*@ requires
+ valid_s1:
+ valid_read_or_empty((void *)s1, (unsigned int)(sizeof(wchar_t) * n));
+ requires
+ valid_s2:
+ valid_read_or_empty((void *)s2, (unsigned int)(sizeof(wchar_t) * n));
+ requires initialization: s1: \initialized(s1 + (0 .. n - 1));
+ requires initialization: s2: \initialized(s2 + (0 .. n - 1));
+ requires
+ danglingness: s1:
+ non_escaping((void *)s1, (unsigned int)(sizeof(wchar_t) * n));
+ requires
+ danglingness: s2:
+ non_escaping((void *)s2, (unsigned int)(sizeof(wchar_t) * n));
+ assigns \result;
assigns \result
\from (indirect: *(s1 + (0 .. n - 1))),
(indirect: *(s2 + (0 .. n - 1))), (indirect: n);
@@ -6339,7 +6511,9 @@ extern int wmemcmp(wchar_t const *s1, wchar_t const *s2, size_t n);
wchar_t *wmemcpy(wchar_t *dest, wchar_t const *src, size_t n);
-/*@ ensures result_ptr: \result ≡ \old(dest);
+/*@ requires valid_src: \valid_read(src + (0 .. n - 1));
+ requires valid_dest: \valid(dest + (0 .. n - 1));
+ ensures result_ptr: \result ≡ \old(dest);
assigns *(dest + (0 .. n - 1)), \result;
assigns *(dest + (0 .. n - 1))
\from *(src + (0 .. n - 1)), (indirect: src), (indirect: n);
@@ -6360,7 +6534,9 @@ wchar_t *wcscat(wchar_t *dest, wchar_t const *src);
*/
extern wchar_t *wcschr(wchar_t const *wcs, wchar_t wc);
-/*@ assigns \result;
+/*@ requires valid_wstring_s1: valid_read_wstring(s1);
+ requires valid_wstring_s2: valid_read_wstring(s2);
+ assigns \result;
assigns \result
\from (indirect: *(s1 + (0 ..))), (indirect: *(s2 + (0 ..)));
*/
@@ -6368,13 +6544,25 @@ extern int wcscmp(wchar_t const *s1, wchar_t const *s2);
wchar_t *wcscpy(wchar_t *dest, wchar_t const *src);
-/*@ assigns \result;
+/*@ requires valid_wstring_wcs: valid_read_wstring(wcs);
+ requires valid_wstring_accept: valid_read_wstring(accept);
+ assigns \result;
assigns \result
\from (indirect: *(wcs + (0 ..))), (indirect: *(accept + (0 ..)));
*/
extern size_t wcscspn(wchar_t const *wcs, wchar_t const *accept);
-/*@ assigns *(dest + (0 ..)), \result;
+/*@ requires valid_nwstring_src: valid_read_nwstring(src, n);
+ requires valid_wstring_dest: valid_wstring(dest);
+ requires
+ room_for_concatenation:
+ \valid(dest + (wcslen(dest) .. wcslen(dest) + \min(wcslen(src), n)));
+ requires
+ separation:
+ \separated(
+ dest + (0 .. wcslen(dest) + wcslen(src)), src + (0 .. wcslen(src))
+ );
+ assigns *(dest + (0 ..)), \result;
assigns *(dest + (0 ..))
\from *(dest + (0 ..)), (indirect: dest), *(src + (0 .. n - 1)),
(indirect: src), (indirect: n);
@@ -6385,7 +6573,9 @@ extern size_t wcscspn(wchar_t const *wcs, wchar_t const *accept);
extern size_t wcslcat(wchar_t * __restrict dest,
wchar_t const * __restrict src, size_t n);
-/*@ requires
+/*@ requires valid_wstring_src: valid_read_wstring(src);
+ requires room_nwstring: \valid(dest + (0 .. n));
+ requires
separation: dest: src:
\separated(dest + (0 .. n - 1), src + (0 .. n - 1));
assigns *(dest + (0 .. n - 1)), \result;
@@ -6401,7 +6591,9 @@ size_t wcslen(wchar_t const *str);
wchar_t *wcsncat(wchar_t *dest, wchar_t const *src, size_t n);
-/*@ assigns \result;
+/*@ requires valid_wstring_s1: valid_read_wstring(s1);
+ requires valid_wstring_s2: valid_read_wstring(s2);
+ assigns \result;
assigns \result
\from (indirect: *(s1 + (0 .. n - 1))),
(indirect: *(s2 + (0 .. n - 1))), (indirect: n);
@@ -6410,7 +6602,9 @@ extern int wcsncmp(wchar_t const *s1, wchar_t const *s2, size_t n);
wchar_t *wcsncpy(wchar_t *dest, wchar_t const *src, size_t n);
-/*@ ensures
+/*@ requires valid_wstring_wcs: valid_read_wstring(wcs);
+ requires valid_wstring_accept: valid_read_wstring(accept);
+ ensures
result_null_or_inside_wcs:
\result ≡ \null ∨ \subset(\result, \old(wcs) + (0 ..));
assigns \result;
@@ -6419,21 +6613,28 @@ wchar_t *wcsncpy(wchar_t *dest, wchar_t const *src, size_t n);
*/
extern wchar_t *wcspbrk(wchar_t const *wcs, wchar_t const *accept);
-/*@ ensures
+/*@ requires valid_wstring_wcs: valid_read_wstring(wcs);
+ ensures
result_null_or_inside_wcs:
\result ≡ \null ∨ \subset(\result, \old(wcs) + (0 ..));
assigns \result;
- assigns \result \from wcs, (indirect: *(wcs + (0 ..))), (indirect: wc);
+ assigns \result
+ \from wcs, (indirect: *(wcs + (0 .. wcslen{Old}(wcs)))), (indirect: wc);
*/
extern wchar_t *wcsrchr(wchar_t const *wcs, wchar_t wc);
-/*@ assigns \result;
+/*@ requires valid_wstring_wcs: valid_read_wstring(wcs);
+ requires valid_wstring_accept: valid_read_wstring(accept);
+ assigns \result;
assigns \result
- \from (indirect: *(wcs + (0 ..))), (indirect: *(accept + (0 ..)));
+ \from (indirect: *(wcs + (0 .. wcslen{Old}(wcs)))),
+ (indirect: *(accept + (0 .. wcslen{Old}(accept))));
*/
extern size_t wcsspn(wchar_t const *wcs, wchar_t const *accept);
-/*@ ensures
+/*@ requires valid_wstring_haystack: valid_read_wstring(haystack);
+ requires valid_wstring_needle: valid_read_wstring(needle);
+ ensures
result_null_or_inside_haystack:
\result ≡ \null ∨ \subset(\result, \old(haystack) + (0 ..));
assigns \result;
@@ -6443,13 +6644,14 @@ extern size_t wcsspn(wchar_t const *wcs, wchar_t const *accept);
*/
extern wchar_t *wcsstr(wchar_t const *haystack, wchar_t const *needle);
-/*@ requires valid_stream: \valid(stream);
+/*@ requires room_nwstring: \valid(ws + (0 .. n - 1));
+ requires valid_stream: \valid(stream);
ensures result_null_or_same: \result ≡ \null ∨ \result ≡ \old(ws);
ensures
terminated_string_on_success:
\result ≢ \null ⇒ valid_wstring(\old(ws));
- assigns *(ws + (0 .. n)), \result;
- assigns *(ws + (0 .. n)) \from (indirect: n), (indirect: *stream);
+ assigns *(ws + (0 .. n - 1)), \result;
+ assigns *(ws + (0 .. n - 1)) \from (indirect: n), (indirect: *stream);
assigns \result \from ws, (indirect: n), (indirect: *stream);
*/
extern wchar_t *fgetws(wchar_t * __restrict ws, int n,
@@ -6462,6 +6664,12 @@ extern wchar_t *fgetws(wchar_t * __restrict ws, int n,
*/
/*@ requires
+ valid_dest:
+ valid_or_empty((void *)dest, (unsigned int)(sizeof(wchar_t) * n));
+ requires
+ valid_src:
+ valid_read_or_empty((void *)src, (unsigned int)(sizeof(wchar_t) * n));
+ requires
separation: dest: src:
\separated(dest + (0 .. n - 1), src + (0 .. n - 1));
ensures result_ptr: \result ≡ \old(dest);
@@ -6482,7 +6690,8 @@ wchar_t *wmemcpy(wchar_t *dest, wchar_t const *src, size_t n)
return dest;
}
-/*@ ensures result_ptr: \result ≡ \old(dest);
+/*@ requires valid_wcs: \valid(dest + (0 .. len - 1));
+ ensures result_ptr: \result ≡ \old(dest);
ensures
initialization: wcs: \initialized(\old(dest) + (0 .. \old(len) - 1));
ensures
@@ -6504,11 +6713,15 @@ wchar_t *wmemset(wchar_t *dest, wchar_t val, size_t len)
return dest;
}
-/*@ ensures result_ptr: \result ≡ \old(dest);
- assigns *(dest + (0 ..)), \result;
- assigns *(dest + (0 ..))
- \from *(src + (0 ..)), (indirect: src), *(dest + (0 ..)),
- (indirect: dest);
+/*@ requires valid_wstring_src: valid_read_wstring(src);
+ requires room_wstring: \valid(dest + (0 .. wcslen(src)));
+ requires
+ separation:
+ \separated(dest + (0 .. wcslen(src)), src + (0 .. wcslen(src)));
+ ensures result_ptr: \result ≡ \old(dest);
+ assigns *(dest + (0 .. wcslen{Old}(src))), \result;
+ assigns *(dest + (0 .. wcslen{Old}(src)))
+ \from *(src + (0 .. wcslen{Old}(src))), (indirect: src);
assigns \result \from dest;
*/
wchar_t *wcscpy(wchar_t *dest, wchar_t const *src)
@@ -6524,8 +6737,9 @@ wchar_t *wcscpy(wchar_t *dest, wchar_t const *src)
}
/*@ requires valid_string_s: valid_read_wstring(str);
+ ensures result_is_length: \result ≡ wcslen(\old(str));
assigns \result;
- assigns \result \from (indirect: *(str + (0 ..)));
+ assigns \result \from (indirect: *(str + (0 .. wcslen{Old}(str))));
*/
size_t wcslen(wchar_t const *str)
{
@@ -6535,10 +6749,13 @@ size_t wcslen(wchar_t const *str)
return i;
}
-/*@ requires
+/*@ requires valid_wstring_src: valid_read_wstring(src);
+ requires room_nwstring: \valid(dest + (0 .. n - 1));
+ requires
separation: dest: src:
\separated(dest + (0 .. n - 1), src + (0 .. n - 1));
ensures result_ptr: \result ≡ \old(dest);
+ ensures initialization: \initialized(\old(dest) + (0 .. \old(n) - 1));
assigns *(dest + (0 .. n - 1)), \result;
assigns *(dest + (0 .. n - 1))
\from *(src + (0 .. n - 1)), (indirect: src), (indirect: n);
@@ -6560,7 +6777,17 @@ wchar_t *wcsncpy(wchar_t *dest, wchar_t const *src, size_t n)
return dest;
}
-/*@ ensures result_ptr: \result ≡ \old(dest);
+/*@ requires valid_wstring_src: valid_read_wstring(src);
+ requires valid_wstring_dest: valid_wstring(dest);
+ requires
+ room_for_concatenation:
+ \valid(dest + (wcslen(dest) .. wcslen(dest) + wcslen(src)));
+ requires
+ separation:
+ \separated(
+ dest + (0 .. wcslen(dest) + wcslen(src)), src + (0 .. wcslen(src))
+ );
+ ensures result_ptr: \result ≡ \old(dest);
assigns *(dest + (0 ..)), \result;
assigns *(dest + (0 ..))
\from *(dest + (0 ..)), (indirect: dest), *(src + (0 ..)),
@@ -6580,7 +6807,17 @@ wchar_t *wcscat(wchar_t *dest, wchar_t const *src)
return dest;
}
-/*@ ensures result_ptr: \result ≡ \old(dest);
+/*@ requires valid_nwstring_src: valid_read_nwstring(src, n);
+ requires valid_wstring_dest: valid_wstring(dest);
+ requires
+ room_for_concatenation:
+ \valid(dest + (wcslen(dest) .. wcslen(dest) + \min(wcslen(src), n)));
+ requires
+ separation:
+ \separated(
+ dest + (0 .. wcslen(dest) + wcslen(src)), src + (0 .. wcslen(src))
+ );
+ ensures result_ptr: \result ≡ \old(dest);
assigns *(dest + (0 ..)), \result;
assigns *(dest + (0 ..))
\from *(dest + (0 ..)), (indirect: dest), *(src + (0 .. n - 1)),
@@ -7028,8 +7265,13 @@ extern int __va_openat_mode_t(int dirfd, char const *filename, int flags,
/*@ ghost extern int __fc_tz __attribute__((__FRAMA_C_MODEL__)); */
-/*@ assigns \result;
- assigns \result \from *(path + (0 ..)), *(times + (0 .. 1));
+/*@ requires valid_path: valid_read_string(path);
+ requires
+ valid_times_or_null: \valid_read(times + (0 .. 1)) ∨ times ≡ \null;
+ assigns \result;
+ assigns \result
+ \from (indirect: *(path + (0 .. strlen{Old}(path)))),
+ (indirect: times), (indirect: *(times + (0 .. 1)));
*/
extern int utimes(char const *path, struct timeval const * /*[2]*/ times);
@@ -7093,13 +7335,15 @@ extern int utimes(char const *path, struct timeval const * /*[2]*/ times);
*/
extern int gettimeofday(struct timeval * __restrict tv, void * __restrict tz);
-/*@ assigns \result, __fc_time, __fc_tz;
- assigns \result
- \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;
+ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+ assigns __fc_time, __fc_tz, \result;
assigns __fc_time
\from tv->tv_sec, tv->tv_usec, tz->tz_dsttime, tz->tz_minuteswest;
assigns __fc_tz
\from tv->tv_sec, tv->tv_usec, tz->tz_dsttime, tz->tz_minuteswest;
+ assigns \result \from (indirect: *tv), (indirect: *tz);
*/
extern int settimeofday(struct timeval const *tv, struct timezone const *tz);
@@ -7603,23 +7847,28 @@ 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, rl->rlim_cur, rl->rlim_max;
- assigns \result \from r;
- assigns rl->rlim_cur \from r;
- assigns rl->rlim_max \from r;
+/*@ requires valid_rlp: \valid(rlp);
+ assigns \result, *rlp;
+ assigns \result \from resource;
+ assigns *rlp \from resource;
*/
-extern int getrlimit(int r, struct rlimit *rl);
+extern int getrlimit(int resource, struct rlimit *rlp);
-/*@ assigns \result, ru->ru_utime, ru->ru_stime;
- assigns \result \from r;
- assigns ru->ru_utime \from r;
- assigns ru->ru_stime \from r;
+/*@ requires valid_r_usage: \valid(r_usage);
+ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+ assigns *r_usage, \result;
+ assigns *r_usage \from who;
+ assigns \result \from (indirect: who);
*/
-extern int getrusage(int r, struct rusage *ru);
+extern int getrusage(int who, struct rusage *r_usage);
-/*@ assigns \result;
- assigns \result \from r, rl->rlim_cur, rl->rlim_max; */
-extern int setrlimit(int r, struct rlimit const *rl);
+/*@ requires valid_rlp: \valid_read(rlp);
+ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+ assigns *rlp, \result;
+ assigns *rlp \from resource;
+ assigns \result \from (indirect: resource), (indirect: *rlp);
+ */
+extern int setrlimit(int resource, struct rlimit const *rlp);
/*@ requires valid_buffer: \valid(buffer);
assigns \result, *buffer;
diff --git a/tests/libc/oracle/poll.res.oracle b/tests/libc/oracle/poll.res.oracle
index 11b20253b1a0df727f0356e029ddf671fa985eb0..311b9eca83445d6938754f8aefda746f0ba0efbb 100644
--- a/tests/libc/oracle/poll.res.oracle
+++ b/tests/libc/oracle/poll.res.oracle
@@ -13,6 +13,8 @@
[eva] computing for function perror <- main.
Called from tests/libc/poll.c:12.
[eva] using specification for function perror
+[eva] tests/libc/poll.c:12:
+ function perror: precondition 'valid_string_s' got status valid.
[eva] Done for function perror
[eva] Recording results for main
[eva] done for function main
diff --git a/tests/libc/oracle/stdio_c.res.oracle b/tests/libc/oracle/stdio_c.res.oracle
index 40428842717797ef2180c0447d600f308ff4e75b..06ba2405258b9311bfeb5ca4f73196a063806ca0 100644
--- a/tests/libc/oracle/stdio_c.res.oracle
+++ b/tests/libc/oracle/stdio_c.res.oracle
@@ -17,18 +17,26 @@
[eva] computing for function ferror <- getline <- main.
Called from share/libc/stdio.c:46.
[eva] using specification for function ferror
+[eva] share/libc/stdio.c:46:
+ function ferror: precondition 'valid_stream' got status valid.
[eva] Done for function ferror
[eva] computing for function feof <- getline <- main.
Called from share/libc/stdio.c:46.
[eva] using specification for function feof
+[eva] share/libc/stdio.c:46:
+ function feof: precondition 'valid_stream' got status valid.
[eva] Done for function feof
[eva] share/libc/stdio.c:51: Call to builtin malloc
[eva] share/libc/stdio.c:51: allocating variable __malloc_getline_l51
[eva] computing for function ferror <- getline <- main.
Called from share/libc/stdio.c:60.
+[eva] share/libc/stdio.c:60:
+ function ferror: precondition 'valid_stream' got status valid.
[eva] Done for function ferror
[eva] computing for function feof <- getline <- main.
Called from share/libc/stdio.c:60.
+[eva] share/libc/stdio.c:60:
+ function feof: precondition 'valid_stream' got status valid.
[eva] Done for function feof
[eva] computing for function fgetc <- getline <- main.
Called from share/libc/stdio.c:62.
diff --git a/tests/libc/oracle/stdio_h.res.oracle b/tests/libc/oracle/stdio_h.res.oracle
index 267bfa3fb5cd00eb5c67fec3ee3113d8729ae044..8262aa6c408e46edf0fd8bb728cb16edf61af046 100644
--- a/tests/libc/oracle/stdio_h.res.oracle
+++ b/tests/libc/oracle/stdio_h.res.oracle
@@ -78,6 +78,22 @@
[eva] tests/libc/stdio_h.c:31:
function fclose: precondition 'valid_stream' got status valid.
[eva] Done for function fclose
+[eva] computing for function fgets <- main.
+ Called from tests/libc/stdio_h.c:34.
+[eva] using specification for function fgets
+[eva] tests/libc/stdio_h.c:34:
+ function fgets: precondition 'valid_stream' got status valid.
+[eva] tests/libc/stdio_h.c:34:
+ function fgets: precondition 'room_s' got status valid.
+[eva] Done for function fgets
+[eva:alarm] tests/libc/stdio_h.c:36: Warning: check got status unknown.
+[eva] computing for function fgets <- main.
+ Called from tests/libc/stdio_h.c:38.
+[eva] tests/libc/stdio_h.c:38:
+ function fgets: precondition 'valid_stream' got status valid.
+[eva:alarm] tests/libc/stdio_h.c:38: Warning:
+ function fgets: precondition 'room_s' got status invalid.
+[eva] Done for function fgets
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -89,5 +105,7 @@
r ∈ [--..--]
tmp_2 ∈ {{ NULL ; &__fc_fopen + [0..120],0%8 }}
redirected ∈ {{ NULL ; &__fc_fopen + [0..120],0%8 }}
+ fgets_buf0[0] ∈ [--..--] or UNINITIALIZED
+ fgets_res ∈ {{ NULL ; &fgets_buf0[0] }}
__retres ∈ {0; 1; 2; 3}
S___fc_stdout[0..1] ∈ [--..--]
diff --git a/tests/libc/oracle/sys_time.res.oracle b/tests/libc/oracle/sys_time.res.oracle
deleted file mode 100644
index 18c18fa9f8cf4ac0e2cd2252f3a3baf3d7dcd62c..0000000000000000000000000000000000000000
--- a/tests/libc/oracle/sys_time.res.oracle
+++ /dev/null
@@ -1,62 +0,0 @@
-[kernel] Parsing tests/libc/sys_time.c (with preprocessing)
-[eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
-
-[eva] computing for function setitimer <- main.
- Called from tests/libc/sys_time.c:6.
-[eva] using specification for function setitimer
-[eva] tests/libc/sys_time.c:6:
- function setitimer: precondition 'valid_new_value' got status valid.
-[eva] tests/libc/sys_time.c:6:
- function setitimer: precondition 'old_value_null_or_valid' got status valid.
-[eva:invalid-assigns] tests/libc/sys_time.c:6:
- Completely invalid destination for assigns clause *old_value. Ignoring.
-[eva] Done for function setitimer
-[eva] tests/libc/sys_time.c:7: assertion got status valid.
-[eva] computing for function setitimer <- main.
- Called from tests/libc/sys_time.c:9.
-[eva] tests/libc/sys_time.c:9:
- function setitimer: precondition 'valid_new_value' got status valid.
-[eva] tests/libc/sys_time.c:9:
- function setitimer: precondition 'old_value_null_or_valid' got status valid.
-[eva] Done for function setitimer
-[eva] tests/libc/sys_time.c:10: assertion got status valid.
-[eva] tests/libc/sys_time.c:11: assertion got status valid.
-[eva] computing for function getitimer <- main.
- Called from tests/libc/sys_time.c:12.
-[eva] using specification for function getitimer
-[eva] tests/libc/sys_time.c:12:
- function getitimer: precondition 'valid_curr_value' got status valid.
-[eva] Done for function getitimer
-[eva] tests/libc/sys_time.c:13: assertion got status valid.
-[eva] tests/libc/sys_time.c:14: assertion got status valid.
-[eva] computing for function getitimer <- main.
- Called from tests/libc/sys_time.c:16.
-[eva] tests/libc/sys_time.c:16:
- function getitimer: precondition 'valid_curr_value' got status valid.
-[eva] Done for function getitimer
-[eva] tests/libc/sys_time.c:17: assertion got status valid.
-[eva] computing for function setitimer <- main.
- Called from tests/libc/sys_time.c:19.
-[eva] tests/libc/sys_time.c:19:
- function setitimer: precondition 'valid_new_value' got status valid.
-[eva] tests/libc/sys_time.c:19:
- function setitimer: precondition 'old_value_null_or_valid' got status valid.
-[eva] Done for function setitimer
-[eva] tests/libc/sys_time.c:20: assertion got status valid.
-[eva] Recording results for main
-[eva] done for function main
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function main:
- i1.it_interval.tv_sec ∈ {1}
- .it_interval.tv_usec ∈ {100}
- .it_value.tv_sec ∈ {2}
- .it_value.tv_usec ∈ {200}
- res ∈ {-1}
- i2.it_interval.tv_sec ∈ [--..--]
- .it_interval.tv_usec ∈ {1000000}
- .it_value ∈ [--..--]
- INVALID_ITIMER ∈ {-1}
- __retres ∈ {0}
diff --git a/tests/libc/oracle/sys_time_h.res.oracle b/tests/libc/oracle/sys_time_h.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..56221db7dec29a071d214607e6c178e1ccc12f1e
--- /dev/null
+++ b/tests/libc/oracle/sys_time_h.res.oracle
@@ -0,0 +1,83 @@
+[kernel] Parsing tests/libc/sys_time_h.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+
+[eva] computing for function setitimer <- main.
+ Called from tests/libc/sys_time_h.c:6.
+[eva] using specification for function setitimer
+[eva] tests/libc/sys_time_h.c:6:
+ function setitimer: precondition 'valid_new_value' got status valid.
+[eva] tests/libc/sys_time_h.c:6:
+ function setitimer: precondition 'old_value_null_or_valid' got status valid.
+[eva:invalid-assigns] tests/libc/sys_time_h.c:6:
+ Completely invalid destination for assigns clause *old_value. Ignoring.
+[eva] Done for function setitimer
+[eva] tests/libc/sys_time_h.c:7: assertion got status valid.
+[eva] computing for function setitimer <- main.
+ Called from tests/libc/sys_time_h.c:9.
+[eva] tests/libc/sys_time_h.c:9:
+ function setitimer: precondition 'valid_new_value' got status valid.
+[eva] tests/libc/sys_time_h.c:9:
+ function setitimer: precondition 'old_value_null_or_valid' got status valid.
+[eva] Done for function setitimer
+[eva] tests/libc/sys_time_h.c:10: assertion got status valid.
+[eva] tests/libc/sys_time_h.c:11: assertion got status valid.
+[eva] computing for function getitimer <- main.
+ Called from tests/libc/sys_time_h.c:12.
+[eva] using specification for function getitimer
+[eva] tests/libc/sys_time_h.c:12:
+ function getitimer: precondition 'valid_curr_value' got status valid.
+[eva] Done for function getitimer
+[eva] tests/libc/sys_time_h.c:13: assertion got status valid.
+[eva] tests/libc/sys_time_h.c:14: assertion got status valid.
+[eva] computing for function getitimer <- main.
+ Called from tests/libc/sys_time_h.c:16.
+[eva] tests/libc/sys_time_h.c:16:
+ function getitimer: precondition 'valid_curr_value' got status valid.
+[eva] Done for function getitimer
+[eva] tests/libc/sys_time_h.c:17: assertion got status valid.
+[eva] computing for function setitimer <- main.
+ Called from tests/libc/sys_time_h.c:19.
+[eva] tests/libc/sys_time_h.c:19:
+ function setitimer: precondition 'valid_new_value' got status valid.
+[eva] tests/libc/sys_time_h.c:19:
+ function setitimer: precondition 'old_value_null_or_valid' got status valid.
+[eva] Done for function setitimer
+[eva] tests/libc/sys_time_h.c:20: assertion got status valid.
+[eva] computing for function utimes <- main.
+ Called from tests/libc/sys_time_h.c:22.
+[eva] using specification for function utimes
+[eva] tests/libc/sys_time_h.c:22:
+ function utimes: precondition 'valid_path' got status valid.
+[eva] tests/libc/sys_time_h.c:22:
+ function utimes: precondition 'valid_times_or_null' got status valid.
+[eva] Done for function utimes
+[eva] computing for function utimes <- main.
+ Called from tests/libc/sys_time_h.c:28.
+[eva] tests/libc/sys_time_h.c:28:
+ function utimes: precondition 'valid_path' got status valid.
+[eva] tests/libc/sys_time_h.c:28:
+ function utimes: precondition 'valid_times_or_null' got status valid.
+[eva] Done for function utimes
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+ i1.it_interval.tv_sec ∈ {1}
+ .it_interval.tv_usec ∈ {100}
+ .it_value.tv_sec ∈ {2}
+ .it_value.tv_usec ∈ {200}
+ res ∈ {-1}
+ i2.it_interval.tv_sec ∈ [--..--]
+ .it_interval.tv_usec ∈ {1000000}
+ .it_value ∈ [--..--]
+ INVALID_ITIMER ∈ {-1}
+ r1 ∈ [--..--]
+ tv[0].tv_sec ∈ {10000000}
+ [0].tv_usec ∈ {999999}
+ [1].tv_sec ∈ {-9000000}
+ [1].tv_usec ∈ {1}
+ r2 ∈ [--..--]
+ __retres ∈ {0}
diff --git a/tests/libc/oracle/time_misc.res.oracle b/tests/libc/oracle/time_misc.res.oracle
index 11b3437a14bb4490511094ca437543e11a7ed99e..b869818342bf421d884def68508d5e0d39319b14 100644
--- a/tests/libc/oracle/time_misc.res.oracle
+++ b/tests/libc/oracle/time_misc.res.oracle
@@ -23,6 +23,8 @@
[eva] computing for function localtime <- test_strftime <- main.
Called from tests/libc/time_misc.c:19.
[eva] using specification for function localtime
+[eva] tests/libc/time_misc.c:19:
+ function localtime: precondition 'valid_timer' got status valid.
[eva] Done for function localtime
[eva] computing for function strftime <- test_strftime <- main.
Called from tests/libc/time_misc.c:21.
diff --git a/tests/libc/oracle/unistd_h.0.res.oracle b/tests/libc/oracle/unistd_h.0.res.oracle
index 5b653c8e60e1ae17db8af7beee6cf8ab0a0e9195..23bd3f50c5392a7f5ff4ec33796919b99c80672b 100644
--- a/tests/libc/oracle/unistd_h.0.res.oracle
+++ b/tests/libc/oracle/unistd_h.0.res.oracle
@@ -9,6 +9,7 @@
\return(gethostname) == 0 (auto)
\return(getpgrp) == 0 (auto)
\return(isatty) == 0 (auto)
+ \return(pipe) == 0 (auto)
\return(setegid) == 0 (auto)
\return(seteuid) == 0 (auto)
\return(setgid) == 0 (auto)
@@ -477,6 +478,8 @@
[eva] computing for function ttyname <- main.
Called from tests/libc/unistd_h.c:86.
[eva] using specification for function ttyname
+[eva] tests/libc/unistd_h.c:86:
+ function ttyname: precondition 'valid_fildes' got status valid.
[eva] Done for function ttyname
[eva] computing for function ttyname <- main.
Called from tests/libc/unistd_h.c:86.
@@ -529,6 +532,32 @@
[eva] computing for function chroot <- main.
Called from tests/libc/unistd_h.c:92.
[eva] Done for function chroot
+[eva] computing for function pipe <- main.
+ Called from tests/libc/unistd_h.c:95.
+[eva] using specification for function pipe
+[eva:alarm] tests/libc/unistd_h.c:95: Warning:
+ function pipe: precondition 'valid_pipefd' got status invalid.
+[eva] Done for function pipe
+[eva] computing for function pipe <- main.
+ Called from tests/libc/unistd_h.c:95.
+[eva] Done for function pipe
+[eva] computing for function pipe <- main.
+ Called from tests/libc/unistd_h.c:100.
+[eva:alarm] tests/libc/unistd_h.c:100: Warning:
+ function pipe: precondition 'valid_pipefd' got status invalid.
+[eva] Done for function pipe
+[eva] computing for function pipe <- main.
+ Called from tests/libc/unistd_h.c:100.
+[eva] Done for function pipe
+[eva] computing for function pipe <- main.
+ Called from tests/libc/unistd_h.c:104.
+[eva] tests/libc/unistd_h.c:104:
+ function pipe: precondition 'valid_pipefd' got status valid.
+[eva] Done for function pipe
+[eva] computing for function pipe <- main.
+ Called from tests/libc/unistd_h.c:104.
+[eva] Done for function pipe
+[eva] tests/libc/unistd_h.c:105: check 'ok' got status valid.
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -554,4 +583,6 @@
sgid ∈ [--..--] or UNINITIALIZED
p ∈ [--..--]
tty ∈ {{ NULL ; &__fc_ttyname[0] }}
+ halfpipe ∈ UNINITIALIZED
+ pipefd[0..1] ∈ [0..1023] or UNINITIALIZED
__retres ∈ {0; 1}
diff --git a/tests/libc/oracle/unistd_h.1.res.oracle b/tests/libc/oracle/unistd_h.1.res.oracle
index 5cd1bf50f5d48d55f8b70a02c7b37f8b1385336f..32c8e8164076a62e38d24dc837301d2d539dd3d8 100644
--- a/tests/libc/oracle/unistd_h.1.res.oracle
+++ b/tests/libc/oracle/unistd_h.1.res.oracle
@@ -9,6 +9,7 @@
\return(gethostname) == 0 (auto)
\return(getpgrp) == 0 (auto)
\return(isatty) == 0 (auto)
+ \return(pipe) == 0 (auto)
\return(setegid) == 0 (auto)
\return(seteuid) == 0 (auto)
\return(setgid) == 0 (auto)
@@ -477,6 +478,8 @@
[eva] computing for function ttyname <- main.
Called from tests/libc/unistd_h.c:86.
[eva] using specification for function ttyname
+[eva] tests/libc/unistd_h.c:86:
+ function ttyname: precondition 'valid_fildes' got status valid.
[eva] Done for function ttyname
[eva] computing for function ttyname <- main.
Called from tests/libc/unistd_h.c:86.
@@ -529,6 +532,32 @@
[eva] computing for function chroot <- main.
Called from tests/libc/unistd_h.c:92.
[eva] Done for function chroot
+[eva] computing for function pipe <- main.
+ Called from tests/libc/unistd_h.c:95.
+[eva] using specification for function pipe
+[eva:alarm] tests/libc/unistd_h.c:95: Warning:
+ function pipe: precondition 'valid_pipefd' got status invalid.
+[eva] Done for function pipe
+[eva] computing for function pipe <- main.
+ Called from tests/libc/unistd_h.c:95.
+[eva] Done for function pipe
+[eva] computing for function pipe <- main.
+ Called from tests/libc/unistd_h.c:100.
+[eva:alarm] tests/libc/unistd_h.c:100: Warning:
+ function pipe: precondition 'valid_pipefd' got status invalid.
+[eva] Done for function pipe
+[eva] computing for function pipe <- main.
+ Called from tests/libc/unistd_h.c:100.
+[eva] Done for function pipe
+[eva] computing for function pipe <- main.
+ Called from tests/libc/unistd_h.c:104.
+[eva] tests/libc/unistd_h.c:104:
+ function pipe: precondition 'valid_pipefd' got status valid.
+[eva] Done for function pipe
+[eva] computing for function pipe <- main.
+ Called from tests/libc/unistd_h.c:104.
+[eva] Done for function pipe
+[eva] tests/libc/unistd_h.c:105: check 'ok' got status valid.
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -554,4 +583,6 @@
sgid ∈ [--..--] or UNINITIALIZED
p ∈ [--..--]
tty ∈ {{ NULL ; &__fc_ttyname[0] }}
+ halfpipe ∈ UNINITIALIZED
+ pipefd[0..1] ∈ [0..1023] or UNINITIALIZED
__retres ∈ {0; 1}
diff --git a/tests/libc/oracle/wchar_c_h.0.res.oracle b/tests/libc/oracle/wchar_c_h.0.res.oracle
index 67067c92b5680061e15983d06f22d8dd457234f0..8e6c444ee9de224d23eb1b8e1040a87196b79489 100644
--- a/tests/libc/oracle/wchar_c_h.0.res.oracle
+++ b/tests/libc/oracle/wchar_c_h.0.res.oracle
@@ -8,9 +8,30 @@
t ∈ {0}
nondet ∈ [--..--]
[eva] tests/libc/wchar_c_h.c:31: Call to builtin wmemchr
+[eva] tests/libc/wchar_c_h.c:31:
+ function wmemchr: precondition 'valid' got status valid.
+[eva] share/libc/wchar.h:58:
+ Cannot evaluate range bound wmemchr_off(s, c, n)
+ (unsupported ACSL construct: logic function wmemchr_off). Approximating
+[eva] tests/libc/wchar_c_h.c:31:
+ function wmemchr: precondition 'initialization' got status valid.
+[eva] tests/libc/wchar_c_h.c:31:
+ function wmemchr: precondition 'danglingness' got status valid.
[eva] computing for function wmemcmp <- main.
Called from tests/libc/wchar_c_h.c:32.
[eva] using specification for function wmemcmp
+[eva] tests/libc/wchar_c_h.c:32:
+ function wmemcmp: precondition 'valid_s1' got status valid.
+[eva] tests/libc/wchar_c_h.c:32:
+ function wmemcmp: precondition 'valid_s2' got status valid.
+[eva] tests/libc/wchar_c_h.c:32:
+ function wmemcmp: precondition 'initialization,s1' got status valid.
+[eva] tests/libc/wchar_c_h.c:32:
+ function wmemcmp: precondition 'initialization,s2' got status valid.
+[eva] tests/libc/wchar_c_h.c:32:
+ function wmemcmp: precondition 'danglingness,s1' got status valid.
+[eva] tests/libc/wchar_c_h.c:32:
+ function wmemcmp: precondition 'danglingness,s2' got status valid.
[eva] Done for function wmemcmp
[eva] computing for function wmemcpy <- main.
Called from tests/libc/wchar_c_h.c:33.
@@ -19,6 +40,10 @@
[eva] computing for function wmemmove <- main.
Called from tests/libc/wchar_c_h.c:34.
[eva] using specification for function wmemmove
+[eva] tests/libc/wchar_c_h.c:34:
+ function wmemmove: precondition 'valid_src' got status valid.
+[eva] tests/libc/wchar_c_h.c:34:
+ function wmemmove: precondition 'valid_dest' got status valid.
[eva] Done for function wmemmove
[eva] computing for function wmemset <- main.
Called from tests/libc/wchar_c_h.c:35.
@@ -30,6 +55,10 @@
[eva] computing for function wcscmp <- main.
Called from tests/libc/wchar_c_h.c:37.
[eva] using specification for function wcscmp
+[eva] tests/libc/wchar_c_h.c:37:
+ function wcscmp: precondition 'valid_wstring_s1' got status valid.
+[eva] tests/libc/wchar_c_h.c:37:
+ function wcscmp: precondition 'valid_wstring_s2' got status valid.
[eva] Done for function wcscmp
[eva] computing for function wcscpy <- main.
Called from tests/libc/wchar_c_h.c:38.
@@ -38,14 +67,30 @@
[eva] computing for function wcscspn <- main.
Called from tests/libc/wchar_c_h.c:39.
[eva] using specification for function wcscspn
+[eva] tests/libc/wchar_c_h.c:39:
+ function wcscspn: precondition 'valid_wstring_wcs' got status valid.
+[eva] tests/libc/wchar_c_h.c:39:
+ function wcscspn: precondition 'valid_wstring_accept' got status valid.
[eva] Done for function wcscspn
[eva] computing for function wcslcat <- main.
Called from tests/libc/wchar_c_h.c:40.
[eva] using specification for function wcslcat
+[eva] tests/libc/wchar_c_h.c:40:
+ function wcslcat: precondition 'valid_nwstring_src' got status valid.
+[eva:alarm] tests/libc/wchar_c_h.c:40: Warning:
+ function wcslcat: precondition 'valid_wstring_dest' got status invalid.
+[eva] tests/libc/wchar_c_h.c:40:
+ function wcslcat: no state left, precondition 'room_for_concatenation' got status valid.
+[eva] tests/libc/wchar_c_h.c:40:
+ function wcslcat: no state left, precondition 'separation' got status valid.
[eva] Done for function wcslcat
[eva] computing for function wcslcpy <- main.
Called from tests/libc/wchar_c_h.c:41.
[eva] using specification for function wcslcpy
+[eva] tests/libc/wchar_c_h.c:41:
+ function wcslcpy: precondition 'valid_wstring_src' got status valid.
+[eva] tests/libc/wchar_c_h.c:41:
+ function wcslcpy: precondition 'room_nwstring' got status valid.
[eva] tests/libc/wchar_c_h.c:41:
function wcslcpy: precondition 'separation,dest,src' got status valid.
[eva] Done for function wcslcpy
@@ -55,6 +100,10 @@
[eva] computing for function wcsncmp <- main.
Called from tests/libc/wchar_c_h.c:43.
[eva] using specification for function wcsncmp
+[eva] tests/libc/wchar_c_h.c:43:
+ function wcsncmp: precondition 'valid_wstring_s1' got status valid.
+[eva] tests/libc/wchar_c_h.c:43:
+ function wcsncmp: precondition 'valid_wstring_s2' got status valid.
[eva] Done for function wcsncmp
[eva] computing for function wcsncpy <- main.
Called from tests/libc/wchar_c_h.c:44.
@@ -63,18 +112,32 @@
[eva] computing for function wcspbrk <- main.
Called from tests/libc/wchar_c_h.c:45.
[eva] using specification for function wcspbrk
+[eva] tests/libc/wchar_c_h.c:45:
+ function wcspbrk: precondition 'valid_wstring_wcs' got status valid.
+[eva] tests/libc/wchar_c_h.c:45:
+ function wcspbrk: precondition 'valid_wstring_accept' got status valid.
[eva] Done for function wcspbrk
[eva] computing for function wcsrchr <- main.
Called from tests/libc/wchar_c_h.c:46.
[eva] using specification for function wcsrchr
+[eva] tests/libc/wchar_c_h.c:46:
+ function wcsrchr: precondition 'valid_wstring_wcs' got status valid.
[eva] Done for function wcsrchr
[eva] computing for function wcsspn <- main.
Called from tests/libc/wchar_c_h.c:47.
[eva] using specification for function wcsspn
+[eva] tests/libc/wchar_c_h.c:47:
+ function wcsspn: precondition 'valid_wstring_wcs' got status valid.
+[eva] tests/libc/wchar_c_h.c:47:
+ function wcsspn: precondition 'valid_wstring_accept' got status valid.
[eva] Done for function wcsspn
[eva] computing for function wcsstr <- main.
Called from tests/libc/wchar_c_h.c:48.
[eva] using specification for function wcsstr
+[eva] tests/libc/wchar_c_h.c:48:
+ function wcsstr: precondition 'valid_wstring_haystack' got status valid.
+[eva] tests/libc/wchar_c_h.c:48:
+ function wcsstr: precondition 'valid_wstring_needle' got status valid.
[eva] Done for function wcsstr
[eva] computing for function wcscat <- main.
Called from tests/libc/wchar_c_h.c:52.
@@ -112,7 +175,19 @@
[eva] tests/libc/wchar_c_h.c:68:
function wcschr: precondition 'valid_wstring_src' got status valid.
[eva] tests/libc/wchar_c_h.c:69: Call to builtin wmemchr
+[eva] tests/libc/wchar_c_h.c:69:
+ function wmemchr: precondition 'valid' got status valid.
+[eva] tests/libc/wchar_c_h.c:69:
+ function wmemchr: precondition 'initialization' got status valid.
+[eva] tests/libc/wchar_c_h.c:69:
+ function wmemchr: precondition 'danglingness' got status valid.
[eva] tests/libc/wchar_c_h.c:70: Call to builtin wmemchr
+[eva] tests/libc/wchar_c_h.c:70:
+ function wmemchr: precondition 'valid' got status valid.
+[eva] tests/libc/wchar_c_h.c:70:
+ function wmemchr: precondition 'initialization' got status valid.
+[eva] tests/libc/wchar_c_h.c:70:
+ function wmemchr: precondition 'danglingness' got status valid.
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -174,7 +249,17 @@
[eva:final-states] Values at end of function main:
sc1 ∈ {{ L"Needle" }}
sc2 ∈ {{ L"Haystack" }}
- buf[0..19] ∈ [--..--] or UNINITIALIZED
+ buf[0..4] ∈ [--..--] or UNINITIALIZED
+ [5] ∈ {0; 72; 97; 115; 116; 121} or UNINITIALIZED
+ [6] ∈ {0; 97; 99; 115; 116; 121} or UNINITIALIZED
+ [7] ∈ {0; 97; 99; 107; 115; 116; 121} or UNINITIALIZED
+ [8] ∈ {0; 97; 99; 107; 115; 116} or UNINITIALIZED
+ [9] ∈ {0; 97; 99; 107; 116} or UNINITIALIZED
+ [10] ∈ {0; 97; 99; 107} or UNINITIALIZED
+ [11] ∈ {0; 99; 107} or UNINITIALIZED
+ [12] ∈ {0; 107} or UNINITIALIZED
+ [13] ∈ {0} or UNINITIALIZED
+ [14..19] ∈ UNINITIALIZED
c ∈ [--..--]
n ∈ {5}
r ∈ [--..--] or UNINITIALIZED
diff --git a/tests/libc/oracle/wchar_c_h.1.res.oracle b/tests/libc/oracle/wchar_c_h.1.res.oracle
index d90fa422c1726b48744c12ed9f5c4b199b9edb7b..8a8b446879fbfa8b923ba6416bbab050564219f2 100644
--- a/tests/libc/oracle/wchar_c_h.1.res.oracle
+++ b/tests/libc/oracle/wchar_c_h.1.res.oracle
@@ -8,23 +8,54 @@
t ∈ {0}
nondet ∈ [--..--]
[eva] tests/libc/wchar_c_h.c:31: Call to builtin wmemchr
+[eva] tests/libc/wchar_c_h.c:31:
+ function wmemchr: precondition 'valid' got status valid.
+[eva] share/libc/wchar.h:58:
+ Cannot evaluate range bound wmemchr_off(s, c, n)
+ (unsupported ACSL construct: logic function wmemchr_off). Approximating
+[eva] tests/libc/wchar_c_h.c:31:
+ function wmemchr: precondition 'initialization' got status valid.
+[eva] tests/libc/wchar_c_h.c:31:
+ function wmemchr: precondition 'danglingness' got status valid.
[eva] computing for function wmemcmp <- main.
Called from tests/libc/wchar_c_h.c:32.
[eva] using specification for function wmemcmp
+[eva] tests/libc/wchar_c_h.c:32:
+ function wmemcmp: precondition 'valid_s1' got status valid.
+[eva] tests/libc/wchar_c_h.c:32:
+ function wmemcmp: precondition 'valid_s2' got status valid.
+[eva] tests/libc/wchar_c_h.c:32:
+ function wmemcmp: precondition 'initialization,s1' got status valid.
+[eva] tests/libc/wchar_c_h.c:32:
+ function wmemcmp: precondition 'initialization,s2' got status valid.
+[eva] tests/libc/wchar_c_h.c:32:
+ function wmemcmp: precondition 'danglingness,s1' got status valid.
+[eva] tests/libc/wchar_c_h.c:32:
+ function wmemcmp: precondition 'danglingness,s2' got status valid.
[eva] Done for function wmemcmp
[eva] computing for function wmemcpy <- main.
Called from tests/libc/wchar_c_h.c:33.
[eva] using specification for function wmemcpy
+[eva] tests/libc/wchar_c_h.c:33:
+ function wmemcpy: precondition 'valid_dest' got status valid.
+[eva] tests/libc/wchar_c_h.c:33:
+ function wmemcpy: precondition 'valid_src' got status valid.
[eva] tests/libc/wchar_c_h.c:33:
function wmemcpy: precondition 'separation,dest,src' got status valid.
[eva] Done for function wmemcpy
[eva] computing for function wmemmove <- main.
Called from tests/libc/wchar_c_h.c:34.
[eva] using specification for function wmemmove
+[eva] tests/libc/wchar_c_h.c:34:
+ function wmemmove: precondition 'valid_src' got status valid.
+[eva] tests/libc/wchar_c_h.c:34:
+ function wmemmove: precondition 'valid_dest' got status valid.
[eva] Done for function wmemmove
[eva] computing for function wmemset <- main.
Called from tests/libc/wchar_c_h.c:35.
[eva] using specification for function wmemset
+[eva] tests/libc/wchar_c_h.c:35:
+ function wmemset: precondition 'valid_wcs' got status valid.
[eva] Done for function wmemset
[eva] tests/libc/wchar_c_h.c:36: Call to builtin wcschr
[eva] tests/libc/wchar_c_h.c:36:
@@ -32,22 +63,48 @@
[eva] computing for function wcscmp <- main.
Called from tests/libc/wchar_c_h.c:37.
[eva] using specification for function wcscmp
+[eva] tests/libc/wchar_c_h.c:37:
+ function wcscmp: precondition 'valid_wstring_s1' got status valid.
+[eva] tests/libc/wchar_c_h.c:37:
+ function wcscmp: precondition 'valid_wstring_s2' got status valid.
[eva] Done for function wcscmp
[eva] computing for function wcscpy <- main.
Called from tests/libc/wchar_c_h.c:38.
[eva] using specification for function wcscpy
+[eva] tests/libc/wchar_c_h.c:38:
+ function wcscpy: precondition 'valid_wstring_src' got status valid.
+[eva] tests/libc/wchar_c_h.c:38:
+ function wcscpy: precondition 'room_wstring' got status valid.
+[eva] tests/libc/wchar_c_h.c:38:
+ function wcscpy: precondition 'separation' got status valid.
[eva] Done for function wcscpy
[eva] computing for function wcscspn <- main.
Called from tests/libc/wchar_c_h.c:39.
[eva] using specification for function wcscspn
+[eva] tests/libc/wchar_c_h.c:39:
+ function wcscspn: precondition 'valid_wstring_wcs' got status valid.
+[eva] tests/libc/wchar_c_h.c:39:
+ function wcscspn: precondition 'valid_wstring_accept' got status valid.
[eva] Done for function wcscspn
[eva] computing for function wcslcat <- main.
Called from tests/libc/wchar_c_h.c:40.
[eva] using specification for function wcslcat
+[eva] tests/libc/wchar_c_h.c:40:
+ function wcslcat: precondition 'valid_nwstring_src' got status valid.
+[eva:alarm] tests/libc/wchar_c_h.c:40: Warning:
+ function wcslcat: precondition 'valid_wstring_dest' got status invalid.
+[eva] tests/libc/wchar_c_h.c:40:
+ function wcslcat: no state left, precondition 'room_for_concatenation' got status valid.
+[eva] tests/libc/wchar_c_h.c:40:
+ function wcslcat: no state left, precondition 'separation' got status valid.
[eva] Done for function wcslcat
[eva] computing for function wcslcpy <- main.
Called from tests/libc/wchar_c_h.c:41.
[eva] using specification for function wcslcpy
+[eva] tests/libc/wchar_c_h.c:41:
+ function wcslcpy: precondition 'valid_wstring_src' got status valid.
+[eva] tests/libc/wchar_c_h.c:41:
+ function wcslcpy: precondition 'room_nwstring' got status valid.
[eva] tests/libc/wchar_c_h.c:41:
function wcslcpy: precondition 'separation,dest,src' got status valid.
[eva] Done for function wcslcpy
@@ -57,36 +114,74 @@
[eva] computing for function wcsncmp <- main.
Called from tests/libc/wchar_c_h.c:43.
[eva] using specification for function wcsncmp
+[eva] tests/libc/wchar_c_h.c:43:
+ function wcsncmp: precondition 'valid_wstring_s1' got status valid.
+[eva] tests/libc/wchar_c_h.c:43:
+ function wcsncmp: precondition 'valid_wstring_s2' got status valid.
[eva] Done for function wcsncmp
[eva] computing for function wcsncpy <- main.
Called from tests/libc/wchar_c_h.c:44.
[eva] using specification for function wcsncpy
+[eva] tests/libc/wchar_c_h.c:44:
+ function wcsncpy: precondition 'valid_wstring_src' got status valid.
+[eva] tests/libc/wchar_c_h.c:44:
+ function wcsncpy: precondition 'room_nwstring' got status valid.
[eva] tests/libc/wchar_c_h.c:44:
function wcsncpy: precondition 'separation,dest,src' got status valid.
[eva] Done for function wcsncpy
[eva] computing for function wcspbrk <- main.
Called from tests/libc/wchar_c_h.c:45.
[eva] using specification for function wcspbrk
+[eva] tests/libc/wchar_c_h.c:45:
+ function wcspbrk: precondition 'valid_wstring_wcs' got status valid.
+[eva] tests/libc/wchar_c_h.c:45:
+ function wcspbrk: precondition 'valid_wstring_accept' got status valid.
[eva] Done for function wcspbrk
[eva] computing for function wcsrchr <- main.
Called from tests/libc/wchar_c_h.c:46.
[eva] using specification for function wcsrchr
+[eva] tests/libc/wchar_c_h.c:46:
+ function wcsrchr: precondition 'valid_wstring_wcs' got status valid.
[eva] Done for function wcsrchr
[eva] computing for function wcsspn <- main.
Called from tests/libc/wchar_c_h.c:47.
[eva] using specification for function wcsspn
+[eva] tests/libc/wchar_c_h.c:47:
+ function wcsspn: precondition 'valid_wstring_wcs' got status valid.
+[eva] tests/libc/wchar_c_h.c:47:
+ function wcsspn: precondition 'valid_wstring_accept' got status valid.
[eva] Done for function wcsspn
[eva] computing for function wcsstr <- main.
Called from tests/libc/wchar_c_h.c:48.
[eva] using specification for function wcsstr
+[eva] tests/libc/wchar_c_h.c:48:
+ function wcsstr: precondition 'valid_wstring_haystack' got status valid.
+[eva] tests/libc/wchar_c_h.c:48:
+ function wcsstr: precondition 'valid_wstring_needle' got status valid.
[eva] Done for function wcsstr
[eva] computing for function wcscat <- main.
Called from tests/libc/wchar_c_h.c:52.
[eva] using specification for function wcscat
+[eva] tests/libc/wchar_c_h.c:52:
+ function wcscat: precondition 'valid_wstring_src' got status valid.
+[eva] tests/libc/wchar_c_h.c:52:
+ function wcscat: precondition 'valid_wstring_dest' got status valid.
+[eva] tests/libc/wchar_c_h.c:52:
+ function wcscat: precondition 'room_for_concatenation' got status valid.
+[eva] tests/libc/wchar_c_h.c:52:
+ function wcscat: precondition 'separation' got status valid.
[eva] Done for function wcscat
[eva] computing for function wcsncat <- main.
Called from tests/libc/wchar_c_h.c:54.
[eva] using specification for function wcsncat
+[eva] tests/libc/wchar_c_h.c:54:
+ function wcsncat: precondition 'valid_nwstring_src' got status valid.
+[eva] tests/libc/wchar_c_h.c:54:
+ function wcsncat: precondition 'valid_wstring_dest' got status valid.
+[eva] tests/libc/wchar_c_h.c:54:
+ function wcsncat: precondition 'room_for_concatenation' got status valid.
+[eva] tests/libc/wchar_c_h.c:54:
+ function wcsncat: precondition 'separation' got status valid.
[eva] Done for function wcsncat
[eva] tests/libc/wchar_c_h.c:57: Call to builtin wcslen
[eva:alarm] tests/libc/wchar_c_h.c:57: Warning:
@@ -110,7 +205,19 @@
[eva] tests/libc/wchar_c_h.c:68:
function wcschr: precondition 'valid_wstring_src' got status valid.
[eva] tests/libc/wchar_c_h.c:69: Call to builtin wmemchr
+[eva] tests/libc/wchar_c_h.c:69:
+ function wmemchr: precondition 'valid' got status valid.
+[eva] tests/libc/wchar_c_h.c:69:
+ function wmemchr: precondition 'initialization' got status valid.
+[eva] tests/libc/wchar_c_h.c:69:
+ function wmemchr: precondition 'danglingness' got status valid.
[eva] tests/libc/wchar_c_h.c:70: Call to builtin wmemchr
+[eva] tests/libc/wchar_c_h.c:70:
+ function wmemchr: precondition 'valid' got status valid.
+[eva] tests/libc/wchar_c_h.c:70:
+ function wmemchr: precondition 'initialization' got status valid.
+[eva] tests/libc/wchar_c_h.c:70:
+ function wmemchr: precondition 'danglingness' got status valid.
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/libc/oracle/wchar_h.res.oracle b/tests/libc/oracle/wchar_h.res.oracle
index e1161566c7fd14a4c7f27edfa0bad2ff7818e2b3..2ffbd071fc836e2895f3dcf5ae60d6a8f06b29ec 100644
--- a/tests/libc/oracle/wchar_h.res.oracle
+++ b/tests/libc/oracle/wchar_h.res.oracle
@@ -3,7 +3,7 @@
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-
+ v ∈ [--..--]
[eva] computing for function fopen <- main.
Called from tests/libc/wchar_h.c:5.
[eva] using specification for function fopen
@@ -15,15 +15,196 @@
[eva] computing for function fgetws <- main.
Called from tests/libc/wchar_h.c:8.
[eva] using specification for function fgetws
+[eva] tests/libc/wchar_h.c:8:
+ function fgetws: precondition 'room_nwstring' got status valid.
[eva] tests/libc/wchar_h.c:8:
function fgetws: precondition 'valid_stream' got status valid.
[eva] Done for function fgetws
[eva] tests/libc/wchar_h.c:10: assertion got status valid.
+[eva] tests/libc/wchar_h.c:13: Call to builtin wmemchr
+[eva] tests/libc/wchar_h.c:13:
+ function wmemchr: precondition 'valid' got status valid.
+[eva] share/libc/wchar.h:58:
+ Cannot evaluate range bound wmemchr_off(s, c, n)
+ (unsupported ACSL construct: logic function wmemchr_off). Approximating
+[eva:alarm] tests/libc/wchar_h.c:13: Warning:
+ function wmemchr: precondition 'initialization' got status unknown.
+[eva] tests/libc/wchar_h.c:13:
+ function wmemchr: precondition 'danglingness' got status valid.
+[eva] tests/libc/wchar_h.c:14: check 'ok' got status valid.
+[eva] tests/libc/wchar_h.c:15: Call to builtin wmemchr
+[eva] share/libc/wchar.h:55:
+ Cannot evaluate range bound wmemchr_off(s, c, n)
+ (unsupported ACSL construct: logic function wmemchr_off). Approximating
+[eva:alarm] tests/libc/wchar_h.c:15: Warning:
+ function wmemchr: precondition 'valid' got status unknown.
+[eva] tests/libc/wchar_h.c:15:
+ function wmemchr: precondition 'initialization' got status valid.
+[eva] tests/libc/wchar_h.c:15:
+ function wmemchr: precondition 'danglingness' got status valid.
+[eva] tests/libc/wchar_h.c:16: check 'ok' got status valid.
+[eva] tests/libc/wchar_h.c:18: Call to builtin wmemchr
+[eva] tests/libc/wchar_h.c:18:
+ function wmemchr: precondition 'valid' got status valid.
+[eva:alarm] tests/libc/wchar_h.c:18: Warning:
+ function wmemchr: precondition 'initialization' got status unknown.
+[eva] tests/libc/wchar_h.c:18:
+ function wmemchr: precondition 'danglingness' got status valid.
+[eva] tests/libc/wchar_h.c:21: Call to builtin wmemchr
+[eva:alarm] tests/libc/wchar_h.c:21: Warning:
+ function wmemchr: precondition 'valid' got status unknown.
+[eva:alarm] tests/libc/wchar_h.c:21: Warning:
+ function wmemchr: precondition 'initialization' got status unknown.
+[eva:alarm] tests/libc/wchar_h.c:21: Warning:
+ function wmemchr: precondition 'danglingness' got status unknown.
+[eva] tests/libc/wchar_h.c:22: check 'ok' got status valid.
+[eva] tests/libc/wchar_h.c:24: Call to builtin wmemchr
+[eva:alarm] tests/libc/wchar_h.c:24: Warning:
+ function wmemchr: precondition 'valid' got status unknown.
+[eva:alarm] tests/libc/wchar_h.c:24: Warning:
+ function wmemchr: precondition 'initialization' got status unknown.
+[eva:alarm] tests/libc/wchar_h.c:24: Warning:
+ function wmemchr: precondition 'danglingness' got status unknown.
+[eva] tests/libc/wchar_h.c:25: check 'ok' got status valid.
+[eva] tests/libc/wchar_h.c:26: Call to builtin wmemchr
+[eva:alarm] tests/libc/wchar_h.c:26: Warning:
+ function wmemchr: precondition 'valid' got status unknown.
+[eva:alarm] tests/libc/wchar_h.c:26: Warning:
+ function wmemchr: precondition 'initialization' got status unknown.
+[eva:alarm] tests/libc/wchar_h.c:26: Warning:
+ function wmemchr: precondition 'danglingness' got status unknown.
+[eva] tests/libc/wchar_h.c:27: check 'ok' got status valid.
+[eva] tests/libc/wchar_h.c:29: Call to builtin wmemchr
+[eva:alarm] tests/libc/wchar_h.c:29: Warning:
+ function wmemchr: precondition 'valid' got status unknown.
+[eva:alarm] tests/libc/wchar_h.c:29: Warning:
+ function wmemchr: precondition 'initialization' got status unknown.
+[eva:alarm] tests/libc/wchar_h.c:29: Warning:
+ function wmemchr: precondition 'danglingness' got status unknown.
+[eva] tests/libc/wchar_h.c:30: check 'ok' got status valid.
+[eva] computing for function wcsncpy <- main.
+ Called from tests/libc/wchar_h.c:33.
+[eva] using specification for function wcsncpy
+[eva] tests/libc/wchar_h.c:33:
+ function wcsncpy: precondition 'valid_wstring_src' got status valid.
+[eva] tests/libc/wchar_h.c:33:
+ function wcsncpy: precondition 'room_nwstring' got status valid.
+[eva] tests/libc/wchar_h.c:33:
+ function wcsncpy: precondition 'separation,dest,src' got status valid.
+[eva] Done for function wcsncpy
+[eva] tests/libc/wchar_h.c:34: check 'ok' got status valid.
+[eva] tests/libc/wchar_h.c:35: check 'ok' got status valid.
+[eva] tests/libc/wchar_h.c:37: Call to builtin wcslen
+[eva] tests/libc/wchar_h.c:37:
+ function wcslen: precondition 'valid_string_s' got status valid.
+[eva] computing for function wcsncpy <- main.
+ Called from tests/libc/wchar_h.c:37.
+[eva] tests/libc/wchar_h.c:37:
+ function wcsncpy: precondition 'valid_wstring_src' got status valid.
+[eva:alarm] tests/libc/wchar_h.c:37: Warning:
+ function wcsncpy: precondition 'room_nwstring' got status invalid.
+[eva] tests/libc/wchar_h.c:37:
+ function wcsncpy: no state left, precondition 'separation,dest,src' got status valid.
+[eva] Done for function wcsncpy
+[eva] computing for function wcsncpy <- main.
+ Called from tests/libc/wchar_h.c:41.
+[eva:alarm] tests/libc/wchar_h.c:41: Warning:
+ function wcsncpy: precondition 'valid_wstring_src' got status unknown.
+[eva] tests/libc/wchar_h.c:41:
+ function wcsncpy: precondition 'room_nwstring' got status valid.
+[eva:alarm] tests/libc/wchar_h.c:41: Warning:
+ function wcsncpy: precondition 'separation,dest,src' got status invalid.
+[eva] Done for function wcsncpy
+[eva] computing for function wcsncpy <- main.
+ Called from tests/libc/wchar_h.c:45.
+[eva] tests/libc/wchar_h.c:45:
+ function wcsncpy: precondition 'valid_wstring_src' got status valid.
+[eva:alarm] tests/libc/wchar_h.c:45: Warning:
+ function wcsncpy: precondition 'room_nwstring' got status invalid.
+[eva] tests/libc/wchar_h.c:45:
+ function wcsncpy: no state left, precondition 'separation,dest,src' got status valid.
+[eva] Done for function wcsncpy
+[eva] computing for function wcsncpy <- main.
+ Called from tests/libc/wchar_h.c:49.
+[eva:alarm] tests/libc/wchar_h.c:49: Warning:
+ function wcsncpy: precondition 'valid_wstring_src' got status invalid.
+[eva] tests/libc/wchar_h.c:49:
+ function wcsncpy: no state left, precondition 'room_nwstring' got status valid.
+[eva] tests/libc/wchar_h.c:49:
+ function wcsncpy: no state left, precondition 'separation,dest,src' got status valid.
+[eva] Done for function wcsncpy
+[eva] computing for function wcsncpy <- main.
+ Called from tests/libc/wchar_h.c:53.
+[eva:alarm] tests/libc/wchar_h.c:53: Warning:
+ function wcsncpy: precondition 'valid_wstring_src' got status unknown.
+[eva:alarm] tests/libc/wchar_h.c:53: Warning:
+ function wcsncpy: precondition 'room_nwstring' got status invalid.
+[eva] tests/libc/wchar_h.c:53:
+ function wcsncpy: no state left, precondition 'separation,dest,src' got status valid.
+[eva] Done for function wcsncpy
+[eva] computing for function wcsncmp <- main.
+ Called from tests/libc/wchar_h.c:56.
+[eva] using specification for function wcsncmp
+[eva] tests/libc/wchar_h.c:56:
+ function wcsncmp: precondition 'valid_wstring_s1' got status valid.
+[eva] tests/libc/wchar_h.c:56:
+ function wcsncmp: precondition 'valid_wstring_s2' got status valid.
+[eva] Done for function wcsncmp
+[eva] computing for function wcsncmp <- main.
+ Called from tests/libc/wchar_h.c:57.
+[eva] tests/libc/wchar_h.c:57:
+ function wcsncmp: precondition 'valid_wstring_s1' got status valid.
+[eva:alarm] tests/libc/wchar_h.c:57: Warning:
+ function wcsncmp: precondition 'valid_wstring_s2' got status unknown.
+[eva] Done for function wcsncmp
+[eva] computing for function wcsncat <- main.
+ Called from tests/libc/wchar_h.c:59.
+[eva] using specification for function wcsncat
+[eva] tests/libc/wchar_h.c:59:
+ function wcsncat: precondition 'valid_nwstring_src' got status valid.
+[eva] tests/libc/wchar_h.c:59:
+ function wcsncat: precondition 'valid_wstring_dest' got status valid.
+[eva] tests/libc/wchar_h.c:59:
+ function wcsncat: precondition 'room_for_concatenation' got status valid.
+[eva] tests/libc/wchar_h.c:59:
+ function wcsncat: precondition 'separation' got status valid.
+[eva] Done for function wcsncat
+[eva] computing for function wcsncat <- main.
+ Called from tests/libc/wchar_h.c:60.
+[eva] tests/libc/wchar_h.c:60:
+ function wcsncat: precondition 'valid_nwstring_src' got status valid.
+[eva:alarm] tests/libc/wchar_h.c:60: Warning:
+ function wcsncat: precondition 'valid_wstring_dest' got status unknown.
+[eva:alarm] tests/libc/wchar_h.c:60: Warning:
+ function wcsncat: precondition 'room_for_concatenation' got status unknown.
+[eva] tests/libc/wchar_h.c:60:
+ function wcsncat: precondition 'separation' got status valid.
+[eva] Done for function wcsncat
+[eva] computing for function wcsncat <- main.
+ Called from tests/libc/wchar_h.c:66.
+[eva] tests/libc/wchar_h.c:66:
+ function wcsncat: precondition 'valid_nwstring_src' got status valid.
+[eva] tests/libc/wchar_h.c:66:
+ function wcsncat: precondition 'valid_wstring_dest' got status valid.
+[eva:alarm] tests/libc/wchar_h.c:66: Warning:
+ function wcsncat: precondition 'room_for_concatenation' got status invalid.
+[eva] tests/libc/wchar_h.c:66:
+ function wcsncat: no state left, precondition 'separation' got status valid.
+[eva] Done for function wcsncat
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
fd ∈ {{ NULL ; &__fc_fopen + [0..120],0%8 }}
- buf[0..29] ∈ [--..--] or UNINITIALIZED
+ buf[0..28] ∈ [--..--] or UNINITIALIZED
+ [29] ∈ UNINITIALIZED
res ∈ {{ NULL ; &buf[0] }}
+ buf2[0] ∈ {97} or UNINITIALIZED
+ [1] ∈ {98} or UNINITIALIZED
+ r ∈ {{ &wdst[0] }}
+ wsrc ∈ {{ L"wide thing" }}
+ wdst[0..9] ∈ [--..--] or UNINITIALIZED
+ wdst2[0..9] ∈ {65}
+ [10] ∈ {0}
+ [11..19] ∈ [--..--]
__retres ∈ {0; 1}
diff --git a/tests/libc/stdio_h.c b/tests/libc/stdio_h.c
index 9e9ac6ba242de5f7bb922d965b18eed6b3393c80..a1d6f3fa161b6d6edc7ac04fd41056285eea2f00 100644
--- a/tests/libc/stdio_h.c
+++ b/tests/libc/stdio_h.c
@@ -29,5 +29,15 @@ int main() {
if (!redirected) return 3;
printf("redirected to file");
fclose(redirected);
+
+ char fgets_buf0[1];
+ char *fgets_res = fgets(fgets_buf0, 1, f); // ok
+ if (!fgets_res) return 1;
+ //@ check \initialized(&fgets_buf0[0]);
+ if (nondet) {
+ fgets(fgets_buf0, 2, f); // error: buf too small
+ //@ assert unreachable: \false;
+ }
+
return 0;
}
diff --git a/tests/libc/sys_time.c b/tests/libc/sys_time_h.c
similarity index 74%
rename from tests/libc/sys_time.c
rename to tests/libc/sys_time_h.c
index 51808be30647c078a6b23b1813df9e5a1b4b9346..2ec5bcf485a068132a17e9885092ab322067fcfe 100644
--- a/tests/libc/sys_time.c
+++ b/tests/libc/sys_time_h.c
@@ -18,5 +18,14 @@ int main() {
i2.it_interval.tv_usec = 1000000; // invalid tv_usec
res = setitimer(ITIMER_VIRTUAL, &i2, &i1);
//@ assert res == -1;
+
+ int r1 = utimes("/tmp/utimes", 0);
+ struct timeval tv[2] =
+ {
+ { .tv_sec = 10000000, .tv_usec = 999999 },
+ { .tv_sec = -9000000, .tv_usec = 1 },
+ };
+ int r2 = utimes("/tmp/utimes", tv);
+
return 0;
}
diff --git a/tests/libc/unistd_h.c b/tests/libc/unistd_h.c
index b625b3b83d2d10e57806e83a9bf73d7521d08134..8c3104215bf71005b84e6d834a103ebe75056110 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;
}
diff --git a/tests/libc/wchar_h.c b/tests/libc/wchar_h.c
index c10e733da9168c3ffb7537e5c97faf20d8727105..e7cb493fa75d8adf0b06af406ebdf64c38dd3463 100644
--- a/tests/libc/wchar_h.c
+++ b/tests/libc/wchar_h.c
@@ -1,6 +1,6 @@
#include <stdio.h>
#include <wchar.h>
-
+volatile int v;
int main() {
FILE *fd = fopen("bla", "r");
if (!fd) return 1;
@@ -8,5 +8,63 @@ int main() {
wchar_t *res = fgetws(buf, 29, fd);
if (!res) return 1;
//@ assert res == buf;
+ wchar_t buf2[2];
+ buf2[0] = L'a';
+ wchar_t *r = wmemchr(buf2, L'a', 2); // no warning
+ //@ check ok: r != \null;
+ r = wmemchr(0, 0, 0); // should be ok
+ //@ check ok: r == \null;
+ if (v) {
+ r = wmemchr(buf2, 0, 2); // red alarm (uninit)
+ //@ assert unreachable:\false;
+ }
+ r = wmemchr(buf2, L'a', 3); // no warning
+ //@ check ok: r != \null;
+ if (v) buf2[1] = L'b';
+ r = wmemchr(buf2, L'a', 3); // no warning
+ //@ check ok: r != \null;
+ r = wmemchr(buf2, L'b', 3); // warning: buf2[1] maybe uninit
+ //@ check ok: r != \null;
+ buf2[1] = L'b';
+ r = wmemchr(buf2, L'b', 3); // no warning
+ //@ check ok: r != \null;
+ wchar_t *wsrc = L"wide thing";
+ wchar_t wdst[10];
+ r = wcsncpy(wdst, wsrc, 10); // no warning
+ //@ check ok: r == wdst;
+ //@ check ok: \initialized(&wdst[9]);
+ if (v) {
+ r = wcsncpy(wdst, wsrc, wcslen(wsrc)+1); // error: not enough room
+ //@ assert unreachable:\false;
+ }
+ if (v) {
+ wcsncpy(wdst, wdst, 10); // error: no separation
+ //@ assert unreachable:\false;
+ }
+ if (v) {
+ wcsncpy(0, wsrc, 10); // error: invalid dest
+ //@ assert unreachable:\false;
+ }
+ if (v) {
+ wcsncpy(wdst, 0, 10); // error: invalid src
+ //@ assert unreachable:\false;
+ }
+ if (v) {
+ wcsncpy(wsrc, wdst, 10); // error: non-writable dest
+ //@ assert unreachable:\false;
+ }
+ wcsncmp(wsrc, wsrc, 11); // no warning
+ wcsncmp(wsrc, wdst, 11); // warning: wdst possibly invalid
+ wchar_t wdst2[20] = {0};
+ wcsncat(wdst2, wsrc, 11); // no warning
+ wcsncat(wdst2, wsrc, 10); // no warning (if wdst2 is precise)
+ //@ loop unroll 10;
+ for (int i = 0; i < 10; i++)
+ wdst2[i] = L'A';
+ wdst2[10] = L'\0'; // wdst2 now has length 10
+ if (v) {
+ wcsncat(wdst2+10, wdst2, 10); // error: no separation
+ //@ assert unreachable:\false;
+ }
return 0;
}
diff --git a/tests/metrics/oracle/libc.1.res.oracle b/tests/metrics/oracle/libc.1.res.oracle
index eca3c4a7d227c3204cc015581c99570d60fa0430..24cfd8d35b1ec774597df2d92db5dcd32f240b4b 100644
--- a/tests/metrics/oracle/libc.1.res.oracle
+++ b/tests/metrics/oracle/libc.1.res.oracle
@@ -53,7 +53,7 @@
==============
Sloc = 17
Decision point = 0
- Global variables = 15
+ Global variables = 17
If = 0
Loop = 0
Goto = 0
diff --git a/tests/misc/custom_machdep/__fc_machdep_custom.h b/tests/misc/custom_machdep/__fc_machdep_custom.h
index fff2b8698abe93f750aeb65fe8ad3506a2a06396..27db308403368e394b64d739b9ac7e2c9699f936 100644
--- a/tests/misc/custom_machdep/__fc_machdep_custom.h
+++ b/tests/misc/custom_machdep/__fc_machdep_custom.h
@@ -74,6 +74,8 @@
/* POSIX */
#define __SSIZE_T int
+/* stdio.h */
+#define __FC_L_tmpnam 1024
/* stdint.h */
#define __FC_PTRDIFF_MIN __FC_INT_MIN
#define __FC_PTRDIFF_MAX __FC_INT_MAX
diff --git a/tests/rte/oracle/value_rte.res.oracle b/tests/rte/oracle/value_rte.res.oracle
index fe5023c92a121cd742479c4988f5163e4386ec40..2cf4947a7f1281fb2a53427ea27d2d494282ebd9 100644
--- a/tests/rte/oracle/value_rte.res.oracle
+++ b/tests/rte/oracle/value_rte.res.oracle
@@ -43,6 +43,7 @@
cpt ∈ {0; 1; 2; 3; 4}
tmp ∈ [-2147483648..4]
__retres ∈ {1}
+ S___fc_stdin[0..1] ∈ [--..--]
[report] Computing properties status...
--------------------------------------------------------------------------------
--- Global Properties
@@ -114,6 +115,10 @@
Unverifiable but considered Valid.
[ Extern ] Axiom 'wcsncmp_zero'
Unverifiable but considered Valid.
+[ Extern ] Axiom 'wmemchr_def'
+ Unverifiable but considered Valid.
+[ Valid ] Axiomatic 'GetsLength'
+ by Frama-C kernel.
[ Valid ] Axiomatic 'MemChr'
by Frama-C kernel.
[ Valid ] Axiomatic 'MemCmp'
@@ -128,6 +133,8 @@
by Frama-C kernel.
[ Valid ] Axiomatic 'StrNCmp'
by Frama-C kernel.
+[ Valid ] Axiomatic 'WMemChr'
+ by Frama-C kernel.
[ Valid ] Axiomatic 'WcsChr'
by Frama-C kernel.
[ Valid ] Axiomatic 'WcsCmp'
@@ -145,8 +152,12 @@
--- Properties of Function 'remove'
--------------------------------------------------------------------------------
+[ Extern ] Post-condition 'result_ok_or_error'
+ Unverifiable but considered Valid.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 76)
+ Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -154,8 +165,12 @@
--- Properties of Function 'rename'
--------------------------------------------------------------------------------
+[ Extern ] Post-condition 'result_ok_or_error'
+ Unverifiable but considered Valid.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 85)
+ Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -167,7 +182,7 @@
Unverifiable but considered Valid.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 80)
+[ Extern ] Froms (file share/libc/stdio.h, line 95)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -176,11 +191,15 @@
--- Properties of Function 'tmpnam'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 87)
+[ Extern ] Post-condition 'result_string_or_null'
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/stdio.h, line 109)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 87)
+[ Extern ] Froms (file share/libc/stdio.h, line 109)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 88)
+[ Extern ] Froms (file share/libc/stdio.h, line 111)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 112)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -193,7 +212,7 @@
Unverifiable but considered Valid.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 95)
+[ Extern ] Froms (file share/libc/stdio.h, line 121)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -204,12 +223,32 @@
[ Extern ] Post-condition 'result_zero_or_EOF'
Unverifiable but considered Valid.
-[ Extern ] Assigns nothing
+[ Extern ] Assigns (file share/libc/stdio.h, line 130)
+ Unverifiable but considered Valid.
+[ Extern ] Assigns for 'flush_all' (file share/libc/stdio.h, line 137)
+ Unverifiable but considered Valid.
+[ Extern ] Assigns for 'flush_stream' (file share/libc/stdio.h, line 142)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 130)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 132)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 132)
+ Unverifiable but considered Valid.
+[ Extern ] Froms for 'flush_all' (file share/libc/stdio.h, line 137)
+ Unverifiable but considered Valid.
+[ Extern ] Froms for 'flush_all' (file share/libc/stdio.h, line 139)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 103)
+[ Extern ] Froms for 'flush_stream' (file share/libc/stdio.h, line 142)
+ Unverifiable but considered Valid.
+[ Extern ] Froms for 'flush_stream' (file share/libc/stdio.h, line 143)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
+[ Valid ] Behavior 'flush_all'
+ by Frama-C kernel.
+[ Valid ] Behavior 'flush_stream'
+ by Frama-C kernel.
--------------------------------------------------------------------------------
--- Properties of Function 'fopen'
@@ -219,7 +258,7 @@
Unverifiable but considered Valid.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 112)
+[ Extern ] Froms (file share/libc/stdio.h, line 152)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -230,11 +269,11 @@
[ Extern ] Post-condition 'result_null_or_valid_fd'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 121)
+[ Extern ] Assigns (file share/libc/stdio.h, line 162)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 121)
+[ Extern ] Froms (file share/libc/stdio.h, line 162)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 121)
+[ Extern ] Froms (file share/libc/stdio.h, line 162)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -247,11 +286,11 @@
Unverifiable but considered Valid.
[ Extern ] Post-condition 'stream_opened'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 132)
+[ Extern ] Assigns (file share/libc/stdio.h, line 174)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 132)
+[ Extern ] Froms (file share/libc/stdio.h, line 174)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 134)
+[ Extern ] Froms (file share/libc/stdio.h, line 176)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -260,9 +299,9 @@
--- Properties of Function 'setbuf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 145)
+[ Extern ] Assigns (file share/libc/stdio.h, line 187)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 145)
+[ Extern ] Froms (file share/libc/stdio.h, line 187)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -271,9 +310,9 @@
--- Properties of Function 'setvbuf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 149)
+[ Extern ] Assigns (file share/libc/stdio.h, line 191)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 149)
+[ Extern ] Froms (file share/libc/stdio.h, line 191)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -282,9 +321,9 @@
--- Properties of Function 'vfprintf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 178)
+[ Extern ] Assigns (file share/libc/stdio.h, line 220)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 178)
+[ Extern ] Froms (file share/libc/stdio.h, line 220)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -293,9 +332,9 @@
--- Properties of Function 'vfscanf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 183)
+[ Extern ] Assigns (file share/libc/stdio.h, line 225)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 183)
+[ Extern ] Froms (file share/libc/stdio.h, line 225)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -304,9 +343,9 @@
--- Properties of Function 'vprintf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 189)
+[ Extern ] Assigns (file share/libc/stdio.h, line 231)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 189)
+[ Extern ] Froms (file share/libc/stdio.h, line 231)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -315,9 +354,9 @@
--- Properties of Function 'vscanf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 193)
+[ Extern ] Assigns (file share/libc/stdio.h, line 235)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 193)
+[ Extern ] Froms (file share/libc/stdio.h, line 235)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -326,9 +365,9 @@
--- Properties of Function 'vsnprintf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 198)
+[ Extern ] Assigns (file share/libc/stdio.h, line 240)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 198)
+[ Extern ] Froms (file share/libc/stdio.h, line 240)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -337,9 +376,9 @@
--- Properties of Function 'vsprintf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 204)
+[ Extern ] Assigns (file share/libc/stdio.h, line 246)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 204)
+[ Extern ] Froms (file share/libc/stdio.h, line 246)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -350,11 +389,11 @@
[ Extern ] Post-condition 'result_uchar_or_eof'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 217)
+[ Extern ] Assigns (file share/libc/stdio.h, line 259)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 217)
+[ Extern ] Froms (file share/libc/stdio.h, line 259)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 218)
+[ Extern ] Froms (file share/libc/stdio.h, line 260)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -365,13 +404,15 @@
[ Extern ] Post-condition 'result_null_or_same'
Unverifiable but considered Valid.
+[ Extern ] Post-condition 'initialization,at_least_one'
+ Unverifiable but considered Valid.
[ Extern ] Post-condition 'terminated_string_on_success'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 225)
+[ Extern ] Assigns (file share/libc/stdio.h, line 268)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 225)
+[ Extern ] Froms (file share/libc/stdio.h, line 268)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 226)
+[ Extern ] Froms (file share/libc/stdio.h, line 269)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -380,7 +421,11 @@
--- Properties of Function 'fputc'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 234)
+[ Extern ] Assigns (file share/libc/stdio.h, line 282)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 282)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 283)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -389,9 +434,11 @@
--- Properties of Function 'fputs'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 237)
+[ Extern ] Assigns (file share/libc/stdio.h, line 289)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 237)
+[ Extern ] Froms (file share/libc/stdio.h, line 289)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 290)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -400,11 +447,11 @@
--- Properties of Function 'getc'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 241)
+[ Extern ] Assigns (file share/libc/stdio.h, line 297)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 241)
+[ Extern ] Froms (file share/libc/stdio.h, line 297)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 241)
+[ Extern ] Froms (file share/libc/stdio.h, line 297)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -413,9 +460,11 @@
--- Properties of Function 'getchar'
--------------------------------------------------------------------------------
-[ Extern ] Assigns nothing
+[ Extern ] Assigns (file share/libc/stdio.h, line 302)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 302)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 244)
+[ Extern ] Froms (file share/libc/stdio.h, line 302)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -426,11 +475,13 @@
[ Extern ] Post-condition 'result_null_or_same'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 248)
+[ Extern ] Assigns (file share/libc/stdio.h, line 315)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 248)
+[ Extern ] Froms (file share/libc/stdio.h, line 315)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 249)
+[ Extern ] Froms (file share/libc/stdio.h, line 316)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 317)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -439,9 +490,11 @@
--- Properties of Function 'putc'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 254)
+[ Extern ] Assigns (file share/libc/stdio.h, line 324)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 254)
+[ Extern ] Froms (file share/libc/stdio.h, line 324)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 325)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -450,9 +503,11 @@
--- Properties of Function 'putchar'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 257)
+[ Extern ] Assigns (file share/libc/stdio.h, line 330)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 330)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 257)
+[ Extern ] Froms (file share/libc/stdio.h, line 331)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -461,9 +516,11 @@
--- Properties of Function 'puts'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 260)
+[ Extern ] Assigns (file share/libc/stdio.h, line 337)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 260)
+[ Extern ] Froms (file share/libc/stdio.h, line 337)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 338)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -472,9 +529,13 @@
--- Properties of Function 'ungetc'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 263)
+[ Extern ] Post-condition 'result_ok_or_error'
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/stdio.h, line 344)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 263)
+[ Extern ] Froms (file share/libc/stdio.h, line 344)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 345)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -487,11 +548,13 @@
Unverifiable but considered Valid.
[ Extern ] Post-condition 'initialization'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 269)
+[ Extern ] Assigns (file share/libc/stdio.h, line 353)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 269)
+[ Extern ] Froms (file share/libc/stdio.h, line 353)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 270)
+[ Extern ] Froms (file share/libc/stdio.h, line 353)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 355)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -502,11 +565,11 @@
[ Extern ] Post-condition 'size_written'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 282)
+[ Extern ] Assigns (file share/libc/stdio.h, line 366)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 282)
+[ Extern ] Froms (file share/libc/stdio.h, line 366)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 282)
+[ Extern ] Froms (file share/libc/stdio.h, line 366)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -515,9 +578,11 @@
--- Properties of Function 'fgetpos'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 290)
+[ Extern ] Assigns (file share/libc/stdio.h, line 377)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 290)
+[ Extern ] Froms (file share/libc/stdio.h, line 377)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 378)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -526,13 +591,13 @@
--- Properties of Function 'fseek'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 297)
+[ Extern ] Assigns (file share/libc/stdio.h, line 386)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 297)
+[ Extern ] Froms (file share/libc/stdio.h, line 386)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 298)
+[ Extern ] Froms (file share/libc/stdio.h, line 387)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 298)
+[ Extern ] Froms (file share/libc/stdio.h, line 387)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -541,9 +606,9 @@
--- Properties of Function 'fsetpos'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 303)
+[ Extern ] Assigns (file share/libc/stdio.h, line 396)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 303)
+[ Extern ] Froms (file share/libc/stdio.h, line 396)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -554,11 +619,11 @@
[ Extern ] Post-condition 'success_or_error'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 308)
+[ Extern ] Assigns (file share/libc/stdio.h, line 402)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 308)
+[ Extern ] Froms (file share/libc/stdio.h, line 402)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 308)
+[ Extern ] Froms (file share/libc/stdio.h, line 402)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -567,9 +632,9 @@
--- Properties of Function 'rewind'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 314)
+[ Extern ] Assigns (file share/libc/stdio.h, line 410)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 314)
+[ Extern ] Froms (file share/libc/stdio.h, line 410)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -578,9 +643,9 @@
--- Properties of Function 'clearerr'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 317)
+[ Extern ] Assigns (file share/libc/stdio.h, line 416)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 317)
+[ Extern ] Froms (file share/libc/stdio.h, line 416)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -591,7 +656,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 320)
+[ Extern ] Froms (file share/libc/stdio.h, line 422)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -602,7 +667,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 323)
+[ Extern ] Froms (file share/libc/stdio.h, line 428)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -611,9 +676,9 @@
--- Properties of Function 'flockfile'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 326)
+[ Extern ] Assigns (file share/libc/stdio.h, line 434)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 326)
+[ Extern ] Froms (file share/libc/stdio.h, line 434)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -622,9 +687,9 @@
--- Properties of Function 'funlockfile'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 329)
+[ Extern ] Assigns (file share/libc/stdio.h, line 440)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 329)
+[ Extern ] Froms (file share/libc/stdio.h, line 440)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -633,11 +698,11 @@
--- Properties of Function 'ftrylockfile'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 332)
+[ Extern ] Assigns (file share/libc/stdio.h, line 446)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 332)
+[ Extern ] Froms (file share/libc/stdio.h, line 446)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 332)
+[ Extern ] Froms (file share/libc/stdio.h, line 446)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -648,7 +713,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 335)
+[ Extern ] Froms (file share/libc/stdio.h, line 452)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -657,9 +722,9 @@
--- Properties of Function 'perror'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 338)
+[ Extern ] Assigns (file share/libc/stdio.h, line 458)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 338)
+[ Extern ] Froms (file share/libc/stdio.h, line 458)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -668,11 +733,11 @@
--- Properties of Function 'getc_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 341)
+[ Extern ] Assigns (file share/libc/stdio.h, line 464)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 341)
+[ Extern ] Froms (file share/libc/stdio.h, line 464)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 341)
+[ Extern ] Froms (file share/libc/stdio.h, line 464)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -683,7 +748,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 343)
+[ Extern ] Froms (file share/libc/stdio.h, line 469)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -692,9 +757,11 @@
--- Properties of Function 'putc_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 345)
+[ Extern ] Assigns (file share/libc/stdio.h, line 475)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 345)
+[ Extern ] Froms (file share/libc/stdio.h, line 475)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 476)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -703,9 +770,11 @@
--- Properties of Function 'putchar_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 347)
+[ Extern ] Assigns (file share/libc/stdio.h, line 481)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/stdio.h, line 481)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 347)
+[ Extern ] Froms (file share/libc/stdio.h, line 482)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -714,9 +783,9 @@
--- Properties of Function 'clearerr_unlocked'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/stdio.h, line 350)
+[ Extern ] Assigns (file share/libc/stdio.h, line 488)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 350)
+[ Extern ] Froms (file share/libc/stdio.h, line 488)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -727,7 +796,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 352)
+[ Extern ] Froms (file share/libc/stdio.h, line 494)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -738,7 +807,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 354)
+[ Extern ] Froms (file share/libc/stdio.h, line 500)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -749,7 +818,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 356)
+[ Extern ] Froms (file share/libc/stdio.h, line 506)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -760,11 +829,11 @@
[ Extern ] Post-condition 'result_error_or_valid_open_pipe'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/stdio.h, line 381)
+[ Extern ] Assigns (file share/libc/stdio.h, line 533)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 381)
+[ Extern ] Froms (file share/libc/stdio.h, line 533)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 383)
+[ Extern ] Froms (file share/libc/stdio.h, line 535)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -777,7 +846,7 @@
Unverifiable but considered Valid.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/stdio.h, line 395)
+[ Extern ] Froms (file share/libc/stdio.h, line 547)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -796,8 +865,8 @@
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
- 68 Completely validated
- 168 Considered valid
+ 72 Completely validated
+ 198 Considered valid
1 To be validated
- 237 Total
+ 271 Total
--------------------------------------------------------------------------------