diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 25b81ff83abfcef7c40a2e6de049149cb7fdbc53..daa84f4342a604432310f38fed6cfe28a467cc15 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -236,6 +236,7 @@ share/libc/ctype.h: CEA_LGPL
share/libc/dirent.h: CEA_LGPL
share/libc/dlfcn.h: CEA_LGPL
share/libc/endian.h: CEA_LGPL
+share/libc/err.h: CEA_LGPL
share/libc/errno.c: CEA_LGPL
share/libc/errno.h: CEA_LGPL
share/libc/fcntl.h: CEA_LGPL
diff --git a/share/libc/__fc_libc.h b/share/libc/__fc_libc.h
index 2f78bbc8bb1d848eeccbe2192d7343b117bee043..4c0bb5e0ce86dc30dd75508c9eca93c06370a356 100644
--- a/share/libc/__fc_libc.h
+++ b/share/libc/__fc_libc.h
@@ -37,6 +37,7 @@
#include "dirent.h"
#include "dlfcn.h"
#include "endian.h"
+#include "err.h"
#include "errno.h"
#include "fcntl.h"
#include "features.h"
diff --git a/share/libc/argz.c b/share/libc/argz.c
index 51f5110052118cafdbe34218164f11870299c802..04744ce2435b680d15d105db6877d0e7ae96ce92 100644
--- a/share/libc/argz.c
+++ b/share/libc/argz.c
@@ -60,7 +60,7 @@ static void str_append (char **to, size_t *to_len, const char *buf,
error_t argz_replace (char **argz, size_t *argz_len, const char *str,
const char *with, unsigned *replace_count) {
- error_t err = 0;
+ error_t er = 0;
if (str && *str) {
char *arg = 0;
@@ -71,7 +71,7 @@ error_t argz_replace (char **argz, size_t *argz_len, const char *str,
int delayed_copy = 1;
size_t str_len = strlen (str), with_len = strlen (with);
- while (!err && (arg = argz_next (src, src_len, arg))) {
+ while (!er && (arg = argz_next (src, src_len, arg))) {
char *match = strstr (arg, str);
if (match) {
char *from = match + str_len;
@@ -95,22 +95,22 @@ error_t argz_replace (char **argz, size_t *argz_len, const char *str,
if (to) {
if (delayed_copy) {
if (arg > src)
- err = argz_append (&dst, &dst_len, src, (arg - src));
+ er = argz_append (&dst, &dst_len, src, (arg - src));
delayed_copy = 0;
}
- if (! err)
- err = argz_add (&dst, &dst_len, to);
+ if (! er)
+ er = argz_add (&dst, &dst_len, to);
free (to);
} else
- err = ENOMEM;
+ er = ENOMEM;
if (replace_count)
(*replace_count)++;
} else if (! delayed_copy)
- err = argz_add (&dst, &dst_len, arg);
+ er = argz_add (&dst, &dst_len, arg);
}
- if (! err) {
+ if (! er) {
if (! delayed_copy) {
free (src);
*argz = dst;
@@ -120,7 +120,7 @@ error_t argz_replace (char **argz, size_t *argz_len, const char *str,
free (dst);
}
- return err;
+ return er;
}
char * argz_next (const char *argz, size_t argz_len, const char *entry) {
diff --git a/share/libc/err.h b/share/libc/err.h
new file mode 100644
index 0000000000000000000000000000000000000000..e2da20ac48182c5568126ab412a67a9ff4d4e63e
--- /dev/null
+++ b/share/libc/err.h
@@ -0,0 +1,96 @@
+/**************************************************************************/
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2021 */
+/* CEA (Commissariat à l'énergie atomique et aux énergies */
+/* alternatives) */
+/* */
+/* you can redistribute it and/or modify it under the terms of the GNU */
+/* Lesser General Public License as published by the Free Software */
+/* Foundation, version 2.1. */
+/* */
+/* It is distributed in the hope that it will be useful, */
+/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
+/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
+/* GNU Lesser General Public License for more details. */
+/* */
+/* See the GNU Lesser General Public License version 2.1 */
+/* for more details (enclosed in the file licenses/LGPLv2.1). */
+/* */
+/**************************************************************************/
+
+// Non-POSIX and not in the C ISO standard; this file is defined in the
+// GNU libc.
+
+#ifndef __FC_ERR_H
+#define __FC_ERR_H
+
+#include "features.h"
+__PUSH_FC_STDLIB
+
+#include "__fc_string_axiomatic.h"
+#include "stdarg.h"
+
+__BEGIN_DECLS
+
+// TODO: extend Variadic to handle these functions, or provide C stubs.
+// Currently, given their limited usage and non-standard status, this
+// lightweight approach seems better suited.
+
+/*@
+ requires fmt_valid_read_or_null: valid_read_string(fmt) || fmt == \null;
+ assigns \exit_status \from eval;
+ ensures never_terminates: \false;
+ */
+void err(int eval, const char *fmt, ...);
+
+/*@
+ requires fmt_valid_read_or_null: valid_read_string(fmt) || fmt == \null;
+ assigns \exit_status \from eval;
+ ensures never_terminates: \false;
+ */
+void errx(int eval, const char *fmt, ...);
+
+/*@
+ requires fmt_valid_read_or_null: valid_read_string(fmt) || fmt == \null;
+ assigns \nothing;
+ */
+void warn(const char *fmt, ...);
+
+/*@
+ requires fmt_valid_read_or_null: valid_read_string(fmt) || fmt == \null;
+ assigns \nothing;
+ */
+void warnx(const char *fmt, ...);
+
+/*@
+ requires fmt_valid_read_or_null: valid_read_string(fmt) || fmt == \null;
+ assigns \exit_status \from eval;
+ ensures never_terminates: \false;
+ */
+void verr(int eval, const char *fmt, va_list args);
+
+/*@
+ requires fmt_valid_read_or_null: valid_read_string(fmt) || fmt == \null;
+ assigns \exit_status \from eval;
+ ensures never_terminates: \false;
+ */
+void verrx(int eval, const char *fmt, va_list args);
+
+/*@
+ requires fmt_valid_read_or_null: valid_read_string(fmt) || fmt == \null;
+ assigns \nothing;
+ */
+void vwarn(const char *fmt, va_list args);
+
+/*@
+ requires fmt_valid_read_or_null: valid_read_string(fmt) || fmt == \null;
+ assigns \nothing;
+ */
+void vwarnx(const char *fmt, va_list args);
+
+__END_DECLS
+
+__POP_FC_STDLIB
+#endif
diff --git a/tests/libc/err_h.c b/tests/libc/err_h.c
new file mode 100644
index 0000000000000000000000000000000000000000..660e350ab1c0ecaa0f00f381e1a8fd0ee19dbceb
--- /dev/null
+++ b/tests/libc/err_h.c
@@ -0,0 +1,65 @@
+/* run.config
+ STDOPT:
+*/
+#include <err.h>
+#include <stdarg.h>
+
+volatile int nondet;
+
+void vaw(const char *fmt, ...) {
+ va_list ap;
+ va_start(ap, fmt);
+ vwarn(fmt, ap);
+ va_end(ap);
+}
+
+void vawx(const char *fmt, ...) {
+ va_list ap;
+ va_start(ap, fmt);
+ vwarnx(fmt, ap);
+ va_end(ap);
+}
+
+void vae(int eval, const char *fmt, ...) {
+ va_list ap;
+ va_start(ap, fmt);
+ verr(eval, fmt, ap);
+ va_end(ap);
+}
+
+void vaex(int eval, const char *fmt, ...) {
+ va_list ap;
+ va_start(ap, fmt);
+ verrx(eval, fmt, ap);
+ va_end(ap);
+}
+
+int main() {
+ int a = 1, *p = 2;
+ warn(0);
+ warn(0, a);
+ warnx("%d", a);
+ vaw("%s", "warn");
+ vawx(0);
+ if (nondet) {
+ err(0, 0);
+ //@ assert unreachable: \false;
+ }
+ if (nondet) {
+ err(1, 0, a);
+ //@ assert unreachable: \false;
+ }
+ if (nondet) {
+ errx(2, "%d", a);
+ //@ assert unreachable: \false;
+ }
+ if (nondet) {
+ vae(0, 0);
+ //@ assert unreachable: \false;
+ }
+ if (nondet) {
+ vaex(-1, "nogood %d", a);
+ //@ assert unreachable: \false;
+ }
+ return 0;
+}
diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c
index c122ff2268ffa3f05bfb7a6677e4ca81e7b84ea2..3a04272a5d77ec26a2126907dcb0406017db67a3 100644
--- a/tests/libc/fc_libc.c
+++ b/tests/libc/fc_libc.c
@@ -37,6 +37,7 @@
#include "dirent.h"
#include "dlfcn.h"
#include "endian.h"
+#include "err.h"
#include "errno.h"
#include "__fc_alloc_axiomatic.h"
#include "__fc_builtin.h"
diff --git a/tests/libc/oracle/argz_c.res.oracle b/tests/libc/oracle/argz_c.res.oracle
index 2ab7a5fe98c630ecf0df81873e164a57a4e0306d..c423da43955093adff4e4b43d14b9e8a0ca50052 100644
--- a/tests/libc/oracle/argz_c.res.oracle
+++ b/tests/libc/oracle/argz_c.res.oracle
@@ -1194,7 +1194,7 @@
[eva:final-states] Values at end of function argz_replace:
__fc_errno ∈ [--..--]
__fc_heap_status ∈ [--..--]
- err ∈ {0; 12}
+ er ∈ {0; 12}
argz ∈
{{ &__realloc_argz_append_l271_1[0] ;
&__realloc_argz_append_l271_7[0] }}
diff --git a/tests/libc/oracle/err_h.res.oracle b/tests/libc/oracle/err_h.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..4c98b5d8c8a1783683870e157b74bc052e4ff502
--- /dev/null
+++ b/tests/libc/oracle/err_h.res.oracle
@@ -0,0 +1,110 @@
+[kernel] Parsing err_h.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ nondet ∈ [--..--]
+[eva] computing for function warn <- main.
+ Called from err_h.c:39.
+[eva] using specification for function warn
+[eva] err_h.c:39:
+ function warn: precondition 'fmt_valid_read_or_null' got status valid.
+[eva] Done for function warn
+[eva] computing for function warn <- main.
+ Called from err_h.c:40.
+[eva] err_h.c:40:
+ function warn: precondition 'fmt_valid_read_or_null' got status valid.
+[eva] Done for function warn
+[eva] computing for function warnx <- main.
+ Called from err_h.c:41.
+[eva] using specification for function warnx
+[eva] err_h.c:41:
+ function warnx: precondition 'fmt_valid_read_or_null' got status valid.
+[eva] Done for function warnx
+[eva] computing for function vaw <- main.
+ Called from err_h.c:42.
+[eva] computing for function vwarn <- vaw <- main.
+ Called from err_h.c:12.
+[eva] using specification for function vwarn
+[eva] err_h.c:12:
+ function vwarn: precondition 'fmt_valid_read_or_null' got status valid.
+[eva] Done for function vwarn
+[eva] Recording results for vaw
+[eva] Done for function vaw
+[eva] computing for function vawx <- main.
+ Called from err_h.c:43.
+[eva] computing for function vwarnx <- vawx <- main.
+ Called from err_h.c:19.
+[eva] using specification for function vwarnx
+[eva] err_h.c:19:
+ function vwarnx: precondition 'fmt_valid_read_or_null' got status valid.
+[eva] Done for function vwarnx
+[eva] Recording results for vawx
+[eva] Done for function vawx
+[eva] computing for function err <- main.
+ Called from err_h.c:45.
+[eva] using specification for function err
+[eva] err_h.c:45:
+ function err: precondition 'fmt_valid_read_or_null' got status valid.
+[eva] err_h.c:45: Warning:
+ cannot interpret assigns clause \exit_status
+ (unsupported logic var \exit_status); effects will be ignored
+[eva] Done for function err
+[eva] computing for function err <- main.
+ Called from err_h.c:49.
+[eva] err_h.c:49:
+ function err: precondition 'fmt_valid_read_or_null' got status valid.
+[eva] err_h.c:49: Warning:
+ cannot interpret assigns clause \exit_status
+ (unsupported logic var \exit_status); effects will be ignored
+[eva] Done for function err
+[eva] computing for function errx <- main.
+ Called from err_h.c:53.
+[eva] using specification for function errx
+[eva] err_h.c:53:
+ function errx: precondition 'fmt_valid_read_or_null' got status valid.
+[eva] err_h.c:53: Warning:
+ cannot interpret assigns clause \exit_status
+ (unsupported logic var \exit_status); effects will be ignored
+[eva] Done for function errx
+[eva] computing for function vae <- main.
+ Called from err_h.c:57.
+[eva] computing for function verr <- vae <- main.
+ Called from err_h.c:26.
+[eva] using specification for function verr
+[eva] err_h.c:26:
+ function verr: precondition 'fmt_valid_read_or_null' got status valid.
+[eva] err_h.c:26: Warning:
+ cannot interpret assigns clause \exit_status
+ (unsupported logic var \exit_status); effects will be ignored
+[eva] Done for function verr
+[eva] Recording results for vae
+[eva] Done for function vae
+[eva] computing for function vaex <- main.
+ Called from err_h.c:61.
+[eva] computing for function verrx <- vaex <- main.
+ Called from err_h.c:33.
+[eva] using specification for function verrx
+[eva] err_h.c:33:
+ function verrx: precondition 'fmt_valid_read_or_null' got status valid.
+[eva] err_h.c:33: Warning:
+ cannot interpret assigns clause \exit_status
+ (unsupported logic var \exit_status); effects will be ignored
+[eva] Done for function verrx
+[eva] Recording results for vaex
+[eva] Done for function vaex
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function vae:
+ NON TERMINATING FUNCTION
+[eva:final-states] Values at end of function vaex:
+ NON TERMINATING FUNCTION
+[eva:final-states] Values at end of function vaw:
+ ap ∈ {{ &__va_args_14[0] }}
+[eva:final-states] Values at end of function vawx:
+ ap ∈ {{ &__va_args_16[0] }}
+[eva:final-states] Values at end of function main:
+ a ∈ {1}
+ p ∈ {2}
+ __retres ∈ {0}
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 96ad940d69778adf1aee7a90d46c4d25b63c46c2..895bbd5f4da69c893b6f69ec798ddffdc7a871f7 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -5,10 +5,10 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] fc_libc.c:172: assertion got status valid.
[eva] fc_libc.c:173: assertion got status valid.
[eva] fc_libc.c:174: assertion got status valid.
[eva] fc_libc.c:175: assertion got status valid.
+[eva] fc_libc.c:176: assertion got status valid.
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -32,6 +32,7 @@
#include "ctype.c"
#include "ctype.h"
#include "dirent.h"
+#include "err.h"
#include "errno.c"
#include "errno.h"
#include "fcntl.h"
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 566c5af75a06db659d7b28cacb1c2f2a69a9640d..366cde03330ee143db757c4a4205b6cf4394e771 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -2047,7 +2047,7 @@ static void str_append(char **to, size_t *to_len, char const *buf,
error_t argz_replace(char **argz, size_t *argz_len, char const *str,
char const *with, unsigned int *replace_count)
{
- error_t err = 0;
+ error_t er = 0;
if (str)
if (*str) {
char *arg = (char *)0;
@@ -2059,7 +2059,7 @@ error_t argz_replace(char **argz, size_t *argz_len, char const *str,
size_t str_len = strlen(str);
size_t with_len = strlen(with);
while (1) {
- if (! err) {
+ if (! er) {
arg = argz_next((char const *)src,src_len,(char const *)arg);
if (! arg) break;
}
@@ -2094,23 +2094,23 @@ error_t argz_replace(char **argz, size_t *argz_len, char const *str,
}
if (to) {
if (delayed_copy) {
- if (arg > src) err = argz_append(& dst,& dst_len,
- (char const *)src,
- (unsigned int)(arg - src));
+ if (arg > src) er = argz_append(& dst,& dst_len,
+ (char const *)src,
+ (unsigned int)(arg - src));
delayed_copy = 0;
}
- if (! err) err = argz_add(& dst,& dst_len,(char const *)to);
+ if (! er) er = argz_add(& dst,& dst_len,(char const *)to);
free((void *)to);
}
- else err = 12;
+ else er = 12;
if (replace_count) (*replace_count) ++;
}
else
- if (! delayed_copy) err = argz_add(& dst,& dst_len,
- (char const *)arg);
+ if (! delayed_copy) er = argz_add(& dst,& dst_len,
+ (char const *)arg);
}
}
- if (! err) {
+ if (! er) {
if (! delayed_copy) {
free((void *)src);
*argz = dst;
@@ -2120,7 +2120,7 @@ error_t argz_replace(char **argz, size_t *argz_len, char const *str,
else
if (dst_len > (size_t)0) free((void *)dst);
}
- return err;
+ return er;
}
char *argz_next(char const *argz, size_t argz_len, char const *entry)
@@ -8402,6 +8402,62 @@ extern DIR *opendir(char const *path);
*/
extern struct dirent *readdir(DIR *dirp);
+/*@ requires
+ fmt_valid_read_or_null: valid_read_string(fmt) ∨ fmt ≡ \null;
+ ensures never_terminates: \false;
+
+ assigns \exit_status \from eval;
+ */
+void err(int eval, char const *fmt, void * const *__va_params);
+
+/*@ requires
+ fmt_valid_read_or_null: valid_read_string(fmt) ∨ fmt ≡ \null;
+ ensures never_terminates: \false;
+
+ assigns \exit_status \from eval;
+ */
+void errx(int eval, char const *fmt, void * const *__va_params);
+
+/*@ requires
+ fmt_valid_read_or_null: valid_read_string(fmt) ∨ fmt ≡ \null;
+ assigns \nothing;
+ */
+void warn(char const *fmt, void * const *__va_params);
+
+/*@ requires
+ fmt_valid_read_or_null: valid_read_string(fmt) ∨ fmt ≡ \null;
+ assigns \nothing;
+ */
+void warnx(char const *fmt, void * const *__va_params);
+
+/*@ requires
+ fmt_valid_read_or_null: valid_read_string(fmt) ∨ fmt ≡ \null;
+ ensures never_terminates: \false;
+
+ assigns \exit_status \from eval;
+ */
+void verr(int eval, char const *fmt, va_list args);
+
+/*@ requires
+ fmt_valid_read_or_null: valid_read_string(fmt) ∨ fmt ≡ \null;
+ ensures never_terminates: \false;
+
+ assigns \exit_status \from eval;
+ */
+void verrx(int eval, char const *fmt, va_list args);
+
+/*@ requires
+ fmt_valid_read_or_null: valid_read_string(fmt) ∨ fmt ≡ \null;
+ assigns \nothing;
+ */
+void vwarn(char const *fmt, va_list args);
+
+/*@ requires
+ fmt_valid_read_or_null: valid_read_string(fmt) ∨ fmt ≡ \null;
+ assigns \nothing;
+ */
+void vwarnx(char const *fmt, va_list args);
+
/*@ requires valid_res: \valid(res);
ensures initialization: res: \initialized(\old(res));
ensures res_wrapped: *\old(res) ≡ (int)(\old(a) + \old(b));
diff --git a/tests/libc/oracle/fc_libc.2.res.oracle b/tests/libc/oracle/fc_libc.2.res.oracle
index 9e97d67741a1d5aa5687dc28730ad2aa41f27b7b..7f56a29b964dc433e9e2517346c1ae83b3c73741 100644
--- a/tests/libc/oracle/fc_libc.2.res.oracle
+++ b/tests/libc/oracle/fc_libc.2.res.oracle
@@ -57,6 +57,7 @@ skipping FRAMAC_SHARE/libc/complex.h
[kernel] Parsing FRAMAC_SHARE/libc/dirent.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/dlfcn.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/endian.h (with preprocessing)
+[kernel] Parsing FRAMAC_SHARE/libc/err.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/errno.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/fcntl.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/features.h (with preprocessing)