From 4a725e30178c10a65f87d5e7dd5ef596c311450b Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Thu, 7 Mar 2024 21:08:07 +0100
Subject: [PATCH] [libc] add assigns for several functions
---
share/libc/argz.c | 1 +
share/libc/netdb.c | 4 ++++
share/libc/netdb.h | 7 ++++++-
share/libc/pwd.c | 5 +++++
share/libc/stdatomic.c | 1 +
share/libc/stdio.h | 2 +-
share/libc/stdlib.c | 4 ++++
share/libc/string.c | 3 +++
8 files changed, 25 insertions(+), 2 deletions(-)
diff --git a/share/libc/argz.c b/share/libc/argz.c
index 61da9d43f1b..fdf81545c9a 100644
--- a/share/libc/argz.c
+++ b/share/libc/argz.c
@@ -43,6 +43,7 @@ void argz_stringify (char *argz, size_t len, int sep) {
}
}
+/*@ assigns *to, *to_len \from buf[0 .. buf_len - 1]; */
static void str_append (char **to, size_t *to_len, const char *buf,
const size_t buf_len) {
size_t new_len = *to_len + buf_len;
diff --git a/share/libc/netdb.c b/share/libc/netdb.c
index 536053ca768..88682b5f915 100644
--- a/share/libc/netdb.c
+++ b/share/libc/netdb.c
@@ -93,6 +93,10 @@ struct __fc_gethostbyname {
struct __fc_gethostbyname __fc_ghbn;
+/*@
+ assigns answer[0 .. anslen-1], \result
+ \from indirect:anslen, Frama_C_entropy_source;
+*/
static int res_search(const char *dname, int rec_class, int type,
char *answer, int anslen) {
for (int i = 0; i < anslen-1; i++) {
diff --git a/share/libc/netdb.h b/share/libc/netdb.h
index a97dc179618..412d06331a4 100644
--- a/share/libc/netdb.h
+++ b/share/libc/netdb.h
@@ -178,7 +178,12 @@ extern int getaddrinfo(
struct addrinfo **restrict res);
extern struct hostent *gethostbyaddr(const void *, socklen_t, int);
-extern struct hostent *gethostbyname(const char *);
+
+/*@
+ assigns \result, *\result \from name[0 .. strlen(name)];
+*/
+extern struct hostent *gethostbyname(const char *name);
+
extern struct hostent *gethostent(void);
extern int getnameinfo(const struct sockaddr *restrict, socklen_t,
char *restrict, socklen_t, char *restrict,
diff --git a/share/libc/pwd.c b/share/libc/pwd.c
index 85cc012618c..92dcae6e471 100644
--- a/share/libc/pwd.c
+++ b/share/libc/pwd.c
@@ -48,6 +48,11 @@ static int __fc_getpw_init; // used to initialize the __fc_getpw* strings
remaining -= len
// Common code between getpwman_r and getpwuid_r
+/*@ assigns __fc_getpw_init, __fc_getpw_pw_name[0..63],
+ __fc_getpw_pw_passwd[0..63], __fc_getpw_pw_gecos[0..63],
+ __fc_getpw_pw_dir[0..63], __fc_getpw_pw_shell[0..63],
+ buf[0 .. buflen-1], *pwd, *result, \result
+ \from __fc_pwd; */
static int __fc_getpw_r(struct passwd *pwd, char *buf,
size_t buflen, struct passwd **result) {
// initialize global strings (only during first execution)
diff --git a/share/libc/stdatomic.c b/share/libc/stdatomic.c
index 28723c038b5..30c975051b9 100644
--- a/share/libc/stdatomic.c
+++ b/share/libc/stdatomic.c
@@ -26,6 +26,7 @@
#include "string.h"
__PUSH_FC_STDLIB
+/*@ assigns \nothing; */
void __fc_atomic_init_marker(void *obj, unsigned long long value) {}
void atomic_thread_fence(memory_order order) {}
diff --git a/share/libc/stdio.h b/share/libc/stdio.h
index 3b614812403..0e82d078e0a 100644
--- a/share/libc/stdio.h
+++ b/share/libc/stdio.h
@@ -581,7 +581,7 @@ extern int pclose(FILE *stream);
// This file may be included by non-POSIX machdeps, which do not define
// ssize_t, so we must check it
#ifdef __FC_POSIX_VERSION
-// No specification given; include "stdio.c" to use Frama-C's implementation
+/*@ assigns (*lineptr)[0 .. *n-1], *n, *stream, \result \from *stream; */
ssize_t getline(char **lineptr, size_t *n, FILE *stream);
#endif
diff --git a/share/libc/stdlib.c b/share/libc/stdlib.c
index 3eed8b81862..ca6863450b7 100644
--- a/share/libc/stdlib.c
+++ b/share/libc/stdlib.c
@@ -80,6 +80,10 @@ char *__fc_env[ARG_MAX];
#define __FC_INITENV_LEN 64
static char __fc_env_strings[__FC_INITENV_LEN];
+/*@
+ assigns __fc_env_strings[0 .. __FC_INITENV_LEN-1], __fc_env[0 .. ARG_MAX - 1]
+ \from Frama_C_entropy_source;
+*/
static void __fc_initenv() {
static char init;
if (!init) {
diff --git a/share/libc/string.c b/share/libc/string.c
index 1ab5d995df5..d546b236cea 100644
--- a/share/libc/string.c
+++ b/share/libc/string.c
@@ -172,6 +172,9 @@ int memcmp(const void *s1, const void *s2, size_t n)
// NOTE: strcasecmp is in POSIX's strings.h but not in C99
// auxiliary function for strcasecmp
+/*@
+ assigns \result \from c1, c2;
+*/
static int char_equal_ignore_case(char c1, char c2)
{
if (c1 >= 'A' && c1 <= 'Z') c1 -= ('A' - 'a');
--
GitLab