From 20987ae23168a64dd68e40caac890b5fee30b6f3 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Mon, 25 Mar 2024 11:48:58 +0100
Subject: [PATCH] [Libc] several fixes and spec improvements
---
share/libc/__fc_builtin.c | 7 ++++++-
share/libc/argz.h | 8 ++++++++
share/libc/fenv.h | 2 +-
share/libc/glob.c | 1 +
share/libc/glob.h | 10 ++++++++--
share/libc/netdb.h | 7 ++++---
share/libc/stdatomic.c | 1 -
share/libc/stdatomic.h | 6 ++++--
share/libc/stdio.c | 9 ++++++---
share/libc/stdio.h | 6 +++---
share/libc/stdlib.h | 14 +++++++-------
share/libc/string.h | 4 ++--
share/libc/wchar.h | 5 +++--
13 files changed, 53 insertions(+), 27 deletions(-)
diff --git a/share/libc/__fc_builtin.c b/share/libc/__fc_builtin.c
index 00963b7c188..40ac7db1413 100644
--- a/share/libc/__fc_builtin.c
+++ b/share/libc/__fc_builtin.c
@@ -247,7 +247,12 @@ wint_t Frama_C_wint_t_interval(wint_t min, wint_t max)
return r;
}
-/*@ assigns \nothing; */
+/*@
+ terminates \false;
+ assigns \nothing;
+ ensures never_terminates: \false;
+ exits always_exits: \true;
+ */
extern void __builtin_abort(void) __attribute__((noreturn)); // GCC builtin
void Frama_C_abort(void)
diff --git a/share/libc/argz.h b/share/libc/argz.h
index 81afda0c725..b68450d44a1 100644
--- a/share/libc/argz.h
+++ b/share/libc/argz.h
@@ -43,12 +43,14 @@ __BEGIN_DECLS
typedef int error_t;
/*@
+ allocates *argz;
assigns (*argz)[0..], *len, \result \from argv[0..][0..];
*/
extern error_t argz_create (char *const argv[], char **restrict argz,
size_t *restrict len);
/*@
+ allocates *argz;
assigns (*argz)[0..], *len, \result \from string[0..], sep, (*argz)[0..], *len;
*/
extern error_t argz_create_sep (const char *restrict string,
@@ -66,6 +68,7 @@ extern void argz_extract (const char *restrict argz, size_t len,
extern void argz_stringify (char *argz, size_t len, int sep);
/*@
+ allocates *argz;
assigns (*argz)[0..], *argz_len \from (*argz)[0..], *argz_len,
buf[0..], buf_len;
assigns \result \from indirect:(*argz)[0..], indirect:*argz_len,
@@ -76,6 +79,7 @@ extern error_t argz_append (char **restrict argz,
const char *restrict buf, size_t buf_len);
/*@
+ allocates *argz;
assigns (*argz)[0..], *argz_len, \result \from (*argz)[0..], *argz_len,
str[0..];
*/
@@ -84,6 +88,7 @@ extern error_t argz_add (char **restrict argz,
const char *restrict str);
/*@
+ allocates *argz;
assigns (*argz)[0..], *argz_len, \result \from string[0..], delim;
*/
extern error_t argz_add_sep (char **restrict argz,
@@ -91,6 +96,7 @@ extern error_t argz_add_sep (char **restrict argz,
const char *restrict string, int delim);
/*@
+ frees *argz;
assigns (*argz)[0..], *argz_len \from (*argz)[0..], *argz_len, entry[0..];
*/
extern void argz_delete (char **restrict argz,
@@ -98,6 +104,7 @@ extern void argz_delete (char **restrict argz,
char *restrict entry);
/*@
+ allocates *argz;
assigns (*argz)[0..], *argz_len, \result \from (*argz)[0..], *argz_len,
before, before[0..],
entry[0..];
@@ -108,6 +115,7 @@ extern error_t argz_insert (char **restrict argz,
const char *restrict entry);
/*@
+ allocates *argz;
assigns (*argz)[0..], *argz_len, *replace_count, \result
\from
(*argz)[0..], *argz_len, str[0..], with[0..], *replace_count;
diff --git a/share/libc/fenv.h b/share/libc/fenv.h
index 2ddec71c27e..1315383cde0 100644
--- a/share/libc/fenv.h
+++ b/share/libc/fenv.h
@@ -108,7 +108,7 @@ extern int fegetexceptflag(fexcept_t *flagp, int excepts);
extern int fegetround(void);
/*@
- assigns *envp \from __fc_fenv_state;
+ assigns *envp, __fc_fenv_state \from __fc_fenv_state;
assigns \result \from indirect:__fc_fenv_state;
*/
extern int feholdexcept(fenv_t *envp);
diff --git a/share/libc/glob.c b/share/libc/glob.c
index 70550765741..83b532b3f0f 100644
--- a/share/libc/glob.c
+++ b/share/libc/glob.c
@@ -74,6 +74,7 @@ int glob(const char *pattern, int flags,
pglob->gl_pathv[reserve_offs + prev_len + i] = (char*)"glob result";
}
pglob->gl_pathv[prev_len + reserve_offs + pglob->gl_pathc] = 0; // terminator
+ pglob->gl_flags = flags | (Frama_C_nondet(0, GLOB_MAGCHAR));
if (Frama_C_nondet(0, 1)) { // simulate "no error"
return 0;
} else {
diff --git a/share/libc/glob.h b/share/libc/glob.h
index 01655d11eef..4046f1efb02 100644
--- a/share/libc/glob.h
+++ b/share/libc/glob.h
@@ -69,14 +69,20 @@ typedef struct __fc_glob_t {
} glob_t;
/*@
- assigns \result, *pglob \from indirect:pattern[0 .. strlen(pattern)],
- indirect:flags, indirect:errfunc;
+ allocates pglob->gl_pathv;
+ assigns *pglob \from indirect:pattern[0 .. strlen(pattern)],
+ flags,
+ indirect:errfunc;
+ assigns \result \from indirect:pattern[0 .. strlen(pattern)],
+ indirect:flags,
+ indirect:errfunc;
*/
extern int glob(const char *pattern, int flags,
int (*errfunc) (const char *epath, int eerrno),
glob_t *pglob);
/*@
+ frees pglob->gl_pathv;
assigns *pglob \from *pglob;
*/
extern void globfree(glob_t *pglob);
diff --git a/share/libc/netdb.h b/share/libc/netdb.h
index 412d06331a4..0b09f4b9d9c 100644
--- a/share/libc/netdb.h
+++ b/share/libc/netdb.h
@@ -123,8 +123,8 @@ extern void endnetent(void);
extern void endprotoent(void);
extern void endservent(void);
/*@ requires addrinfo_valid: \valid(addrinfo);
- assigns \nothing;
frees addrinfo;
+ assigns \nothing;
ensures allocation: \allocable(addrinfo);
*/
extern void freeaddrinfo(struct addrinfo * addrinfo);
@@ -143,12 +143,12 @@ extern const char *gai_strerror(int errcode);
requires hints_option: hints == \null || \valid_read(hints);
requires valid_res: \valid(res);
+ allocates *res;
+
assigns *res \from indirect:nodename, indirect:servname, indirect:hints;
assigns \result \from indirect:nodename, indirect:servname,indirect:hints;
assigns errno \from indirect:nodename, indirect:servname, indirect:hints;
- allocates *res;
-
behavior empty_request:
assumes empty: nodename == \null && servname == \null;
assigns \result \from indirect:nodename, indirect:servname;
@@ -180,6 +180,7 @@ extern int getaddrinfo(
extern struct hostent *gethostbyaddr(const void *, socklen_t, int);
/*@
+ allocates \result;
assigns \result, *\result \from name[0 .. strlen(name)];
*/
extern struct hostent *gethostbyname(const char *name);
diff --git a/share/libc/stdatomic.c b/share/libc/stdatomic.c
index 30c975051b9..28723c038b5 100644
--- a/share/libc/stdatomic.c
+++ b/share/libc/stdatomic.c
@@ -26,7 +26,6 @@
#include "string.h"
__PUSH_FC_STDLIB
-/*@ assigns \nothing; */
void __fc_atomic_init_marker(void *obj, unsigned long long value) {}
void atomic_thread_fence(memory_order order) {}
diff --git a/share/libc/stdatomic.h b/share/libc/stdatomic.h
index 32ef8fafd80..f02aee8016e 100644
--- a/share/libc/stdatomic.h
+++ b/share/libc/stdatomic.h
@@ -101,6 +101,8 @@ typedef _Atomic uintmax_t atomic_uintmax_t;
// NOTE: The stubs below serve only to help parsing succeed and do not
// match expected concurrence semantics.
+/*@ assigns \nothing; */
+void __fc_atomic_init_marker(void *obj, unsigned long long value);
#define atomic_init(obj, value) \
do { __fc_atomic_init_marker(obj, value); *obj = value; } while (0)
@@ -185,7 +187,7 @@ unsigned long long __fc_atomic_exchange_explicit(void *object,
*((char*)expected+(0 .. obj_size-1)), desired, indirect:obj_size;
assigns \result \from indirect:*((char*)object+(0 .. obj_size-1)),
indirect:*((char*)expected+(0 .. obj_size-1)),
- indirect:desired, indirect:obj_size;
+ indirect:obj_size;
*/
_Bool __fc_atomic_compare_exchange_strong(void *object, void *expected,
unsigned long long desired,
@@ -201,7 +203,7 @@ _Bool __fc_atomic_compare_exchange_strong(void *object, void *expected,
desired, indirect:success, indirect:failure, indirect:obj_size;
assigns \result \from indirect:*((char*)object+(0 .. obj_size-1)),
indirect:*((char*)expected+(0 .. obj_size-1)),
- indirect:desired, indirect:success, indirect:failure,
+ indirect:success, indirect:failure,
indirect:obj_size;
*/
_Bool __fc_atomic_compare_exchange_strong_explicit(void *object, void *expected,
diff --git a/share/libc/stdio.c b/share/libc/stdio.c
index 5db9ebdf4af..eda30573e2d 100644
--- a/share/libc/stdio.c
+++ b/share/libc/stdio.c
@@ -251,7 +251,7 @@ enum length_modifier {
};
int vfscanf(FILE * restrict stream, const char * restrict format, va_list arg) {
- char *p = format;
+ const char *p = format;
char conversion_counter = 0;
while (*p) {
if (*p == '%') {
@@ -429,8 +429,11 @@ int vfscanf(FILE * restrict stream, const char * restrict format, va_list arg) {
*va_arg(arg, double*) = Frama_C_double_interval(-DBL_MAX, DBL_MAX);
break;
case UPPER_L:
- *va_arg(arg, long double*) =
- Frama_C_long_double_interval(-LDBL_MAX, LDBL_MAX);
+ // TODO: use Frama_C_long_double_interval when it will be supported
+ {
+ volatile long double vld;
+ *va_arg(arg, long double*) = vld;
+ }
break;
default:
// Undefined behavior
diff --git a/share/libc/stdio.h b/share/libc/stdio.h
index e6978f505ec..20b060c2f08 100644
--- a/share/libc/stdio.h
+++ b/share/libc/stdio.h
@@ -589,6 +589,7 @@ extern ssize_t getline(char **lineptr, size_t *n, FILE *stream);
/*@
requires valid_or_null_buff: buf == \null || \valid((char*)buf + (0 .. size-1));
requires valid_mode: valid_read_string(mode);
+ allocates buf;
assigns __fc_errno \from indirect: buf, indirect: size,
indirect: mode[0..strlen(mode)];
assigns \result \from __fc_p_fopen,
@@ -598,7 +599,6 @@ extern ssize_t getline(char **lineptr, size_t *n, FILE *stream);
ensures errno_set:
__fc_errno == \old(errno) ||
__fc_errno \in {EINVAL, EMFILE, ENOMEM};
- allocates buf;
*/
extern FILE *fmemopen(void *restrict buf, size_t size,
const char *restrict mode);
@@ -610,12 +610,12 @@ extern FILE *fmemopen(void *restrict buf, size_t size,
/*@
requires valid_strp: \valid(strp);
requires valid_fmt: valid_read_string(fmt);
+ allocates *strp;
assigns __fc_heap_status \from indirect:fmt[0 ..], __fc_heap_status;
assigns \result \from indirect:fmt[0 ..], indirect:__fc_heap_status;
assigns *strp \from fmt[0 ..], indirect:__fc_heap_status;
//missing: variadic arguments
ensures result_error_or_written_bytes: \result == -1 || \result >= 0;
- allocates *strp;
*/
extern int asprintf(char **strp, const char *fmt, ...);
@@ -623,13 +623,13 @@ extern int asprintf(char **strp, const char *fmt, ...);
/*@
requires valid_strp: \valid(strp);
requires valid_fmt: valid_read_string(fmt);
+ allocates *strp;
assigns __fc_heap_status
\from indirect:fmt[0 ..], indirect:ap, __fc_heap_status;
assigns \result \from indirect:fmt[0 ..], indirect:__fc_heap_status;
assigns *strp \from fmt[0 ..], ap, indirect:__fc_heap_status;
//missing: variadic arguments
ensures result_error_or_written_bytes: \result == -1 || \result >= 0;
- allocates *strp;
*/
extern int vasprintf(char **restrict strp, const char *restrict fmt,
va_list ap);
diff --git a/share/libc/stdlib.h b/share/libc/stdlib.h
index d792f95c989..4ac3ce4bd90 100644
--- a/share/libc/stdlib.h
+++ b/share/libc/stdlib.h
@@ -377,8 +377,8 @@ extern long int jrand48 (unsigned short xsubi[3]);
behavior no_allocation:
assumes cannot_allocate: !is_allocable(nmemb * size);
- assigns \result \from \nothing;
allocates \nothing;
+ assigns \result \from \nothing;
ensures null_result: \result == \null;
complete behaviors;
@@ -395,8 +395,8 @@ extern void *calloc(size_t nmemb, size_t size);
@ ensures allocation: \fresh(\result,size);
@ behavior no_allocation:
@ assumes cannot_allocate: !is_allocable(size);
- @ assigns \result \from \nothing;
@ allocates \nothing;
+ @ assigns \result \from \nothing;
@ ensures null_result: \result==\null;
@ complete behaviors;
@ disjoint behaviors;
@@ -412,8 +412,8 @@ extern void *malloc(size_t size);
@ ensures freed: \allocable(p);
@ behavior no_deallocation:
@ assumes null_p: p==\null;
- @ assigns \nothing;
@ frees \nothing;
+ @ assigns \nothing;
@ complete behaviors;
@ disjoint behaviors;
@*/
@@ -716,8 +716,8 @@ extern size_t wcstombs(char * restrict s,
ensures result_zero: \result == 0;
behavior no_allocation:
assumes cannot_allocate: !is_allocable(size);
- assigns \result \from indirect:alignment;
allocates \nothing;
+ assigns \result \from indirect:alignment;
ensures result_non_zero: \result < 0 || \result > 0;
complete behaviors;
disjoint behaviors;
@@ -779,14 +779,15 @@ extern int mkstemps(char *templat, int suffixlen);
assumes valid_file_name: valid_read_string(file_name);
assumes resolved_name_null: resolved_name == \null;
assumes cannot_allocate: !is_allocable(PATH_MAX);
- assigns \result \from \nothing;
allocates \nothing;
+ assigns \result \from \nothing;
ensures null_result: \result == \null;
ensures errno_set: __fc_errno == ENOMEM;
behavior resolved_name_buffer:
assumes valid_file_name: valid_read_string(file_name);
assumes allocated_resolved_name_or_fail:
\valid(resolved_name+(0 .. PATH_MAX-1));
+ allocates \nothing;
assigns \result \from resolved_name;
assigns resolved_name[0 .. PATH_MAX-1] \from indirect:file_name[0..];
ensures valid_string_resolved_name: valid_string(resolved_name)
@@ -794,15 +795,14 @@ extern int mkstemps(char *templat, int suffixlen);
// missing: assigns \result,
// resolved_name[0 .. PATH_MAX-1] \from 'filesystem';
ensures resolved_result: \result == resolved_name;
- allocates \nothing;
behavior filesystem_error:
assumes valid_file_name: valid_read_string(file_name);
+ allocates \nothing;
assigns \result, __fc_errno
\from indirect:file_name[0..]; // missing: indirect:'filesystem';
ensures null_result: \result == \null;
ensures errno_set:
__fc_errno \in {EACCES, EIO, ELOOP, ENAMETOOLONG, ENOENT, ENOTDIR};
- allocates \nothing;
*/
extern char *realpath(const char *restrict file_name,
char *restrict resolved_name);
diff --git a/share/libc/string.h b/share/libc/string.h
index 0d6379e24f0..9ef1f1620be 100644
--- a/share/libc/string.h
+++ b/share/libc/string.h
@@ -528,8 +528,8 @@ extern void *memmem(const void *haystack, size_t haystacklen,
@ valid_string(\result) && strcmp(\result,s) == 0;
@ behavior no_allocation:
@ assumes cannot_allocate: !is_allocable(strlen(s));
- @ assigns \result \from \nothing;
@ allocates \nothing;
+ @ assigns \result \from \nothing;
@ ensures result_null: \result == \null;
@*/
extern char *strdup (const char *s);
@@ -550,8 +550,8 @@ extern char *strdup (const char *s);
@ strncmp(\result,s,n) == 0;
@ behavior no_allocation:
@ assumes cannot_allocate: !is_allocable(\min(strlen(s), n+1));
- @ assigns \result \from \nothing;
@ allocates \nothing;
+ @ assigns \result \from \nothing;
@ ensures result_null: \result == \null;
@*/
extern char *strndup (const char *s, size_t n);
diff --git a/share/libc/wchar.h b/share/libc/wchar.h
index 645abea7371..c3a5d51c94b 100644
--- a/share/libc/wchar.h
+++ b/share/libc/wchar.h
@@ -273,15 +273,16 @@ extern int wcscasecmp(const wchar_t *ws1, const wchar_t *ws2);
assigns \result \from indirect:ws[0..wcslen(ws)], indirect:__fc_heap_status;
behavior allocation:
assumes can_allocate: is_allocable(wcslen(ws));
- assigns __fc_heap_status \from indirect:ws, __fc_heap_status;
+ assigns __fc_heap_status \from indirect:ws[0 .. wcslen(ws),
+ __fc_heap_status;
assigns \result \from indirect:ws[0..wcslen(ws)], indirect:__fc_heap_status;
ensures allocation: \fresh(\result,wcslen(ws) * sizeof(wchar_t));
ensures result_valid_string_and_same_contents:
valid_wstring(\result) && wcscmp(\result,ws) == 0;
behavior no_allocation:
assumes cannot_allocate: !is_allocable(wcslen(ws));
- assigns \result \from \nothing;
allocates \nothing;
+ assigns \result \from \nothing;
ensures result_null: \result == \null;
*/
extern wchar_t *wcsdup(const wchar_t *ws);
--
GitLab