[Libc] improve several specifications (mainly string.h/stdlib.h) and add tests

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

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.  */

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;
   }
 

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 */

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));

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;
 }

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;
 }

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;
 }