From aa2e89406871bce6a5409a1a67a52bcdf3f9ac37 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 6 Mar 2024 15:42:19 +0100
Subject: [PATCH] [libc] add assigns for a few functions
---
share/libc/__fc_builtin.c | 1 +
share/libc/__fc_builtin.h | 6 ++++++
share/libc/stdio.c | 1 +
share/libc/stdlib.h | 4 ++++
4 files changed, 12 insertions(+)
diff --git a/share/libc/__fc_builtin.c b/share/libc/__fc_builtin.c
index d6bf3d907e9..af58bb50735 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 d02295e8127..3e174f67b34 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 e7e3c0c39de..6c3b7745509 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 7038f5df1f1..d792f95c989 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
--
GitLab