[libc] add assigns for a few functions

share/libc/__fc_builtin.c

@@ -130,6 +130,7 @@ unsigned long Frama_C_unsigned_long_interval(unsigned long min, unsigned long ma
   return r;
 }
 
+/*@ assigns \nothing; */
 extern void __builtin_abort(void) __attribute__((noreturn)); // GCC builtin
 
 void Frama_C_abort(void)

share/libc/__fc_builtin.h

@@ -24,6 +24,7 @@
 #define Frama_C_BUILTIN
 #include "features.h"
 __PUSH_FC_STDLIB
+#include "__fc_alloc_axiomatic.h"
 #include "__fc_define_size_t.h"
 
 __BEGIN_DECLS
@@ -192,6 +193,11 @@ __attribute__((FC_BUILTIN));
 /*@ assigns \result \from p; */
 extern size_t Frama_C_offset(const void *p) __attribute__((FC_BUILTIN));
 
+/*@
+  allocates \result;
+  assigns __fc_heap_status \from size, __fc_heap_status;
+  assigns \result \from indirect:size, indirect:__fc_heap_status;
+*/
 extern void *Frama_C_malloc_fresh(size_t size) __attribute__((FC_BUILTIN));
 
 //@ assigns \result \from i;

share/libc/stdio.c

@@ -44,6 +44,7 @@ FILE * __fc_stdin = &__fc_initial_stdin;
 // "rb+","r+b","wb+","w+b","ab+","a+b".
 /*@
   requires valid_mode: valid_read_string(mode);
+  assigns \result \from mode[0 .. strlen(mode)];
  */
 static bool is_valid_mode(char const *mode) {
   if (!(mode[0] != 'r' || mode[0] != 'w' || mode[0] != 'a')) return false;

share/libc/stdlib.h

@@ -811,6 +811,10 @@ extern char *realpath(const char *restrict file_name,
 // This function may allocate memory for the result, which is not supported by
 // some plugins such as Eva. In such cases, it is preferable to use the stub
 // provided in stdlib.c.
+/*@
+  allocates \result;
+  assigns \result \from path[0 .. strlen(path)];
+ */
 extern char *canonicalize_file_name(const char *path);
 
 __END_DECLS