diff --git a/share/libc/__fc_builtin.c b/share/libc/__fc_builtin.c
index d6bf3d907e987b4102e90144bf65df220e759d82..af58bb507356e496b140a90f202e7f66b70b49ea 100644
--- a/share/libc/__fc_builtin.c
+++ b/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)
diff --git a/share/libc/__fc_builtin.h b/share/libc/__fc_builtin.h
index d02295e8127d65423803b0abe9f092cad85281b4..3e174f67b340c06c2036fbf927351f2e04e58484 100644
--- a/share/libc/__fc_builtin.h
+++ b/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;
diff --git a/share/libc/stdio.c b/share/libc/stdio.c
index e7e3c0c39de3a3c207ad5e3d0b0916da3fd246c2..6c3b7745509854b91a677a985e0ab8341e26f673 100644
--- a/share/libc/stdio.c
+++ b/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;
diff --git a/share/libc/stdlib.h b/share/libc/stdlib.h
index 7038f5df1f1a3dc067029ffbb96a9c64f59e865c..d792f95c989291d8dbbf957fd803a41969d5a0bb 100644
--- a/share/libc/stdlib.h
+++ b/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