From ed30a473761d1e1125532420686392d07d8c43f8 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Tue, 26 Mar 2024 18:34:16 +0100
Subject: [PATCH] [Libc] improve several specifications (mainly
string.h/stdlib.h) and add tests
---
share/libc/__fc_string_axiomatic.h | 7 +-
share/libc/glob.h | 1 +
share/libc/stdlib.c | 12 +-
share/libc/stdlib.h | 211 +++++++++-----
share/libc/string.h | 445 +++++++++++++++++------------
share/libc/wchar.h | 2 +-
tests/libc/stdlib_c_env.c | 4 +
tests/libc/stdlib_h.c | 23 ++
tests/libc/string_h.c | 87 +++++-
9 files changed, 516 insertions(+), 276 deletions(-)
diff --git a/share/libc/__fc_string_axiomatic.h b/share/libc/__fc_string_axiomatic.h
index c1b90dce4bc..d137cba4eeb 100644
--- a/share/libc/__fc_string_axiomatic.h
+++ b/share/libc/__fc_string_axiomatic.h
@@ -270,10 +270,6 @@ __BEGIN_DECLS
@ }
@*/
-/*@ logic ℤ minimum(ℤ i, ℤ j) = i < j ? i : j;
- @ logic ℤ maximum(ℤ i, ℤ j) = i < j ? j : i;
- @*/
-
/*@ predicate valid_string{L}(char *s) =
@ 0 <= strlen(s) && \valid(s+(0..strlen(s)));
@
@@ -299,6 +295,9 @@ __BEGIN_DECLS
@
@ predicate valid_wstring_or_null{L}(wchar_t *s) =
@ s == \null || valid_wstring(s);
+ @
+ @ logic ℤ strnlen(char *s, ℤ n) =
+ @ \min(strlen(s), n);
@*/
__END_DECLS
diff --git a/share/libc/glob.h b/share/libc/glob.h
index 4046f1efb02..44a09d7cf70 100644
--- a/share/libc/glob.h
+++ b/share/libc/glob.h
@@ -36,6 +36,7 @@ __PUSH_FC_STDLIB
#define GLOB_APPEND (1 << 5)/* Append to results of a previous call. */
#define GLOB_NOESCAPE (1 << 6)/* Backslashes don't quote metacharacters. */
#define GLOB_PERIOD (1 << 7)/* Leading `.' can be matched by metachars. */
+#define GLOB_MAGCHAR (1 << 8)/* GNU-specific */
#define GLOB_NOSPACE 1 /* Ran out of memory. */
#define GLOB_ABORTED 2 /* Read error. */
diff --git a/share/libc/stdlib.c b/share/libc/stdlib.c
index ca6863450b7..c3fd0cfcbd0 100644
--- a/share/libc/stdlib.c
+++ b/share/libc/stdlib.c
@@ -128,7 +128,7 @@ int putenv(char *string)
// 2. key in string found in env ==> modify an existing entry
if (Frama_C_nondet(0, 1)) {
if (Frama_C_nondet(0, 1)) {
- //TODO: errno = ENOMEM;
+ errno = ENOMEM;
return Frama_C_interval(INT_MIN, INT_MAX); // return a non-zero value
}
__fc_env[Frama_C_interval(0, ARG_MAX-1)] = string;
@@ -139,12 +139,12 @@ int putenv(char *string)
int setenv(const char *name, const char *value, int overwrite)
{
if (strchr(name, '=')) {
- //TODO: errno = EINVAL;
+ errno = EINVAL;
return -1;
}
size_t namelen = strlen(name);
if (namelen == 0) {
- //TODO: errno = EINVAL;
+ errno = EINVAL;
return -1;
}
@@ -155,7 +155,7 @@ int setenv(const char *name, const char *value, int overwrite)
// 2. found 'name' but will not overwrite
// 3. did not find name and has available memory
if (Frama_C_nondet(0, 1)) {
- //TODO: errno = ENOMEM;
+ errno = ENOMEM;
return -1;
} else {
if (Frama_C_nondet(0, 1)) {
@@ -169,12 +169,12 @@ int setenv(const char *name, const char *value, int overwrite)
int unsetenv(const char *name)
{
if (strchr(name, '=')) {
- //TODO: errno = EINVAL;
+ errno = EINVAL;
return -1;
}
size_t namelen = strlen(name);
if (namelen == 0) {
- //TODO: errno = EINVAL;
+ errno = EINVAL;
return -1;
}
diff --git a/share/libc/stdlib.h b/share/libc/stdlib.h
index 4ac3ce4bd90..9042a4ca36c 100644
--- a/share/libc/stdlib.h
+++ b/share/libc/stdlib.h
@@ -70,26 +70,26 @@ typedef struct __fc_lldiv_t {
#define MB_CUR_MAX __FC_MB_CUR_MAX
/*@
- requires valid_nptr: \valid_read(nptr); // cannot be precise, valid_read_string too strong
- assigns \result \from indirect:nptr, indirect:nptr[0 ..];
+ requires valid_nptr: valid_read_string(nptr);
+ assigns \result \from indirect:nptr, indirect:nptr[0 .. strlen(nptr)];
*/
extern double atof(const char *nptr);
/*@
- requires valid_nptr: \valid_read(nptr); // cannot be precise, valid_read_string too strong
- assigns \result \from indirect:nptr, indirect:nptr[0 ..];
+ requires valid_nptr: valid_read_string(nptr);
+ assigns \result \from indirect:nptr, indirect:nptr[0 .. strlen(nptr)];
*/
extern int atoi(const char *nptr);
/*@
- requires valid_nptr: \valid_read(nptr); // cannot be precise, valid_read_string too strong
- assigns \result \from indirect:nptr, indirect:nptr[0 ..];
+ requires valid_nptr: valid_read_string(nptr);
+ assigns \result \from indirect:nptr, indirect:nptr[0 .. strlen(nptr)];
*/
extern long int atol(const char *nptr);
/*@
- requires valid_nptr: \valid_read(nptr); // cannot be precise, valid_read_string too strong
- assigns \result \from indirect:nptr, indirect:nptr[0 ..];
+ requires valid_nptr: valid_read_string(nptr);
+ assigns \result \from indirect:nptr, indirect:nptr[0 .. strlen(nptr)];
*/
extern long long int atoll(const char *nptr);
@@ -98,19 +98,21 @@ extern long long int atoll(const char *nptr);
/*@
requires valid_string_nptr: valid_read_string(nptr);
requires separation: \separated(nptr, endptr);
- assigns \result \from indirect:nptr, indirect:nptr[0 ..];
- assigns *endptr \from nptr, indirect:nptr[0 ..], indirect:endptr;
+ assigns \result \from indirect:nptr, indirect:nptr[0 .. strlen(nptr)];
+ assigns *endptr \from nptr, indirect:nptr[0 .. strlen(nptr)],
+ indirect:endptr;
behavior no_storage:
assumes null_endptr: endptr == \null;
- assigns \result \from indirect:nptr, indirect:nptr[0 ..];
+ assigns \result \from indirect:nptr, indirect:nptr[0 .. strlen(nptr)];
behavior store_position:
assumes nonnull_endptr: endptr != \null;
requires valid_endptr: \valid(endptr);
- assigns \result \from indirect:nptr, indirect:nptr[0 ..];
- assigns *endptr \from nptr, indirect:nptr[0 ..], indirect:endptr;
+ assigns \result \from indirect:nptr, indirect:nptr[0 .. strlen(nptr)];
+ assigns *endptr \from nptr, indirect:nptr[0 .. strlen(nptr)],
+ indirect:endptr;
ensures initialization: \initialized(endptr);
ensures valid_endptr_content: \valid_read(*endptr);
- ensures position_subset: \subset(*endptr, nptr + (0 ..));
+ ensures endptr_same_base: \base_addr(*endptr) == \base_addr(nptr);
complete behaviors;
disjoint behaviors;
*/
@@ -120,19 +122,20 @@ extern double strtod(const char * restrict nptr,
/*@
requires valid_string_nptr: valid_read_string(nptr);
requires separation: \separated(nptr, endptr);
- assigns \result \from indirect:nptr, indirect:nptr[0 ..];
- assigns *endptr \from nptr, indirect:nptr[0 ..], indirect:endptr;
+ assigns \result \from indirect:nptr, indirect:nptr[0 .. strlen(nptr)];
+ assigns *endptr \from nptr, indirect:nptr[0 .. strlen(nptr)],
+ indirect:endptr;
behavior no_storage:
assumes null_endptr: endptr == \null;
- assigns \result \from indirect:nptr, indirect:nptr[0 ..];
+ assigns \result \from indirect:nptr, indirect:nptr[0 .. strlen(nptr)];
behavior store_position:
assumes nonnull_endptr: endptr != \null;
requires valid_endptr: \valid(endptr);
- assigns \result \from indirect:nptr, indirect:nptr[0 ..];
+ assigns \result \from indirect:nptr, indirect:nptr[0 .. strlen(nptr)];
assigns *endptr \from nptr, indirect:nptr[0 ..], indirect:endptr;
ensures initialization: \initialized(endptr);
ensures valid_endptr_content: \valid_read(*endptr);
- ensures position_subset: \subset(*endptr, nptr + (0 ..));
+ ensures endptr_same_base: \base_addr(*endptr) == \base_addr(nptr);
complete behaviors;
disjoint behaviors;
*/
@@ -142,19 +145,21 @@ extern float strtof(const char * restrict nptr,
/*@
requires valid_string_nptr: valid_read_string(nptr);
requires separation: \separated(nptr, endptr);
- assigns \result \from indirect:nptr, indirect:nptr[0 ..];
- assigns *endptr \from nptr, indirect:nptr[0 ..], indirect:endptr;
+ assigns \result \from indirect:nptr, indirect:nptr[0 .. strlen(nptr)];
+ assigns *endptr \from nptr, indirect:nptr[0 .. strlen(nptr)],
+ indirect:endptr;
behavior no_storage:
assumes null_endptr: endptr == \null;
- assigns \result \from indirect:nptr, indirect:nptr[0 ..];
+ assigns \result \from indirect:nptr, indirect:nptr[0 .. strlen(nptr)];
behavior store_position:
assumes nonnull_endptr: endptr != \null;
requires valid_endptr: \valid(endptr);
- assigns \result \from indirect:nptr, indirect:nptr[0 ..];
- assigns *endptr \from nptr, indirect:nptr[0 ..], indirect:endptr;
+ assigns \result \from indirect:nptr, indirect:nptr[0 .. strlen(nptr)];
+ assigns *endptr \from nptr, indirect:nptr[0 .. strlen(nptr)],
+ indirect:endptr;
ensures initialization: \initialized(endptr);
ensures valid_endptr_content: \valid_read(*endptr);
- ensures position_subset: \subset(*endptr, nptr + (0 ..));
+ ensures endptr_same_base: \base_addr(*endptr) == \base_addr(nptr);
complete behaviors;
disjoint behaviors;
*/
@@ -166,19 +171,24 @@ extern long double strtold(const char * restrict nptr,
requires valid_string_nptr: valid_read_string(nptr);
requires separation: \separated(nptr, endptr);
requires base_range: base == 0 || 2 <= base <= 36;
- assigns \result \from indirect:nptr, indirect:nptr[0 ..], indirect:base;
- assigns *endptr \from nptr, indirect:nptr[0 ..], indirect:endptr, indirect:base;
+ assigns \result \from indirect:nptr, indirect:nptr[0 .. strlen(nptr)],
+ indirect:base;
+ assigns *endptr \from nptr, indirect:nptr[0 .. strlen(nptr)],
+ indirect:endptr, indirect:base;
behavior no_storage:
assumes null_endptr: endptr == \null;
- assigns \result \from indirect:nptr, indirect:nptr[0 ..], indirect:base;
+ assigns \result \from indirect:nptr, indirect:nptr[0 .. strlen(nptr)],
+ indirect:base;
behavior store_position:
assumes nonnull_endptr: endptr != \null;
requires valid_endptr: \valid(endptr);
- assigns \result \from indirect:nptr, indirect:nptr[0 ..], indirect:base;
- assigns *endptr \from nptr, indirect:nptr[0 ..], indirect:endptr, indirect:base;
+ assigns \result \from indirect:nptr, indirect:nptr[0 .. strlen(nptr)],
+ indirect:base;
+ assigns *endptr \from nptr, indirect:nptr[0 .. strlen(nptr)],
+ indirect:endptr, indirect:base;
ensures initialization: \initialized(endptr);
ensures valid_endptr_content: \valid_read(*endptr);
- ensures position_subset: \subset(*endptr, nptr + (0 ..));
+ ensures endptr_same_base: \base_addr(*endptr) == \base_addr(nptr);
complete behaviors;
disjoint behaviors;
*/
@@ -191,19 +201,24 @@ extern long int strtol(
requires valid_string_nptr: valid_read_string(nptr);
requires separation: \separated(nptr, endptr);
requires base_range: base == 0 || 2 <= base <= 36;
- assigns \result \from indirect:nptr, indirect:nptr[0 ..], indirect:base;
- assigns *endptr \from nptr, indirect:nptr[0 ..], indirect:endptr, indirect:base;
+ assigns \result \from indirect:nptr, indirect:nptr[0 .. strlen(nptr)],
+ indirect:base;
+ assigns *endptr \from nptr, indirect:nptr[0 .. strlen(nptr)],
+ indirect:endptr, indirect:base;
behavior no_storage:
assumes null_endptr: endptr == \null;
- assigns \result \from indirect:nptr, indirect:nptr[0 ..], indirect:base;
+ assigns \result \from indirect:nptr, indirect:nptr[0 .. strlen(nptr)],
+ indirect:base;
behavior store_position:
assumes nonnull_endptr: endptr != \null;
requires valid_endptr: \valid(endptr);
- assigns \result \from indirect:nptr, indirect:nptr[0 ..], indirect:base;
- assigns *endptr \from nptr, indirect:nptr[0 ..], indirect:endptr, indirect:base;
+ assigns \result \from indirect:nptr, indirect:nptr[0 .. strlen(nptr)],
+ indirect:base;
+ assigns *endptr \from nptr, indirect:nptr[0 .. strlen(nptr)],
+ indirect:endptr, indirect:base;
ensures initialization: \initialized(endptr);
ensures valid_endptr_content: \valid_read(*endptr);
- ensures position_subset: \subset(*endptr, nptr + (0 ..));
+ ensures endptr_same_base: \base_addr(*endptr) == \base_addr(nptr);
complete behaviors;
disjoint behaviors;
*/
@@ -216,19 +231,24 @@ extern long long int strtoll(
requires valid_string_nptr: valid_read_string(nptr);
requires separation: \separated(nptr, endptr);
requires base_range: base == 0 || 2 <= base <= 36;
- assigns \result \from indirect:nptr, indirect:nptr[0 ..], indirect:base;
- assigns *endptr \from nptr, indirect:nptr[0 ..], indirect:endptr, indirect:base;
+ assigns \result \from indirect:nptr, indirect:nptr[0 .. strlen(nptr)],
+ indirect:base;
+ assigns *endptr \from nptr, indirect:nptr[0 .. strlen(nptr)],
+ indirect:endptr, indirect:base;
behavior no_storage:
assumes null_endptr: endptr == \null;
- assigns \result \from indirect:nptr, indirect:nptr[0 ..], indirect:base;
+ assigns \result \from indirect:nptr, indirect:nptr[0 .. strlen(nptr)],
+ indirect:base;
behavior store_position:
assumes nonnull_endptr: endptr != \null;
requires valid_endptr: \valid(endptr);
- assigns \result \from indirect:nptr, indirect:nptr[0 ..], indirect:base;
- assigns *endptr \from nptr, indirect:nptr[0 ..], indirect:endptr, indirect:base;
+ assigns \result \from indirect:nptr, indirect:nptr[0 .. strlen(nptr)],
+ indirect:base;
+ assigns *endptr \from nptr, indirect:nptr[0 .. strlen(nptr)],
+ indirect:endptr, indirect:base;
ensures initialization: \initialized(endptr);
ensures valid_endptr_content: \valid_read(*endptr);
- ensures position_subset: \subset(*endptr, nptr + (0 ..));
+ ensures endptr_same_base: \base_addr(*endptr) == \base_addr(nptr);
complete behaviors;
disjoint behaviors;
*/
@@ -241,19 +261,24 @@ extern unsigned long int strtoul(
requires valid_string_nptr: valid_read_string(nptr);
requires separation: \separated(nptr, endptr);
requires base_range: base == 0 || 2 <= base <= 36;
- assigns \result \from indirect:nptr, indirect:nptr[0 ..], indirect:base;
- assigns *endptr \from nptr, indirect:nptr[0 ..], indirect:endptr, indirect:base;
+ assigns \result \from indirect:nptr, indirect:nptr[0 .. strlen(nptr)],
+ indirect:base;
+ assigns *endptr \from nptr, indirect:nptr[0 .. strlen(nptr)],
+ indirect:endptr, indirect:base;
behavior no_storage:
assumes null_endptr: endptr == \null;
- assigns \result \from indirect:nptr, indirect:nptr[0 ..], indirect:base;
+ assigns \result \from indirect:nptr, indirect:nptr[0 .. strlen(nptr)],
+ indirect:base;
behavior store_position:
assumes nonnull_endptr: endptr != \null;
requires valid_endptr: \valid(endptr);
- assigns \result \from indirect:nptr, indirect:nptr[0 ..], indirect:base;
- assigns *endptr \from nptr, indirect:nptr[0 ..], indirect:endptr, indirect:base;
+ assigns \result \from indirect:nptr, indirect:nptr[0 .. strlen(nptr)],
+ indirect:base;
+ assigns *endptr \from nptr, indirect:nptr[0 .. strlen(nptr)],
+ indirect:endptr, indirect:base;
ensures initialization: \initialized(endptr);
ensures valid_endptr_content: \valid_read(*endptr);
- ensures position_subset: \subset(*endptr, nptr + (0 ..));
+ ensures endptr_same_base: \base_addr(*endptr) == \base_addr(nptr);
complete behaviors;
disjoint behaviors;
*/
@@ -266,9 +291,10 @@ extern unsigned long long int strtoull(
const unsigned long __fc_rand_max = __FC_RAND_MAX;
/* ISO C: 7.20.2 */
-/*@ assigns \result \from __fc_random_counter ;
- @ assigns __fc_random_counter \from __fc_random_counter ;
- @ ensures result_range: 0 <= \result <= __fc_rand_max ;
+/*@
+ assigns \result \from indirect:__fc_random_counter;
+ assigns __fc_random_counter \from __fc_random_counter;
+ ensures result_range: 0 <= \result <= __fc_rand_max;
*/
extern int rand(void);
@@ -276,7 +302,7 @@ extern int rand(void);
extern void srand(unsigned int seed);
/*@
- assigns \result \from __fc_random_counter;
+ assigns \result \from indirect:__fc_random_counter;
ensures result_range: 0 <= \result <= __fc_rand_max;
*/
extern long int random(void);
@@ -298,8 +324,9 @@ unsigned short *__fc_p_random48_counter = __fc_random48_counter;
extern void srand48 (long int seed);
/*@
+ requires valid_seed16v: \valid(seed16v+(0..2));
requires initialization:initialized_seed16v: \initialized(seed16v+(0..2));
- assigns __fc_random48_counter[0..2] \from indirect:seed16v[0..2];
+ assigns __fc_random48_counter[0..2] \from seed16v[0..2];
assigns __fc_random48_init \from \nothing;
assigns \result \from __fc_p_random48_counter;
ensures random48_initialized: __fc_random48_init == 1;
@@ -308,7 +335,9 @@ extern void srand48 (long int seed);
extern unsigned short *seed48(unsigned short seed16v[3]);
/*@
- assigns __fc_random48_counter[0..2] \from param[0..5];
+ requires valid_param: \valid(param+(0..6));
+ requires initialization:initialized_param: \initialized(param+(0..6));
+ assigns __fc_random48_counter[0..2] \from param[0..6];
assigns __fc_random48_init \from \nothing;
ensures random48_initialized: __fc_random48_init == 1;
*/
@@ -323,6 +352,7 @@ extern void lcong48(unsigned short param[7]);
extern double drand48(void);
/*@
+ requires valid_xsubi: \valid(xsubi+(0..2));
requires initialization:initialized_xsubi: \initialized(xsubi+(0..2));
assigns __fc_random48_counter[0..2] \from __fc_random48_counter[0..2];
assigns \result \from __fc_random48_counter[0..2];
@@ -339,6 +369,7 @@ extern double erand48(unsigned short xsubi[3]);
extern long int lrand48 (void);
/*@
+ requires valid_xsubi: \valid(xsubi+(0..2));
requires initialization:initialized_xsubi: \initialized(xsubi+(0..2));
assigns __fc_random48_counter[0..2] \from __fc_random48_counter[0..2];
assigns \result \from __fc_random48_counter[0..2];
@@ -355,6 +386,7 @@ extern long int nrand48 (unsigned short xsubi[3]);
extern long int mrand48 (void);
/*@
+ requires valid_xsubi: \valid(xsubi+(0..2));
requires initialization:initialized_xsubi: \initialized(xsubi+(0..2));
assigns __fc_random48_counter[0..2] \from __fc_random48_counter[0..2];
assigns \result \from __fc_random48_counter[0..2];
@@ -520,8 +552,10 @@ extern char *__fc_env[ARG_MAX];
/*@
requires valid_name: valid_read_string(name);
- assigns \result \from __fc_env[0..], indirect:name, name[0 ..];
- ensures null_or_valid_result: \result == \null || \valid(\result);
+ assigns \result \from __fc_env[0..], indirect:name,
+ indirect:name[0 .. strlen(name)];
+ ensures null_or_valid_result:
+ \result == \null || (\valid(\result) && valid_read_string(\result));
*/
extern char *getenv(const char *name);
@@ -535,17 +569,51 @@ extern int putenv(char *string);
/*@
requires valid_name: valid_read_string(name);
requires valid_value: valid_read_string(value);
+ allocates __fc_env[0..];
assigns \result, __fc_env[0..]
- \from __fc_env[0..], indirect:name, indirect:name[0 ..],
- indirect:value, indirect:value[0 ..], indirect:overwrite;
+ \from __fc_env[0..], indirect:name[0 .. strlen(name)],
+ indirect:value[0 .. strlen(value)], indirect:overwrite;
+ assigns __fc_env[0..][0..] \from name[0 .. strlen(name)],
+ value[0 .. strlen(value)],
+ indirect:__fc_env[0..],
+ indirect:overwrite;
ensures result_ok_or_error: \result == 0 || \result == -1;
+ behavior invalid_name:
+ assumes name_empty_or_with_equals_sign:
+ strlen(name) == 0 || strchr(name, '=');
+ allocates \nothing;
+ assigns \result \from indirect:name[0 .. strlen(name)];
+ assigns __fc_errno \from indirect:name[0 .. strlen(name)];
+ ensures error: \result == -1;
+ ensures errno_set: __fc_errno == EINVAL;
+ behavior out_of_memory:
+ assumes not_enough_memory: !is_allocable(strlen(name) + strlen(value) + 2);
+ allocates \nothing;
+ assigns \result, __fc_errno \from indirect:name[0 .. strlen(name)],
+ indirect:value[0 .. strlen(value)],
+ indirect:overwrite;
+ ensures error: \result == -1;
+ ensures errno_set: __fc_errno == ENOMEM;
+ behavior ok:
+ assumes name_not_empty: strlen(name) > 0;
+ assumes name_has_no_equals_sign: !strchr(name, '=');
+ assumes enough_memory: is_allocable(strlen(name) + strlen(value) + 2);
+ allocates __fc_env[0..];
+ assigns \result, __fc_env[0..]
+ \from __fc_env[0..], indirect:name[0 .. strlen(name)],
+ indirect:value[0 .. strlen(value)], indirect:overwrite;
+ assigns __fc_env[0..][0..] \from name[0 .. strlen(name)],
+ value[0 .. strlen(value)],
+ indirect:__fc_env[0..],
+ indirect:overwrite;
+ ensures ok: \result == 0;
*/
extern int setenv(const char *name, const char *value, int overwrite);
/*@
requires valid_name: valid_read_string(name);
assigns \result, __fc_env[0..]
- \from __fc_env[0..], indirect:name, indirect:name[0 ..];
+ \from __fc_env[0..], indirect:name, indirect:name[0 .. strlen(name)];
ensures result_ok_or_error: \result == 0 || \result == -1;
*/
extern int unsetenv(const char *name);
@@ -559,7 +627,8 @@ extern void quick_exit(int status) __attribute__ ((__noreturn__));
/*@
requires null_or_valid_string_command:
command == \null || valid_read_string(command);
- assigns \result \from indirect:command, indirect:command[0 ..];
+ assigns \result \from indirect:command,
+ indirect:command[0 .. strlen(command)];
*/
extern int system(const char *command);
@@ -638,11 +707,25 @@ extern long int labs(long int j);
*/
extern long long int llabs(long long int j);
-/*@ assigns \result \from numer,denom ; */
+/*@
+ requires denom_nonzero: denom != 0;
+ requires no_overflow: !(numer == INT_MIN && denom == -1);
+ assigns \result \from numer, denom;
+*/
extern div_t div(int numer, int denom);
-/*@ assigns \result \from numer,denom ; */
+
+/*@
+ requires denom_nonzero: denom != 0;
+ requires no_overflow: !(numer == LONG_MIN && denom == -1);
+ assigns \result \from numer, denom;
+*/
extern ldiv_t ldiv(long int numer, long int denom);
-/*@ assigns \result \from numer,denom ; */
+
+/*@
+ requires denom_nonzero: denom != 0;
+ requires no_overflow: !(numer == LLONG_MIN && denom == -1);
+ assigns \result \from numer, denom;
+*/
extern lldiv_t lldiv(long long int numer, long long int denom);
/* ISO C: 7.20.7 */
diff --git a/share/libc/string.h b/share/libc/string.h
index 9ef1f1620be..e6af50f03f3 100644
--- a/share/libc/string.h
+++ b/share/libc/string.h
@@ -76,6 +76,7 @@ extern int memcmp (const void *s1, const void *s2, size_t n);
@ assigns \result \from s, c, ((unsigned char*)s)[0..n-1];
@ behavior found:
@ assumes char_found: memchr((char*)s,c,n);
+ @ ensures result_valid_read: \valid_read((char*)\result);
@ ensures result_same_base: \base_addr(\result) == \base_addr(s);
@ ensures result_char: *(char*)\result == c;
@ ensures result_in_str: \forall integer i;
@@ -88,9 +89,7 @@ extern int memcmp (const void *s1, const void *s2, size_t n);
extern void *memchr(const void *s, int c, size_t n);
// Non-POSIX; GNU extension
-// Note: these specifications are simplified w.r.t memchr's; in particular,
-// since we start searching from the end of the string, we assume the entire
-// string is valid, initialized, non-escaping, etc.
+// Note: these specifications are simplified w.r.t memchr's
/*@
requires valid: valid_read_or_empty(s, n);
requires initialization: \initialized(((unsigned char*)s)+(0 .. n - 1));
@@ -98,8 +97,8 @@ extern void *memchr(const void *s, int c, size_t n);
assigns \result \from s, indirect:c, indirect:((unsigned char*)s)[0..n-1];
behavior found:
assumes char_found: memchr((char*)s,c,n);
+ ensures result_valid_read: \valid_read((char*)\result);
ensures result_same_base: \base_addr(\result) == \base_addr(s);
- ensures result_points_to_same_base: \subset(\result, s+(0 .. n));
behavior not_found:
assumes char_not_found: !memchr((char*)s,c,n);
ensures result_null: \result == \null;
@@ -170,7 +169,8 @@ extern size_t strnlen (const char *s, size_t n);
/*@ requires valid_string_s1: valid_read_string(s1);
@ requires valid_string_s2: valid_read_string(s2);
- @ assigns \result \from indirect:s1[0..], indirect:s2[0..];
+ @ assigns \result \from indirect:s1[0..strlen(s1)],
+ @ indirect:s2[0..strlen(s1)];
@ ensures acsl_c_equiv: \result == strcmp(s1,s2);
@*/
extern int strcmp (const char *s1, const char *s2);
@@ -184,189 +184,221 @@ extern int strncmp (const char *s1, const char *s2, size_t n);
/*@ requires valid_string_s1: valid_read_string(s1); // over-strong
@ requires valid_string_s2: valid_read_string(s2); // over-strong
- @ assigns \result \from indirect:s1[0..], indirect:s2[0..];
+ @ assigns \result \from indirect:s1[0..strlen(s1)],
+ @ indirect:s2[0..strlen(s2)]; //missing: \from 'locale'
@*/
extern int strcoll (const char *s1, const char *s2);
-/*@ requires valid_string_s: valid_read_string(s);
- @ assigns \result \from s, indirect:s[0..strlen(s)], indirect:c;
- @ behavior found:
- @ assumes char_found: strchr(s,c);
- @ ensures result_char: *\result == (char)c;
- @ ensures result_same_base: \base_addr(\result) == \base_addr(s);
- @ ensures result_in_length: s <= \result <= s + strlen(s);
- @ ensures result_valid_string: valid_read_string(\result);
- @ ensures result_first_occur: \forall char* p; s<=p<\result ==> *p != (char)c;
- @ behavior not_found:
- @ assumes char_not_found: !strchr(s,c);
- @ ensures result_null: \result == \null;
- @ behavior default:
- @ ensures result_null_or_same_base:
- @ \result == \null || \base_addr(\result) == \base_addr(s);
- @*/
+/*@
+ requires valid_string_s: valid_read_string(s);
+ assigns \result \from s, indirect:s[0..strlen(s)], indirect:c;
+ behavior found:
+ assumes char_found: strchr(s,c);
+ ensures result_valid_string: valid_read_string(\result);
+ ensures result_char: *\result == (char)c;
+ ensures result_same_base: \base_addr(\result) == \base_addr(s);
+ ensures result_in_length: s <= \result <= s + strlen(s);
+ ensures result_first_occurrence:
+ \forall char* p; s <= p < \result ==> *p != (char)c;
+ behavior not_found:
+ assumes char_not_found: !strchr(s,c);
+ ensures result_null: \result == \null;
+ complete behaviors;
+ disjoint behaviors;
+*/
extern char *strchr(const char *s, int c);
-/*@ requires valid_string_s: valid_read_string(s);
- @ assigns \result \from s, indirect:s[0..strlen(s)], indirect:c;
- @ ensures result_same_base: \subset(\result, s+(0..strlen(s)));
- @*/
+/*@
+ requires valid_string_s: valid_read_string(s);
+ assigns \result \from s, indirect:s[0..strlen(s)], indirect:c;
+ ensures result_valid_string: valid_read_string(\result);
+ ensures result_same_base: \base_addr(\result) == \base_addr(s);
+*/
extern char *strchrnul(const char *s, int c);
-/*@ requires valid_string_s: valid_read_string(s);
- @ assigns \result \from s, indirect:s[0 .. strlen(s)], indirect:c;
- @ behavior found:
- @ assumes char_found: strchr(s,c);
- @ ensures result_char: *\result == c;
- @ ensures result_same_base: \base_addr(\result) == \base_addr(s);
- @ ensures result_valid_string: valid_read_string(\result);
- @ behavior not_found:
- @ assumes char_not_found: !strchr(s,c);
- @ ensures result_null: \result == \null;
- @ behavior default:
- @ ensures result_null_or_same_base:
- @ \result == \null || \base_addr(\result) == \base_addr(s);
- @ ensures result_null_or_points_to_same:
- @ \result == \null || \subset(\result, s + (0 .. strlen(s)));
- @*/
+/*@
+ requires valid_string_s: valid_read_string(s);
+ assigns \result \from s, indirect:s[0 .. strlen(s)], indirect:c;
+ ensures result_null_or_same_base:
+ \result == \null ||
+ (valid_read_string(\result) && \base_addr(\result) == \base_addr(s));
+*/
extern char *strrchr(const char *s, int c);
-/*@ requires valid_string_s: valid_read_string(s);
- @ requires valid_string_reject: valid_read_string(reject);
- @ assigns \result \from indirect:s[0..], indirect:reject[0..];
- @ ensures result_bounded: 0 <= \result <= strlen(s);
- @*/
+/*@
+ requires valid_string_s: valid_read_string(s);
+ requires valid_string_reject: valid_read_string(reject);
+ assigns \result \from indirect:s[0..strlen(s)],
+ indirect:reject[0..strlen(reject)];
+ ensures result_bounded: 0 <= \result <= strlen(s);
+*/
extern size_t strcspn(const char *s, const char *reject);
-/*@ requires valid_string_s: valid_read_string(s);
- @ requires valid_string_accept: valid_read_string(accept);
- @ assigns \result \from s[0..], accept[0..];
- @ assigns \result \from indirect:s[0..], indirect:accept[0..];
- @ ensures result_bounded: 0 <= \result <= strlen(s);
- @*/
+/*@
+ requires valid_string_s: valid_read_string(s);
+ requires valid_string_accept: valid_read_string(accept);
+ assigns \result \from indirect:s[0..strlen(s)],
+ indirect:accept[0..strlen(accept)];
+ ensures result_bounded: 0 <= \result <= strlen(s);
+*/
extern size_t strspn(const char *s, const char *accept);
-/*@ requires valid_string_s: valid_read_string(s);
- @ requires valid_string_accept: valid_read_string(accept);
- @ assigns \result \from s, s[0..], accept[0..];
- @ ensures result_null_or_same_base:
- @ \result == \null || \base_addr(\result) == \base_addr(s);
- @*/
+/*@
+ requires valid_string_s: valid_read_string(s);
+ requires valid_string_accept: valid_read_string(accept);
+ assigns \result \from s, indirect:s[0..strlen(s)],
+ indirect:accept[0..strlen(accept)];
+ ensures result_null_or_same_base:
+ \result == \null ||
+ (valid_read_string(\result) && \base_addr(\result) == \base_addr(s));
+*/
extern char *strpbrk(const char *s, const char *accept);
-/*@ requires valid_string_haystack: valid_read_string(haystack);
- @ requires valid_string_needle: valid_read_string(needle);
- @ assigns \result \from haystack, indirect:haystack[0..],
- @ indirect:needle[0..];
- @ ensures result_null_or_in_haystack:
- @ \result == \null
- @ || (\subset(\result, haystack+(0..)) && \valid_read(\result)
- @ && memcmp{Pre,Pre}(\result,needle,strlen(needle)) == 0);
- @*/
+/*@
+ requires valid_string_haystack: valid_read_string(haystack);
+ requires valid_string_needle: valid_read_string(needle);
+ assigns \result \from haystack, indirect:haystack[0..strlen(haystack)],
+ indirect:needle[0..strlen(needle)];
+ ensures result_null_or_in_haystack:
+ \result == \null ||
+ (valid_read_string(\result) &&
+ \base_addr(\result) == \base_addr(haystack) &&
+ memcmp{Pre,Pre}(\result,needle,strlen(needle)) == 0);
+*/
extern char *strstr(const char *haystack, const char *needle);
-/*@ requires valid_string_haystack: valid_read_string(haystack);
- @ requires valid_string_needle: valid_read_string(needle);
- @ assigns \result \from haystack, indirect:haystack[0..],
- @ indirect:needle[0..];
- @ ensures result_null_or_in_haystack:
- @ \result == \null
- @ || (\subset(\result, haystack+(0..)) && \valid_read(\result));
- @*/
-extern char *strcasestr (const char *haystack, const char *needle);
+/*@
+ requires valid_string_haystack: valid_read_string(haystack);
+ requires valid_string_needle: valid_read_string(needle);
+ assigns \result \from haystack, indirect:haystack[0..strlen(haystack)],
+ indirect:needle[0..strlen(needle)];
+ ensures result_null_or_in_haystack:
+ \result == \null ||
+ (valid_read_string(\result) &&
+ \base_addr(\result) == \base_addr(haystack));
+ // Note: there is currently no way to concisely write 'memcmp_ignore_case'
+*/
+extern char *strcasestr(const char *haystack, const char *needle);
// internal state of strtok
char *__fc_strtok_ptr;
-/*@ // missing: separation
+/*@
requires valid_string_delim: valid_read_string(delim);
+ requires separation: \separated(delim+(0..strlen(delim)), s+(0..strlen(s)));
assigns s[0..] \from s[0..],
- indirect:s, indirect:__fc_strtok_ptr, indirect:delim[0..];
+ indirect:s, indirect:__fc_strtok_ptr, indirect:delim[0..strlen(delim)];
assigns __fc_strtok_ptr[0..] \from __fc_strtok_ptr[0..],
- indirect:s, indirect:__fc_strtok_ptr, indirect:delim[0..];
+ indirect:s, indirect:__fc_strtok_ptr, indirect:delim[0..strlen(delim)];
assigns \result \from s, __fc_strtok_ptr, indirect:s[0..],
- indirect:__fc_strtok_ptr[0..], indirect:delim[0..];
+ indirect:__fc_strtok_ptr[0..], indirect:delim[0..strlen(delim)];
assigns __fc_strtok_ptr \from \old(__fc_strtok_ptr), s,
indirect:__fc_strtok_ptr[0..],
- indirect:delim[0..];
+ indirect:delim[0..strlen(delim)];
behavior new_str:
assumes s_not_null: s != \null;
requires valid_string_s_or_delim_not_found:
valid_string(s) ||
(valid_read_string(s) &&
- \forall int i; 0 <= i < strlen(delim) ==> !strchr(s,delim[i]));
- assigns __fc_strtok_ptr \from s, indirect:s[0..], indirect:delim[0..];
- assigns s[0..] \from s[0..], indirect:s, indirect:delim[0..];
- assigns \result \from s, indirect:s[0..], indirect:delim[0..];
- ensures result_subset: \result == \null || \subset(\result, s+(0..));
- ensures ptr_subset: \subset(__fc_strtok_ptr, s+(0..));
+ \forall ℤ i; 0 <= i < strlen(delim) ==> !strchr(s,delim[i]));
+ assigns __fc_strtok_ptr
+ \from s, indirect:s[0..], indirect:delim[0..strlen(delim)];
+ assigns s[0..] \from s[0..], indirect:s, indirect:delim[0..strlen(delim)];
+ assigns \result \from s, indirect:s[0..], indirect:delim[0..strlen(delim)];
+ ensures result_same_base:
+ \result == \null ||
+ (valid_read_string(\result) && \base_addr(\result) == \base_addr(s));
+ ensures ptr_valid_string: valid_read_string(__fc_strtok_ptr);
+ ensures ptr_same_base: \base_addr(__fc_strtok_ptr) == \base_addr(s);
behavior resume_str:
assumes s_null: s == \null;
requires not_first_call: __fc_strtok_ptr != \null;
assigns __fc_strtok_ptr[0..] \from __fc_strtok_ptr[0..],
indirect:__fc_strtok_ptr,
- indirect:delim[0..];
+ indirect:delim[0..strlen(delim)];
assigns __fc_strtok_ptr \from \old(__fc_strtok_ptr),
indirect:__fc_strtok_ptr[0..],
- indirect:delim[0..];
+ indirect:delim[0..strlen(delim)];
assigns \result \from __fc_strtok_ptr, indirect:__fc_strtok_ptr[0..],
- indirect:delim[0..];
- ensures result_subset: \result == \null ||
- \subset(\result, \old(__fc_strtok_ptr)+(0..));
- ensures ptr_subset: \subset(__fc_strtok_ptr, \old(__fc_strtok_ptr)+(0..));
+ indirect:delim[0..strlen(delim)];
+ ensures result_same_base:
+ \result == \null ||
+ (valid_read_string(\result) &&
+ \base_addr(\result) == \base_addr(\old(__fc_strtok_ptr)));
+ ensures ptr_valid_string: valid_read_string(__fc_strtok_ptr);
+ ensures ptr_same_base:
+ \base_addr(__fc_strtok_ptr) == \base_addr(\old(__fc_strtok_ptr));
complete behaviors;
disjoint behaviors;
*/
extern char *strtok(char *restrict s, const char *restrict delim);
-/*@ // missing: separation
+/*@
requires valid_string_delim: valid_read_string(delim);
+ requires separation: \separated(delim+(0..strlen(delim)), s+(0..strlen(s)),
+ *saveptr+(0..));
requires valid_saveptr: \valid(saveptr);
assigns s[0..] \from s[0..],
- indirect:s, indirect:*saveptr, indirect:delim[0..];
+ indirect:s, indirect:*saveptr, indirect:delim[0..strlen(delim)];
assigns (*saveptr)[0..] \from (*saveptr)[0..],
- indirect:s, indirect:*saveptr, indirect:delim[0..];
+ indirect:s, indirect:*saveptr, indirect:delim[0..strlen(delim)];
assigns \result \from s, *saveptr, indirect:s[0..],
- indirect:(*saveptr)[0..], indirect:delim[0..];
+ indirect:(*saveptr)[0..], indirect:delim[0..strlen(delim)];
assigns *saveptr \from \old(*saveptr), s,
indirect:(*saveptr)[0..],
- indirect:delim[0..];
+ indirect:delim[0..strlen(delim)];
behavior new_str:
assumes s_not_null: s != \null;
requires valid_string_s_or_delim_not_found:
valid_string(s) ||
(valid_read_string(s) &&
- \forall int i; 0 <= i < strlen(delim) ==> !strchr(s,delim[i]));
- assigns *saveptr \from s, indirect:s[0..], indirect:delim[0..];
- assigns s[0..] \from s[0..], indirect:s, indirect:delim[0..];
- assigns \result \from s, indirect:s[0..], indirect:delim[0..];
- ensures result_subset: \result == \null || \subset(\result, s+(0..));
- ensures initialization: \initialized(saveptr);
- ensures saveptr_subset: \subset(*saveptr, s+(0..));
+ \forall ℤ i; 0 <= i < strlen(delim) ==> !strchr(s,delim[i]));
+ assigns *saveptr
+ \from s, indirect:s[0..], indirect:delim[0..strlen(delim)];
+ assigns s[0..] \from s[0..], indirect:s, indirect:delim[0..strlen(delim)];
+ assigns \result \from s, indirect:s[0..], indirect:delim[0..strlen(delim)];
+ ensures result_same_base:
+ \result == \null ||
+ (valid_read_string(\result) && \base_addr(\result) == \base_addr(s));
+ ensures saveptr_valid_string: valid_read_string(*saveptr);
+ ensures saveptr_same_base: \base_addr(*saveptr) == \base_addr(s);
behavior resume_str:
assumes s_null: s == \null;
requires not_first_call: *saveptr != \null;
requires initialization:saveptr: \initialized(saveptr);
assigns (*saveptr)[0..] \from (*saveptr)[0..],
indirect:*saveptr,
- indirect:delim[0..];
+ indirect:delim[0..strlen(delim)];
assigns *saveptr \from \old(*saveptr),
indirect:(*saveptr)[0..],
- indirect:delim[0..];
+ indirect:delim[0..strlen(delim)];
assigns \result \from *saveptr, indirect:(*saveptr)[0..],
- indirect:delim[0..];
- ensures result_subset: \result == \null ||
- \subset(\result, \old(*saveptr)+(0..));
- ensures saveptr_subset: \subset(*saveptr, \old(*saveptr)+(0..));
+ indirect:delim[0..strlen(delim)];
+ ensures result_same_base:
+ \result == \null ||
+ (valid_read_string(\result) &&
+ \base_addr(\result) == \base_addr(\old(*saveptr)));
+ ensures saveptr_valid_string: valid_read_string(*saveptr);
+ ensures saveptr_same_base:
+ \base_addr(*saveptr) == \base_addr(\old(*saveptr));
complete behaviors;
disjoint behaviors;
*/
extern char *strtok_r(char *restrict s, const char *restrict delim, char **restrict saveptr);
-/*@ requires valid_string_stringp: \valid(stringp) && valid_string(*stringp);
- @ requires valid_string_delim: valid_read_string(delim);
- @ assigns *stringp \from delim[..], *stringp[..];
- @ assigns \result \from delim[..], *stringp[..];
- @*/
+/*@
+ requires valid_stringp: \valid(stringp);
+ assigns *stringp[0..] \from indirect:delim[0..strlen(delim)], *stringp[0..];
+ assigns \result \from *stringp;
+ behavior no_stringp:
+ assumes stringp_null: *stringp == \null;
+ ensures result_null: \result == \null;
+ behavior valid_stringp:
+ assumes stringp_not_null: *stringp != \null;
+ requires valid_string_stringp: valid_string(*stringp);
+ ensures valid_result: valid_string(\result) &&
+ \base_addr(\result) == \base_addr(*stringp);
+*/
extern char *strsep (char **stringp, const char *delim);
__FC_EXTERN char __fc_strerror[64];
@@ -440,10 +472,12 @@ size_t strlcpy(char * restrict dest, const char * restrict src, size_t n);
@*/
extern char *stpcpy(char *restrict dest, const char *restrict src);
-/*@ // missing: separation
+/*@
@ requires valid_string_src: valid_read_string(src);
@ requires valid_string_dest: valid_string(dest);
@ requires room_string: \valid(dest+(0..strlen(dest) + strlen(src)));
+ @ requires separation:
+ @ \separated(dest+(0..strlen(dest)+strlen(src)), src+(0..strlen(src)));
@ assigns dest[strlen(dest)..strlen(dest) + strlen(src)]
@ \from src[0..strlen(src)];
@ ensures sum_of_lengths: strlen(dest) == \old(strlen(dest) + strlen(src));
@@ -455,49 +489,60 @@ extern char *stpcpy(char *restrict dest, const char *restrict src);
@*/
extern char *strcat(char *restrict dest, const char *restrict src);
-/*@ // missing: separation
- @ requires valid_nstring_src: valid_read_nstring(src, n);
- @ requires valid_string_dest: valid_string(dest);
- @ assigns dest[strlen(dest) .. strlen(dest) + n] \from src[0..n];
- @ assigns \result \from dest;
- @ ensures result_ptr: \result == dest;
- @ behavior complete:
- @ assumes valid_string_src_fits: valid_read_string(src) && strlen(src) <= n;
- @ requires room_string: \valid(dest + strlen(dest) + (0 .. strlen(src)));
- @ assigns dest[strlen(dest)..strlen(dest) + strlen(src)]
- @ \from src[0..strlen(src)];
- @ assigns \result \from dest;
- @ ensures sum_of_lengths: strlen(dest) == \old(strlen(dest) + strlen(src));
- @ behavior partial:
- @ assumes valid_string_src_too_large:
- @ !(valid_read_string(src) && strlen(src) <= n);
- @ requires room_string: \valid(dest + strlen(dest) + (0 .. n));
- @ assigns dest[strlen(dest)..strlen(dest) + n]
- @ \from src[0..strlen(src)];
- @ assigns \result \from dest;
- @ ensures sum_of_bounded_lengths: strlen(dest) == \old(strlen(dest)) + n;
- @*/
+// ISO C23, 7.26.3.2, footnote 378:
+// "A terminating null character is always appended to the result.
+// Thus, the maximum number of characters that can end up in the array pointed
+// to by s1 is strlen(s1)+n+1"
+/*@
+ requires valid_nstring_src: valid_read_nstring(src, n);
+ requires valid_string_dest: valid_string(dest);
+ requires separation:
+ \separated(dest+(0..strlen(dest)+strnlen(src, n)),
+ src+(0..strnlen(src, n)));
+ assigns dest[strlen(dest) .. strlen(dest) + n] \from src[0 .. n-1];
+ assigns \result \from dest;
+ ensures result_ptr: \result == dest;
+ behavior complete:
+ assumes src_fits: strnlen(src, n) < n; // strnlen(src, n) == strlen(src)
+ requires room_string: \valid(dest + strlen(dest) + (0 .. strlen(src)));
+ assigns dest[strlen(dest) .. strlen(dest) + strlen(src)]
+ \from src[0 .. strlen(src)-1];
+ assigns \result \from dest;
+ ensures sum_of_lengths: strlen(dest) == \old(strlen(dest) + strlen(src));
+ behavior partial:
+ assumes src_too_large: strnlen(src, n) == n;
+ requires room_string: \valid(dest + strlen(dest) + (0 .. n));
+ assigns dest[strlen(dest) .. strlen(dest) + n]
+ \from src[0 .. n - 1];
+ assigns \result \from dest;
+ ensures sum_of_bounded_lengths: strlen(dest) == \old(strlen(dest)) + n;
+ complete behaviors;
+ disjoint behaviors;
+*/
extern char *strncat(char *restrict dest, const char *restrict src, size_t n);
/*@ // Non-POSIX, but often present
- @ // missing: separation
+ @
@ requires valid_string_src: valid_read_string(src);
@ requires valid_string_dest: valid_string(dest);
@ requires room_nstring: \valid(dest+(0..n-1));
+ @ requires separation:
+ @ \separated(dest+(0..\min(n-1, strlen(dest)+strlen(src))),
+ @ src+(0..strnlen(src, n-1)));
@ assigns dest[strlen(dest)..n] \from indirect:n, src[0..strlen(src)];
@ assigns \result \from indirect:src, indirect:src[0..n-1], indirect:n;
@ ensures bounded_result: \result == strlen(dest) + strlen(src);
@*/
extern size_t strlcat(char *restrict dest, const char *restrict src, size_t n);
-/*@ // missing: separation
- @ requires valid_dest: \valid(dest+(0..n - 1));
- @ requires valid_string_src: valid_read_string(src);
- @ assigns dest[0..n - 1] \from indirect:src[0..], indirect:n;
- @ assigns \result \from dest;
- @*/
-extern size_t strxfrm (char *restrict dest,
- const char *restrict src, size_t n);
+/*@ // missing: assigns ... \from 'locale';
+ requires valid_dest: \valid(dest+(0..n - 1));
+ requires valid_string_src: valid_read_string(src);
+ requires separation: \separated(dest+(0..n - 1), src+(0..strlen(src)));
+ assigns dest[0..n - 1] \from src[0..strlen(src)], indirect:n;
+ assigns \result \from indirect:src[0..strlen(src)]; // can be greater than n
+*/
+extern size_t strxfrm(char *restrict dest, const char *restrict src, size_t n);
// Non-POSIX; GNU extension
/*@
@@ -516,56 +561,84 @@ extern void *memmem(const void *haystack, size_t haystacklen,
// Allocate strings
-/*@ requires valid_string_s: valid_read_string(s);
- @ allocates \result;
- @ assigns \result \from indirect:s[0..strlen(s)], indirect:__fc_heap_status;
- @ behavior allocation:
- @ assumes can_allocate: is_allocable(strlen(s));
- @ assigns __fc_heap_status \from indirect:s, __fc_heap_status;
- @ assigns \result \from indirect:s[0..strlen(s)], indirect:__fc_heap_status;
- @ ensures allocation: \fresh(\result,strlen(s));
- @ ensures result_valid_string_and_same_contents:
- @ valid_string(\result) && strcmp(\result,s) == 0;
- @ behavior no_allocation:
- @ assumes cannot_allocate: !is_allocable(strlen(s));
- @ allocates \nothing;
- @ assigns \result \from \nothing;
- @ ensures result_null: \result == \null;
- @*/
+/*@
+ requires valid_string_s: valid_read_string(s);
+ allocates \result;
+ assigns \result \from indirect:s[0..strlen(s)], indirect:__fc_heap_status;
+ behavior allocation:
+ assumes can_allocate: is_allocable(strlen(s)+1);
+ assigns __fc_heap_status \from __fc_heap_status,
+ indirect:s[0 .. strlen(s)];
+ assigns \result \from indirect:s[0..strlen(s)], indirect:__fc_heap_status;
+ ensures allocation: \fresh(\result,strlen(s)+1);
+ ensures result_valid_string_and_same_contents:
+ valid_string(\result) && strcmp(\result,s) == 0;
+ behavior no_allocation:
+ assumes cannot_allocate: !is_allocable(strlen(s)+1);
+ allocates \nothing;
+ assigns \result \from \nothing;
+ ensures result_null: \result == \null;
+*/
extern char *strdup (const char *s);
-/*@ requires valid_string_s: valid_read_string(s);
- @ allocates \result;
- @ assigns \result \from indirect:s[0..strlen(s)], indirect:n,
- @ indirect:__fc_heap_status;
- @ behavior allocation:
- @ assumes can_allocate: is_allocable(\min(strlen(s), n+1));
- @ assigns __fc_heap_status \from indirect:s, indirect:n, __fc_heap_status;
- @ assigns \result \from indirect:s[0..strlen(s)], indirect:n,
- @ indirect:__fc_heap_status;
- @ ensures allocation: \fresh(\result,\min(strlen(s), n+1));
- @ ensures result_valid_string_bounded_and_same_prefix:
- @ \valid(\result+(0..\min(strlen(s),n))) &&
- @ valid_string(\result) && strlen(\result) <= n &&
- @ strncmp(\result,s,n) == 0;
- @ behavior no_allocation:
- @ assumes cannot_allocate: !is_allocable(\min(strlen(s), n+1));
- @ allocates \nothing;
- @ assigns \result \from \nothing;
- @ ensures result_null: \result == \null;
- @*/
+// From the strndup(3p) POSIX man page:
+// ... strndup() copies at most size plus one bytes into the newly allocated
+// memory, terminating the new string with a NUL character.
+/*@
+ requires valid_string_s: valid_read_string(s);
+ allocates \result;
+ assigns \result \from indirect:s[0..strlen(s)], indirect:n,
+ indirect:__fc_heap_status;
+ behavior allocation:
+ assumes can_allocate: is_allocable(strnlen(s, n) + 1);
+ assigns __fc_heap_status \from indirect:s, indirect:n, __fc_heap_status;
+ assigns \result \from indirect:s[0 .. strlen(s)], indirect:n,
+ indirect:__fc_heap_status;
+ ensures allocation: \fresh(\result, strnlen(s, n) + 1);
+ ensures result_valid_string_bounded_and_same_prefix:
+ \valid(\result+(0 .. strnlen(s,n))) &&
+ valid_string(\result) && strlen(\result) <= n &&
+ strncmp(\result,s,n) == 0;
+ behavior no_allocation:
+ assumes cannot_allocate: !is_allocable(strnlen(s, n) + 1);
+ allocates \nothing;
+ assigns \result \from \nothing;
+ ensures result_null: \result == \null;
+*/
extern char *strndup (const char *s, size_t n);
// More POSIX, non-C99 functions
+/*@
+ requires valid_string_src: valid_read_nstring(src, n);
+ requires valid_dest: \valid(dest+(0 .. n-1));
+ requires separation: \separated(src+(0 .. n-1), dest+(0 .. n-1));
+ assigns dest[0 .. n-1] \from src[0 .. n-1], indirect:n;
+ assigns \result \from dest, indirect:src[0 .. n-1], indirect:n;
+ ensures initialization: \initialized(dest+(0 .. n-1));
+ behavior src_is_a_string:
+ assumes src_has_nul: strlen(src) < n;
+ ensures valid_string_dest: valid_read_string(dest);
+ ensures same_contents: strcmp(dest, src) == 0;
+ ensures dest_nul_padded:
+ \forall integer i; strlen(src) <= i < n ==> dest[i] == 0;
+ ensures result_points_to_nul: \result == dest + strlen(src);
+ behavior src_too_long:
+ assumes src_no_nul: \forall integer i; 0 <= i < n ==> src[i] != 0;
+ ensures same_partial_contents: strncmp(src, dest, n) == 0;
+ ensures result_points_to_end: \result == dest + n;
+*/
extern char *stpncpy(char *restrict dest, const char *restrict src, size_t n);
+
//extern int strcoll_l(const char *s1, const char *s2, locale_t locale);
+
//extern char *strerror_l(int errnum, locale_t locale);
+
extern int strerror_r(int errnum, char *strerrbuf, size_t buflen);
__FC_EXTERN char __fc_strsignal[64];
char * const __fc_p_strsignal = __fc_strsignal;
-/*@ //missing: requires valid_signal(signum);
+/*@ //missing: requires valid_signal(signum); assigns \from 'locale';
@ assigns \result \from __fc_p_strsignal, indirect:signum;
@ ensures result_internal_str: \result == __fc_p_strsignal;
@ ensures result_nul_terminated: \result[63] == 0;
diff --git a/share/libc/wchar.h b/share/libc/wchar.h
index c3a5d51c94b..38bcc2d98cc 100644
--- a/share/libc/wchar.h
+++ b/share/libc/wchar.h
@@ -273,7 +273,7 @@ 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[0 .. wcslen(ws),
+ 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));
diff --git a/tests/libc/stdlib_c_env.c b/tests/libc/stdlib_c_env.c
index 65fc13a16cc..12bce8dbf2c 100644
--- a/tests/libc/stdlib_c_env.c
+++ b/tests/libc/stdlib_c_env.c
@@ -23,5 +23,9 @@ int main() {
//@ assert i7 == -1; // contains '='
int i8 = unsetenv(r2);
char *r3 = getenv(r2);
+ int i9 = setenv("BLA=", "val", 0);
+ //@ check i9 == -1; // contains '='
+ int i10 = setenv("", "val", 0);
+ //@ check i10 == -1; // empty name
return 0;
}
diff --git a/tests/libc/stdlib_h.c b/tests/libc/stdlib_h.c
index 7c9aa731e60..a29dc625702 100644
--- a/tests/libc/stdlib_h.c
+++ b/tests/libc/stdlib_h.c
@@ -12,6 +12,8 @@ int compare_int(const void *a, const void *b) {
return (*(int*)a < *(int*)b) ? -1 : (*(int*)a > *(int*)b);
}
+char putenv_buf[30] = "PATH3=/:/foo:/bar:";
+
volatile int nondet;
int main() {
int base = nondet ? 0 : nondet ? 2 : 36;
@@ -122,5 +124,26 @@ int main() {
l = lrand48();
//@ assert 0 <= l < 2147483648;
+ char *path = getenv("PATH");
+ if (path) {
+ //@ check imprecise: valid_read_string(path);
+ }
+ int setenv_res = setenv("PATH2", "/", 0);
+ //@ check setenv_res == -1 || setenv_res == 0;
+ int putenv_res = putenv(putenv_buf);
+
+ div_t div_res;
+ if (nondet) {
+ div_res = div(1, 0);
+ //@ check unreachable: \false;
+ }
+ if (nondet) {
+ div_res = div(INT_MIN, -1);
+ //@ check unreachable: \false;
+ }
+ div_res = div(INT_MAX, -1);
+
+ ldiv_t ldiv_res = ldiv(LONG_MAX, -1);
+ lldiv_t lldiv_res = lldiv(LLONG_MAX, -1);
return 0;
}
diff --git a/tests/libc/string_h.c b/tests/libc/string_h.c
index 090b9f60561..471e6e3a08b 100644
--- a/tests/libc/string_h.c
+++ b/tests/libc/string_h.c
@@ -3,7 +3,7 @@
void test_strcmp(void)
{
int res = strcmp("hello", "world");
- //@ assert res == 0;
+ //@ check res == 0;
}
void test_strcat(void)
@@ -22,7 +22,7 @@ void test_strstr(void)
char *s = nondet ? "aba" : "bab";
char *needle = nondet ? "a" : "b";
char *res = strstr(s, needle);
- //@ assert res != 0;
+ //@ check res != 0;
}
void test_strncat(void)
@@ -34,6 +34,16 @@ void test_strncat(void)
for (int i = 0; i < 99; i++) source[i] = 'Z';
source[99] = '\0';
strncat(data, source, 100);
+
+ // index: 0 1 2 3 4 5 6 7
+ char buf1[] = { 'a', 'b', 0, 'c', 'd', 0, 'f', 'g' };
+ strncat(buf1+3, buf1, 2); // valid: 'ab\0cdab\0'
+
+ if (nondet) {
+ char buf1[] = { 'a', 'b', 0, 'c', 'd', 0, 'f' };
+ strncat(buf1+3, buf1, 2); // invalid: strncat will add a final '\0'
+ //@ assert unreachable: \false;
+ }
}
struct s {
@@ -60,17 +70,17 @@ void test_strtok() {
}
char buf[2] = {0};
char *a = strtok(buf, " ");
- //@ assert a == \null || \subset(a, buf+(0..));
+ //@ check a == \null || \subset(a, buf+(0..));
char *b = strtok(NULL, " ");
- //@ assert b == \null || \subset(b, buf+(0..));
+ //@ check b == \null || \subset(b, buf+(0..));
char buf2[4] = "abc";
char *p = strtok(buf2, "b");
- //@ assert p == \null || \subset(p, buf2+(0..));
+ //@ check p == \null || \subset(p, buf2+(0..));
char *q = strtok(NULL, "c");
- //@ assert q == \null || \subset(p, buf2+(0..));
+ //@ check q == \null || \subset(p, buf2+(0..));
// test with non-writable string, but delimiter not found
char *r = strtok((char*)"constant!", "NONE_TO_BE_FOUND");
- //@ assert r == \null;
+ //@ check r == \null;
if (nondet) {
strtok((char*)"constant!", "!");
//@ assert unreachable_if_precise: \false;
@@ -89,18 +99,18 @@ void test_strtok_r() {
strtok_r(buf, " ", NULL); // must fail
//@ assert unreachable: \false;
}
- //@ assert a == \null || \subset(a, buf+(0..));
+ //@ check a == \null || \subset(a, buf+(0..));
char *b = strtok_r(NULL, " ", &saveptr);
Frama_C_show_each_saveptr(saveptr);
- //@ assert b == \null || \subset(b, buf+(0..));
+ //@ check b == \null || \subset(b, buf+(0..));
char buf2[4] = "abc";
char *p = strtok_r(buf2, "b", &saveptr);
- //@ assert p == \null || \subset(p, buf2+(0..));
+ //@ check p == \null || \subset(p, buf2+(0..));
char *q = strtok_r(NULL, "c", &saveptr);
- //@ assert q == \null || \subset(p, buf2+(0..));
+ //@ check q == \null || \subset(p, buf2+(0..));
// test with non-writable string, but delimiter not found
char *r = strtok_r((char*)"constant!", "NONE_TO_BE_FOUND", &saveptr);
- //@ assert r == \null;
+ //@ check r == \null;
if (nondet) {
strtok_r((char*)"constant!", "!", &saveptr);
//@ assert unreachable_if_precise: \false;
@@ -154,20 +164,20 @@ int main(int argc, char **argv)
char *a = strdup("bla"); // unsound; specification currently unsupported
char *b = strndup("bla", 2); // unsound; specification currently unsupported
char *strsig = strsignal(1);
- //@ assert valid_read_string(strsig);
+ //@ check valid_read_string(strsig);
test_strncpy();
test_strlcpy();
test_strrchr();
char *c = "haystack";
char d = nondet ? 'y' : 'k';
- char *chr1 = strchr(c, d);
+ char *chr1 = strchr(c, d); //@ check *chr1 == d;
char *nul1 = strchrnul(c, d);
d = nondet ? 'a' : 'n';
char *chr2 = strchr(c, d);
char *nul2 = strchrnul(c, d);
char pdest[10];
char *pend = mempcpy(pdest, "gnu-only function", 9);
- //@ assert imprecise: pend == pdest + 9 && *pend == '\0';
+ //@ check imprecise: pend == pdest + 9 && *pend == '\0';
char *rchr = memrchr(c, 'a', strlen(c));
//@ check imprecise: rchr == c + strlen("haysta");
@@ -184,5 +194,52 @@ int main(int argc, char **argv)
memmem(mm_haystack, sizeof(mm_haystack), mm_needle2, sizeof(mm_needle2));
//@ check imprecise: memm == \null;
+ char strsep_buf[8] = "a,b,,cc", *strsep_p1 = &strsep_buf[0];
+ char strsep_needle[] = ",./";
+ char *strsep_p2 = strsep(&strsep_p1, strsep_needle);
+ //@ check \base_addr(strsep_p1) == \base_addr(strsep_p2);
+ strsep_p2 = strsep(&strsep_p1, strsep_needle);
+ //@ check \base_addr(strsep_p1) == \base_addr(strsep_p2);
+ char *strsep_null = NULL;
+ strsep_p2 = strsep(&strsep_null, strsep_needle);
+ //@ check strsep_p2 == \null;
+
+ char *stpncpy_src = "12345678";
+ char stpncpy_dest[5];
+ char *stpncpy_res = stpncpy(stpncpy_dest, stpncpy_src, 5);
+ //@ check stpncpy_res == stpncpy_dest + 5;
+ //@ check \forall integer i; 0 <= i < 5 ==> stpncpy_dest[i] != 0;
+ char *stpncpy_src2 = "12";
+ stpncpy_res = stpncpy(stpncpy_dest, stpncpy_src2, 5);
+ //@ check stpncpy_dest[0] == '1' && stpncpy_dest[1] == '1';
+ //@ check stpncpy_dest[2..4] == 0;
+ //@ check stpncpy_res == stpncpy_dest + 2;
+
+ char *strlcat_src = "cat";
+ char strlcat_buf[10] = "dog";
+ size_t strlcat_res = strlcat(strlcat_buf, strlcat_src, 10); // "dogcat"
+ //@ check imprecise: strlcat_res == 6;
+ strlcat_res = strlcat(strlcat_buf, strlcat_buf, 0); // no overlap: n too small
+ char strlcat_buf2[10] = "dogcat";
+ strlcat_buf2[3] = 0; // "dog\0at"
+ if (nondet) {
+ // must fail: overlap between 'future string' "dogat" and source "at"
+ strlcat_res = strlcat(strlcat_buf2, strlcat_buf2 + 4, 10); // overlap
+ //@ assert unreachable: \false;
+ }
+ // no overlap: n too small; no changes to buffer
+ strlcat_res = strlcat(strlcat_buf2, strlcat_buf2 + 4, 4);
+ char strlcat_buf3[10] = "dogcat";
+ strlcat_buf3[3] = 0; // "dog\0at"
+ // no overlap: "dogt\0" and "t"
+ strlcat_res = strlcat(strlcat_buf3, strlcat_buf3 + 5, 10);
+ // check imprecise: strlcat_res == 5;
+
+ char *strxfrm_src = "harr";
+ // dest can be NULL if length is zero
+ size_t strxfrm_res = strxfrm(0, strxfrm_src, 0);
+ char strxfrm_dest[10];
+ strxfrm_res = strxfrm(strxfrm_dest, strxfrm_src, 10);
+
return 0;
}
--
GitLab