From 4ad5aad6d68f89ea9ace6f3881f3cf288da411e3 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Thu, 14 Mar 2019 20:04:03 +0100
Subject: [PATCH] [libc] add experimental support for <stdatomic.h>
---
headers/header_spec.txt | 2 +
share/libc/__fc_libc.h | 1 +
share/libc/__fc_runtime.c | 1 +
share/libc/stdatomic.c | 280 ++
share/libc/stdatomic.h | 253 ++
tests/libc/fc_libc.c | 1 +
tests/libc/oracle/fc_libc.0.res.oracle | 61 +-
tests/libc/oracle/fc_libc.1.res.oracle | 4628 ++++++++++++----------
tests/libc/oracle/fc_libc.2.res.oracle | 1 +
tests/libc/oracle/stdatomic_c.res.oracle | 357 ++
tests/libc/stdatomic_c.c | 47 +
11 files changed, 3562 insertions(+), 2070 deletions(-)
create mode 100644 share/libc/stdatomic.c
create mode 100644 share/libc/stdatomic.h
create mode 100644 tests/libc/oracle/stdatomic_c.res.oracle
create mode 100644 tests/libc/stdatomic_c.c
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index a4b16fda1c0..135ae1a904e 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -282,6 +282,8 @@ share/libc/setjmp.h: CEA_LGPL
share/libc/signal.c: CEA_LGPL
share/libc/signal.h: CEA_LGPL
share/libc/stdarg.h: CEA_LGPL
+share/libc/stdatomic.c: CEA_LGPL
+share/libc/stdatomic.h: CEA_LGPL
share/libc/stdbool.h: CEA_LGPL
share/libc/stddef.h: CEA_LGPL
share/libc/stdint.h: CEA_LGPL
diff --git a/share/libc/__fc_libc.h b/share/libc/__fc_libc.h
index 70797ab496b..310a2148445 100644
--- a/share/libc/__fc_libc.h
+++ b/share/libc/__fc_libc.h
@@ -73,6 +73,7 @@
#include "setjmp.h"
#include "signal.h"
#include "stdarg.h"
+#include "stdatomic.h"
#include "stdbool.h"
#include "stddef.h"
#include "stdint.h"
diff --git a/share/libc/__fc_runtime.c b/share/libc/__fc_runtime.c
index b7c3903f469..ad250213938 100644
--- a/share/libc/__fc_runtime.c
+++ b/share/libc/__fc_runtime.c
@@ -34,6 +34,7 @@
#include "netdb.c"
#include "netinet/in.c"
#include "signal.c"
+#include "stdatomic.c"
#include "stdio.c"
#include "stdlib.c"
#include "string.c"
diff --git a/share/libc/stdatomic.c b/share/libc/stdatomic.c
new file mode 100644
index 00000000000..caaeb092968
--- /dev/null
+++ b/share/libc/stdatomic.c
@@ -0,0 +1,280 @@
+/**************************************************************************/
+/* */
+/* 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). */
+/* */
+/**************************************************************************/
+
+#include "__fc_builtin.h"
+#include "stdatomic.h"
+#include "assert.h"
+#include "string.h"
+__PUSH_FC_STDLIB
+
+void __fc_atomic_init_marker(void *obj, unsigned long long value) {}
+
+void atomic_thread_fence(memory_order order) {}
+
+void atomic_signal_fence(memory_order order) {}
+
+_Bool __fc_atomic_is_lock_free(void *obj) { return Frama_C_nondet(0, 1); }
+
+void __fc_atomic_store_marker(void *object, unsigned long long desired) {}
+
+void __fc_atomic_store_explicit_marker(void *object,
+ unsigned long long desired,
+ memory_order order) {}
+
+unsigned long long __fc_atomic_load(void *obj, size_t obj_size) {
+ if (obj_size == sizeof(char)) return *((volatile atomic_uchar *)obj);
+ else if (obj_size == sizeof(short)) return *((volatile atomic_ushort *)obj);
+ else if (obj_size == sizeof(int)) return *((volatile atomic_uint *)obj);
+ else if (obj_size == sizeof(long)) return *((volatile atomic_ulong *)obj);
+ else if (obj_size == sizeof(long long))
+ return *((volatile atomic_ullong *)obj);
+ else assert(0);
+ return 0;
+}
+
+unsigned long long __fc_atomic_load_explicit(void *object,
+ memory_order order,
+ size_t obj_size) {
+ return __fc_atomic_load(object, obj_size);
+}
+
+unsigned long long __fc_atomic_exchange(void *obj,
+ unsigned long long desired,
+ size_t obj_size) {
+ unsigned long long r;
+ if (obj_size == sizeof(char)) {
+ r = *((volatile atomic_uchar *)obj);
+ *((volatile atomic_uchar *)obj) = desired;
+ } else if (obj_size == sizeof(short)) {
+ r = *((volatile atomic_ushort *)obj);
+ *((volatile atomic_ushort *)obj) = desired;
+ } else if (obj_size == sizeof(int)) {
+ r = *((volatile atomic_uint *)obj);
+ *((volatile atomic_uint *)obj) = desired;
+ } else if (obj_size == sizeof(long)) {
+ r = *((volatile atomic_ulong *)obj);
+ *((volatile atomic_ulong *)obj) = desired;
+ } else if (obj_size == sizeof(long long)) {
+ r = *((volatile atomic_ullong *)obj);
+ *((volatile atomic_ullong *)obj) = desired;
+ } else assert(0);
+ return r;
+}
+
+unsigned long long __fc_atomic_exchange_explicit(void *object,
+ unsigned long long desired,
+ memory_order order,
+ size_t obj_size) {
+ return __fc_atomic_exchange(object, desired, obj_size);
+}
+
+_Bool __fc_atomic_compare_exchange_strong(void *object, void *expected,
+ unsigned long long desired,
+ size_t obj_size) {
+ int r = memcmp(object, expected, obj_size);
+ if (r == 0) memcpy(object, &desired, obj_size);
+ else memcpy(expected, object, obj_size);
+ return r == 0;
+}
+
+_Bool __fc_atomic_compare_exchange_strong_explicit(void *object, void *expected,
+ unsigned long long desired,
+ memory_order success,
+ memory_order failure,
+ size_t obj_size) {
+ return __fc_atomic_compare_exchange_strong(object, expected, desired, obj_size);
+}
+
+_Bool __fc_atomic_compare_exchange_weak(void *object, void *expected,
+ unsigned long long desired,
+ size_t obj_size) {
+ return __fc_atomic_compare_exchange_strong(object, expected, desired, obj_size);
+}
+
+_Bool __fc_atomic_compare_exchange_weak_explicit(void *object, void *expected,
+ unsigned long long desired,
+ memory_order success,
+ memory_order failure,
+ size_t obj_size) {
+ return __fc_atomic_compare_exchange_strong(object, expected, desired, obj_size);
+}
+
+unsigned long long __fc_atomic_fetch_add(void *obj, unsigned long long operand,
+ size_t obj_size) {
+ unsigned long long r;
+ if (obj_size == sizeof(char)) {
+ r = *((volatile atomic_uchar *)obj);
+ *((volatile atomic_uchar *)obj) += operand;
+ } else if (obj_size == sizeof(short)) {
+ r = *((volatile atomic_ushort *)obj);
+ *((volatile atomic_ushort *)obj) += operand;
+ } else if (obj_size == sizeof(int)) {
+ r = *((volatile atomic_uint *)obj);
+ *((volatile atomic_uint *)obj) += operand;
+ } else if (obj_size == sizeof(long)) {
+ r = *((volatile atomic_ulong *)obj);
+ *((volatile atomic_ulong *)obj) += operand;
+ } else if (obj_size == sizeof(long long)) {
+ r = *((volatile atomic_ullong *)obj);
+ *((volatile atomic_ullong *)obj) += operand;
+ } else assert(0);
+ return r;
+}
+
+unsigned long long __fc_atomic_fetch_add_explicit(void *obj,
+ unsigned long long operand,
+ memory_order order,
+ size_t obj_size) {
+ return __fc_atomic_fetch_add(obj, operand, obj_size);
+}
+
+unsigned long long __fc_atomic_fetch_sub(void *obj, unsigned long long operand,
+ size_t obj_size) {
+ unsigned long long r;
+ if (obj_size == sizeof(char)) { r = *((volatile atomic_uchar *)obj);
+ *((volatile atomic_uchar *)obj) -= operand; }
+ else if (obj_size == sizeof(short)) { r = *((volatile atomic_ushort *)obj);
+ *((volatile atomic_ushort *)obj) -= operand; }
+ else if (obj_size == sizeof(int)) { r = *((volatile atomic_uint *)obj);
+ *((volatile atomic_uint *)obj) -= operand; }
+ else if (obj_size == sizeof(long)) { r = *((volatile atomic_ulong *)obj);
+ *((volatile atomic_ulong *)obj) -= operand; }
+ else if (obj_size == sizeof(long long)) { r = *((volatile atomic_ullong *)obj);
+ *((volatile atomic_ullong *)obj) -= operand; }
+ else assert(0);
+ return r;
+}
+
+unsigned long long __fc_atomic_fetch_sub_explicit(void *obj,
+ unsigned long long operand,
+ memory_order order,
+ size_t obj_size) {
+ return __fc_atomic_fetch_sub(obj, operand, obj_size);
+}
+
+unsigned long long __fc_atomic_fetch_or(void *obj, unsigned long long operand,
+ size_t obj_size) {
+ unsigned long long r;
+ if (obj_size == sizeof(char)) { r = *((volatile atomic_uchar *)obj);
+ *((volatile atomic_uchar *)obj) |= operand; }
+ else if (obj_size == sizeof(short)) { r = *((volatile atomic_ushort *)obj);
+ *((volatile atomic_ushort *)obj) |= operand; }
+ else if (obj_size == sizeof(int)) { r = *((volatile atomic_uint *)obj);
+ *((volatile atomic_uint *)obj) |= operand; }
+ else if (obj_size == sizeof(long)) { r = *((volatile atomic_ulong *)obj);
+ *((volatile atomic_ulong *)obj) |= operand; }
+ else if (obj_size == sizeof(long long)) { r = *((volatile atomic_ullong *)obj);
+ *((volatile atomic_ullong *)obj) |= operand; }
+ else assert(0);
+ return r;
+}
+
+unsigned long long __fc_atomic_fetch_or_explicit(void *obj,
+ unsigned long long operand,
+ memory_order order,
+ size_t obj_size) {
+ return __fc_atomic_fetch_or(obj, operand, obj_size);
+}
+
+unsigned long long __fc_atomic_fetch_xor(void *obj, unsigned long long operand,
+ size_t obj_size) {
+ unsigned long long r;
+ if (obj_size == sizeof(char)) {
+ r = *((volatile atomic_uchar *)obj);
+ *((volatile atomic_uchar *)obj) ^= operand;
+ } else if (obj_size == sizeof(short)) {
+ r = *((volatile atomic_ushort *)obj);
+ *((volatile atomic_ushort *)obj) ^= operand;
+ } else if (obj_size == sizeof(int)) {
+ r = *((volatile atomic_uint *)obj);
+ *((volatile atomic_uint *)obj) ^= operand;
+ } else if (obj_size == sizeof(long)) {
+ r = *((volatile atomic_ulong *)obj);
+ *((volatile atomic_ulong *)obj) ^= operand;
+ } else if (obj_size == sizeof(long long)) {
+ r = *((volatile atomic_ullong *)obj);
+ *((volatile atomic_ullong *)obj) ^= operand;
+ }
+ else assert(0);
+ return r;
+}
+
+unsigned long long __fc_atomic_fetch_xor_explicit(void *obj,
+ unsigned long long operand,
+ memory_order order,
+ size_t obj_size) {
+ return __fc_atomic_fetch_xor(obj, operand, obj_size);
+}
+
+unsigned long long __fc_atomic_fetch_and(void *obj,
+ unsigned long long operand,
+ size_t obj_size) {
+ unsigned long long r;
+ if (obj_size == sizeof(char)) {
+ r = *((volatile atomic_uchar *)obj);
+ *((volatile atomic_uchar *)obj) &= operand;
+ } else if (obj_size == sizeof(short)) {
+ r = *((volatile atomic_ushort *)obj);
+ *((volatile atomic_ushort *)obj) &= operand;
+ } else if (obj_size == sizeof(int)) {
+ r = *((volatile atomic_uint *)obj);
+ *((volatile atomic_uint *)obj) &= operand;
+ } else if (obj_size == sizeof(long)) {
+ r = *((volatile atomic_ulong *)obj);
+ *((volatile atomic_ulong *)obj) &= operand;
+ } else if (obj_size == sizeof(long long)) {
+ r = *((volatile atomic_ullong *)obj);
+ *((volatile atomic_ullong *)obj) &= operand;
+ } else assert(0);
+ return r;
+}
+
+unsigned long long __fc_atomic_fetch_and_explicit(void *obj,
+ unsigned long long operand,
+ memory_order order,
+ size_t obj_size) {
+ return __fc_atomic_fetch_and(obj, operand, obj_size);
+}
+
+_Bool atomic_flag_test_and_set(volatile atomic_flag *object) {
+ _Bool r = object->__fc_val;
+ object->__fc_val = 1;
+ return r;
+}
+
+_Bool atomic_flag_test_and_set_explicit(volatile atomic_flag *object,
+ memory_order order) {
+ _Bool r = object->__fc_val;
+ object->__fc_val = 1;
+ return r;
+}
+
+void atomic_flag_clear(volatile atomic_flag *object) {
+ object->__fc_val = 0;
+}
+
+void atomic_flag_clear_explicit(volatile atomic_flag *object,
+ memory_order order) {
+ object->__fc_val = 0;
+}
+
+__POP_FC_STDLIB
diff --git a/share/libc/stdatomic.h b/share/libc/stdatomic.h
new file mode 100644
index 00000000000..bbf15ca1a5b
--- /dev/null
+++ b/share/libc/stdatomic.h
@@ -0,0 +1,253 @@
+/**************************************************************************/
+/* */
+/* 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). */
+/* */
+/**************************************************************************/
+
+#ifndef __FC_STDATOMIC
+#define __FC_STDATOMIC
+#include "features.h"
+__PUSH_FC_STDLIB
+#include "wchar.h"
+#include "stddef.h"
+
+__BEGIN_DECLS
+
+#define ATOMIC_BOOL_LOCK_FREE 2
+#define ATOMIC_CHAR_LOCK_FREE 2
+#define ATOMIC_CHAR16_T_LOCK_FREE 2
+#define ATOMIC_CHAR32_T_LOCK_FREE 2
+#define ATOMIC_WCHAR_T_LOCK_FREE 2
+#define ATOMIC_SHORT_LOCK_FREE 2
+#define ATOMIC_INT_LOCK_FREE 2
+#define ATOMIC_LONG_LOCK_FREE 2
+#define ATOMIC_LLONG_LOCK_FREE 2
+#define ATOMIC_POINTER_LOCK_FREE 2
+
+typedef enum __fc_memory_order {
+ memory_order_relaxed,
+ memory_order_consume,
+ memory_order_acquire,
+ memory_order_release,
+ memory_order_acq_rel,
+ memory_order_seq_cst
+} memory_order;
+
+// _Atomic is currently ignored by Frama-C
+#define _Atomic
+
+typedef _Atomic struct __fc_atomic_flag {
+ unsigned char __fc_val;
+} atomic_flag;
+
+#define ATOMIC_VAR_INIT(V) (V)
+#define ATOMIC_FLAG_INIT {0}
+
+typedef _Atomic _Bool atomic_bool;
+typedef _Atomic char atomic_char;
+typedef _Atomic signed char atomic_schar;
+typedef _Atomic unsigned char atomic_uchar;
+typedef _Atomic short atomic_short;
+typedef _Atomic unsigned short atomic_ushort;
+typedef _Atomic int atomic_int;
+typedef _Atomic unsigned int atomic_uint;
+typedef _Atomic long atomic_long;
+typedef _Atomic unsigned long atomic_ulong;
+typedef _Atomic long long atomic_llong;
+typedef _Atomic unsigned long long atomic_ullong;
+//typedef _Atomic char16_t atomic_char16_t;
+//typedef _Atomic char32_t atomic_char32_t;
+typedef _Atomic wchar_t atomic_wchar_t;
+typedef _Atomic int_least8_t atomic_int_least8_t;
+typedef _Atomic uint_least8_t atomic_uint_least8_t;
+typedef _Atomic int_least16_t atomic_int_least16_t;
+typedef _Atomic uint_least16_t atomic_uint_least16_t;
+typedef _Atomic int_least32_t atomic_int_least32_t;
+typedef _Atomic uint_least32_t atomic_uint_least32_t;
+typedef _Atomic int_least64_t atomic_int_least64_t;
+typedef _Atomic uint_least64_t atomic_uint_least64_t;
+typedef _Atomic int_fast8_t atomic_int_fast8_t;
+typedef _Atomic uint_fast8_t atomic_uint_fast8_t;
+typedef _Atomic int_fast16_t atomic_int_fast16_t;
+typedef _Atomic uint_fast16_t atomic_uint_fast16_t;
+typedef _Atomic int_fast32_t atomic_int_fast32_t;
+typedef _Atomic uint_fast32_t atomic_uint_fast32_t;
+typedef _Atomic int_fast64_t atomic_int_fast64_t;
+typedef _Atomic uint_fast64_t atomic_uint_fast64_t;
+typedef _Atomic intptr_t atomic_intptr_t;
+typedef _Atomic uintptr_t atomic_uintptr_t;
+typedef _Atomic size_t atomic_size_t;
+typedef _Atomic ptrdiff_t atomic_ptrdiff_t;
+typedef _Atomic intmax_t atomic_intmax_t;
+typedef _Atomic uintmax_t atomic_uintmax_t;
+
+
+// NOTE: The stubs below serve only to help parsing succeed and do not
+// match expected concurrence semantics.
+
+#define atomic_init(obj, value) \
+ do { __fc_atomic_init_marker(obj, value); *obj = value; } while (0)
+
+#define kill_dependency(y) (y)
+
+extern void atomic_thread_fence(memory_order order);
+extern void atomic_signal_fence(memory_order order);
+
+_Bool __fc_atomic_is_lock_free(void *obj);
+#define atomic_is_lock_free(obj) __fc_atomic_is_lock_free(obj)
+
+void __fc_atomic_store_marker(void *object, unsigned long long desired);
+#define atomic_store(obj, value) \
+ do { __fc_atomic_store_marker(obj, value); *obj = value; } while (0)
+
+void __fc_atomic_store_explicit_marker(void *object, unsigned long long desired,
+ memory_order order);
+#define atomic_store_explicit(obj, value, order) \
+ do { __fc_atomic_store_explicit_marker(obj, value, order); *obj = value; } \
+ while (0)
+
+unsigned long long __fc_atomic_load(void *object, size_t obj_size);
+#define atomic_load(obj) __fc_atomic_load(obj, sizeof(*obj))
+
+unsigned long long __fc_atomic_load_explicit(void *object, memory_order order,
+ size_t obj_size);
+#define atomic_load_explicit(obj, order) \
+ __fc_atomic_load_explicit(obj, order, sizeof(*obj))
+
+unsigned long long __fc_atomic_exchange(void *object,
+ unsigned long long desired,
+ size_t obj_size);
+#define atomic_exchange(obj, desired) \
+ __fc_atomic_exchange(obj, desired, sizeof(*obj))
+
+unsigned long long __fc_atomic_exchange_explicit(void *object,
+ unsigned long long desired,
+ memory_order order,
+ size_t obj_size);
+#define atomic_exchange_explicit(obj, desired, order) \
+ __fc_atomic_exchange_explicit(obj, desired, order, sizeof(*obj))
+
+_Bool __fc_atomic_compare_exchange_strong(void *object, void *expected,
+ unsigned long long desired,
+ size_t obj_size);
+#define atomic_compare_exchange_strong(obj, desired, expected) \
+ __fc_atomic_compare_exchange_strong(obj, desired, expected, sizeof(*obj))
+
+_Bool __fc_atomic_compare_exchange_strong_explicit(void *object, void *expected,
+ unsigned long long desired,
+ memory_order success,
+ memory_order failure,
+ size_t obj_size);
+#define atomic_compare_exchange_strong_explicit(obj, desired, expected, \
+ success, failure) \
+ __fc_atomic_compare_exchange_strong_explicit(obj, desired, expected, \
+ success, failure, sizeof(*obj))
+
+_Bool __fc_atomic_compare_exchange_weak(void *object, void *expected,
+ unsigned long long desired,
+ size_t obj_size);
+#define atomic_compare_exchange_weak(obj, desired, expected) \
+ __fc_atomic_compare_exchange_weak(obj, desired, expected, sizeof(*obj))
+
+_Bool __fc_atomic_compare_exchange_weak_explicit(void *object, void *expected,
+ unsigned long long desired,
+ memory_order success,
+ memory_order failure,
+ size_t obj_size);
+#define atomic_compare_exchange_weak_explicit(obj, desired, expected, \
+ success, failure) \
+ __fc_atomic_compare_exchange_weak_explicit(obj, desired, expected, success, \
+ failure, sizeof(*obj))
+
+unsigned long long __fc_atomic_fetch_add(void *object,
+ unsigned long long operand,
+ size_t obj_size);
+#define atomic_fetch_add(obj, operand) \
+ __fc_atomic_fetch_add(obj, operand, sizeof(*obj))
+
+unsigned long long __fc_atomic_fetch_add_explicit(void *object,
+ unsigned long long operand,
+ memory_order order,
+ size_t obj_size);
+#define atomic_fetch_add_explicit(obj, operand, order) \
+ __fc_atomic_fetch_add_explicit(obj, operand, order, sizeof(*obj))
+
+unsigned long long __fc_atomic_fetch_sub(void *object,
+ unsigned long long operand,
+ size_t obj_size);
+#define atomic_fetch_sub(obj, operand) \
+ __fc_atomic_fetch_sub(obj, operand, sizeof(*obj))
+
+unsigned long long __fc_atomic_fetch_sub_explicit(void *object,
+ unsigned long long operand,
+ memory_order order,
+ size_t obj_size);
+#define atomic_fetch_sub_explicit(obj, operand, order) \
+ __fc_atomic_fetch_sub_explicit(obj, operand, order, sizeof(*obj))
+
+unsigned long long __fc_atomic_fetch_or(void *object,
+ unsigned long long operand,
+ size_t obj_size);
+#define atomic_fetch_or(obj, operand) \
+ __fc_atomic_fetch_or(obj, operand, sizeof(*obj))
+
+unsigned long long __fc_atomic_fetch_or_explicit(void *object,
+ unsigned long long operand,
+ memory_order order,
+ size_t obj_size);
+#define atomic_fetch_or_explicit(obj, operand, order) \
+ __fc_atomic_fetch_or_explicit(obj, operand, order, sizeof(*obj))
+
+unsigned long long __fc_atomic_fetch_xor(void *object,
+ unsigned long long operand,
+ size_t obj_size);
+#define atomic_fetch_xor(obj, operand) \
+ __fc_atomic_fetch_xor(obj, operand, sizeof(*obj))
+
+unsigned long long __fc_atomic_fetch_xor_explicit(void *object,
+ unsigned long long operand,
+ memory_order order,
+ size_t obj_size);
+#define atomic_fetch_xor_explicit(obj, operand, order) \
+ __fc_atomic_fetch_xor_explicit(obj, operand, order, sizeof(*obj))
+
+unsigned long long __fc_atomic_fetch_and(void *object,
+ unsigned long long operand,
+ size_t obj_size);
+#define atomic_fetch_and(obj, operand) \
+ __fc_atomic_fetch_and(obj, operand, sizeof(*obj))
+
+unsigned long long __fc_atomic_fetch_and_explicit(void *object,
+ unsigned long long operand,
+ memory_order order,
+ size_t obj_size);
+#define atomic_fetch_and_explicit(obj, operand, order) \
+ __fc_atomic_fetch_and_explicit(obj, operand, order, sizeof(*obj))
+
+extern _Bool atomic_flag_test_and_set(volatile atomic_flag *object);
+extern _Bool atomic_flag_test_and_set_explicit(volatile atomic_flag *object,
+ memory_order order);
+extern void atomic_flag_clear(volatile atomic_flag *object);
+extern void atomic_flag_clear_explicit(volatile atomic_flag *object,
+ memory_order order);
+
+__END_DECLS
+
+__POP_FC_STDLIB
+#endif
diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c
index 53b38f02cd5..f570af584e7 100644
--- a/tests/libc/fc_libc.c
+++ b/tests/libc/fc_libc.c
@@ -119,6 +119,7 @@
#include "setjmp.h"
#include "signal.h"
#include "stdarg.h"
+#include "stdatomic.h"
#include "stdbool.h"
#include "stddef.h"
#include "stdint.h"
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index c300bb3596b..297a5e0531d 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -4,28 +4,45 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] tests/libc/fc_libc.c:166: assertion got status valid.
[eva] tests/libc/fc_libc.c:167: assertion got status valid.
[eva] tests/libc/fc_libc.c:168: assertion got status valid.
[eva] tests/libc/fc_libc.c:169: assertion got status valid.
+[eva] tests/libc/fc_libc.c:170: assertion got status valid.
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
-[metrics] Defined functions (100)
+[metrics] Defined functions (128)
=======================
Frama_C_abort (1 call); Frama_C_char_interval (1 call);
Frama_C_double_interval (0 call); Frama_C_float_interval (0 call);
Frama_C_interval (17 calls); Frama_C_make_unknown (6 calls);
- Frama_C_nondet (12 calls); Frama_C_nondet_ptr (0 call);
- Frama_C_update_entropy (7 calls); __FC_assert (0 call);
- __fc_initenv (4 calls); __finite (0 call); __finitef (0 call); abs (0 call);
- argz_add (3 calls); argz_add_sep (0 call); argz_append (2 calls);
- argz_count (0 call); argz_create (0 call); argz_create_sep (0 call);
- argz_delete (0 call); argz_extract (0 call); argz_insert (0 call);
- argz_next (1 call); argz_replace (0 call); argz_stringify (0 call);
- asprintf (0 call); atoi (0 call); calloc (0 call);
+ Frama_C_nondet (13 calls); Frama_C_nondet_ptr (0 call);
+ Frama_C_update_entropy (7 calls); __FC_assert (7 calls);
+ __fc_atomic_compare_exchange_strong (3 calls);
+ __fc_atomic_compare_exchange_strong_explicit (0 call);
+ __fc_atomic_compare_exchange_weak (0 call);
+ __fc_atomic_compare_exchange_weak_explicit (0 call);
+ __fc_atomic_exchange (1 call); __fc_atomic_exchange_explicit (0 call);
+ __fc_atomic_fetch_add (1 call); __fc_atomic_fetch_add_explicit (0 call);
+ __fc_atomic_fetch_and (1 call); __fc_atomic_fetch_and_explicit (0 call);
+ __fc_atomic_fetch_or (1 call); __fc_atomic_fetch_or_explicit (0 call);
+ __fc_atomic_fetch_sub (1 call); __fc_atomic_fetch_sub_explicit (0 call);
+ __fc_atomic_fetch_xor (1 call); __fc_atomic_fetch_xor_explicit (0 call);
+ __fc_atomic_init_marker (0 call); __fc_atomic_is_lock_free (0 call);
+ __fc_atomic_load (1 call); __fc_atomic_load_explicit (0 call);
+ __fc_atomic_store_explicit_marker (0 call);
+ __fc_atomic_store_marker (0 call); __fc_initenv (4 calls);
+ __finite (0 call); __finitef (0 call); abs (0 call); argz_add (3 calls);
+ argz_add_sep (0 call); argz_append (2 calls); argz_count (0 call);
+ argz_create (0 call); argz_create_sep (0 call); argz_delete (0 call);
+ argz_extract (0 call); argz_insert (0 call); argz_next (1 call);
+ argz_replace (0 call); argz_stringify (0 call); asprintf (0 call);
+ atoi (0 call); atomic_flag_clear (0 call);
+ atomic_flag_clear_explicit (0 call); atomic_flag_test_and_set (0 call);
+ atomic_flag_test_and_set_explicit (0 call); atomic_signal_fence (0 call);
+ atomic_thread_fence (0 call); calloc (0 call);
char_equal_ignore_case (1 call); fabs (0 call); fabsf (0 call);
feholdexcept (0 call); fesetenv (0 call); fetestexcept (0 call);
getaddrinfo (0 call); getenv (0 call); gethostbyname (0 call);
@@ -34,7 +51,7 @@
iscntrl (0 call); isdigit (3 calls); isgraph (0 call); islower (0 call);
isprint (0 call); ispunct (0 call); isspace (1 call); isupper (0 call);
isxdigit (0 call); localeconv (0 call); main (0 call); memchr (0 call);
- memcmp (0 call); memcpy (5 calls); memmove (3 calls); memoverlap (1 call);
+ memcmp (1 call); memcpy (7 calls); memmove (3 calls); memoverlap (1 call);
mempcpy (1 call); memrchr (0 call); memset (1 call);
posix_memalign (0 call); putenv (0 call); realpath (0 call);
res_search (1 call); setenv (0 call); setlocale (0 call); stpcpy (1 call);
@@ -196,18 +213,18 @@
Global metrics
==============
- Sloc = 1472
- Decision point = 271
+ Sloc = 1641
+ Decision point = 307
Global variables = 86
- If = 256
+ If = 292
Loop = 55
- Goto = 113
- Assignment = 625
- Exit point = 100
- Function = 528
- Function call = 144
- Pointer dereferencing = 254
- Cyclomatic complexity = 371
+ Goto = 118
+ Assignment = 711
+ Exit point = 128
+ Function = 556
+ Function call = 165
+ Pointer dereferencing = 350
+ Cyclomatic complexity = 435
[kernel] share/libc/sys/socket.h:451: Warning:
clause with '\initialized' must contain name 'initialization'
/* Generated by Frama-C */
@@ -253,6 +270,8 @@
#include "signal.c"
#include "signal.h"
#include "stdarg.h"
+#include "stdatomic.c"
+#include "stdatomic.h"
#include "stddef.h"
#include "stdint.h"
#include "stdio.c"
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 38af9dde42f..7053e853eee 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -235,7 +235,6 @@ struct __fc_gethostbyname {
char *host_aliases[2] ;
char hostbuf[128] ;
};
-typedef void * const * va_list;
typedef unsigned int ino_t;
typedef long time_t;
typedef unsigned int blkcnt_t;
@@ -267,8 +266,6 @@ struct __fc_FILE {
unsigned int __fc_FILE_data ;
};
typedef struct __fc_FILE FILE;
-typedef unsigned int id_t;
-typedef int suseconds_t;
typedef int clockid_t;
struct timespec {
long tv_sec ;
@@ -286,6 +283,27 @@ struct tm {
int tm_yday ;
int tm_isdst ;
};
+enum __fc_memory_order {
+ memory_order_relaxed = 0,
+ memory_order_consume = 1,
+ memory_order_acquire = 2,
+ memory_order_release = 3,
+ memory_order_acq_rel = 4,
+ memory_order_seq_cst = 5
+};
+typedef enum __fc_memory_order memory_order;
+struct __fc_atomic_flag {
+ unsigned char __fc_val ;
+};
+typedef struct __fc_atomic_flag atomic_flag;
+typedef unsigned char atomic_uchar;
+typedef unsigned short atomic_ushort;
+typedef unsigned int atomic_uint;
+typedef unsigned long atomic_ulong;
+typedef unsigned long long atomic_ullong;
+typedef void * const * va_list;
+typedef unsigned int id_t;
+typedef int suseconds_t;
struct dirent {
ino_t d_ino ;
off_t d_off ;
@@ -5186,2413 +5204,2925 @@ struct in6_addr const in6addr_loopback =
(unsigned char)0,
(unsigned char)0,
(unsigned char)1}};
-FILE *__fc_stderr;
-
-FILE *__fc_stdin;
-
-FILE *__fc_stdout;
-
-/*@ requires valid_filename: valid_read_string(filename);
- ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
- assigns \result;
- assigns \result
- \from (indirect: *(filename + (0 .. strlen{Old}(filename))));
- */
-extern int remove(char const *filename);
+/*@ ghost unsigned int volatile __fc_time; */
+/*@ assigns \result;
+ assigns \result \from __fc_time; */
+extern clock_t clock(void);
-/*@ requires valid_old_name: valid_read_string(old_name);
- requires valid_new_name: valid_read_string(new_name);
- ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
- assigns \result;
- assigns \result
- \from (indirect: *(old_name + (0 .. strlen{Old}(old_name)))),
- (indirect: *(new_name + (0 .. strlen{Old}(new_name))));
- */
-extern int rename(char const *old_name, char const *new_name);
+/*@ assigns \result;
+ assigns \result \from time1, time0; */
+extern double difftime(time_t time1, time_t time0);
-FILE __fc_fopen[16];
-FILE * const __fc_p_fopen = __fc_fopen;
-/*@ ensures
- result_null_or_valid_fd:
- \result ≡ \null ∨ \subset(\result, &__fc_fopen[0 .. 16 - 1]);
- assigns \result;
- assigns \result \from __fc_p_fopen;
+/*@ requires valid_timeptr: \valid(timeptr);
+ assigns *timeptr, \result;
+ assigns *timeptr \from *timeptr;
+ assigns \result \from (indirect: *timeptr);
*/
-extern FILE *tmpfile(void);
+extern time_t mktime(struct tm *timeptr);
-char __fc_tmpnam[2048];
-char * const __fc_p_tmpnam = __fc_tmpnam;
-/*@ requires valid_s_or_null: s ≡ \null ∨ \valid(s + (0 .. 2048));
- ensures
- result_string_or_null:
- \result ≡ \null ∨ \result ≡ \old(s) ∨
- \result ≡ __fc_p_tmpnam;
- assigns *(__fc_p_tmpnam + (0 .. 2048)), *(s + (0 .. 2048)), \result;
- assigns *(__fc_p_tmpnam + (0 .. 2048))
- \from *(__fc_p_tmpnam + (0 .. 2048)), (indirect: s);
- assigns *(s + (0 .. 2048))
- \from (indirect: s), *(__fc_p_tmpnam + (0 .. 2048));
- assigns \result \from s, __fc_p_tmpnam;
+/*@ assigns *timer, \result;
+ assigns *timer \from __fc_time;
+ assigns \result \from __fc_time;
+
+ behavior null:
+ assumes timer_null: timer ≡ \null;
+ assigns \result;
+ assigns \result \from __fc_time;
+
+ behavior not_null:
+ assumes timer_non_null: timer ≢ \null;
+ requires valid_timer: \valid(timer);
+ ensures initialization: timer: \initialized(\old(timer));
+ assigns *timer, \result;
+ assigns *timer \from __fc_time;
+ assigns \result \from __fc_time;
+
+ complete behaviors not_null, null;
+ disjoint behaviors not_null, null;
*/
-extern char *tmpnam(char *s);
+extern time_t time(time_t *timer);
-/*@ requires valid_stream: \valid(stream);
- ensures result_zero_or_EOF: \result ≡ 0 ∨ \result ≡ -1;
- assigns \result;
- assigns \result \from (indirect: stream), (indirect: *stream);
+char __fc_ctime[26];
+char * const __fc_p_ctime = __fc_ctime;
+/*@ requires valid_timeptr: \valid_read(timeptr);
+ requires initialization: init_timeptr: \initialized(timeptr);
+ ensures result_points_to_ctime: \result ≡ __fc_p_ctime;
+ ensures result_valid_string: valid_read_string(__fc_p_ctime);
+ assigns __fc_ctime[0 .. 25], \result;
+ assigns __fc_ctime[0 .. 25]
+ \from (indirect: *timeptr), (indirect: __fc_time);
+ assigns \result
+ \from (indirect: *timeptr), (indirect: __fc_time), __fc_p_ctime;
*/
-extern int fclose(FILE *stream);
+extern char *asctime(struct tm const *timeptr);
-/*@ requires null_or_valid_stream: stream ≡ \null ∨ \valid_read(stream);
- ensures result_zero_or_EOF: \result ≡ 0 ∨ \result ≡ -1;
- assigns \result, *stream, __fc_fopen[0 .. 16 - 1];
+/*@ requires valid_timer: \valid_read(timer);
+ requires initialization: init_timer: \initialized(timer);
+ ensures result_points_to_ctime: \result ≡ __fc_p_ctime;
+ ensures result_valid_string: valid_read_string(__fc_p_ctime);
+ assigns __fc_ctime[0 .. 25], \result;
+ assigns __fc_ctime[0 .. 25]
+ \from (indirect: *timer), (indirect: __fc_time);
assigns \result
- \from (indirect: *stream), (indirect: __fc_fopen[0 .. 16 - 1]);
- assigns *stream
- \from (indirect: stream), *stream, __fc_fopen[0 .. 16 - 1];
- assigns __fc_fopen[0 .. 16 - 1]
- \from (indirect: stream), *stream, __fc_fopen[0 .. 16 - 1];
-
- behavior flush_all:
- assumes all_streams: stream ≡ \null;
- assigns __fc_fopen[0 .. 16 - 1], \result;
- assigns __fc_fopen[0 .. 16 - 1] \from __fc_fopen[0 .. 16 - 1];
- assigns \result \from (indirect: __fc_fopen[0 .. 16 - 1]);
-
- behavior flush_stream:
- assumes single_stream: stream ≢ \null;
- assigns *stream, \result;
- assigns *stream \from *stream;
- assigns \result \from (indirect: *stream);
-
- complete behaviors flush_stream, flush_all;
- disjoint behaviors flush_stream, flush_all;
+ \from (indirect: *timer), (indirect: __fc_time), __fc_p_ctime;
*/
-extern int fflush(FILE *stream);
+extern char *ctime(time_t const *timer);
-/*@ requires valid_filename: valid_read_string(filename);
- requires valid_mode: valid_read_string(mode);
+struct tm __fc_time_tm;
+struct tm * const __fc_p_time_tm = & __fc_time_tm;
+/*@ requires valid_timer: \valid_read(timer);
ensures
- result_null_or_valid_fd:
- \result ≡ \null ∨ \subset(\result, &__fc_fopen[0 .. 16 - 1]);
- assigns \result;
- assigns \result
- \from (indirect: *(filename + (0 .. strlen{Old}(filename)))),
- (indirect: *(mode + (0 .. strlen{Old}(mode)))), __fc_p_fopen;
+ result_null_or_internal_tm:
+ \result ≡ &__fc_time_tm ∨ \result ≡ \null;
+ assigns \result, __fc_time_tm;
+ assigns \result \from __fc_p_time_tm;
+ assigns __fc_time_tm \from *timer;
*/
-extern FILE *fopen(char const * restrict filename, char const * restrict mode);
+extern struct tm *gmtime(time_t const *timer);
-/*@ requires valid_mode: valid_read_string(mode);
+/*@ requires valid_timer: \valid_read(timer);
ensures
- result_null_or_valid_fd:
- \result ≡ \null ∨ \subset(\result, &__fc_fopen[0 .. 16 - 1]);
- assigns \result, __fc_fopen[fd];
- assigns \result
- \from (indirect: fd), (indirect: *(mode + (0 .. strlen{Old}(mode)))),
- (indirect: __fc_fopen[fd]), __fc_p_fopen;
- assigns __fc_fopen[fd]
- \from (indirect: fd), (indirect: *(mode + (0 .. strlen{Old}(mode)))),
- (indirect: __fc_fopen[fd]), __fc_p_fopen;
+ result_null_or_internal_tm:
+ \result ≡ &__fc_time_tm ∨ \result ≡ \null;
+ assigns \result, __fc_time_tm;
+ assigns \result \from __fc_p_time_tm;
+ assigns __fc_time_tm \from *timer;
*/
-extern FILE *fdopen(int fd, char const *mode);
+extern struct tm *localtime(time_t const *timer);
-/*@ requires valid_filename: valid_read_string(filename);
- requires valid_mode: valid_read_string(mode);
- requires valid_stream: \valid(stream);
- ensures
- result_null_or_valid_fd:
- \result ≡ \null ∨ \result ∈ &__fc_fopen[0 .. 16 - 1];
- ensures stream_opened: *\old(stream) ∈ __fc_fopen[0 .. 16 - 1];
- assigns \result, *stream;
+/*@ requires dst_has_room: \valid(s + (0 .. max - 1));
+ requires valid_format: valid_read_string(format);
+ requires valid_tm: \valid_read(tm);
+ ensures result_bounded: \result ≤ \old(max);
+ assigns *(s + (0 .. max - 1)), \result;
+ assigns *(s + (0 .. max - 1))
+ \from (indirect: max), (indirect: *(format + (0 ..))), (indirect: *tm);
assigns \result
- \from (indirect: *(filename + (..))), (indirect: *(mode + (..))),
- __fc_p_fopen, (indirect: stream);
- assigns *stream
- \from (indirect: *(filename + (..))), (indirect: *(mode + (..))),
- __fc_p_fopen, (indirect: stream);
+ \from (indirect: max), (indirect: *(format + (0 ..))), (indirect: *tm);
*/
-extern FILE *freopen(char const * restrict filename,
- char const * restrict mode, FILE * restrict stream);
-
-/*@ assigns *stream;
- assigns *stream \from buf; */
-extern void setbuf(FILE * restrict stream, char * restrict buf);
+extern size_t strftime(char * restrict s, size_t max,
+ char const * restrict format,
+ struct tm const * restrict tm);
-/*@ assigns *stream;
- assigns *stream \from buf, mode, size; */
-extern int setvbuf(FILE * restrict stream, char * restrict buf, int mode,
- size_t size);
+/*@ requires tp: \valid(tp);
+ assigns \result, *tp, __fc_time;
+ assigns \result \from __fc_time;
+ assigns *tp \from __fc_time;
+ assigns __fc_time \from __fc_time;
+
+ behavior realtime_clock:
+ assumes realtime: clk_id ≡ 666;
+ ensures success: \result ≡ 0;
+ ensures initialization: \initialized(\old(tp));
+
+ behavior monotonic_clock:
+ assumes monotonic: clk_id ≡ 1;
+ ensures success: \result ≡ 0;
+ ensures initialization: \initialized(\old(tp));
+
+ behavior bad_clock_id:
+ assumes bad_id: clk_id ≢ 666 ∧ clk_id ≢ 1;
+ ensures error: \result ≡ 22;
+ assigns \result;
+ assigns \result \from clk_id;
+
+ complete behaviors bad_clock_id, monotonic_clock, realtime_clock;
+ disjoint behaviors bad_clock_id, monotonic_clock, realtime_clock;
+ */
+extern int clock_gettime(clockid_t clk_id, struct timespec *tp);
-/*@ axiomatic format_length {
- logic ℤ format_length{L}(char *format) ;
-
- }
+/*@
+axiomatic nanosleep_predicates {
+ predicate abs_clock_in_range{L}(clockid_t id, struct timespec *tm)
+ reads __fc_time;
+
+ predicate valid_clock_id{L}(clockid_t id)
+ reads __fc_time;
+
+ }
*/
-/*@ assigns *stream;
- assigns *stream \from *(format + (..)), arg; */
-extern int vfprintf(FILE * restrict stream, char const * restrict format,
- va_list arg);
-
-/*@ assigns *stream;
- assigns *stream \from *(format + (..)), *stream; */
-extern int vfscanf(FILE * restrict stream, char const * restrict format,
- va_list arg);
-
-/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from arg; */
-extern int vprintf(char const * restrict format, va_list arg);
-
-/*@ assigns *__fc_stdin;
- assigns *__fc_stdin \from *(format + (..)); */
-extern int vscanf(char const * restrict format, va_list arg);
-
-/*@ assigns *(s + (0 .. n - 1));
- assigns *(s + (0 .. n - 1)) \from *(format + (..)), arg;
- */
-extern int vsnprintf(char * restrict s, size_t n,
- char const * restrict format, va_list arg);
-
-/*@ assigns *(s + (0 ..));
- assigns *(s + (0 ..)) \from *(format + (..)), arg;
+/*@ ghost int volatile __fc_interrupted; */
+/*@ requires valid_request: \valid_read(rqtp);
+ requires
+ initialization: initialized_request:
+ \initialized(&rqtp->tv_sec) ∧ \initialized(&rqtp->tv_nsec);
+ requires valid_nanosecs: 0 ≤ rqtp->tv_nsec < 1000000000;
+ requires valid_remaining_or_null: rmtp ≡ \null ∨ \valid(rmtp);
+ assigns \result;
+ assigns \result
+ \from (indirect: __fc_time), (indirect: __fc_interrupted),
+ (indirect: clock_id), (indirect: flags), (indirect: rqtp),
+ (indirect: *rqtp);
+
+ behavior absolute:
+ assumes absolute_time: (flags & 1) ≢ 0;
+ assumes
+ no_einval:
+ abs_clock_in_range(clock_id, rqtp) ∧ valid_clock_id(clock_id);
+ ensures
+ result_ok_or_error:
+ \result ≡ 0 ∨ \result ≡ 4 ∨ \result ≡ 22 ∨
+ \result ≡ 95;
+ assigns \result;
+ assigns \result
+ \from (indirect: __fc_time), (indirect: __fc_interrupted),
+ (indirect: clock_id), (indirect: rqtp), (indirect: *rqtp);
+
+ behavior relative_interrupted:
+ assumes relative_time: (flags & 1) ≡ 0;
+ assumes interrupted: __fc_interrupted ≢ 0;
+ assumes no_einval: valid_clock_id(clock_id);
+ ensures result_interrupted: \result ≡ 4;
+ ensures
+ initialization: interrupted_remaining:
+ \old(rmtp) ≢ \null ⇒
+ \initialized(&\old(rmtp)->tv_sec) ∧
+ \initialized(&\old(rmtp)->tv_nsec);
+ ensures
+ interrupted_remaining_decreases:
+ \old(rmtp) ≢ \null ⇒
+ \old(rqtp)->tv_sec * 1000000000 + \old(rqtp)->tv_nsec ≥
+ \old(rmtp)->tv_sec * 1000000000 + \old(rmtp)->tv_nsec;
+ ensures
+ remaining_valid:
+ \old(rmtp) ≢ \null ⇒ 0 ≤ \old(rmtp)->tv_nsec < 1000000000;
+ assigns \result, *rmtp;
+ assigns \result
+ \from (indirect: __fc_time), (indirect: clock_id), (indirect: rqtp),
+ (indirect: *rqtp);
+ assigns *rmtp
+ \from __fc_time, (indirect: clock_id), (indirect: rqtp),
+ (indirect: *rqtp), (indirect: rmtp);
+
+ behavior relative_no_error:
+ assumes relative_time: (flags & 1) ≡ 0;
+ assumes not_interrupted: __fc_interrupted ≡ 0;
+ assumes no_einval: valid_clock_id(clock_id);
+ ensures result_ok: \result ≡ 0;
+ assigns \result;
+ assigns \result
+ \from (indirect: __fc_time), (indirect: clock_id), (indirect: rqtp),
+ (indirect: *rqtp);
+
+ behavior relative_invalid_clock_id:
+ assumes relative_time: (flags & 1) ≡ 0;
+ assumes not_interrupted: __fc_interrupted ≡ 0;
+ assumes einval: ¬valid_clock_id(clock_id);
+ ensures result_einval: \result ≡ 22;
+ assigns \result;
+ assigns \result
+ \from (indirect: __fc_time), (indirect: clock_id), (indirect: rqtp),
+ (indirect: *rqtp);
+
+ complete behaviors relative_invalid_clock_id,
+ relative_no_error,
+ relative_interrupted,
+ absolute;
+ disjoint behaviors relative_invalid_clock_id,
+ relative_no_error,
+ relative_interrupted,
+ absolute;
*/
-extern int vsprintf(char * restrict s, char const * restrict format,
- va_list arg);
+extern int clock_nanosleep(clockid_t clock_id, int flags,
+ struct timespec const *rqtp, struct timespec *rmtp);
-/*@ requires valid_stream: \valid(stream);
- ensures result_uchar_or_eof: (0 ≤ \result ≤ 255) ∨ \result ≡ -1;
- assigns *stream, \result;
- assigns *stream \from *stream;
- assigns \result \from (indirect: *stream);
+/*@ requires valid_timer: \valid_read(timer);
+ requires valid_result: \valid(result);
+ ensures
+ result_null_or_result: \result ≡ \old(result) ∨ \result ≡ \null;
+ assigns \result, *result;
+ assigns \result \from (indirect: *timer), result;
+ assigns *result \from (indirect: *timer);
*/
-extern int fgetc(FILE *stream);
+extern struct tm *gmtime_r(time_t const * restrict timer,
+ struct tm * restrict result);
-/*@ requires valid_stream: \valid(stream);
- requires room_s: \valid(s + (0 .. size - 1));
- ensures result_null_or_same: \result ≡ \null ∨ \result ≡ \old(s);
+/*@ requires valid_request: \valid_read(rqtp);
+ requires
+ initialization: initialized_request:
+ \initialized(&rqtp->tv_sec) ∧ \initialized(&rqtp->tv_nsec);
+ requires valid_nanosecs: 0 ≤ rqtp->tv_nsec < 1000000000;
+ requires valid_remaining_or_null: rmtp ≡ \null ∨ \valid(rmtp);
+ ensures result_elapsed_or_interrupted: \result ≡ 0 ∨ \result ≡ -1;
ensures
- initialization: at_least_one:
- \result ≢ \null ⇒ \initialized(\old(s) + 0);
+ initialization: interrupted_remaining:
+ \old(rmtp) ≢ \null ∧ \result ≡ -1 ⇒
+ \initialized(&\old(rmtp)->tv_sec) ∧
+ \initialized(&\old(rmtp)->tv_nsec);
ensures
- terminated_string_on_success:
- \result ≢ \null ⇒ valid_string(\old(s));
- assigns *(s + (0 .. size - 1)), \result;
- assigns *(s + (0 .. size - 1))
- \from (indirect: size), (indirect: *stream);
- assigns \result \from s, (indirect: size), (indirect: *stream);
+ interrupted_remaining_decreases:
+ \old(rmtp) ≢ \null ∧ \result ≡ -1 ⇒
+ \old(rqtp)->tv_sec * 1000000000 + \old(rqtp)->tv_nsec ≥
+ \old(rmtp)->tv_sec * 1000000000 + \old(rmtp)->tv_nsec;
+ ensures
+ interrupted_remaining_valid:
+ \old(rmtp) ≢ \null ∧ \result ≡ -1 ⇒
+ 0 ≤ \old(rmtp)->tv_nsec < 1000000000;
+ assigns \result, *rmtp;
+ assigns \result
+ \from (indirect: __fc_time), (indirect: rqtp), (indirect: *rqtp);
+ assigns *rmtp
+ \from (indirect: __fc_time), (indirect: rqtp), (indirect: *rqtp),
+ (indirect: rmtp);
*/
-extern char *fgets(char * restrict s, int size, FILE * restrict stream);
+extern int nanosleep(struct timespec const *rqtp, struct timespec *rmtp);
-/*@ requires valid_stream: \valid(stream);
- assigns *stream, \result;
- assigns *stream \from c, *stream;
- assigns \result \from (indirect: *stream);
+extern char *tzname[2];
+
+/*@ assigns *(tzname[0 .. 1] + (0 ..));
+ assigns *(tzname[0 .. 1] + (0 ..)) \from \nothing;
*/
-extern int fputc(int c, FILE *stream);
+extern void tzset(void);
-/*@ requires valid_string_s: valid_read_string(s);
- assigns *stream, \result;
- assigns *stream \from *(s + (0 .. strlen{Old}(s))), *stream;
+/*@ requires
+ valid:
+ valid_read_or_empty((void *)s, (unsigned int)(sizeof(wchar_t) * n)) ∨
+ \valid_read((unsigned char *)s + (0 .. wmemchr_off(s, c, n)));
+ requires
+ initialization:
+ \initialized(s + (0 .. n - 1)) ∨
+ \initialized(s + (0 .. wmemchr_off(s, c, n)));
+ requires
+ danglingness:
+ non_escaping((void *)s, (unsigned int)(sizeof(wchar_t) * n)) ∨
+ non_escaping((void *)s,
+ (unsigned int)(sizeof(wchar_t) *
+ (wmemchr_off(s, c, n) + 1)));
+ ensures
+ result_null_or_inside_s:
+ \result ≡ \null ∨ \subset(\result, \old(s) + (0 .. \old(n) - 1));
+ assigns \result;
assigns \result
- \from (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: *stream);
+ \from s, (indirect: *(s + (0 .. n - 1))), (indirect: c), (indirect: n);
*/
-extern int fputs(char const * restrict s, FILE * restrict stream);
+extern wchar_t *wmemchr(wchar_t const *s, wchar_t c, size_t n);
-/*@ requires valid_stream: \valid(stream);
- assigns \result, *stream;
- assigns \result \from *stream;
- assigns *stream \from *stream;
+/*@ requires
+ valid_s1:
+ valid_read_or_empty((void *)s1, (unsigned int)(sizeof(wchar_t) * n));
+ requires
+ valid_s2:
+ valid_read_or_empty((void *)s2, (unsigned int)(sizeof(wchar_t) * n));
+ requires initialization: s1: \initialized(s1 + (0 .. n - 1));
+ requires initialization: s2: \initialized(s2 + (0 .. n - 1));
+ requires
+ danglingness: s1:
+ non_escaping((void *)s1, (unsigned int)(sizeof(wchar_t) * n));
+ requires
+ danglingness: s2:
+ non_escaping((void *)s2, (unsigned int)(sizeof(wchar_t) * n));
+ assigns \result;
+ assigns \result
+ \from (indirect: *(s1 + (0 .. n - 1))),
+ (indirect: *(s2 + (0 .. n - 1))), (indirect: n);
*/
-extern int getc(FILE *stream);
+extern int wmemcmp(wchar_t const *s1, wchar_t const *s2, size_t n);
-/*@ assigns \result, *__fc_stdin;
- assigns \result \from *__fc_stdin;
- assigns *__fc_stdin \from *__fc_stdin;
+wchar_t *wmemcpy(wchar_t *dest, wchar_t const *src, size_t n);
+
+/*@ requires valid_src: \valid_read(src + (0 .. n - 1));
+ requires valid_dest: \valid(dest + (0 .. n - 1));
+ ensures result_ptr: \result ≡ \old(dest);
+ assigns *(dest + (0 .. n - 1)), \result;
+ assigns *(dest + (0 .. n - 1))
+ \from *(src + (0 .. n - 1)), (indirect: src), (indirect: n);
+ assigns \result \from dest;
*/
-extern int getchar(void);
+extern wchar_t *wmemmove(wchar_t *dest, wchar_t const *src, size_t n);
-/*@ axiomatic GetsLength {
- logic size_t gets_length{L}
- reads *__fc_stdin;
-
- }
+wchar_t *wmemset(wchar_t *dest, wchar_t val, size_t len);
-*/
-/*@ requires room_s: \valid(s + (0 .. gets_length));
- ensures result_null_or_same: \result ≡ \old(s) ∨ \result ≡ \null;
- assigns *(s + (0 .. gets_length{Old})), \result, *__fc_stdin;
- assigns *(s + (0 .. gets_length{Old})) \from *__fc_stdin;
- assigns \result \from s, *__fc_stdin;
- assigns *__fc_stdin \from *__fc_stdin;
- */
-extern char *gets(char *s);
+wchar_t *wcscat(wchar_t *dest, wchar_t const *src);
-/*@ requires valid_stream: \valid(stream);
- assigns *stream, \result;
- assigns *stream \from c, *stream;
- assigns \result \from (indirect: *stream);
+/*@ requires valid_wstring_src: valid_read_wstring(wcs);
+ ensures
+ result_null_or_inside_wcs:
+ \result ≡ \null ∨ \subset(\result, \old(wcs) + (0 ..));
+ assigns \result;
+ assigns \result \from wcs, (indirect: *(wcs + (0 ..))), (indirect: wc);
*/
-extern int putc(int c, FILE *stream);
+extern wchar_t *wcschr(wchar_t const *wcs, wchar_t wc);
-/*@ assigns *__fc_stdout, \result;
- assigns *__fc_stdout \from c, *__fc_stdout;
- assigns \result \from (indirect: *__fc_stdout);
- */
-extern int putchar(int c);
-
-/*@ requires valid_string_s: valid_read_string(s);
- assigns *__fc_stdout, \result;
- assigns *__fc_stdout \from *(s + (0 .. strlen{Old}(s))), *__fc_stdout;
+/*@ requires valid_wstring_s1: valid_read_wstring(s1);
+ requires valid_wstring_s2: valid_read_wstring(s2);
+ assigns \result;
assigns \result
- \from (indirect: *(s + (0 .. strlen{Old}(s)))),
- (indirect: *__fc_stdout);
+ \from (indirect: *(s1 + (0 ..))), (indirect: *(s2 + (0 ..)));
*/
-extern int puts(char const *s);
+extern int wcscmp(wchar_t const *s1, wchar_t const *s2);
-/*@ requires valid_stream: \valid(stream);
- ensures result_ok_or_error: \result ≡ \old(c) ∨ \result ≡ -1;
- assigns *stream, \result;
- assigns *stream \from (indirect: c);
- assigns \result \from (indirect: c), (indirect: *stream);
+wchar_t *wcscpy(wchar_t *dest, wchar_t const *src);
+
+/*@ requires valid_wstring_wcs: valid_read_wstring(wcs);
+ requires valid_wstring_accept: valid_read_wstring(accept);
+ assigns \result;
+ assigns \result
+ \from (indirect: *(wcs + (0 ..))), (indirect: *(accept + (0 ..)));
*/
-extern int ungetc(int c, FILE *stream);
+extern size_t wcscspn(wchar_t const *wcs, wchar_t const *accept);
-/*@ requires valid_ptr_block: \valid((char *)ptr + (0 .. nmemb * size - 1));
- requires valid_stream: \valid(stream);
- ensures size_read: \result ≤ \old(nmemb);
- ensures
- initialization:
- \initialized((char *)\old(ptr) + (0 .. \result * \old(size) - 1));
- assigns *((char *)ptr + (0 .. nmemb * size - 1)), *stream, \result;
- assigns *((char *)ptr + (0 .. nmemb * size - 1))
- \from (indirect: size), (indirect: nmemb), (indirect: *stream);
- assigns *stream
- \from (indirect: size), (indirect: nmemb), (indirect: *stream);
- assigns \result \from size, (indirect: *stream);
+/*@ requires valid_nwstring_src: valid_read_nwstring(src, n);
+ requires valid_wstring_dest: valid_wstring(dest);
+ requires
+ room_for_concatenation:
+ \valid(dest + (wcslen(dest) .. wcslen(dest) + \min(wcslen(src), n)));
+ requires
+ separation:
+ \separated(
+ dest + (0 .. wcslen(dest) + wcslen(src)), src + (0 .. wcslen(src))
+ );
+ assigns *(dest + (0 ..)), \result;
+ assigns *(dest + (0 ..))
+ \from *(dest + (0 ..)), (indirect: dest), *(src + (0 .. n - 1)),
+ (indirect: src), (indirect: n);
+ assigns \result
+ \from (indirect: *(dest + (0 ..))), (indirect: *(src + (0 .. n - 1))),
+ (indirect: n);
*/
-extern size_t fread(void * restrict ptr, size_t size, size_t nmemb,
- FILE * restrict stream);
+extern size_t wcslcat(wchar_t * restrict dest, wchar_t const * restrict src,
+ size_t n);
-/*@ requires
- valid_ptr_block: \valid_read((char *)ptr + (0 .. nmemb * size - 1));
- requires valid_stream: \valid(stream);
- ensures size_written: \result ≤ \old(nmemb);
- assigns *stream, \result;
- assigns *stream
- \from (indirect: *((char *)ptr + (0 .. nmemb * size - 1)));
+/*@ requires valid_wstring_src: valid_read_wstring(src);
+ requires room_nwstring: \valid(dest + (0 .. n));
+ requires
+ separation: dest: src:
+ \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
+ assigns *(dest + (0 .. n - 1)), \result;
+ assigns *(dest + (0 .. n - 1))
+ \from *(src + (0 .. n - 1)), (indirect: src), (indirect: n);
assigns \result
- \from (indirect: *((char *)ptr + (0 .. nmemb * size - 1)));
+ \from (indirect: *(dest + (0 .. n - 1))), (indirect: dest),
+ (indirect: *(src + (0 .. n - 1))), (indirect: src), (indirect: n);
*/
-extern size_t fwrite(void const * restrict ptr, size_t size, size_t nmemb,
- FILE * restrict stream);
+extern size_t wcslcpy(wchar_t *dest, wchar_t const *src, size_t n);
-/*@ requires valid_stream: \valid(stream);
- requires valid_pos: \valid(pos);
- ensures initialization: pos: \initialized(\old(pos));
- assigns \result, *pos;
- assigns \result \from (indirect: *stream);
- assigns *pos \from (indirect: *stream);
+size_t wcslen(wchar_t const *str);
+
+wchar_t *wcsncat(wchar_t *dest, wchar_t const *src, size_t n);
+
+/*@ requires valid_wstring_s1: valid_read_wstring(s1);
+ requires valid_wstring_s2: valid_read_wstring(s2);
+ assigns \result;
+ assigns \result
+ \from (indirect: *(s1 + (0 .. n - 1))),
+ (indirect: *(s2 + (0 .. n - 1))), (indirect: n);
*/
-extern int fgetpos(FILE * restrict stream, fpos_t * restrict pos);
+extern int wcsncmp(wchar_t const *s1, wchar_t const *s2, size_t n);
-/*@ requires valid_stream: \valid(stream);
- requires whence_enum: whence ≡ 0 ∨ whence ≡ 1 ∨ whence ≡ 2;
+wchar_t *wcsncpy(wchar_t *dest, wchar_t const *src, size_t n);
+
+/*@ requires valid_wstring_wcs: valid_read_wstring(wcs);
+ requires valid_wstring_accept: valid_read_wstring(accept);
ensures
- errno_set: __fc_errno ∈ {11, 9, 27, 4, 22, 5, 28, 75, 32, 29, 6};
- assigns *stream, \result, __fc_errno;
- assigns *stream \from *stream, (indirect: offset), (indirect: whence);
+ result_null_or_inside_wcs:
+ \result ≡ \null ∨ \subset(\result, \old(wcs) + (0 ..));
+ assigns \result;
assigns \result
- \from (indirect: *stream), (indirect: offset), (indirect: whence);
- assigns __fc_errno
- \from (indirect: *stream), (indirect: offset), (indirect: whence);
+ \from wcs, (indirect: *(wcs + (0 ..))), (indirect: *(accept + (0 ..)));
*/
-extern int fseek(FILE *stream, long offset, int whence);
+extern wchar_t *wcspbrk(wchar_t const *wcs, wchar_t const *accept);
-/*@ requires valid_stream: \valid(stream);
- requires whence_enum: whence ≡ 0 ∨ whence ≡ 1 ∨ whence ≡ 2;
+/*@ requires valid_wstring_wcs: valid_read_wstring(wcs);
ensures
- errno_set: __fc_errno ∈ {11, 9, 27, 4, 22, 5, 28, 75, 32, 29, 6};
- assigns *stream, \result, __fc_errno;
- assigns *stream \from *stream, (indirect: offset), (indirect: whence);
+ result_null_or_inside_wcs:
+ \result ≡ \null ∨ \subset(\result, \old(wcs) + (0 ..));
+ assigns \result;
assigns \result
- \from (indirect: *stream), (indirect: offset), (indirect: whence);
- assigns __fc_errno
- \from (indirect: *stream), (indirect: offset), (indirect: whence);
+ \from wcs, (indirect: *(wcs + (0 .. wcslen{Old}(wcs)))), (indirect: wc);
*/
-extern int fseeko(FILE *stream, off_t offset, int whence);
+extern wchar_t *wcsrchr(wchar_t const *wcs, wchar_t wc);
-/*@ requires valid_stream: \valid(stream);
- requires valid_pos: \valid_read(pos);
- requires initialization: pos: \initialized(pos);
- ensures errno_set: __fc_errno ∈ {11, 9, 27, 4, 5, 28, 32, 29, 6};
- assigns *stream, \result, __fc_errno;
- assigns *stream \from *pos;
- assigns \result \from (indirect: *stream), (indirect: *pos);
- assigns __fc_errno
- \from __fc_errno, (indirect: *stream), (indirect: *pos);
+/*@ requires valid_wstring_wcs: valid_read_wstring(wcs);
+ requires valid_wstring_accept: valid_read_wstring(accept);
+ assigns \result;
+ assigns \result
+ \from (indirect: *(wcs + (0 .. wcslen{Old}(wcs)))),
+ (indirect: *(accept + (0 .. wcslen{Old}(accept))));
*/
-extern int fsetpos(FILE *stream, fpos_t const *pos);
+extern size_t wcsspn(wchar_t const *wcs, wchar_t const *accept);
-/*@ requires valid_stream: \valid(stream);
+/*@ requires valid_wstring_haystack: valid_read_wstring(haystack);
+ requires valid_wstring_needle: valid_read_wstring(needle);
ensures
- success_or_error:
- \result ≡ -1 ∨
- (\result ≥ 0 ∧ __fc_errno ≡ \old(__fc_errno));
- ensures errno_set: __fc_errno ∈ {9, 75, 29};
- assigns \result, __fc_errno;
- assigns \result \from (indirect: *stream);
- assigns __fc_errno \from (indirect: *stream);
+ result_null_or_inside_haystack:
+ \result ≡ \null ∨ \subset(\result, \old(haystack) + (0 ..));
+ assigns \result;
+ assigns \result
+ \from haystack, (indirect: *(haystack + (0 ..))),
+ (indirect: *(needle + (0 ..)));
*/
-extern long ftell(FILE *stream);
+extern wchar_t *wcsstr(wchar_t const *haystack, wchar_t const *needle);
-/*@ requires valid_stream: \valid(stream);
+/*@ requires room_nwstring: \valid(ws + (0 .. n - 1));
+ requires valid_stream: \valid(stream);
+ ensures result_null_or_same: \result ≡ \null ∨ \result ≡ \old(ws);
ensures
- success_or_error:
- \result ≡ -1 ∨
- (\result ≥ 0 ∧ __fc_errno ≡ \old(__fc_errno));
- ensures errno_set: __fc_errno ∈ {9, 75, 29};
- assigns \result, __fc_errno;
- assigns \result \from (indirect: *stream);
- assigns __fc_errno \from (indirect: *stream);
- */
-extern off_t ftello(FILE *stream);
-
-/*@ requires valid_stream: \valid(stream);
- assigns *stream;
- assigns *stream \from \nothing;
+ terminated_string_on_success:
+ \result ≢ \null ⇒ valid_wstring(\old(ws));
+ assigns *(ws + (0 .. n - 1)), \result;
+ assigns *(ws + (0 .. n - 1)) \from (indirect: n), (indirect: *stream);
+ assigns \result \from ws, (indirect: n), (indirect: *stream);
*/
-extern void rewind(FILE *stream);
+extern wchar_t *fgetws(wchar_t * restrict ws, int n, FILE * restrict stream);
-/*@ requires valid_stream: \valid(stream);
- assigns *stream;
- assigns *stream \from \nothing;
- */
-extern void clearerr(FILE *stream);
+/*@ axiomatic wformat_length {
+ logic ℤ wformat_length{L}(wchar_t *format) ;
+
+ }
-/*@ requires valid_stream: \valid(stream);
+*/
+/*@ requires valid_wstring_ws1: valid_read_wstring(ws1);
+ requires valid_wstring_ws2: valid_read_wstring(ws2);
assigns \result;
- assigns \result \from (indirect: *stream);
+ assigns \result
+ \from (indirect: *(ws1 + (0 ..))), (indirect: *(ws2 + (0 ..)));
*/
-extern int feof(FILE *stream);
+extern int wcscasecmp(wchar_t const *ws1, wchar_t const *ws2);
-/*@ requires valid_stream: \valid(stream);
- assigns \result;
- assigns \result \from (indirect: *stream);
- */
-extern int fileno(FILE *stream);
+void atomic_thread_fence(memory_order order);
-/*@ requires valid_stream: \valid(stream);
- assigns *stream;
- assigns *stream \from \nothing;
- */
-extern void flockfile(FILE *stream);
+void atomic_signal_fence(memory_order order);
-/*@ requires valid_stream: \valid(stream);
- assigns *stream;
- assigns *stream \from \nothing;
- */
-extern void funlockfile(FILE *stream);
+_Bool __fc_atomic_is_lock_free(void *obj);
-/*@ requires valid_stream: \valid(stream);
- assigns \result, *stream;
- assigns \result \from \nothing;
- assigns *stream \from \nothing;
- */
-extern int ftrylockfile(FILE *stream);
+void __fc_atomic_store_marker(void *object, unsigned long long desired);
-/*@ requires valid_stream: \valid(stream);
- assigns \result;
- assigns \result \from (indirect: *stream);
- */
-extern int ferror(FILE *stream);
+void __fc_atomic_store_explicit_marker(void *object,
+ unsigned long long desired,
+ memory_order order);
-/*@ requires valid_string_s: valid_read_string(s);
- assigns __fc_stdout;
- assigns __fc_stdout \from __fc_errno, *(s + (0 .. strlen{Old}(s)));
- */
-extern void perror(char const *s);
+unsigned long long __fc_atomic_load(void *obj, size_t obj_size);
-/*@ requires valid_stream: \valid(stream);
- assigns \result, *stream;
- assigns \result \from *stream;
- assigns *stream \from *stream;
- */
-extern int getc_unlocked(FILE *stream);
+unsigned long long __fc_atomic_load_explicit(void *object,
+ memory_order order,
+ size_t obj_size);
-/*@ assigns \result;
- assigns \result \from *__fc_stdin; */
-extern int getchar_unlocked(void);
+unsigned long long __fc_atomic_exchange(void *obj,
+ unsigned long long desired,
+ size_t obj_size);
-/*@ requires valid_stream: \valid(stream);
- assigns *stream, \result;
- assigns *stream \from c;
- assigns \result \from (indirect: *stream);
- */
-extern int putc_unlocked(int c, FILE *stream);
+unsigned long long __fc_atomic_exchange_explicit(void *object,
+ unsigned long long desired,
+ memory_order order,
+ size_t obj_size);
-/*@ assigns *__fc_stdout, \result;
- assigns *__fc_stdout \from c;
- assigns \result \from (indirect: *__fc_stdout);
- */
-extern int putchar_unlocked(int c);
+_Bool __fc_atomic_compare_exchange_strong(void *object, void *expected,
+ unsigned long long desired,
+ size_t obj_size);
-/*@ requires valid_stream: \valid(stream);
- assigns *stream;
- assigns *stream \from \nothing;
- */
-extern void clearerr_unlocked(FILE *stream);
+_Bool __fc_atomic_compare_exchange_strong_explicit(void *object,
+ void *expected,
+ unsigned long long desired,
+ memory_order success,
+ memory_order failure,
+ size_t obj_size);
-/*@ requires valid_stream: \valid(stream);
- assigns \result;
- assigns \result \from (indirect: *stream);
- */
-extern int feof_unlocked(FILE *stream);
+_Bool __fc_atomic_compare_exchange_weak(void *object, void *expected,
+ unsigned long long desired,
+ size_t obj_size);
-/*@ requires valid_stream: \valid(stream);
- assigns \result;
- assigns \result \from (indirect: *stream);
- */
-extern int ferror_unlocked(FILE *stream);
+_Bool __fc_atomic_compare_exchange_weak_explicit(void *object,
+ void *expected,
+ unsigned long long desired,
+ memory_order success,
+ memory_order failure,
+ size_t obj_size);
-/*@ requires valid_stream: \valid(stream);
- assigns \result;
- assigns \result \from (indirect: *stream);
- */
-extern int fileno_unlocked(FILE *stream);
+unsigned long long __fc_atomic_fetch_add(void *obj,
+ unsigned long long operand,
+ size_t obj_size);
-/*@ axiomatic pipe_streams {
- predicate is_open_pipe{L}(FILE *stream) ;
-
- }
+unsigned long long __fc_atomic_fetch_add_explicit(void *obj,
+ unsigned long long operand,
+ memory_order order,
+ size_t obj_size);
-*/
-/*@ requires valid_command: valid_read_string(command);
- requires valid_type: valid_read_string(type);
- ensures
- result_error_or_valid_open_pipe:
- \result ≡ \null ∨
- (\subset(\result, &__fc_fopen[0 .. 16 - 1]) ∧ is_open_pipe(\result));
- assigns \result, __fc_fopen[0 ..];
- assigns \result
- \from (indirect: *command), (indirect: *type), __fc_p_fopen;
- assigns __fc_fopen[0 ..]
- \from (indirect: *command), (indirect: *type), __fc_fopen[0 ..];
- */
-extern FILE *popen(char const *command, char const *type);
+unsigned long long __fc_atomic_fetch_sub(void *obj,
+ unsigned long long operand,
+ size_t obj_size);
-/*@ requires valid_stream: \valid(stream);
- requires open_pipe: is_open_pipe(stream);
- ensures closed_stream: ¬is_open_pipe(\old(stream));
- assigns \result;
- assigns \result \from (indirect: *stream);
- */
-extern int pclose(FILE *stream);
+unsigned long long __fc_atomic_fetch_sub_explicit(void *obj,
+ unsigned long long operand,
+ memory_order order,
+ size_t obj_size);
-ssize_t getline(char **lineptr, size_t *n, FILE *stream);
+unsigned long long __fc_atomic_fetch_or(void *obj,
+ unsigned long long operand,
+ size_t obj_size);
-int asprintf(char **strp, char const *fmt, void * const *__va_params);
+unsigned long long __fc_atomic_fetch_or_explicit(void *obj,
+ unsigned long long operand,
+ memory_order order,
+ size_t obj_size);
-/*@ assigns \result;
- assigns \result \from maj, min; */
-extern dev_t makedev(int maj, int min);
+unsigned long long __fc_atomic_fetch_xor(void *obj,
+ unsigned long long operand,
+ size_t obj_size);
-FILE __fc_initial_stdout =
- {.__fc_FILE_id = (unsigned int)1, .__fc_FILE_data = 0U};
-FILE *__fc_stdout = & __fc_initial_stdout;
-FILE __fc_initial_stderr =
- {.__fc_FILE_id = (unsigned int)2, .__fc_FILE_data = 0U};
-FILE *__fc_stderr = & __fc_initial_stderr;
-FILE __fc_initial_stdin =
- {.__fc_FILE_id = (unsigned int)0, .__fc_FILE_data = 0U};
-FILE *__fc_stdin = & __fc_initial_stdin;
-ssize_t getline(char **lineptr, size_t *n, FILE *stream)
+unsigned long long __fc_atomic_fetch_xor_explicit(void *obj,
+ unsigned long long operand,
+ memory_order order,
+ size_t obj_size);
+
+unsigned long long __fc_atomic_fetch_and(void *obj,
+ unsigned long long operand,
+ size_t obj_size);
+
+unsigned long long __fc_atomic_fetch_and_explicit(void *obj,
+ unsigned long long operand,
+ memory_order order,
+ size_t obj_size);
+
+_Bool atomic_flag_test_and_set(atomic_flag volatile *object);
+
+_Bool atomic_flag_test_and_set_explicit(atomic_flag volatile *object,
+ memory_order order);
+
+void atomic_flag_clear(atomic_flag volatile *object);
+
+void atomic_flag_clear_explicit(atomic_flag volatile *object,
+ memory_order order);
+
+void __fc_atomic_init_marker(void *obj, unsigned long long value)
{
- ssize_t __retres;
+ return;
+}
+
+void atomic_thread_fence(memory_order order)
+{
+ return;
+}
+
+void atomic_signal_fence(memory_order order)
+{
+ return;
+}
+
+_Bool __fc_atomic_is_lock_free(void *obj)
+{
+ _Bool __retres;
int tmp;
- if (! lineptr) goto _LOR;
+ tmp = Frama_C_nondet(0,1);
+ __retres = (_Bool)(tmp != 0);
+ return __retres;
+}
+
+void __fc_atomic_store_marker(void *object, unsigned long long desired)
+{
+ return;
+}
+
+void __fc_atomic_store_explicit_marker(void *object,
+ unsigned long long desired,
+ memory_order order)
+{
+ return;
+}
+
+unsigned long long __fc_atomic_load(void *obj, size_t obj_size)
+{
+ unsigned long long __retres;
+ if (obj_size == sizeof(char)) {
+ __retres = (unsigned long long)*((atomic_uchar volatile *)obj);
+ goto return_label;
+ }
else
- if (! n) goto _LOR;
+ if (obj_size == sizeof(short)) {
+ __retres = (unsigned long long)*((atomic_ushort volatile *)obj);
+ goto return_label;
+ }
else
- if (! stream) {
- _LOR: {
- __fc_errno = 22;
- __retres = -1;
- goto return_label;
- }
+ if (obj_size == sizeof(int)) {
+ __retres = (unsigned long long)*((atomic_uint volatile *)obj);
+ goto return_label;
}
- tmp = ferror(stream);
- if (tmp) goto _LOR_0;
- else {
- int tmp_0;
- tmp_0 = feof(stream);
- if (tmp_0) {
- _LOR_0: {
- __retres = -1;
- goto return_label;
- }
- }
- }
- if (! *lineptr) goto _LOR_1;
- else
- if (*n == (size_t)0) {
- _LOR_1:
- {
- *lineptr = (char *)malloc((unsigned int)2);
- if (! lineptr) {
- __fc_errno = 12;
- __retres = -1;
+ else
+ if (obj_size == sizeof(long)) {
+ __retres = (unsigned long long)*((atomic_ulong volatile *)obj);
goto return_label;
}
- *n = (unsigned int)2;
- }
- }
- size_t cur = (unsigned int)0;
- while (1) {
- int tmp_3;
- tmp_3 = ferror(stream);
- if (tmp_3) break;
- else {
- int tmp_4;
- tmp_4 = feof(stream);
- if (tmp_4) break;
- }
- {
- while (cur < *n - (size_t)1) {
- int tmp_1;
- tmp_1 = fgetc(stream);
- char c = (char)tmp_1;
- if ((int)c == -1)
- if (cur == (size_t)0) {
- __retres = -1;
- goto return_label;
- }
- if ((int)c != -1) {
- size_t tmp_2;
- tmp_2 = cur;
- cur += (size_t)1;
- *(*lineptr + tmp_2) = c;
- }
- if ((int)c == '\n') goto _LOR_2;
else
- if ((int)c == -1) {
- _LOR_2:
- {
- *(*lineptr + cur) = (char)'\000';
- __retres = (int)cur;
- goto return_label;
- }
+ if (obj_size == sizeof(long long)) {
+ __retres = *((atomic_ullong volatile *)obj);
+ goto return_label;
}
- }
- if (*n == (size_t)2147483647) {
- __fc_errno = 75;
- __retres = -1;
- goto return_label;
- }
- size_t new_size = *n + (size_t)1;
- *lineptr = (char *)realloc((void *)*lineptr,new_size);
- if (! *lineptr) {
- __fc_errno = 12;
- __retres = -1;
- goto return_label;
- }
- *n = new_size;
- }
- }
- __retres = -1;
+ else __FC_assert(0 != 0,"share/libc/stdatomic.c",50,"0");
+ __retres = (unsigned long long)0;
return_label: return __retres;
}
-/*@ requires valid_strp: \valid(strp);
- requires valid_fmt: valid_read_string(fmt);
- ensures result_error_or_written_byes: \result ≡ -1 ∨ \result ≥ 0;
- assigns __fc_heap_status, \result, *strp;
- assigns __fc_heap_status
- \from (indirect: *(fmt + (0 ..))), __fc_heap_status;
- assigns \result
- \from (indirect: *(fmt + (0 ..))), (indirect: __fc_heap_status);
- assigns *strp \from *(fmt + (0 ..)), (indirect: __fc_heap_status);
- allocates *\old(strp);
- */
-int asprintf(char **strp, char const *fmt, void * const *__va_params)
+unsigned long long __fc_atomic_load_explicit(void *object,
+ memory_order order,
+ size_t obj_size)
{
- int __retres;
- va_list args;
- int tmp;
- args = __va_params;
- tmp = Frama_C_interval(1,256);
- size_t len = (unsigned int)tmp;
- *strp = (char *)malloc(len);
- if (! *strp) {
- __retres = -1;
- goto return_label;
- }
- Frama_C_make_unknown(*strp,len - 1U);
- *(*strp + (len - 1U)) = (char)0;
- __retres = (int)len;
- return_label: return __retres;
+ unsigned long long tmp;
+ tmp = __fc_atomic_load(object,obj_size);
+ return tmp;
}
-/*@ requires abs_representable: i > -2147483647 - 1;
- assigns \result;
- assigns \result \from i;
-
- behavior negative:
- assumes negative: i < 0;
- ensures opposite_result: \result ≡ -\old(i);
-
- behavior nonnegative:
- assumes nonnegative: i ≥ 0;
- ensures same_result: \result ≡ \old(i);
-
- complete behaviors nonnegative, negative;
- disjoint behaviors nonnegative, negative;
- */
-int abs(int i)
+unsigned long long __fc_atomic_exchange(void *obj,
+ unsigned long long desired,
+ size_t obj_size)
{
- int __retres;
- if (i < 0) {
- __retres = - i;
- goto return_label;
+ unsigned long long r;
+ if (obj_size == sizeof(char)) {
+ r = (unsigned long long)*((atomic_uchar volatile *)obj);
+ *((atomic_uchar volatile *)obj) = (unsigned char)desired;
}
- __retres = i;
- return_label: return __retres;
+ else
+ if (obj_size == sizeof(short)) {
+ r = (unsigned long long)*((atomic_ushort volatile *)obj);
+ *((atomic_ushort volatile *)obj) = (unsigned short)desired;
+ }
+ else
+ if (obj_size == sizeof(int)) {
+ r = (unsigned long long)*((atomic_uint volatile *)obj);
+ *((atomic_uint volatile *)obj) = (unsigned int)desired;
+ }
+ else
+ if (obj_size == sizeof(long)) {
+ r = (unsigned long long)*((atomic_ulong volatile *)obj);
+ *((atomic_ulong volatile *)obj) = (unsigned long)desired;
+ }
+ else
+ if (obj_size == sizeof(long long)) {
+ r = *((atomic_ullong volatile *)obj);
+ *((atomic_ullong volatile *)obj) = desired;
+ }
+ else __FC_assert(0 != 0,"share/libc/stdatomic.c",79,"0");
+ return r;
}
-/*@ requires valid_nptr: \valid_read(p);
- assigns \result;
- assigns \result \from (indirect: p), (indirect: *(p + (0 ..)));
- */
-int atoi(char const *p)
+unsigned long long __fc_atomic_exchange_explicit(void *object,
+ unsigned long long desired,
+ memory_order order,
+ size_t obj_size)
{
- int __retres;
- int n;
- int c;
- int tmp_1;
- int tmp_3;
- int neg = 0;
- unsigned char *up = (unsigned char *)p;
- c = (int)*up;
- tmp_1 = isdigit(c);
- if (! tmp_1) {
- int tmp_0;
- while (1) {
- int tmp;
- tmp = isspace(c);
- if (! tmp) break;
- up ++;
- c = (int)*up;
- }
- switch (c) {
- case '-': neg ++;
- case '+': { /* sequence */
- up ++;
- c = (int)*up;
- }
- }
- tmp_0 = isdigit(c);
- if (! tmp_0) {
- __retres = 0;
- goto return_label;
- }
- }
- n = '0' - c;
- while (1) {
- int tmp_2;
- up ++;
- c = (int)*up;
- tmp_2 = isdigit(c);
- if (! tmp_2) break;
- n *= 10;
- n += '0' - c;
- }
- if (neg) tmp_3 = n; else tmp_3 = - n;
- __retres = tmp_3;
- return_label: return __retres;
+ unsigned long long tmp;
+ tmp = __fc_atomic_exchange(object,desired,obj_size);
+ return tmp;
}
-/*@ assigns __fc_heap_status, \result;
- assigns __fc_heap_status
- \from (indirect: nmemb), (indirect: size), __fc_heap_status;
- assigns \result
- \from (indirect: nmemb), (indirect: size), (indirect: __fc_heap_status);
- allocates \result;
-
- behavior allocation:
- assumes can_allocate: is_allocable(nmemb * size);
- ensures
- allocation: \fresh{Old, Here}(\result,\old(nmemb) * \old(size));
- ensures
- initialization:
- \initialized((char *)\result + (0 .. \old(nmemb) * \old(size) - 1));
- ensures
- zero_initialization:
- \subset(*((char *)\result + (0 .. \old(nmemb) * \old(size) - 1)),
- {0});
-
- behavior no_allocation:
- assumes cannot_allocate: ¬is_allocable(nmemb * size);
- ensures null_result: \result ≡ \null;
- assigns \result;
- assigns \result \from \nothing;
- allocates \nothing;
-
- complete behaviors no_allocation, allocation;
- disjoint behaviors no_allocation, allocation;
- */
-void *calloc(size_t nmemb, size_t size)
+_Bool __fc_atomic_compare_exchange_strong(void *object, void *expected,
+ unsigned long long desired,
+ size_t obj_size)
{
- void *__retres;
- size_t l = nmemb * size;
- if (size != (size_t)0)
- if (l / size != nmemb) {
- __retres = (void *)0;
- goto return_label;
- }
- char *p = malloc(l);
- if (p) memset((void *)p,0,l);
- __retres = (void *)p;
- return_label: return __retres;
+ _Bool __retres;
+ int r = memcmp((void const *)object,(void const *)expected,obj_size);
+ if (r == 0) memcpy(object,(void const *)(& desired),obj_size);
+ else memcpy(expected,(void const *)object,obj_size);
+ __retres = (_Bool)(r == 0);
+ return __retres;
}
-static char __fc_env_strings[64];
-static char __fc_initenv_init;
-static void __fc_initenv(void)
+_Bool __fc_atomic_compare_exchange_strong_explicit(void *object,
+ void *expected,
+ unsigned long long desired,
+ memory_order success,
+ memory_order failure,
+ size_t obj_size)
{
- if (! __fc_initenv_init) {
- Frama_C_make_unknown(__fc_env_strings,(unsigned int)(64 - 1));
- {
- int i = 0;
- while (i < 4096) {
- {
- int tmp;
- tmp = Frama_C_interval(0,64 - 1);
- __fc_env[i] = & __fc_env_strings[tmp];
- }
- i ++;
- }
- }
- __fc_initenv_init = (char)1;
- }
- return;
+ _Bool tmp;
+ tmp = __fc_atomic_compare_exchange_strong(object,expected,desired,obj_size);
+ return tmp;
}
-/*@ requires valid_name: valid_read_string(name);
- ensures null_or_valid_result: \result ≡ \null ∨ \valid(\result);
- assigns \result;
- assigns \result \from __fc_env[0 ..], (indirect: name), *(name + (0 ..));
- */
-char *getenv(char const *name)
+_Bool __fc_atomic_compare_exchange_weak(void *object, void *expected,
+ unsigned long long desired,
+ size_t obj_size)
{
- char *__retres;
- int tmp_0;
- /*@ assert ¬(strchr(name, '=') ≡ \true); */ ;
- __fc_initenv();
- tmp_0 = Frama_C_nondet(0,1);
- if (tmp_0) {
- int tmp;
- tmp = Frama_C_interval(0,4096 - 1);
- ;
- __retres = __fc_env[tmp];
- goto return_label;
- }
- else {
- __retres = (char *)0;
- goto return_label;
- }
- return_label: return __retres;
+ _Bool tmp;
+ tmp = __fc_atomic_compare_exchange_strong(object,expected,desired,obj_size);
+ return tmp;
}
-/*@ requires valid_string: valid_read_string(string);
- assigns __fc_env[0 ..], \result;
- assigns __fc_env[0 ..] \from __fc_env[0 ..], string;
- assigns \result \from (indirect: __fc_env[0 ..]), (indirect: string);
- */
-int putenv(char *string)
+_Bool __fc_atomic_compare_exchange_weak_explicit(void *object,
+ void *expected,
+ unsigned long long desired,
+ memory_order success,
+ memory_order failure,
+ size_t obj_size)
{
- int __retres;
- int tmp_3;
- char *separator __attribute__((__unused__)) =
- strchr((char const *)string,'=');
- /*@ assert string_contains_separator: separator ≢ \null; */ ;
- /*@ assert name_is_not_empty: separator ≢ string; */ ;
- __fc_initenv();
- tmp_3 = Frama_C_nondet(0,1);
- if (tmp_3) {
- int tmp_1;
- int tmp_2;
- tmp_1 = Frama_C_nondet(0,1);
- if (tmp_1) {
- int tmp_0;
- tmp_0 = Frama_C_interval(-2147483647 - 1,2147483647);
- __retres = tmp_0;
- goto return_label;
- }
- tmp_2 = Frama_C_interval(0,4096 - 1);
- __fc_env[tmp_2] = string;
- }
- __retres = 0;
- return_label: return __retres;
+ _Bool tmp;
+ tmp = __fc_atomic_compare_exchange_strong(object,expected,desired,obj_size);
+ return tmp;
}
-/*@ requires valid_name: valid_read_string(name);
- requires valid_value: valid_read_string(value);
- ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
- assigns \result, __fc_env[0 ..];
- assigns \result
- \from __fc_env[0 ..], (indirect: name), (indirect: *(name + (0 ..))),
- (indirect: value), (indirect: *(value + (0 ..))),
- (indirect: overwrite);
- assigns __fc_env[0 ..]
- \from __fc_env[0 ..], (indirect: name), (indirect: *(name + (0 ..))),
- (indirect: value), (indirect: *(value + (0 ..))),
- (indirect: overwrite);
- */
-int setenv(char const *name, char const *value, int overwrite)
+unsigned long long __fc_atomic_fetch_add(void *obj,
+ unsigned long long operand,
+ size_t obj_size)
{
- int __retres;
- char *tmp;
- int tmp_4;
- tmp = strchr(name,'=');
- if (tmp) {
- __retres = -1;
- goto return_label;
- }
- size_t namelen = strlen(name);
- if (namelen == (size_t)0) {
- __retres = -1;
- goto return_label;
- }
- __fc_initenv();
- tmp_4 = Frama_C_nondet(0,1);
- if (tmp_4) {
- __retres = -1;
- goto return_label;
- }
- else {
- int tmp_1;
- int tmp_2;
- int tmp_3;
- tmp_1 = Frama_C_nondet(0,1);
- if (tmp_1) Frama_C_make_unknown(__fc_env_strings,(unsigned int)(64 - 1));
- tmp_2 = Frama_C_interval(0,4096 - 1);
- tmp_3 = Frama_C_interval(0,64 - 1);
- __fc_env[tmp_2] = & __fc_env_strings[tmp_3];
- __retres = 0;
- goto return_label;
+ unsigned long long r;
+ if (obj_size == sizeof(char)) {
+ r = (unsigned long long)*((atomic_uchar volatile *)obj);
+ *((atomic_uchar volatile *)obj) = (unsigned char)((unsigned long long)*((atomic_uchar volatile *)obj) + operand);
}
- return_label: return __retres;
+ else
+ if (obj_size == sizeof(short)) {
+ r = (unsigned long long)*((atomic_ushort volatile *)obj);
+ *((atomic_ushort volatile *)obj) = (unsigned short)((unsigned long long)*((atomic_ushort volatile *)obj) + operand);
+ }
+ else
+ if (obj_size == sizeof(int)) {
+ r = (unsigned long long)*((atomic_uint volatile *)obj);
+ *((atomic_uint volatile *)obj) = (unsigned int)((unsigned long long)*((atomic_uint volatile *)obj) + operand);
+ }
+ else
+ if (obj_size == sizeof(long)) {
+ r = (unsigned long long)*((atomic_ulong volatile *)obj);
+ *((atomic_ulong volatile *)obj) = (unsigned long)((unsigned long long)*((atomic_ulong volatile *)obj) + operand);
+ }
+ else
+ if (obj_size == sizeof(long long)) {
+ r = *((atomic_ullong volatile *)obj);
+ *((atomic_ullong volatile *)obj) += operand;
+ }
+ else __FC_assert(0 != 0,"share/libc/stdatomic.c",139,"0");
+ return r;
}
-/*@ requires valid_name: valid_read_string(name);
- ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
- assigns \result, __fc_env[0 ..];
- assigns \result
- \from __fc_env[0 ..], (indirect: name), (indirect: *(name + (0 ..)));
- assigns __fc_env[0 ..]
- \from __fc_env[0 ..], (indirect: name), (indirect: *(name + (0 ..)));
- */
-int unsetenv(char const *name)
+unsigned long long __fc_atomic_fetch_add_explicit(void *obj,
+ unsigned long long operand,
+ memory_order order,
+ size_t obj_size)
{
- int __retres;
- char *tmp;
- int tmp_2;
- tmp = strchr(name,'=');
- if (tmp) {
- __retres = -1;
- goto return_label;
- }
- size_t namelen = strlen(name);
- if (namelen == (size_t)0) {
- __retres = -1;
- goto return_label;
- }
- __fc_initenv();
- tmp_2 = Frama_C_nondet(0,1);
- if (tmp_2) {
- int tmp_1;
- tmp_1 = Frama_C_interval(0,4096 - 1);
- __fc_env[tmp_1] = (char *)0;
+ unsigned long long tmp;
+ tmp = __fc_atomic_fetch_add(obj,operand,obj_size);
+ return tmp;
+}
+
+unsigned long long __fc_atomic_fetch_sub(void *obj,
+ unsigned long long operand,
+ size_t obj_size)
+{
+ unsigned long long r;
+ if (obj_size == sizeof(char)) {
+ r = (unsigned long long)*((atomic_uchar volatile *)obj);
+ *((atomic_uchar volatile *)obj) = (unsigned char)((unsigned long long)*((atomic_uchar volatile *)obj) - operand);
}
- __retres = 0;
- return_label: return __retres;
+ else
+ if (obj_size == sizeof(short)) {
+ r = (unsigned long long)*((atomic_ushort volatile *)obj);
+ *((atomic_ushort volatile *)obj) = (unsigned short)((unsigned long long)*((atomic_ushort volatile *)obj) - operand);
+ }
+ else
+ if (obj_size == sizeof(int)) {
+ r = (unsigned long long)*((atomic_uint volatile *)obj);
+ *((atomic_uint volatile *)obj) = (unsigned int)((unsigned long long)*((atomic_uint volatile *)obj) - operand);
+ }
+ else
+ if (obj_size == sizeof(long)) {
+ r = (unsigned long long)*((atomic_ulong volatile *)obj);
+ *((atomic_ulong volatile *)obj) = (unsigned long)((unsigned long long)*((atomic_ulong volatile *)obj) - operand);
+ }
+ else
+ if (obj_size == sizeof(long long)) {
+ r = *((atomic_ullong volatile *)obj);
+ *((atomic_ullong volatile *)obj) -= operand;
+ }
+ else __FC_assert(0 != 0,"share/libc/stdatomic.c",163,"0");
+ return r;
}
-/*@ requires valid_memptr: \valid(memptr);
- requires
- alignment_is_a_suitable_power_of_two:
- alignment ≥ sizeof(void *) ∧
- ((size_t)alignment & ((size_t)alignment - 1)) ≡ 0;
- assigns __fc_heap_status, \result;
- assigns __fc_heap_status
- \from (indirect: alignment), size, __fc_heap_status;
- assigns \result
- \from (indirect: alignment), (indirect: size),
- (indirect: __fc_heap_status);
- allocates *\old(memptr);
-
- behavior allocation:
- assumes can_allocate: is_allocable(size);
- ensures allocation: \fresh{Old, Here}(*\old(memptr),\old(size));
- ensures result_zero: \result ≡ 0;
- assigns __fc_heap_status, \result;
- assigns __fc_heap_status
- \from (indirect: alignment), size, __fc_heap_status;
- assigns \result
- \from (indirect: alignment), (indirect: size),
- (indirect: __fc_heap_status);
-
- behavior no_allocation:
- assumes cannot_allocate: ¬is_allocable(size);
- ensures result_non_zero: \result < 0 ∨ \result > 0;
- assigns \result;
- assigns \result \from (indirect: alignment);
- allocates \nothing;
-
- complete behaviors no_allocation, allocation;
- disjoint behaviors no_allocation, allocation;
- */
-int posix_memalign(void **memptr, size_t alignment, size_t size)
+unsigned long long __fc_atomic_fetch_sub_explicit(void *obj,
+ unsigned long long operand,
+ memory_order order,
+ size_t obj_size)
{
- int __retres;
- /*@
- assert
- alignment_is_a_suitable_power_of_two:
- alignment ≥ sizeof(void *) ∧
- ((size_t)alignment & ((size_t)alignment - 1)) ≡ 0;
- */
- ;
- *memptr = malloc(size);
- if (! *memptr) {
- __retres = 12;
- goto return_label;
- }
- __retres = 0;
- return_label: return __retres;
+ unsigned long long tmp;
+ tmp = __fc_atomic_fetch_sub(obj,operand,obj_size);
+ return tmp;
}
-char *realpath(char const * restrict file_name, char * restrict resolved_name)
+unsigned long long __fc_atomic_fetch_or(void *obj,
+ unsigned long long operand,
+ size_t obj_size)
{
- char *__retres;
- int tmp;
- if (! file_name) {
- __fc_errno = 22;
- __retres = (char *)0;
- goto return_label;
- }
- tmp = Frama_C_interval(0,6);
- switch (tmp) {
- case 0: __fc_errno = 13;
- __retres = (char *)0;
- goto return_label;
- case 1: __fc_errno = 5;
- __retres = (char *)0;
- goto return_label;
- case 2: __fc_errno = 40;
- __retres = (char *)0;
- goto return_label;
- case 3: __fc_errno = 36;
- __retres = (char *)0;
- goto return_label;
- case 4: __fc_errno = 2;
- __retres = (char *)0;
- goto return_label;
- case 5: __fc_errno = 20;
- __retres = (char *)0;
- goto return_label;
- default: break;
+ unsigned long long r;
+ if (obj_size == sizeof(char)) {
+ r = (unsigned long long)*((atomic_uchar volatile *)obj);
+ *((atomic_uchar volatile *)obj) = (unsigned char)((unsigned long long)*((atomic_uchar volatile *)obj) | operand);
}
- int realpath_len = Frama_C_interval(1,256);
- if (! resolved_name) {
- resolved_name = (char *)malloc((unsigned int)256);
- if (! resolved_name) {
- __fc_errno = 12;
- __retres = (char *)0;
- goto return_label;
+ else
+ if (obj_size == sizeof(short)) {
+ r = (unsigned long long)*((atomic_ushort volatile *)obj);
+ *((atomic_ushort volatile *)obj) = (unsigned short)((unsigned long long)*((atomic_ushort volatile *)obj) | operand);
}
- }
- Frama_C_make_unknown(resolved_name,(unsigned int)realpath_len);
- *(resolved_name + (realpath_len - 1)) = (char)'\000';
- __retres = resolved_name;
- return_label: return __retres;
+ else
+ if (obj_size == sizeof(int)) {
+ r = (unsigned long long)*((atomic_uint volatile *)obj);
+ *((atomic_uint volatile *)obj) = (unsigned int)((unsigned long long)*((atomic_uint volatile *)obj) | operand);
+ }
+ else
+ if (obj_size == sizeof(long)) {
+ r = (unsigned long long)*((atomic_ulong volatile *)obj);
+ *((atomic_ulong volatile *)obj) = (unsigned long)((unsigned long long)*((atomic_ulong volatile *)obj) | operand);
+ }
+ else
+ if (obj_size == sizeof(long long)) {
+ r = *((atomic_ullong volatile *)obj);
+ *((atomic_ullong volatile *)obj) |= operand;
+ }
+ else __FC_assert(0 != 0,"share/libc/stdatomic.c",187,"0");
+ return r;
}
-/*@ requires valid_dest: valid_or_empty(dest, n);
- requires valid_src: valid_read_or_empty(src, n);
- requires
- separation:
- \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1));
- ensures
- copied_contents:
- memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡
- 0;
- ensures result_ptr: \result ≡ \old(dest);
- assigns *((char *)dest + (0 .. n - 1)), \result;
- assigns *((char *)dest + (0 .. n - 1))
- \from *((char *)src + (0 .. n - 1));
- assigns \result \from dest;
- */
-void *memcpy(void * restrict dest, void const * restrict src, size_t n)
+unsigned long long __fc_atomic_fetch_or_explicit(void *obj,
+ unsigned long long operand,
+ memory_order order,
+ size_t obj_size)
{
- {
- size_t i = (unsigned int)0;
- /*@ loop invariant no_eva: 0 ≤ i ≤ n;
- loop invariant
- no_eva:
- ∀ ℤ k;
- 0 ≤ k < i ⇒ *((char *)dest + k) ≡ *((char *)src + k);
- loop assigns i, *((char *)dest + (0 .. n - 1));
- loop variant n - i;
- */
- while (i < n) {
- *((char *)dest + i) = *((char *)src + i);
- i += (size_t)1;
- }
- }
- return dest;
+ unsigned long long tmp;
+ tmp = __fc_atomic_fetch_or(obj,operand,obj_size);
+ return tmp;
}
-/*@ requires valid_dest: valid_or_empty(dest, n);
- requires valid_src: valid_read_or_empty(src, n);
- requires
- separation:
- \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1));
- ensures
- copied_contents:
- memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡
- 0;
- ensures result_next_byte: \result ≡ \old(dest) + \old(n);
- assigns *((char *)dest + (0 .. n - 1)), \result;
- assigns *((char *)dest + (0 .. n - 1))
- \from *((char *)src + (0 .. n - 1));
- assigns \result \from dest, n;
- */
-void *mempcpy(void * restrict dest, void const * restrict src, size_t n)
+unsigned long long __fc_atomic_fetch_xor(void *obj,
+ unsigned long long operand,
+ size_t obj_size)
{
- void *__retres;
- size_t i;
- i = (unsigned int)0;
- /*@ loop invariant no_eva: 0 ≤ i ≤ n;
- loop invariant
- no_eva:
- ∀ ℤ k;
- 0 ≤ k < i ⇒ *((char *)dest + k) ≡ *((char *)src + k);
- loop assigns i, *((char *)dest + (0 .. n - 1));
- loop variant n - i;
- */
- while (i < n) {
- *((char *)dest + i) = *((char *)src + i);
- i += (size_t)1;
+ unsigned long long r;
+ if (obj_size == sizeof(char)) {
+ r = (unsigned long long)*((atomic_uchar volatile *)obj);
+ *((atomic_uchar volatile *)obj) = (unsigned char)((unsigned long long)*((atomic_uchar volatile *)obj) ^ operand);
}
- __retres = (void *)((char *)dest + i);
- return __retres;
+ else
+ if (obj_size == sizeof(short)) {
+ r = (unsigned long long)*((atomic_ushort volatile *)obj);
+ *((atomic_ushort volatile *)obj) = (unsigned short)((unsigned long long)*((atomic_ushort volatile *)obj) ^ operand);
+ }
+ else
+ if (obj_size == sizeof(int)) {
+ r = (unsigned long long)*((atomic_uint volatile *)obj);
+ *((atomic_uint volatile *)obj) = (unsigned int)((unsigned long long)*((atomic_uint volatile *)obj) ^ operand);
+ }
+ else
+ if (obj_size == sizeof(long)) {
+ r = (unsigned long long)*((atomic_ulong volatile *)obj);
+ *((atomic_ulong volatile *)obj) = (unsigned long)((unsigned long long)*((atomic_ulong volatile *)obj) ^ operand);
+ }
+ else
+ if (obj_size == sizeof(long long)) {
+ r = *((atomic_ullong volatile *)obj);
+ *((atomic_ullong volatile *)obj) ^= operand;
+ }
+ else __FC_assert(0 != 0,"share/libc/stdatomic.c",217,"0");
+ return r;
}
-/*@ assigns \result;
- assigns \result \from (indirect: p), (indirect: q), (indirect: n);
-
- behavior separated:
- assumes
- separation: no_overlap:
- \separated(p + (0 .. n - 1), q + (0 .. n - 1));
- ensures result_no_overlap: \result ≡ 0;
-
- behavior not_separated_lt:
- assumes
- separation: overlap: ¬\separated(p + (0 .. n - 1), q + (0 .. n - 1));
- assumes p_before_q: p ≤ q < p + n;
- ensures result_p_before_q: \result ≡ -1;
-
- behavior not_separated_gt:
- assumes
- separation: overlap: ¬\separated(p + (0 .. n - 1), q + (0 .. n - 1));
- assumes p_after_q: q < p ≤ q + n;
- ensures result_p_after_q: \result ≡ 1;
-
- complete behaviors not_separated_gt, not_separated_lt, separated;
- disjoint behaviors not_separated_gt, not_separated_lt, separated;
- */
-static int memoverlap(char const *p, char const *q, size_t n)
+unsigned long long __fc_atomic_fetch_xor_explicit(void *obj,
+ unsigned long long operand,
+ memory_order order,
+ size_t obj_size)
{
- int __retres;
- uintptr_t p1 = (unsigned int)p;
- uintptr_t p2 = (unsigned int)(p + n);
- uintptr_t q1 = (unsigned int)q;
- uintptr_t q2 = (unsigned int)(q + n);
- if (p1 <= q1) {
- if (p2 > q1) {
- __retres = -1;
- goto return_label;
- }
- else goto _LAND;
+ unsigned long long tmp;
+ tmp = __fc_atomic_fetch_xor(obj,operand,obj_size);
+ return tmp;
+}
+
+unsigned long long __fc_atomic_fetch_and(void *obj,
+ unsigned long long operand,
+ size_t obj_size)
+{
+ unsigned long long r;
+ if (obj_size == sizeof(char)) {
+ r = (unsigned long long)*((atomic_uchar volatile *)obj);
+ *((atomic_uchar volatile *)obj) = (unsigned char)((unsigned long long)*((atomic_uchar volatile *)obj) & operand);
}
- else {
- _LAND: ;
- if (q1 <= p1)
- if (q2 > p1) {
- __retres = 1;
- goto return_label;
- }
- else {
- __retres = 0;
- goto return_label;
- }
- else {
- __retres = 0;
- goto return_label;
+ else
+ if (obj_size == sizeof(short)) {
+ r = (unsigned long long)*((atomic_ushort volatile *)obj);
+ *((atomic_ushort volatile *)obj) = (unsigned short)((unsigned long long)*((atomic_ushort volatile *)obj) & operand);
}
- }
- return_label: return __retres;
+ else
+ if (obj_size == sizeof(int)) {
+ r = (unsigned long long)*((atomic_uint volatile *)obj);
+ *((atomic_uint volatile *)obj) = (unsigned int)((unsigned long long)*((atomic_uint volatile *)obj) & operand);
+ }
+ else
+ if (obj_size == sizeof(long)) {
+ r = (unsigned long long)*((atomic_ulong volatile *)obj);
+ *((atomic_ulong volatile *)obj) = (unsigned long)((unsigned long long)*((atomic_ulong volatile *)obj) & operand);
+ }
+ else
+ if (obj_size == sizeof(long long)) {
+ r = *((atomic_ullong volatile *)obj);
+ *((atomic_ullong volatile *)obj) &= operand;
+ }
+ else __FC_assert(0 != 0,"share/libc/stdatomic.c",247,"0");
+ return r;
}
-/*@ requires valid_dest: valid_or_empty(dest, n);
- requires valid_src: valid_read_or_empty(src, n);
- ensures
- copied_contents:
- memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡
- 0;
- ensures result_ptr: \result ≡ \old(dest);
- assigns *((char *)dest + (0 .. n - 1)), \result;
- assigns *((char *)dest + (0 .. n - 1))
- \from *((char *)src + (0 .. n - 1));
- assigns \result \from dest;
- */
-void *memmove(void *dest, void const *src, size_t n)
+unsigned long long __fc_atomic_fetch_and_explicit(void *obj,
+ unsigned long long operand,
+ memory_order order,
+ size_t obj_size)
{
- void *__retres;
- int tmp;
- if (n == (size_t)0) {
- __retres = dest;
- goto return_label;
- }
- char *s = (char *)src;
- char *d = (char *)dest;
- tmp = memoverlap((char const *)dest,(char const *)src,n);
- if (tmp <= 0) {
- size_t i = (unsigned int)0;
- /*@ loop invariant no_eva: 0 ≤ i ≤ n;
- loop invariant
- no_eva:
- ∀ ℤ k;
- 0 ≤ k < i ⇒
- *((char *)dest + k) ≡ \at(*((char *)src + k),LoopEntry);
- loop invariant
- no_eva:
- ∀ ℤ k;
- i ≤ k < n ⇒
- *((char *)src + k) ≡ \at(*((char *)src + k),LoopEntry);
- loop assigns i, *((char *)dest + (0 .. n - 1));
- loop variant n - i;
- */
- while (i < n) {
- *(d + i) = *(s + i);
- i += (size_t)1;
- }
- }
- else {
- {
- size_t i_0 = n - (size_t)1;
- /*@ loop invariant no_eva: 0 ≤ i_0 < n;
- loop invariant
- no_eva:
- ∀ ℤ k;
- i_0 < k < n ⇒
- *((char *)dest + k) ≡ \at(*((char *)src + k),LoopEntry);
- loop invariant
- no_eva:
- ∀ ℤ k;
- 0 ≤ k ≤ i_0 ⇒
- *((char *)src + k) ≡ \at(*((char *)src + k),LoopEntry);
- loop assigns i_0, *((char *)dest + (0 .. n - 1));
- loop variant i_0;
- */
- while (i_0 > (size_t)0) {
- *(d + i_0) = *(s + i_0);
- i_0 -= (size_t)1;
- }
- }
- *(d + 0) = *(s + 0);
- }
- __retres = dest;
- return_label: return __retres;
+ unsigned long long tmp;
+ tmp = __fc_atomic_fetch_and(obj,operand,obj_size);
+ return tmp;
}
-/*@ requires valid_string_s: valid_read_string(s);
- ensures acsl_c_equiv: \result ≡ strlen(\old(s));
- assigns \result;
- assigns \result \from (indirect: *(s + (0 ..)));
- */
-size_t strlen(char const *s)
+_Bool atomic_flag_test_and_set(atomic_flag volatile *object)
{
- size_t i;
- i = (unsigned int)0;
- while ((int)*(s + i) != 0) i += (size_t)1;
- return i;
+ _Bool r = (_Bool)(object->__fc_val != 0);
+ object->__fc_val = (unsigned char)1;
+ return r;
}
-/*@ requires valid_string_s: valid_read_nstring(s, maxlen);
- ensures
- result_bounded:
- \result ≡ strlen(\old(s)) ∨ \result ≡ \old(maxlen);
- assigns \result;
- assigns \result
- \from (indirect: *(s + (0 .. maxlen - 1))), (indirect: maxlen);
- */
-size_t strnlen(char const *s, size_t maxlen)
+_Bool atomic_flag_test_and_set_explicit(atomic_flag volatile *object,
+ memory_order order)
{
- size_t i;
- i = (unsigned int)0;
- while (1) {
- if (i < maxlen) {
- if (! ((int)*(s + i) != 0)) break;
- }
- else break;
- i += (size_t)1;
- }
- return i;
+ _Bool r = (_Bool)(object->__fc_val != 0);
+ object->__fc_val = (unsigned char)1;
+ return r;
}
-/*@ requires valid_s: valid_or_empty(s, n);
- ensures
- acsl_c_equiv: memset((char *)\old(s), \old(c), \old(n)) ≡ \true;
- ensures result_ptr: \result ≡ \old(s);
- assigns *((char *)s + (0 .. n - 1)), \result;
- assigns *((char *)s + (0 .. n - 1)) \from c;
- assigns \result \from s;
- */
-void *memset(void *s, int c, size_t n)
+void atomic_flag_clear(atomic_flag volatile *object)
{
- unsigned char *p = (unsigned char *)s;
- {
- size_t i = (unsigned int)0;
- while (i < n) {
- *(p + i) = (unsigned char)c;
- i += (size_t)1;
- }
- }
- return s;
+ object->__fc_val = (unsigned char)0;
+ return;
}
-/*@ requires valid_string_s1: valid_read_string(s1);
- requires valid_string_s2: valid_read_string(s2);
- ensures acsl_c_equiv: \result ≡ strcmp(\old(s1), \old(s2));
- assigns \result;
- assigns \result
- \from (indirect: *(s1 + (0 ..))), (indirect: *(s2 + (0 ..)));
- */
-int strcmp(char const *s1, char const *s2)
+void atomic_flag_clear_explicit(atomic_flag volatile *object,
+ memory_order order)
{
- int __retres;
- size_t i;
- i = (unsigned int)0;
- while ((int)*(s1 + i) == (int)*(s2 + i)) {
- if ((int)*(s1 + i) == 0) {
- __retres = 0;
- goto return_label;
- }
- i += (size_t)1;
- }
- __retres = (int)*((unsigned char *)s1 + i) - (int)*((unsigned char *)s2 + i);
- return_label: return __retres;
+ object->__fc_val = (unsigned char)0;
+ return;
}
-/*@ requires valid_string_s1: valid_read_nstring(s1, n);
- requires valid_string_s2: valid_read_nstring(s2, n);
- ensures acsl_c_equiv: \result ≡ strncmp(\old(s1), \old(s2), \old(n));
+FILE *__fc_stderr;
+
+FILE *__fc_stdin;
+
+FILE *__fc_stdout;
+
+/*@ requires valid_filename: valid_read_string(filename);
+ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
assigns \result;
assigns \result
- \from (indirect: *(s1 + (0 .. n - 1))),
- (indirect: *(s2 + (0 .. n - 1))), (indirect: n);
+ \from (indirect: *(filename + (0 .. strlen{Old}(filename))));
*/
-int strncmp(char const *s1, char const *s2, size_t n)
-{
- int __retres;
- {
- size_t i = (unsigned int)0;
- while (i < n) {
- if ((int)*(s1 + i) != (int)*(s2 + i)) {
- __retres = (int)*((unsigned char *)s1 + i) - (int)*((unsigned char *)s2 + i);
- goto return_label;
- }
- if ((int)*(s1 + i) == 0) {
- __retres = 0;
- goto return_label;
- }
- i += (size_t)1;
- }
- }
- __retres = 0;
- return_label: return __retres;
-}
+extern int remove(char const *filename);
-/*@ requires valid_s1: valid_read_or_empty(s1, n);
- requires valid_s2: valid_read_or_empty(s2, n);
- requires initialization: s1: \initialized((char *)s1 + (0 .. n - 1));
- requires initialization: s2: \initialized((char *)s2 + (0 .. n - 1));
- requires danglingness: s1: non_escaping(s1, n);
- requires danglingness: s2: non_escaping(s2, n);
- ensures
- logic_spec:
- \result ≡
- memcmp{Pre, Pre}((char *)\old(s1), (char *)\old(s2), \old(n));
+/*@ requires valid_old_name: valid_read_string(old_name);
+ requires valid_new_name: valid_read_string(new_name);
+ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
assigns \result;
assigns \result
- \from (indirect: *((char *)s1 + (0 .. n - 1))),
- (indirect: *((char *)s2 + (0 .. n - 1)));
+ \from (indirect: *(old_name + (0 .. strlen{Old}(old_name)))),
+ (indirect: *(new_name + (0 .. strlen{Old}(new_name))));
*/
-int memcmp(void const *s1, void const *s2, size_t n)
-{
- int __retres;
- unsigned char const *p1;
- unsigned char const *p2;
- p1 = (unsigned char const *)s1;
- p2 = (unsigned char const *)s2;
- {
- size_t i = (unsigned int)0;
- while (i < n) {
- if ((int)*(p1 + i) != (int)*(p2 + i)) {
- __retres = (int)*(p1 + i) - (int)*(p2 + i);
- goto return_label;
- }
- i += (size_t)1;
- }
- }
- __retres = 0;
- return_label: return __retres;
-}
+extern int rename(char const *old_name, char const *new_name);
-static int char_equal_ignore_case(char c1, char c2)
-{
- int __retres;
- if ((int)c1 >= 'A')
- if ((int)c1 <= 'Z') c1 = (char)((int)c1 - ('A' - 'a'));
- if ((int)c2 >= 'A')
- if ((int)c2 <= 'Z') c2 = (char)((int)c2 - ('A' - 'a'));
- if ((int)c1 == (int)c2) {
- __retres = 0;
- goto return_label;
- }
- else {
- __retres = (int)((unsigned char)c2) - (int)((unsigned char)c1);
- goto return_label;
- }
- return_label: return __retres;
-}
+FILE __fc_fopen[16];
+FILE * const __fc_p_fopen = __fc_fopen;
+/*@ ensures
+ result_null_or_valid_fd:
+ \result ≡ \null ∨ \subset(\result, &__fc_fopen[0 .. 16 - 1]);
+ assigns \result;
+ assigns \result \from __fc_p_fopen;
+ */
+extern FILE *tmpfile(void);
-/*@ requires valid_string_s1: valid_read_string(s1);
- requires valid_string_s2: valid_read_string(s2);
+char __fc_tmpnam[2048];
+char * const __fc_p_tmpnam = __fc_tmpnam;
+/*@ requires valid_s_or_null: s ≡ \null ∨ \valid(s + (0 .. 2048));
+ ensures
+ result_string_or_null:
+ \result ≡ \null ∨ \result ≡ \old(s) ∨
+ \result ≡ __fc_p_tmpnam;
+ assigns *(__fc_p_tmpnam + (0 .. 2048)), *(s + (0 .. 2048)), \result;
+ assigns *(__fc_p_tmpnam + (0 .. 2048))
+ \from *(__fc_p_tmpnam + (0 .. 2048)), (indirect: s);
+ assigns *(s + (0 .. 2048))
+ \from (indirect: s), *(__fc_p_tmpnam + (0 .. 2048));
+ assigns \result \from s, __fc_p_tmpnam;
+ */
+extern char *tmpnam(char *s);
+
+/*@ requires valid_stream: \valid(stream);
+ ensures result_zero_or_EOF: \result ≡ 0 ∨ \result ≡ -1;
assigns \result;
- assigns \result
- \from (indirect: *(s1 + (0 ..))), (indirect: *(s2 + (0 ..)));
+ assigns \result \from (indirect: stream), (indirect: *stream);
*/
-int strcasecmp(char const *s1, char const *s2)
-{
- int __retres;
- size_t i;
- i = (unsigned int)0;
- while (1) {
- if ((int)*(s1 + i) != 0) {
- if (! ((int)*(s2 + i) != 0)) break;
- }
- else break;
- {
- int res = char_equal_ignore_case(*(s1 + i),*(s2 + i));
- if (res != 0) {
- __retres = res;
- goto return_label;
+extern int fclose(FILE *stream);
+
+/*@ requires null_or_valid_stream: stream ≡ \null ∨ \valid_read(stream);
+ ensures result_zero_or_EOF: \result ≡ 0 ∨ \result ≡ -1;
+ assigns \result, *stream, __fc_fopen[0 .. 16 - 1];
+ assigns \result
+ \from (indirect: *stream), (indirect: __fc_fopen[0 .. 16 - 1]);
+ assigns *stream
+ \from (indirect: stream), *stream, __fc_fopen[0 .. 16 - 1];
+ assigns __fc_fopen[0 .. 16 - 1]
+ \from (indirect: stream), *stream, __fc_fopen[0 .. 16 - 1];
+
+ behavior flush_all:
+ assumes all_streams: stream ≡ \null;
+ assigns __fc_fopen[0 .. 16 - 1], \result;
+ assigns __fc_fopen[0 .. 16 - 1] \from __fc_fopen[0 .. 16 - 1];
+ assigns \result \from (indirect: __fc_fopen[0 .. 16 - 1]);
+
+ behavior flush_stream:
+ assumes single_stream: stream ≢ \null;
+ assigns *stream, \result;
+ assigns *stream \from *stream;
+ assigns \result \from (indirect: *stream);
+
+ complete behaviors flush_stream, flush_all;
+ disjoint behaviors flush_stream, flush_all;
+ */
+extern int fflush(FILE *stream);
+
+/*@ requires valid_filename: valid_read_string(filename);
+ requires valid_mode: valid_read_string(mode);
+ ensures
+ result_null_or_valid_fd:
+ \result ≡ \null ∨ \subset(\result, &__fc_fopen[0 .. 16 - 1]);
+ assigns \result;
+ assigns \result
+ \from (indirect: *(filename + (0 .. strlen{Old}(filename)))),
+ (indirect: *(mode + (0 .. strlen{Old}(mode)))), __fc_p_fopen;
+ */
+extern FILE *fopen(char const * restrict filename, char const * restrict mode);
+
+/*@ requires valid_mode: valid_read_string(mode);
+ ensures
+ result_null_or_valid_fd:
+ \result ≡ \null ∨ \subset(\result, &__fc_fopen[0 .. 16 - 1]);
+ assigns \result, __fc_fopen[fd];
+ assigns \result
+ \from (indirect: fd), (indirect: *(mode + (0 .. strlen{Old}(mode)))),
+ (indirect: __fc_fopen[fd]), __fc_p_fopen;
+ assigns __fc_fopen[fd]
+ \from (indirect: fd), (indirect: *(mode + (0 .. strlen{Old}(mode)))),
+ (indirect: __fc_fopen[fd]), __fc_p_fopen;
+ */
+extern FILE *fdopen(int fd, char const *mode);
+
+/*@ requires valid_filename: valid_read_string(filename);
+ requires valid_mode: valid_read_string(mode);
+ requires valid_stream: \valid(stream);
+ ensures
+ result_null_or_valid_fd:
+ \result ≡ \null ∨ \result ∈ &__fc_fopen[0 .. 16 - 1];
+ ensures stream_opened: *\old(stream) ∈ __fc_fopen[0 .. 16 - 1];
+ assigns \result, *stream;
+ assigns \result
+ \from (indirect: *(filename + (..))), (indirect: *(mode + (..))),
+ __fc_p_fopen, (indirect: stream);
+ assigns *stream
+ \from (indirect: *(filename + (..))), (indirect: *(mode + (..))),
+ __fc_p_fopen, (indirect: stream);
+ */
+extern FILE *freopen(char const * restrict filename,
+ char const * restrict mode, FILE * restrict stream);
+
+/*@ assigns *stream;
+ assigns *stream \from buf; */
+extern void setbuf(FILE * restrict stream, char * restrict buf);
+
+/*@ assigns *stream;
+ assigns *stream \from buf, mode, size; */
+extern int setvbuf(FILE * restrict stream, char * restrict buf, int mode,
+ size_t size);
+
+/*@ axiomatic format_length {
+ logic ℤ format_length{L}(char *format) ;
+
+ }
+
+*/
+/*@ assigns *stream;
+ assigns *stream \from *(format + (..)), arg; */
+extern int vfprintf(FILE * restrict stream, char const * restrict format,
+ va_list arg);
+
+/*@ assigns *stream;
+ assigns *stream \from *(format + (..)), *stream; */
+extern int vfscanf(FILE * restrict stream, char const * restrict format,
+ va_list arg);
+
+/*@ assigns *__fc_stdout;
+ assigns *__fc_stdout \from arg; */
+extern int vprintf(char const * restrict format, va_list arg);
+
+/*@ assigns *__fc_stdin;
+ assigns *__fc_stdin \from *(format + (..)); */
+extern int vscanf(char const * restrict format, va_list arg);
+
+/*@ assigns *(s + (0 .. n - 1));
+ assigns *(s + (0 .. n - 1)) \from *(format + (..)), arg;
+ */
+extern int vsnprintf(char * restrict s, size_t n,
+ char const * restrict format, va_list arg);
+
+/*@ assigns *(s + (0 ..));
+ assigns *(s + (0 ..)) \from *(format + (..)), arg;
+ */
+extern int vsprintf(char * restrict s, char const * restrict format,
+ va_list arg);
+
+/*@ requires valid_stream: \valid(stream);
+ ensures result_uchar_or_eof: (0 ≤ \result ≤ 255) ∨ \result ≡ -1;
+ assigns *stream, \result;
+ assigns *stream \from *stream;
+ assigns \result \from (indirect: *stream);
+ */
+extern int fgetc(FILE *stream);
+
+/*@ requires valid_stream: \valid(stream);
+ requires room_s: \valid(s + (0 .. size - 1));
+ ensures result_null_or_same: \result ≡ \null ∨ \result ≡ \old(s);
+ ensures
+ initialization: at_least_one:
+ \result ≢ \null ⇒ \initialized(\old(s) + 0);
+ ensures
+ terminated_string_on_success:
+ \result ≢ \null ⇒ valid_string(\old(s));
+ assigns *(s + (0 .. size - 1)), \result;
+ assigns *(s + (0 .. size - 1))
+ \from (indirect: size), (indirect: *stream);
+ assigns \result \from s, (indirect: size), (indirect: *stream);
+ */
+extern char *fgets(char * restrict s, int size, FILE * restrict stream);
+
+/*@ requires valid_stream: \valid(stream);
+ assigns *stream, \result;
+ assigns *stream \from c, *stream;
+ assigns \result \from (indirect: *stream);
+ */
+extern int fputc(int c, FILE *stream);
+
+/*@ requires valid_string_s: valid_read_string(s);
+ assigns *stream, \result;
+ assigns *stream \from *(s + (0 .. strlen{Old}(s))), *stream;
+ assigns \result
+ \from (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: *stream);
+ */
+extern int fputs(char const * restrict s, FILE * restrict stream);
+
+/*@ requires valid_stream: \valid(stream);
+ assigns \result, *stream;
+ assigns \result \from *stream;
+ assigns *stream \from *stream;
+ */
+extern int getc(FILE *stream);
+
+/*@ assigns \result, *__fc_stdin;
+ assigns \result \from *__fc_stdin;
+ assigns *__fc_stdin \from *__fc_stdin;
+ */
+extern int getchar(void);
+
+/*@ axiomatic GetsLength {
+ logic size_t gets_length{L}
+ reads *__fc_stdin;
+
+ }
+
+*/
+/*@ requires room_s: \valid(s + (0 .. gets_length));
+ ensures result_null_or_same: \result ≡ \old(s) ∨ \result ≡ \null;
+ assigns *(s + (0 .. gets_length{Old})), \result, *__fc_stdin;
+ assigns *(s + (0 .. gets_length{Old})) \from *__fc_stdin;
+ assigns \result \from s, *__fc_stdin;
+ assigns *__fc_stdin \from *__fc_stdin;
+ */
+extern char *gets(char *s);
+
+/*@ requires valid_stream: \valid(stream);
+ assigns *stream, \result;
+ assigns *stream \from c, *stream;
+ assigns \result \from (indirect: *stream);
+ */
+extern int putc(int c, FILE *stream);
+
+/*@ assigns *__fc_stdout, \result;
+ assigns *__fc_stdout \from c, *__fc_stdout;
+ assigns \result \from (indirect: *__fc_stdout);
+ */
+extern int putchar(int c);
+
+/*@ requires valid_string_s: valid_read_string(s);
+ assigns *__fc_stdout, \result;
+ assigns *__fc_stdout \from *(s + (0 .. strlen{Old}(s))), *__fc_stdout;
+ assigns \result
+ \from (indirect: *(s + (0 .. strlen{Old}(s)))),
+ (indirect: *__fc_stdout);
+ */
+extern int puts(char const *s);
+
+/*@ requires valid_stream: \valid(stream);
+ ensures result_ok_or_error: \result ≡ \old(c) ∨ \result ≡ -1;
+ assigns *stream, \result;
+ assigns *stream \from (indirect: c);
+ assigns \result \from (indirect: c), (indirect: *stream);
+ */
+extern int ungetc(int c, FILE *stream);
+
+/*@ requires valid_ptr_block: \valid((char *)ptr + (0 .. nmemb * size - 1));
+ requires valid_stream: \valid(stream);
+ ensures size_read: \result ≤ \old(nmemb);
+ ensures
+ initialization:
+ \initialized((char *)\old(ptr) + (0 .. \result * \old(size) - 1));
+ assigns *((char *)ptr + (0 .. nmemb * size - 1)), *stream, \result;
+ assigns *((char *)ptr + (0 .. nmemb * size - 1))
+ \from (indirect: size), (indirect: nmemb), (indirect: *stream);
+ assigns *stream
+ \from (indirect: size), (indirect: nmemb), (indirect: *stream);
+ assigns \result \from size, (indirect: *stream);
+ */
+extern size_t fread(void * restrict ptr, size_t size, size_t nmemb,
+ FILE * restrict stream);
+
+/*@ requires
+ valid_ptr_block: \valid_read((char *)ptr + (0 .. nmemb * size - 1));
+ requires valid_stream: \valid(stream);
+ ensures size_written: \result ≤ \old(nmemb);
+ assigns *stream, \result;
+ assigns *stream
+ \from (indirect: *((char *)ptr + (0 .. nmemb * size - 1)));
+ assigns \result
+ \from (indirect: *((char *)ptr + (0 .. nmemb * size - 1)));
+ */
+extern size_t fwrite(void const * restrict ptr, size_t size, size_t nmemb,
+ FILE * restrict stream);
+
+/*@ requires valid_stream: \valid(stream);
+ requires valid_pos: \valid(pos);
+ ensures initialization: pos: \initialized(\old(pos));
+ assigns \result, *pos;
+ assigns \result \from (indirect: *stream);
+ assigns *pos \from (indirect: *stream);
+ */
+extern int fgetpos(FILE * restrict stream, fpos_t * restrict pos);
+
+/*@ requires valid_stream: \valid(stream);
+ requires whence_enum: whence ≡ 0 ∨ whence ≡ 1 ∨ whence ≡ 2;
+ ensures
+ errno_set: __fc_errno ∈ {11, 9, 27, 4, 22, 5, 28, 75, 32, 29, 6};
+ assigns *stream, \result, __fc_errno;
+ assigns *stream \from *stream, (indirect: offset), (indirect: whence);
+ assigns \result
+ \from (indirect: *stream), (indirect: offset), (indirect: whence);
+ assigns __fc_errno
+ \from (indirect: *stream), (indirect: offset), (indirect: whence);
+ */
+extern int fseek(FILE *stream, long offset, int whence);
+
+/*@ requires valid_stream: \valid(stream);
+ requires whence_enum: whence ≡ 0 ∨ whence ≡ 1 ∨ whence ≡ 2;
+ ensures
+ errno_set: __fc_errno ∈ {11, 9, 27, 4, 22, 5, 28, 75, 32, 29, 6};
+ assigns *stream, \result, __fc_errno;
+ assigns *stream \from *stream, (indirect: offset), (indirect: whence);
+ assigns \result
+ \from (indirect: *stream), (indirect: offset), (indirect: whence);
+ assigns __fc_errno
+ \from (indirect: *stream), (indirect: offset), (indirect: whence);
+ */
+extern int fseeko(FILE *stream, off_t offset, int whence);
+
+/*@ requires valid_stream: \valid(stream);
+ requires valid_pos: \valid_read(pos);
+ requires initialization: pos: \initialized(pos);
+ ensures errno_set: __fc_errno ∈ {11, 9, 27, 4, 5, 28, 32, 29, 6};
+ assigns *stream, \result, __fc_errno;
+ assigns *stream \from *pos;
+ assigns \result \from (indirect: *stream), (indirect: *pos);
+ assigns __fc_errno
+ \from __fc_errno, (indirect: *stream), (indirect: *pos);
+ */
+extern int fsetpos(FILE *stream, fpos_t const *pos);
+
+/*@ requires valid_stream: \valid(stream);
+ ensures
+ success_or_error:
+ \result ≡ -1 ∨
+ (\result ≥ 0 ∧ __fc_errno ≡ \old(__fc_errno));
+ ensures errno_set: __fc_errno ∈ {9, 75, 29};
+ assigns \result, __fc_errno;
+ assigns \result \from (indirect: *stream);
+ assigns __fc_errno \from (indirect: *stream);
+ */
+extern long ftell(FILE *stream);
+
+/*@ requires valid_stream: \valid(stream);
+ ensures
+ success_or_error:
+ \result ≡ -1 ∨
+ (\result ≥ 0 ∧ __fc_errno ≡ \old(__fc_errno));
+ ensures errno_set: __fc_errno ∈ {9, 75, 29};
+ assigns \result, __fc_errno;
+ assigns \result \from (indirect: *stream);
+ assigns __fc_errno \from (indirect: *stream);
+ */
+extern off_t ftello(FILE *stream);
+
+/*@ requires valid_stream: \valid(stream);
+ assigns *stream;
+ assigns *stream \from \nothing;
+ */
+extern void rewind(FILE *stream);
+
+/*@ requires valid_stream: \valid(stream);
+ assigns *stream;
+ assigns *stream \from \nothing;
+ */
+extern void clearerr(FILE *stream);
+
+/*@ requires valid_stream: \valid(stream);
+ assigns \result;
+ assigns \result \from (indirect: *stream);
+ */
+extern int feof(FILE *stream);
+
+/*@ requires valid_stream: \valid(stream);
+ assigns \result;
+ assigns \result \from (indirect: *stream);
+ */
+extern int fileno(FILE *stream);
+
+/*@ requires valid_stream: \valid(stream);
+ assigns *stream;
+ assigns *stream \from \nothing;
+ */
+extern void flockfile(FILE *stream);
+
+/*@ requires valid_stream: \valid(stream);
+ assigns *stream;
+ assigns *stream \from \nothing;
+ */
+extern void funlockfile(FILE *stream);
+
+/*@ requires valid_stream: \valid(stream);
+ assigns \result, *stream;
+ assigns \result \from \nothing;
+ assigns *stream \from \nothing;
+ */
+extern int ftrylockfile(FILE *stream);
+
+/*@ requires valid_stream: \valid(stream);
+ assigns \result;
+ assigns \result \from (indirect: *stream);
+ */
+extern int ferror(FILE *stream);
+
+/*@ requires valid_string_s: valid_read_string(s);
+ assigns __fc_stdout;
+ assigns __fc_stdout \from __fc_errno, *(s + (0 .. strlen{Old}(s)));
+ */
+extern void perror(char const *s);
+
+/*@ requires valid_stream: \valid(stream);
+ assigns \result, *stream;
+ assigns \result \from *stream;
+ assigns *stream \from *stream;
+ */
+extern int getc_unlocked(FILE *stream);
+
+/*@ assigns \result;
+ assigns \result \from *__fc_stdin; */
+extern int getchar_unlocked(void);
+
+/*@ requires valid_stream: \valid(stream);
+ assigns *stream, \result;
+ assigns *stream \from c;
+ assigns \result \from (indirect: *stream);
+ */
+extern int putc_unlocked(int c, FILE *stream);
+
+/*@ assigns *__fc_stdout, \result;
+ assigns *__fc_stdout \from c;
+ assigns \result \from (indirect: *__fc_stdout);
+ */
+extern int putchar_unlocked(int c);
+
+/*@ requires valid_stream: \valid(stream);
+ assigns *stream;
+ assigns *stream \from \nothing;
+ */
+extern void clearerr_unlocked(FILE *stream);
+
+/*@ requires valid_stream: \valid(stream);
+ assigns \result;
+ assigns \result \from (indirect: *stream);
+ */
+extern int feof_unlocked(FILE *stream);
+
+/*@ requires valid_stream: \valid(stream);
+ assigns \result;
+ assigns \result \from (indirect: *stream);
+ */
+extern int ferror_unlocked(FILE *stream);
+
+/*@ requires valid_stream: \valid(stream);
+ assigns \result;
+ assigns \result \from (indirect: *stream);
+ */
+extern int fileno_unlocked(FILE *stream);
+
+/*@ axiomatic pipe_streams {
+ predicate is_open_pipe{L}(FILE *stream) ;
+
+ }
+
+*/
+/*@ requires valid_command: valid_read_string(command);
+ requires valid_type: valid_read_string(type);
+ ensures
+ result_error_or_valid_open_pipe:
+ \result ≡ \null ∨
+ (\subset(\result, &__fc_fopen[0 .. 16 - 1]) ∧ is_open_pipe(\result));
+ assigns \result, __fc_fopen[0 ..];
+ assigns \result
+ \from (indirect: *command), (indirect: *type), __fc_p_fopen;
+ assigns __fc_fopen[0 ..]
+ \from (indirect: *command), (indirect: *type), __fc_fopen[0 ..];
+ */
+extern FILE *popen(char const *command, char const *type);
+
+/*@ requires valid_stream: \valid(stream);
+ requires open_pipe: is_open_pipe(stream);
+ ensures closed_stream: ¬is_open_pipe(\old(stream));
+ assigns \result;
+ assigns \result \from (indirect: *stream);
+ */
+extern int pclose(FILE *stream);
+
+ssize_t getline(char **lineptr, size_t *n, FILE *stream);
+
+int asprintf(char **strp, char const *fmt, void * const *__va_params);
+
+/*@ assigns \result;
+ assigns \result \from maj, min; */
+extern dev_t makedev(int maj, int min);
+
+FILE __fc_initial_stdout =
+ {.__fc_FILE_id = (unsigned int)1, .__fc_FILE_data = 0U};
+FILE *__fc_stdout = & __fc_initial_stdout;
+FILE __fc_initial_stderr =
+ {.__fc_FILE_id = (unsigned int)2, .__fc_FILE_data = 0U};
+FILE *__fc_stderr = & __fc_initial_stderr;
+FILE __fc_initial_stdin =
+ {.__fc_FILE_id = (unsigned int)0, .__fc_FILE_data = 0U};
+FILE *__fc_stdin = & __fc_initial_stdin;
+ssize_t getline(char **lineptr, size_t *n, FILE *stream)
+{
+ ssize_t __retres;
+ int tmp;
+ if (! lineptr) goto _LOR;
+ else
+ if (! n) goto _LOR;
+ else
+ if (! stream) {
+ _LOR: {
+ __fc_errno = 22;
+ __retres = -1;
+ goto return_label;
+ }
}
+ tmp = ferror(stream);
+ if (tmp) goto _LOR_0;
+ else {
+ int tmp_0;
+ tmp_0 = feof(stream);
+ if (tmp_0) {
+ _LOR_0: {
+ __retres = -1;
+ goto return_label;
+ }
}
- i += (size_t)1;
- }
- if ((int)*(s1 + i) == 0) {
- if ((int)*(s2 + i) == 0) {
- __retres = 0;
- goto return_label;
- }
- else goto _LAND;
}
- else {
- _LAND: ;
- if ((int)*(s1 + i) == 0) {
- __retres = -1;
- goto return_label;
+ if (! *lineptr) goto _LOR_1;
+ else
+ if (*n == (size_t)0) {
+ _LOR_1:
+ {
+ *lineptr = (char *)malloc((unsigned int)2);
+ if (! lineptr) {
+ __fc_errno = 12;
+ __retres = -1;
+ goto return_label;
+ }
+ *n = (unsigned int)2;
+ }
}
+ size_t cur = (unsigned int)0;
+ while (1) {
+ int tmp_3;
+ tmp_3 = ferror(stream);
+ if (tmp_3) break;
else {
- __retres = 1;
- goto return_label;
+ int tmp_4;
+ tmp_4 = feof(stream);
+ if (tmp_4) break;
+ }
+ {
+ while (cur < *n - (size_t)1) {
+ int tmp_1;
+ tmp_1 = fgetc(stream);
+ char c = (char)tmp_1;
+ if ((int)c == -1)
+ if (cur == (size_t)0) {
+ __retres = -1;
+ goto return_label;
+ }
+ if ((int)c != -1) {
+ size_t tmp_2;
+ tmp_2 = cur;
+ cur += (size_t)1;
+ *(*lineptr + tmp_2) = c;
+ }
+ if ((int)c == '\n') goto _LOR_2;
+ else
+ if ((int)c == -1) {
+ _LOR_2:
+ {
+ *(*lineptr + cur) = (char)'\000';
+ __retres = (int)cur;
+ goto return_label;
+ }
+ }
+ }
+ if (*n == (size_t)2147483647) {
+ __fc_errno = 75;
+ __retres = -1;
+ goto return_label;
+ }
+ size_t new_size = *n + (size_t)1;
+ *lineptr = (char *)realloc((void *)*lineptr,new_size);
+ if (! *lineptr) {
+ __fc_errno = 12;
+ __retres = -1;
+ goto return_label;
+ }
+ *n = new_size;
}
}
+ __retres = -1;
return_label: return __retres;
}
-/*@ requires valid_string_src: valid_read_string(src);
- requires valid_string_dest: valid_string(dest);
- requires room_string: \valid(dest + (0 .. strlen(dest) + strlen(src)));
- ensures
- sum_of_lengths: strlen(\old(dest)) ≡ \old(strlen(dest) + strlen(src));
- ensures
- initialization: dest:
- \initialized(\old(dest) + (0 .. \old(strlen(dest) + strlen(src))));
- ensures
- dest_null_terminated:
- *(\old(dest) + \old(strlen(dest) + strlen(src))) ≡ 0;
- ensures result_ptr: \result ≡ \old(dest);
- assigns *(dest +
- (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src))),
- \result;
- assigns
- *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src)))
- \from *(src + (0 .. strlen{Old}(src)));
- assigns \result \from dest;
+/*@ requires valid_strp: \valid(strp);
+ requires valid_fmt: valid_read_string(fmt);
+ ensures result_error_or_written_byes: \result ≡ -1 ∨ \result ≥ 0;
+ assigns __fc_heap_status, \result, *strp;
+ assigns __fc_heap_status
+ \from (indirect: *(fmt + (0 ..))), __fc_heap_status;
+ assigns \result
+ \from (indirect: *(fmt + (0 ..))), (indirect: __fc_heap_status);
+ assigns *strp \from *(fmt + (0 ..)), (indirect: __fc_heap_status);
+ allocates *\old(strp);
*/
-char *strcat(char *dest, char const *src)
+int asprintf(char **strp, char const *fmt, void * const *__va_params)
{
- size_t i;
- size_t n = strlen((char const *)dest);
- i = (unsigned int)0;
- while ((int)*(src + i) != 0) {
- *(dest + (n + i)) = *(src + i);
- i += (size_t)1;
+ int __retres;
+ va_list args;
+ int tmp;
+ args = __va_params;
+ tmp = Frama_C_interval(1,256);
+ size_t len = (unsigned int)tmp;
+ *strp = (char *)malloc(len);
+ if (! *strp) {
+ __retres = -1;
+ goto return_label;
}
- *(dest + (n + i)) = (char)0;
- return dest;
+ Frama_C_make_unknown(*strp,len - 1U);
+ *(*strp + (len - 1U)) = (char)0;
+ __retres = (int)len;
+ return_label: return __retres;
}
-/*@ requires valid_nstring_src: valid_read_nstring(src, n);
- requires valid_string_dest: valid_string(dest);
- ensures result_ptr: \result ≡ \old(dest);
- assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n)), \result;
- assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n))
- \from *(src + (0 .. n));
- assigns \result \from dest;
+/*@ requires abs_representable: i > -2147483647 - 1;
+ assigns \result;
+ assigns \result \from i;
- behavior complete:
- assumes
- valid_string_src_fits: valid_read_string(src) ∧ strlen(src) ≤ n;
- requires
- room_string: \valid((dest + strlen(dest)) + (0 .. strlen(src)));
- ensures
- sum_of_lengths:
- strlen(\old(dest)) ≡ \old(strlen(dest) + strlen(src));
- assigns *(dest +
- (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src))),
- \result;
- assigns
- *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src)))
- \from *(src + (0 .. strlen{Old}(src)));
- assigns \result \from dest;
+ behavior negative:
+ assumes negative: i < 0;
+ ensures opposite_result: \result ≡ -\old(i);
- behavior partial:
- assumes
- valid_string_src_too_large:
- ¬(valid_read_string(src) ∧ strlen(src) ≤ n);
- requires room_string: \valid((dest + strlen(dest)) + (0 .. n));
- ensures
- sum_of_bounded_lengths:
- strlen(\old(dest)) ≡ \old(strlen(dest)) + \old(n);
- assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n)),
- \result;
- assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n))
- \from *(src + (0 .. strlen{Old}(src)));
- assigns \result \from dest;
- */
-char *strncat(char *dest, char const *src, size_t n)
-{
- size_t i;
- size_t dest_len = strlen((char const *)dest);
- i = (unsigned int)0;
- while (i < n) {
- if ((int)*(src + i) == 0) break;
- *(dest + (dest_len + i)) = *(src + i);
- i += (size_t)1;
- }
- *(dest + (dest_len + i)) = (char)0;
- return dest;
-}
-
-/*@ requires valid_string_src: valid_read_string(src);
- requires room_string: \valid(dest + (0 .. strlen(src)));
- requires
- separation:
- \separated(dest + (0 .. strlen(src)), src + (0 .. strlen(src)));
- ensures equal_contents: strcmp(\old(dest), \old(src)) ≡ 0;
- ensures result_ptr: \result ≡ \old(dest);
- assigns *(dest + (0 .. strlen{Old}(src))), \result;
- assigns *(dest + (0 .. strlen{Old}(src)))
- \from *(src + (0 .. strlen{Old}(src)));
- assigns \result \from dest;
- */
-char *strcpy(char *dest, char const *src)
-{
- size_t i;
- i = (unsigned int)0;
- while ((int)*(src + i) != 0) {
- *(dest + i) = *(src + i);
- i += (size_t)1;
- }
- *(dest + i) = (char)0;
- return dest;
-}
-
-/*@ requires valid_string_src: valid_read_string(src);
- requires room_string: \valid(dest + (0 .. strlen(src)));
- requires
- separation:
- \separated(dest + (0 .. strlen(src)), src + (0 .. strlen(src)));
- ensures equal_contents: strcmp(\old(dest), \old(src)) ≡ 0;
- ensures points_to_end: \result ≡ \old(dest) + strlen(\old(dest));
- assigns *(dest + (0 .. strlen{Old}(src))), \result;
- assigns *(dest + (0 .. strlen{Old}(src)))
- \from *(src + (0 .. strlen{Old}(src)));
- assigns \result \from dest;
- */
-char *stpcpy(char *dest, char const *src)
-{
- char *__retres;
- size_t i;
- i = (unsigned int)0;
- while ((int)*(src + i) != 0) {
- *(dest + i) = *(src + i);
- i += (size_t)1;
+ behavior nonnegative:
+ assumes nonnegative: i ≥ 0;
+ ensures same_result: \result ≡ \old(i);
+
+ complete behaviors nonnegative, negative;
+ disjoint behaviors nonnegative, negative;
+ */
+int abs(int i)
+{
+ int __retres;
+ if (i < 0) {
+ __retres = - i;
+ goto return_label;
}
- *(dest + i) = (char)0;
- __retres = dest + i;
- return __retres;
+ __retres = i;
+ return_label: return __retres;
}
-/*@ requires valid_nstring_src: valid_read_nstring(src, n);
- requires room_nstring: \valid(dest + (0 .. n - 1));
- requires separation: \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
- ensures result_ptr: \result ≡ \old(dest);
- ensures initialization: \initialized(\old(dest) + (0 .. \old(n) - 1));
- assigns *(dest + (0 .. n - 1)), \result;
- assigns *(dest + (0 .. n - 1)) \from *(src + (0 .. n - 1));
- assigns \result \from dest;
-
- behavior complete:
- assumes src_fits: strlen(src) < n;
- ensures equal_after_copy: strcmp(\old(dest), \old(src)) ≡ 0;
-
- behavior partial:
- assumes src_too_long: n ≤ strlen(src);
- ensures
- equal_prefix:
- memcmp{Post, Post}(\old(dest), \old(src), \old(n)) ≡ 0;
+/*@ requires valid_nptr: \valid_read(p);
+ assigns \result;
+ assigns \result \from (indirect: p), (indirect: *(p + (0 ..)));
*/
-char *strncpy(char *dest, char const *src, size_t n)
+int atoi(char const *p)
{
- size_t i;
- i = (unsigned int)0;
- while (i < n) {
- *(dest + i) = *(src + i);
- if ((int)*(src + i) == 0) break;
- i += (size_t)1;
+ int __retres;
+ int n;
+ int c;
+ int tmp_1;
+ int tmp_3;
+ int neg = 0;
+ unsigned char *up = (unsigned char *)p;
+ c = (int)*up;
+ tmp_1 = isdigit(c);
+ if (! tmp_1) {
+ int tmp_0;
+ while (1) {
+ int tmp;
+ tmp = isspace(c);
+ if (! tmp) break;
+ up ++;
+ c = (int)*up;
+ }
+ switch (c) {
+ case '-': neg ++;
+ case '+': { /* sequence */
+ up ++;
+ c = (int)*up;
+ }
+ }
+ tmp_0 = isdigit(c);
+ if (! tmp_0) {
+ __retres = 0;
+ goto return_label;
+ }
}
- while (i < n) {
- *(dest + i) = (char)0;
- i += (size_t)1;
+ n = '0' - c;
+ while (1) {
+ int tmp_2;
+ up ++;
+ c = (int)*up;
+ tmp_2 = isdigit(c);
+ if (! tmp_2) break;
+ n *= 10;
+ n += '0' - c;
}
- return dest;
+ if (neg) tmp_3 = n; else tmp_3 = - n;
+ __retres = tmp_3;
+ return_label: return __retres;
}
-/*@ requires valid_string_s: valid_read_string(s);
- assigns \result;
+/*@ assigns __fc_heap_status, \result;
+ assigns __fc_heap_status
+ \from (indirect: nmemb), (indirect: size), __fc_heap_status;
assigns \result
- \from s, (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: c);
+ \from (indirect: nmemb), (indirect: size), (indirect: __fc_heap_status);
+ allocates \result;
- behavior found:
- assumes char_found: strchr(s, c) ≡ \true;
- ensures result_char: *\result ≡ (char)\old(c);
- ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
+ behavior allocation:
+ assumes can_allocate: is_allocable(nmemb * size);
ensures
- result_in_length: \old(s) ≤ \result ≤ \old(s) + strlen(\old(s));
- ensures result_valid_string: valid_read_string(\result);
+ allocation: \fresh{Old, Here}(\result,\old(nmemb) * \old(size));
ensures
- result_first_occur:
- ∀ char *p; \old(s) ≤ p < \result ⇒ *p ≢ (char)\old(c);
+ initialization:
+ \initialized((char *)\result + (0 .. \old(nmemb) * \old(size) - 1));
+ ensures
+ zero_initialization:
+ \subset(*((char *)\result + (0 .. \old(nmemb) * \old(size) - 1)),
+ {0});
- behavior not_found:
- assumes char_not_found: ¬(strchr(s, c) ≡ \true);
- ensures result_null: \result ≡ \null;
+ behavior no_allocation:
+ assumes cannot_allocate: ¬is_allocable(nmemb * size);
+ ensures null_result: \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
- behavior default:
- ensures
- result_null_or_same_base:
- \result ≡ \null ∨ \base_addr(\result) ≡ \base_addr(\old(s));
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
*/
-char *strchr(char const *s, int c)
+void *calloc(size_t nmemb, size_t size)
{
- char *__retres;
- size_t i;
- char const ch = (char)c;
- i = (unsigned int)0;
- while ((int)*(s + i) != (int)ch) {
- if ((int)*(s + i) == 0) {
- __retres = (char *)0;
+ void *__retres;
+ size_t l = nmemb * size;
+ if (size != (size_t)0)
+ if (l / size != nmemb) {
+ __retres = (void *)0;
goto return_label;
}
- i += (size_t)1;
- }
- __retres = (char *)(s + i);
+ char *p = malloc(l);
+ if (p) memset((void *)p,0,l);
+ __retres = (void *)p;
return_label: return __retres;
}
-/*@ requires valid_string_s: valid_read_string(s);
- assigns \result;
- assigns \result \from s, *(s + (0 ..)), c;
-
- behavior found:
- assumes char_found: strchr(s, c) ≡ \true;
- ensures result_char: (int)*\result ≡ \old(c);
- ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
- ensures result_valid_string: valid_read_string(\result);
-
- behavior not_found:
- assumes char_not_found: ¬(strchr(s, c) ≡ \true);
- ensures result_null: \result ≡ \null;
-
- behavior default:
- ensures
- result_null_or_same_base:
- \result ≡ \null ∨ \base_addr(\result) ≡ \base_addr(\old(s));
- */
-char *strrchr(char const *s, int c)
+static char __fc_env_strings[64];
+static char __fc_initenv_init;
+static void __fc_initenv(void)
{
- char *__retres;
- char const ch = (char)c;
- {
- size_t tmp;
- tmp = strlen(s);
- size_t i = tmp + (size_t)1;
- while (i > (size_t)0) {
- if ((int)*(s + (i - (size_t)1)) == (int)ch) {
- __retres = (char *)(s + (i - (size_t)1));
- goto return_label;
+ if (! __fc_initenv_init) {
+ Frama_C_make_unknown(__fc_env_strings,(unsigned int)(64 - 1));
+ {
+ int i = 0;
+ while (i < 4096) {
+ {
+ int tmp;
+ tmp = Frama_C_interval(0,64 - 1);
+ __fc_env[i] = & __fc_env_strings[tmp];
+ }
+ i ++;
}
- i -= (size_t)1;
}
+ __fc_initenv_init = (char)1;
}
- __retres = (char *)0;
- return_label: return __retres;
+ return;
}
-/*@ requires
- valid:
- valid_read_or_empty(s, n) ∨
- \valid_read((unsigned char *)s + (0 .. memchr_off((char *)s, c, n)));
- requires
- initialization:
- \initialized((unsigned char *)s + (0 .. n - 1)) ∨
- \initialized((unsigned char *)s + (0 .. memchr_off((char *)s, c, n)));
- requires
- danglingness:
- non_escaping(s, n) ∨
- non_escaping(s, (unsigned int)(memchr_off((char *)s, c, n) + 1));
+/*@ requires valid_name: valid_read_string(name);
+ ensures null_or_valid_result: \result ≡ \null ∨ \valid(\result);
assigns \result;
- assigns \result \from s, c, *((unsigned char *)s + (0 .. n - 1));
-
- behavior found:
- assumes char_found: memchr((char *)s, c, n) ≡ \true;
- ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
- ensures result_char: (int)*((char *)\result) ≡ \old(c);
- ensures
- result_in_str:
- ∀ ℤ i;
- 0 ≤ i < \old(n) ⇒
- *((unsigned char *)\old(s) + i) ≡ \old(c) ⇒
- (unsigned char *)\result ≤ (unsigned char *)\old(s) + i;
-
- behavior not_found:
- assumes char_not_found: ¬(memchr((char *)s, c, n) ≡ \true);
- ensures result_null: \result ≡ \null;
+ assigns \result \from __fc_env[0 ..], (indirect: name), *(name + (0 ..));
*/
-void *memchr(void const *s, int c, size_t n)
+char *getenv(char const *name)
{
- void *__retres;
- unsigned char const ch = (unsigned char)c;
- unsigned char const *ss = (unsigned char const *)s;
- {
- size_t i = (unsigned int)0;
- while (i < n) {
- if ((int)*(ss + i) == (int)ch) {
- __retres = (void *)(ss + i);
- goto return_label;
- }
- i += (size_t)1;
- }
+ char *__retres;
+ int tmp_0;
+ /*@ assert ¬(strchr(name, '=') ≡ \true); */ ;
+ __fc_initenv();
+ tmp_0 = Frama_C_nondet(0,1);
+ if (tmp_0) {
+ int tmp;
+ tmp = Frama_C_interval(0,4096 - 1);
+ ;
+ __retres = __fc_env[tmp];
+ goto return_label;
+ }
+ else {
+ __retres = (char *)0;
+ goto return_label;
}
- __retres = (void *)0;
return_label: return __retres;
}
-void *memrchr(void const *s, int c, size_t n)
+/*@ requires valid_string: valid_read_string(string);
+ assigns __fc_env[0 ..], \result;
+ assigns __fc_env[0 ..] \from __fc_env[0 ..], string;
+ assigns \result \from (indirect: __fc_env[0 ..]), (indirect: string);
+ */
+int putenv(char *string)
{
- void *__retres;
- unsigned char const ch = (unsigned char)c;
- unsigned char const *ss = (unsigned char const *)s;
- {
- size_t i = n;
- while (i > (size_t)0) {
- if ((int)*(ss + (i - (size_t)1)) == (int)ch) {
- __retres = (void *)(ss + (i - (size_t)1));
- goto return_label;
- }
- i -= (size_t)1;
+ int __retres;
+ int tmp_3;
+ char *separator __attribute__((__unused__)) =
+ strchr((char const *)string,'=');
+ /*@ assert string_contains_separator: separator ≢ \null; */ ;
+ /*@ assert name_is_not_empty: separator ≢ string; */ ;
+ __fc_initenv();
+ tmp_3 = Frama_C_nondet(0,1);
+ if (tmp_3) {
+ int tmp_1;
+ int tmp_2;
+ tmp_1 = Frama_C_nondet(0,1);
+ if (tmp_1) {
+ int tmp_0;
+ tmp_0 = Frama_C_interval(-2147483647 - 1,2147483647);
+ __retres = tmp_0;
+ goto return_label;
}
+ tmp_2 = Frama_C_interval(0,4096 - 1);
+ __fc_env[tmp_2] = string;
}
- __retres = (void *)0;
+ __retres = 0;
return_label: return __retres;
}
-/*@ requires valid_string_haystack: valid_read_string(haystack);
- requires valid_string_needle: valid_read_string(needle);
- ensures
- result_null_or_in_haystack:
- \result ≡ \null ∨
- (\subset(\result, \old(haystack) + (0 ..)) ∧
- \valid_read(\result) ∧
- memcmp{Pre, Pre}(\result, \old(needle), strlen(\old(needle))) ≡ 0);
- assigns \result;
+/*@ requires valid_name: valid_read_string(name);
+ requires valid_value: valid_read_string(value);
+ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+ assigns \result, __fc_env[0 ..];
assigns \result
- \from haystack, (indirect: *(haystack + (0 ..))),
- (indirect: *(needle + (0 ..)));
+ \from __fc_env[0 ..], (indirect: name), (indirect: *(name + (0 ..))),
+ (indirect: value), (indirect: *(value + (0 ..))),
+ (indirect: overwrite);
+ assigns __fc_env[0 ..]
+ \from __fc_env[0 ..], (indirect: name), (indirect: *(name + (0 ..))),
+ (indirect: value), (indirect: *(value + (0 ..))),
+ (indirect: overwrite);
*/
-char *strstr(char const *haystack, char const *needle)
+int setenv(char const *name, char const *value, int overwrite)
{
- char *__retres;
- if ((int)*(needle + 0) == 0) {
- __retres = (char *)haystack;
+ int __retres;
+ char *tmp;
+ int tmp_4;
+ tmp = strchr(name,'=');
+ if (tmp) {
+ __retres = -1;
goto return_label;
}
- {
- size_t i = (unsigned int)0;
- while ((int)*(haystack + i) != 0) {
- {
- size_t j;
- j = (unsigned int)0;
- while ((int)*(haystack + (i + j)) != 0) {
- if ((int)*(haystack + (i + j)) != (int)*(needle + j)) break;
- j += (size_t)1;
- }
- if ((int)*(needle + j) == 0) {
- __retres = (char *)(haystack + i);
- goto return_label;
- }
- }
- i += (size_t)1;
- }
+ size_t namelen = strlen(name);
+ if (namelen == (size_t)0) {
+ __retres = -1;
+ goto return_label;
+ }
+ __fc_initenv();
+ tmp_4 = Frama_C_nondet(0,1);
+ if (tmp_4) {
+ __retres = -1;
+ goto return_label;
+ }
+ else {
+ int tmp_1;
+ int tmp_2;
+ int tmp_3;
+ tmp_1 = Frama_C_nondet(0,1);
+ if (tmp_1) Frama_C_make_unknown(__fc_env_strings,(unsigned int)(64 - 1));
+ tmp_2 = Frama_C_interval(0,4096 - 1);
+ tmp_3 = Frama_C_interval(0,64 - 1);
+ __fc_env[tmp_2] = & __fc_env_strings[tmp_3];
+ __retres = 0;
+ goto return_label;
}
- __retres = (char *)0;
return_label: return __retres;
}
-static int strerror___fc_strerror_init;
-/*@ ensures result_internal_str: \result ≡ __fc_p_strerror;
- ensures result_nul_terminated: *(\result + 63) ≡ 0;
- ensures result_valid_string: valid_read_string(\result);
- assigns \result;
- assigns \result \from __fc_p_strerror, (indirect: errnum);
+/*@ requires valid_name: valid_read_string(name);
+ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+ assigns \result, __fc_env[0 ..];
+ assigns \result
+ \from __fc_env[0 ..], (indirect: name), (indirect: *(name + (0 ..)));
+ assigns __fc_env[0 ..]
+ \from __fc_env[0 ..], (indirect: name), (indirect: *(name + (0 ..)));
*/
-char *strerror(int errnum)
+int unsetenv(char const *name)
{
- char *__retres;
- if (! strerror___fc_strerror_init) {
- Frama_C_make_unknown(__fc_strerror,(unsigned int)63);
- __fc_strerror[63] = (char)0;
- strerror___fc_strerror_init = 1;
+ int __retres;
+ char *tmp;
+ int tmp_2;
+ tmp = strchr(name,'=');
+ if (tmp) {
+ __retres = -1;
+ goto return_label;
}
- __retres = __fc_strerror;
- return __retres;
+ size_t namelen = strlen(name);
+ if (namelen == (size_t)0) {
+ __retres = -1;
+ goto return_label;
+ }
+ __fc_initenv();
+ tmp_2 = Frama_C_nondet(0,1);
+ if (tmp_2) {
+ int tmp_1;
+ tmp_1 = Frama_C_interval(0,4096 - 1);
+ __fc_env[tmp_1] = (char *)0;
+ }
+ __retres = 0;
+ return_label: return __retres;
}
-/*@ requires valid_string_s: valid_read_string(s);
- assigns \result;
+/*@ requires valid_memptr: \valid(memptr);
+ requires
+ alignment_is_a_suitable_power_of_two:
+ alignment ≥ sizeof(void *) ∧
+ ((size_t)alignment & ((size_t)alignment - 1)) ≡ 0;
+ assigns __fc_heap_status, \result;
+ assigns __fc_heap_status
+ \from (indirect: alignment), size, __fc_heap_status;
assigns \result
- \from (indirect: *(s + (0 .. strlen{Old}(s)))),
+ \from (indirect: alignment), (indirect: size),
(indirect: __fc_heap_status);
- allocates \result;
+ allocates *\old(memptr);
behavior allocation:
- assumes can_allocate: is_allocable(strlen(s));
- ensures allocation: \fresh{Old, Here}(\result,strlen(\old(s)));
- ensures
- result_valid_string_and_same_contents:
- valid_string(\result) ∧ strcmp(\result, \old(s)) ≡ 0;
+ assumes can_allocate: is_allocable(size);
+ ensures allocation: \fresh{Old, Here}(*\old(memptr),\old(size));
+ ensures result_zero: \result ≡ 0;
assigns __fc_heap_status, \result;
- assigns __fc_heap_status \from (indirect: s), __fc_heap_status;
+ assigns __fc_heap_status
+ \from (indirect: alignment), size, __fc_heap_status;
assigns \result
- \from (indirect: *(s + (0 .. strlen{Old}(s)))),
+ \from (indirect: alignment), (indirect: size),
(indirect: __fc_heap_status);
behavior no_allocation:
- assumes cannot_allocate: ¬is_allocable(strlen(s));
- ensures result_null: \result ≡ \null;
+ assumes cannot_allocate: ¬is_allocable(size);
+ ensures result_non_zero: \result < 0 ∨ \result > 0;
assigns \result;
- assigns \result \from \nothing;
+ assigns \result \from (indirect: alignment);
allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
*/
-char *strdup(char const *s)
+int posix_memalign(void **memptr, size_t alignment, size_t size)
{
- char *__retres;
- size_t tmp;
- tmp = strlen(s);
- size_t l = tmp + (size_t)1;
- char *p = malloc(l);
- if (! p) {
- __fc_errno = 12;
- __retres = (char *)0;
+ int __retres;
+ /*@
+ assert
+ alignment_is_a_suitable_power_of_two:
+ alignment ≥ sizeof(void *) ∧
+ ((size_t)alignment & ((size_t)alignment - 1)) ≡ 0;
+ */
+ ;
+ *memptr = malloc(size);
+ if (! *memptr) {
+ __retres = 12;
goto return_label;
}
- memcpy((void *)p,(void const *)s,l);
- __retres = p;
+ __retres = 0;
return_label: return __retres;
}
-/*@ requires valid_string_s: valid_read_string(s);
- assigns \result;
- assigns \result
- \from (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: n),
- (indirect: __fc_heap_status);
- allocates \result;
-
- behavior allocation:
- assumes can_allocate: is_allocable(\min(strlen(s), n + 1));
- ensures
- allocation:
- \fresh{Old, Here}(\result,\min(strlen(\old(s)), \old(n) + 1));
- ensures
- result_valid_string_bounded_and_same_prefix:
- \valid(\result + (0 .. \min(strlen(\old(s)), \old(n)))) ∧
- valid_string(\result) ∧ strlen(\result) ≤ \old(n) ∧
- strncmp(\result, \old(s), \old(n)) ≡ 0;
- assigns __fc_heap_status, \result;
- assigns __fc_heap_status
- \from (indirect: s), (indirect: n), __fc_heap_status;
- assigns \result
- \from (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: n),
- (indirect: __fc_heap_status);
-
- behavior no_allocation:
- assumes cannot_allocate: ¬is_allocable(\min(strlen(s), n + 1));
- ensures result_null: \result ≡ \null;
- assigns \result;
- assigns \result \from \nothing;
- allocates \nothing;
- */
-char *strndup(char const *s, size_t n)
+char *realpath(char const * restrict file_name, char * restrict resolved_name)
{
char *__retres;
- size_t l;
- l = (unsigned int)0;
- while (l < n) {
- if ((int)*(s + l) == 0) break;
- l += (size_t)1;
+ int tmp;
+ if (! file_name) {
+ __fc_errno = 22;
+ __retres = (char *)0;
+ goto return_label;
}
- char *p = malloc(l + (size_t)1);
- if (! p) {
- __fc_errno = 12;
+ tmp = Frama_C_interval(0,6);
+ switch (tmp) {
+ case 0: __fc_errno = 13;
+ __retres = (char *)0;
+ goto return_label;
+ case 1: __fc_errno = 5;
+ __retres = (char *)0;
+ goto return_label;
+ case 2: __fc_errno = 40;
__retres = (char *)0;
goto return_label;
+ case 3: __fc_errno = 36;
+ __retres = (char *)0;
+ goto return_label;
+ case 4: __fc_errno = 2;
+ __retres = (char *)0;
+ goto return_label;
+ case 5: __fc_errno = 20;
+ __retres = (char *)0;
+ goto return_label;
+ default: break;
}
- memcpy((void *)p,(void const *)s,l);
- *(p + l) = (char)0;
- __retres = p;
+ int realpath_len = Frama_C_interval(1,256);
+ if (! resolved_name) {
+ resolved_name = (char *)malloc((unsigned int)256);
+ if (! resolved_name) {
+ __fc_errno = 12;
+ __retres = (char *)0;
+ goto return_label;
+ }
+ }
+ Frama_C_make_unknown(resolved_name,(unsigned int)realpath_len);
+ *(resolved_name + (realpath_len - 1)) = (char)'\000';
+ __retres = resolved_name;
return_label: return __retres;
}
-static int strsignal___fc_strsignal_init;
-/*@ ensures result_internal_str: \result ≡ __fc_p_strsignal;
- ensures result_nul_terminated: *(\result + 63) ≡ 0;
- ensures result_valid_string: valid_read_string(\result);
- assigns \result;
- assigns \result \from __fc_p_strsignal, (indirect: signum);
+/*@ requires valid_dest: valid_or_empty(dest, n);
+ requires valid_src: valid_read_or_empty(src, n);
+ requires
+ separation:
+ \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1));
+ ensures
+ copied_contents:
+ memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡
+ 0;
+ ensures result_ptr: \result ≡ \old(dest);
+ assigns *((char *)dest + (0 .. n - 1)), \result;
+ assigns *((char *)dest + (0 .. n - 1))
+ \from *((char *)src + (0 .. n - 1));
+ assigns \result \from dest;
*/
-char *strsignal(int signum)
+void *memcpy(void * restrict dest, void const * restrict src, size_t n)
{
- char *__retres;
- if (! strsignal___fc_strsignal_init) {
- Frama_C_make_unknown(__fc_strsignal,(unsigned int)63);
- __fc_strsignal[63] = (char)0;
- strsignal___fc_strsignal_init = 1;
+ {
+ size_t i = (unsigned int)0;
+ /*@ loop invariant no_eva: 0 ≤ i ≤ n;
+ loop invariant
+ no_eva:
+ ∀ ℤ k;
+ 0 ≤ k < i ⇒ *((char *)dest + k) ≡ *((char *)src + k);
+ loop assigns i, *((char *)dest + (0 .. n - 1));
+ loop variant n - i;
+ */
+ while (i < n) {
+ *((char *)dest + i) = *((char *)src + i);
+ i += (size_t)1;
+ }
}
- __retres = __fc_strsignal;
- return __retres;
+ return dest;
}
-/*@ ghost unsigned int volatile __fc_time; */
-/*@ assigns \result;
- assigns \result \from __fc_time; */
-extern clock_t clock(void);
-
-/*@ assigns \result;
- assigns \result \from time1, time0; */
-extern double difftime(time_t time1, time_t time0);
-
-/*@ requires valid_timeptr: \valid(timeptr);
- assigns *timeptr, \result;
- assigns *timeptr \from *timeptr;
- assigns \result \from (indirect: *timeptr);
+/*@ requires valid_dest: valid_or_empty(dest, n);
+ requires valid_src: valid_read_or_empty(src, n);
+ requires
+ separation:
+ \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1));
+ ensures
+ copied_contents:
+ memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡
+ 0;
+ ensures result_next_byte: \result ≡ \old(dest) + \old(n);
+ assigns *((char *)dest + (0 .. n - 1)), \result;
+ assigns *((char *)dest + (0 .. n - 1))
+ \from *((char *)src + (0 .. n - 1));
+ assigns \result \from dest, n;
*/
-extern time_t mktime(struct tm *timeptr);
+void *mempcpy(void * restrict dest, void const * restrict src, size_t n)
+{
+ void *__retres;
+ size_t i;
+ i = (unsigned int)0;
+ /*@ loop invariant no_eva: 0 ≤ i ≤ n;
+ loop invariant
+ no_eva:
+ ∀ ℤ k;
+ 0 ≤ k < i ⇒ *((char *)dest + k) ≡ *((char *)src + k);
+ loop assigns i, *((char *)dest + (0 .. n - 1));
+ loop variant n - i;
+ */
+ while (i < n) {
+ *((char *)dest + i) = *((char *)src + i);
+ i += (size_t)1;
+ }
+ __retres = (void *)((char *)dest + i);
+ return __retres;
+}
-/*@ assigns *timer, \result;
- assigns *timer \from __fc_time;
- assigns \result \from __fc_time;
+/*@ assigns \result;
+ assigns \result \from (indirect: p), (indirect: q), (indirect: n);
- behavior null:
- assumes timer_null: timer ≡ \null;
- assigns \result;
- assigns \result \from __fc_time;
+ behavior separated:
+ assumes
+ separation: no_overlap:
+ \separated(p + (0 .. n - 1), q + (0 .. n - 1));
+ ensures result_no_overlap: \result ≡ 0;
- behavior not_null:
- assumes timer_non_null: timer ≢ \null;
- requires valid_timer: \valid(timer);
- ensures initialization: timer: \initialized(\old(timer));
- assigns *timer, \result;
- assigns *timer \from __fc_time;
- assigns \result \from __fc_time;
+ behavior not_separated_lt:
+ assumes
+ separation: overlap: ¬\separated(p + (0 .. n - 1), q + (0 .. n - 1));
+ assumes p_before_q: p ≤ q < p + n;
+ ensures result_p_before_q: \result ≡ -1;
- complete behaviors not_null, null;
- disjoint behaviors not_null, null;
- */
-extern time_t time(time_t *timer);
-
-char __fc_ctime[26];
-char * const __fc_p_ctime = __fc_ctime;
-/*@ requires valid_timeptr: \valid_read(timeptr);
- requires initialization: init_timeptr: \initialized(timeptr);
- ensures result_points_to_ctime: \result ≡ __fc_p_ctime;
- ensures result_valid_string: valid_read_string(__fc_p_ctime);
- assigns __fc_ctime[0 .. 25], \result;
- assigns __fc_ctime[0 .. 25]
- \from (indirect: *timeptr), (indirect: __fc_time);
- assigns \result
- \from (indirect: *timeptr), (indirect: __fc_time), __fc_p_ctime;
+ behavior not_separated_gt:
+ assumes
+ separation: overlap: ¬\separated(p + (0 .. n - 1), q + (0 .. n - 1));
+ assumes p_after_q: q < p ≤ q + n;
+ ensures result_p_after_q: \result ≡ 1;
+
+ complete behaviors not_separated_gt, not_separated_lt, separated;
+ disjoint behaviors not_separated_gt, not_separated_lt, separated;
*/
-extern char *asctime(struct tm const *timeptr);
+static int memoverlap(char const *p, char const *q, size_t n)
+{
+ int __retres;
+ uintptr_t p1 = (unsigned int)p;
+ uintptr_t p2 = (unsigned int)(p + n);
+ uintptr_t q1 = (unsigned int)q;
+ uintptr_t q2 = (unsigned int)(q + n);
+ if (p1 <= q1) {
+ if (p2 > q1) {
+ __retres = -1;
+ goto return_label;
+ }
+ else goto _LAND;
+ }
+ else {
+ _LAND: ;
+ if (q1 <= p1)
+ if (q2 > p1) {
+ __retres = 1;
+ goto return_label;
+ }
+ else {
+ __retres = 0;
+ goto return_label;
+ }
+ else {
+ __retres = 0;
+ goto return_label;
+ }
+ }
+ return_label: return __retres;
+}
-/*@ requires valid_timer: \valid_read(timer);
- requires initialization: init_timer: \initialized(timer);
- ensures result_points_to_ctime: \result ≡ __fc_p_ctime;
- ensures result_valid_string: valid_read_string(__fc_p_ctime);
- assigns __fc_ctime[0 .. 25], \result;
- assigns __fc_ctime[0 .. 25]
- \from (indirect: *timer), (indirect: __fc_time);
- assigns \result
- \from (indirect: *timer), (indirect: __fc_time), __fc_p_ctime;
+/*@ requires valid_dest: valid_or_empty(dest, n);
+ requires valid_src: valid_read_or_empty(src, n);
+ ensures
+ copied_contents:
+ memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡
+ 0;
+ ensures result_ptr: \result ≡ \old(dest);
+ assigns *((char *)dest + (0 .. n - 1)), \result;
+ assigns *((char *)dest + (0 .. n - 1))
+ \from *((char *)src + (0 .. n - 1));
+ assigns \result \from dest;
*/
-extern char *ctime(time_t const *timer);
+void *memmove(void *dest, void const *src, size_t n)
+{
+ void *__retres;
+ int tmp;
+ if (n == (size_t)0) {
+ __retres = dest;
+ goto return_label;
+ }
+ char *s = (char *)src;
+ char *d = (char *)dest;
+ tmp = memoverlap((char const *)dest,(char const *)src,n);
+ if (tmp <= 0) {
+ size_t i = (unsigned int)0;
+ /*@ loop invariant no_eva: 0 ≤ i ≤ n;
+ loop invariant
+ no_eva:
+ ∀ ℤ k;
+ 0 ≤ k < i ⇒
+ *((char *)dest + k) ≡ \at(*((char *)src + k),LoopEntry);
+ loop invariant
+ no_eva:
+ ∀ ℤ k;
+ i ≤ k < n ⇒
+ *((char *)src + k) ≡ \at(*((char *)src + k),LoopEntry);
+ loop assigns i, *((char *)dest + (0 .. n - 1));
+ loop variant n - i;
+ */
+ while (i < n) {
+ *(d + i) = *(s + i);
+ i += (size_t)1;
+ }
+ }
+ else {
+ {
+ size_t i_0 = n - (size_t)1;
+ /*@ loop invariant no_eva: 0 ≤ i_0 < n;
+ loop invariant
+ no_eva:
+ ∀ ℤ k;
+ i_0 < k < n ⇒
+ *((char *)dest + k) ≡ \at(*((char *)src + k),LoopEntry);
+ loop invariant
+ no_eva:
+ ∀ ℤ k;
+ 0 ≤ k ≤ i_0 ⇒
+ *((char *)src + k) ≡ \at(*((char *)src + k),LoopEntry);
+ loop assigns i_0, *((char *)dest + (0 .. n - 1));
+ loop variant i_0;
+ */
+ while (i_0 > (size_t)0) {
+ *(d + i_0) = *(s + i_0);
+ i_0 -= (size_t)1;
+ }
+ }
+ *(d + 0) = *(s + 0);
+ }
+ __retres = dest;
+ return_label: return __retres;
+}
-struct tm __fc_time_tm;
-struct tm * const __fc_p_time_tm = & __fc_time_tm;
-/*@ requires valid_timer: \valid_read(timer);
- ensures
- result_null_or_internal_tm:
- \result ≡ &__fc_time_tm ∨ \result ≡ \null;
- assigns \result, __fc_time_tm;
- assigns \result \from __fc_p_time_tm;
- assigns __fc_time_tm \from *timer;
+/*@ requires valid_string_s: valid_read_string(s);
+ ensures acsl_c_equiv: \result ≡ strlen(\old(s));
+ assigns \result;
+ assigns \result \from (indirect: *(s + (0 ..)));
*/
-extern struct tm *gmtime(time_t const *timer);
+size_t strlen(char const *s)
+{
+ size_t i;
+ i = (unsigned int)0;
+ while ((int)*(s + i) != 0) i += (size_t)1;
+ return i;
+}
-/*@ requires valid_timer: \valid_read(timer);
+/*@ requires valid_string_s: valid_read_nstring(s, maxlen);
ensures
- result_null_or_internal_tm:
- \result ≡ &__fc_time_tm ∨ \result ≡ \null;
- assigns \result, __fc_time_tm;
- assigns \result \from __fc_p_time_tm;
- assigns __fc_time_tm \from *timer;
- */
-extern struct tm *localtime(time_t const *timer);
-
-/*@ requires dst_has_room: \valid(s + (0 .. max - 1));
- requires valid_format: valid_read_string(format);
- requires valid_tm: \valid_read(tm);
- ensures result_bounded: \result ≤ \old(max);
- assigns *(s + (0 .. max - 1)), \result;
- assigns *(s + (0 .. max - 1))
- \from (indirect: max), (indirect: *(format + (0 ..))), (indirect: *tm);
+ result_bounded:
+ \result ≡ strlen(\old(s)) ∨ \result ≡ \old(maxlen);
+ assigns \result;
assigns \result
- \from (indirect: max), (indirect: *(format + (0 ..))), (indirect: *tm);
+ \from (indirect: *(s + (0 .. maxlen - 1))), (indirect: maxlen);
*/
-extern size_t strftime(char * restrict s, size_t max,
- char const * restrict format,
- struct tm const * restrict tm);
+size_t strnlen(char const *s, size_t maxlen)
+{
+ size_t i;
+ i = (unsigned int)0;
+ while (1) {
+ if (i < maxlen) {
+ if (! ((int)*(s + i) != 0)) break;
+ }
+ else break;
+ i += (size_t)1;
+ }
+ return i;
+}
-/*@ requires tp: \valid(tp);
- assigns \result, *tp, __fc_time;
- assigns \result \from __fc_time;
- assigns *tp \from __fc_time;
- assigns __fc_time \from __fc_time;
-
- behavior realtime_clock:
- assumes realtime: clk_id ≡ 666;
- ensures success: \result ≡ 0;
- ensures initialization: \initialized(\old(tp));
-
- behavior monotonic_clock:
- assumes monotonic: clk_id ≡ 1;
- ensures success: \result ≡ 0;
- ensures initialization: \initialized(\old(tp));
-
- behavior bad_clock_id:
- assumes bad_id: clk_id ≢ 666 ∧ clk_id ≢ 1;
- ensures error: \result ≡ 22;
- assigns \result;
- assigns \result \from clk_id;
-
- complete behaviors bad_clock_id, monotonic_clock, realtime_clock;
- disjoint behaviors bad_clock_id, monotonic_clock, realtime_clock;
+/*@ requires valid_s: valid_or_empty(s, n);
+ ensures
+ acsl_c_equiv: memset((char *)\old(s), \old(c), \old(n)) ≡ \true;
+ ensures result_ptr: \result ≡ \old(s);
+ assigns *((char *)s + (0 .. n - 1)), \result;
+ assigns *((char *)s + (0 .. n - 1)) \from c;
+ assigns \result \from s;
*/
-extern int clock_gettime(clockid_t clk_id, struct timespec *tp);
-
-/*@
-axiomatic nanosleep_predicates {
- predicate abs_clock_in_range{L}(clockid_t id, struct timespec *tm)
- reads __fc_time;
-
- predicate valid_clock_id{L}(clockid_t id)
- reads __fc_time;
-
+void *memset(void *s, int c, size_t n)
+{
+ unsigned char *p = (unsigned char *)s;
+ {
+ size_t i = (unsigned int)0;
+ while (i < n) {
+ *(p + i) = (unsigned char)c;
+ i += (size_t)1;
+ }
}
+ return s;
+}
-*/
-/*@ ghost int volatile __fc_interrupted; */
-/*@ requires valid_request: \valid_read(rqtp);
- requires
- initialization: initialized_request:
- \initialized(&rqtp->tv_sec) ∧ \initialized(&rqtp->tv_nsec);
- requires valid_nanosecs: 0 ≤ rqtp->tv_nsec < 1000000000;
- requires valid_remaining_or_null: rmtp ≡ \null ∨ \valid(rmtp);
+/*@ requires valid_string_s1: valid_read_string(s1);
+ requires valid_string_s2: valid_read_string(s2);
+ ensures acsl_c_equiv: \result ≡ strcmp(\old(s1), \old(s2));
assigns \result;
assigns \result
- \from (indirect: __fc_time), (indirect: __fc_interrupted),
- (indirect: clock_id), (indirect: flags), (indirect: rqtp),
- (indirect: *rqtp);
-
- behavior absolute:
- assumes absolute_time: (flags & 1) ≢ 0;
- assumes
- no_einval:
- abs_clock_in_range(clock_id, rqtp) ∧ valid_clock_id(clock_id);
- ensures
- result_ok_or_error:
- \result ≡ 0 ∨ \result ≡ 4 ∨ \result ≡ 22 ∨
- \result ≡ 95;
- assigns \result;
- assigns \result
- \from (indirect: __fc_time), (indirect: __fc_interrupted),
- (indirect: clock_id), (indirect: rqtp), (indirect: *rqtp);
-
- behavior relative_interrupted:
- assumes relative_time: (flags & 1) ≡ 0;
- assumes interrupted: __fc_interrupted ≢ 0;
- assumes no_einval: valid_clock_id(clock_id);
- ensures result_interrupted: \result ≡ 4;
- ensures
- initialization: interrupted_remaining:
- \old(rmtp) ≢ \null ⇒
- \initialized(&\old(rmtp)->tv_sec) ∧
- \initialized(&\old(rmtp)->tv_nsec);
- ensures
- interrupted_remaining_decreases:
- \old(rmtp) ≢ \null ⇒
- \old(rqtp)->tv_sec * 1000000000 + \old(rqtp)->tv_nsec ≥
- \old(rmtp)->tv_sec * 1000000000 + \old(rmtp)->tv_nsec;
- ensures
- remaining_valid:
- \old(rmtp) ≢ \null ⇒ 0 ≤ \old(rmtp)->tv_nsec < 1000000000;
- assigns \result, *rmtp;
- assigns \result
- \from (indirect: __fc_time), (indirect: clock_id), (indirect: rqtp),
- (indirect: *rqtp);
- assigns *rmtp
- \from __fc_time, (indirect: clock_id), (indirect: rqtp),
- (indirect: *rqtp), (indirect: rmtp);
-
- behavior relative_no_error:
- assumes relative_time: (flags & 1) ≡ 0;
- assumes not_interrupted: __fc_interrupted ≡ 0;
- assumes no_einval: valid_clock_id(clock_id);
- ensures result_ok: \result ≡ 0;
- assigns \result;
- assigns \result
- \from (indirect: __fc_time), (indirect: clock_id), (indirect: rqtp),
- (indirect: *rqtp);
-
- behavior relative_invalid_clock_id:
- assumes relative_time: (flags & 1) ≡ 0;
- assumes not_interrupted: __fc_interrupted ≡ 0;
- assumes einval: ¬valid_clock_id(clock_id);
- ensures result_einval: \result ≡ 22;
- assigns \result;
- assigns \result
- \from (indirect: __fc_time), (indirect: clock_id), (indirect: rqtp),
- (indirect: *rqtp);
-
- complete behaviors relative_invalid_clock_id,
- relative_no_error,
- relative_interrupted,
- absolute;
- disjoint behaviors relative_invalid_clock_id,
- relative_no_error,
- relative_interrupted,
- absolute;
+ \from (indirect: *(s1 + (0 ..))), (indirect: *(s2 + (0 ..)));
*/
-extern int clock_nanosleep(clockid_t clock_id, int flags,
- struct timespec const *rqtp, struct timespec *rmtp);
-
-/*@ requires valid_timer: \valid_read(timer);
- requires valid_result: \valid(result);
- ensures
- result_null_or_result: \result ≡ \old(result) ∨ \result ≡ \null;
- assigns \result, *result;
- assigns \result \from (indirect: *timer), result;
- assigns *result \from (indirect: *timer);
+int strcmp(char const *s1, char const *s2)
+{
+ int __retres;
+ size_t i;
+ i = (unsigned int)0;
+ while ((int)*(s1 + i) == (int)*(s2 + i)) {
+ if ((int)*(s1 + i) == 0) {
+ __retres = 0;
+ goto return_label;
+ }
+ i += (size_t)1;
+ }
+ __retres = (int)*((unsigned char *)s1 + i) - (int)*((unsigned char *)s2 + i);
+ return_label: return __retres;
+}
+
+/*@ requires valid_string_s1: valid_read_nstring(s1, n);
+ requires valid_string_s2: valid_read_nstring(s2, n);
+ ensures acsl_c_equiv: \result ≡ strncmp(\old(s1), \old(s2), \old(n));
+ assigns \result;
+ assigns \result
+ \from (indirect: *(s1 + (0 .. n - 1))),
+ (indirect: *(s2 + (0 .. n - 1))), (indirect: n);
*/
-extern struct tm *gmtime_r(time_t const * restrict timer,
- struct tm * restrict result);
+int strncmp(char const *s1, char const *s2, size_t n)
+{
+ int __retres;
+ {
+ size_t i = (unsigned int)0;
+ while (i < n) {
+ if ((int)*(s1 + i) != (int)*(s2 + i)) {
+ __retres = (int)*((unsigned char *)s1 + i) - (int)*((unsigned char *)s2 + i);
+ goto return_label;
+ }
+ if ((int)*(s1 + i) == 0) {
+ __retres = 0;
+ goto return_label;
+ }
+ i += (size_t)1;
+ }
+ }
+ __retres = 0;
+ return_label: return __retres;
+}
-/*@ requires valid_request: \valid_read(rqtp);
- requires
- initialization: initialized_request:
- \initialized(&rqtp->tv_sec) ∧ \initialized(&rqtp->tv_nsec);
- requires valid_nanosecs: 0 ≤ rqtp->tv_nsec < 1000000000;
- requires valid_remaining_or_null: rmtp ≡ \null ∨ \valid(rmtp);
- ensures result_elapsed_or_interrupted: \result ≡ 0 ∨ \result ≡ -1;
- ensures
- initialization: interrupted_remaining:
- \old(rmtp) ≢ \null ∧ \result ≡ -1 ⇒
- \initialized(&\old(rmtp)->tv_sec) ∧
- \initialized(&\old(rmtp)->tv_nsec);
- ensures
- interrupted_remaining_decreases:
- \old(rmtp) ≢ \null ∧ \result ≡ -1 ⇒
- \old(rqtp)->tv_sec * 1000000000 + \old(rqtp)->tv_nsec ≥
- \old(rmtp)->tv_sec * 1000000000 + \old(rmtp)->tv_nsec;
+/*@ requires valid_s1: valid_read_or_empty(s1, n);
+ requires valid_s2: valid_read_or_empty(s2, n);
+ requires initialization: s1: \initialized((char *)s1 + (0 .. n - 1));
+ requires initialization: s2: \initialized((char *)s2 + (0 .. n - 1));
+ requires danglingness: s1: non_escaping(s1, n);
+ requires danglingness: s2: non_escaping(s2, n);
ensures
- interrupted_remaining_valid:
- \old(rmtp) ≢ \null ∧ \result ≡ -1 ⇒
- 0 ≤ \old(rmtp)->tv_nsec < 1000000000;
- assigns \result, *rmtp;
+ logic_spec:
+ \result ≡
+ memcmp{Pre, Pre}((char *)\old(s1), (char *)\old(s2), \old(n));
+ assigns \result;
assigns \result
- \from (indirect: __fc_time), (indirect: rqtp), (indirect: *rqtp);
- assigns *rmtp
- \from (indirect: __fc_time), (indirect: rqtp), (indirect: *rqtp),
- (indirect: rmtp);
+ \from (indirect: *((char *)s1 + (0 .. n - 1))),
+ (indirect: *((char *)s2 + (0 .. n - 1)));
*/
-extern int nanosleep(struct timespec const *rqtp, struct timespec *rmtp);
+int memcmp(void const *s1, void const *s2, size_t n)
+{
+ int __retres;
+ unsigned char const *p1;
+ unsigned char const *p2;
+ p1 = (unsigned char const *)s1;
+ p2 = (unsigned char const *)s2;
+ {
+ size_t i = (unsigned int)0;
+ while (i < n) {
+ if ((int)*(p1 + i) != (int)*(p2 + i)) {
+ __retres = (int)*(p1 + i) - (int)*(p2 + i);
+ goto return_label;
+ }
+ i += (size_t)1;
+ }
+ }
+ __retres = 0;
+ return_label: return __retres;
+}
-extern char *tzname[2];
+static int char_equal_ignore_case(char c1, char c2)
+{
+ int __retres;
+ if ((int)c1 >= 'A')
+ if ((int)c1 <= 'Z') c1 = (char)((int)c1 - ('A' - 'a'));
+ if ((int)c2 >= 'A')
+ if ((int)c2 <= 'Z') c2 = (char)((int)c2 - ('A' - 'a'));
+ if ((int)c1 == (int)c2) {
+ __retres = 0;
+ goto return_label;
+ }
+ else {
+ __retres = (int)((unsigned char)c2) - (int)((unsigned char)c1);
+ goto return_label;
+ }
+ return_label: return __retres;
+}
-/*@ assigns *(tzname[0 .. 1] + (0 ..));
- assigns *(tzname[0 .. 1] + (0 ..)) \from \nothing;
+/*@ requires valid_string_s1: valid_read_string(s1);
+ requires valid_string_s2: valid_read_string(s2);
+ assigns \result;
+ assigns \result
+ \from (indirect: *(s1 + (0 ..))), (indirect: *(s2 + (0 ..)));
*/
-extern void tzset(void);
+int strcasecmp(char const *s1, char const *s2)
+{
+ int __retres;
+ size_t i;
+ i = (unsigned int)0;
+ while (1) {
+ if ((int)*(s1 + i) != 0) {
+ if (! ((int)*(s2 + i) != 0)) break;
+ }
+ else break;
+ {
+ int res = char_equal_ignore_case(*(s1 + i),*(s2 + i));
+ if (res != 0) {
+ __retres = res;
+ goto return_label;
+ }
+ }
+ i += (size_t)1;
+ }
+ if ((int)*(s1 + i) == 0) {
+ if ((int)*(s2 + i) == 0) {
+ __retres = 0;
+ goto return_label;
+ }
+ else goto _LAND;
+ }
+ else {
+ _LAND: ;
+ if ((int)*(s1 + i) == 0) {
+ __retres = -1;
+ goto return_label;
+ }
+ else {
+ __retres = 1;
+ goto return_label;
+ }
+ }
+ return_label: return __retres;
+}
-/*@ requires
- valid:
- valid_read_or_empty((void *)s, (unsigned int)(sizeof(wchar_t) * n)) ∨
- \valid_read((unsigned char *)s + (0 .. wmemchr_off(s, c, n)));
- requires
- initialization:
- \initialized(s + (0 .. n - 1)) ∨
- \initialized(s + (0 .. wmemchr_off(s, c, n)));
- requires
- danglingness:
- non_escaping((void *)s, (unsigned int)(sizeof(wchar_t) * n)) ∨
- non_escaping((void *)s,
- (unsigned int)(sizeof(wchar_t) *
- (wmemchr_off(s, c, n) + 1)));
+/*@ requires valid_string_src: valid_read_string(src);
+ requires valid_string_dest: valid_string(dest);
+ requires room_string: \valid(dest + (0 .. strlen(dest) + strlen(src)));
ensures
- result_null_or_inside_s:
- \result ≡ \null ∨ \subset(\result, \old(s) + (0 .. \old(n) - 1));
- assigns \result;
- assigns \result
- \from s, (indirect: *(s + (0 .. n - 1))), (indirect: c), (indirect: n);
+ sum_of_lengths: strlen(\old(dest)) ≡ \old(strlen(dest) + strlen(src));
+ ensures
+ initialization: dest:
+ \initialized(\old(dest) + (0 .. \old(strlen(dest) + strlen(src))));
+ ensures
+ dest_null_terminated:
+ *(\old(dest) + \old(strlen(dest) + strlen(src))) ≡ 0;
+ ensures result_ptr: \result ≡ \old(dest);
+ assigns *(dest +
+ (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src))),
+ \result;
+ assigns
+ *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src)))
+ \from *(src + (0 .. strlen{Old}(src)));
+ assigns \result \from dest;
*/
-extern wchar_t *wmemchr(wchar_t const *s, wchar_t c, size_t n);
+char *strcat(char *dest, char const *src)
+{
+ size_t i;
+ size_t n = strlen((char const *)dest);
+ i = (unsigned int)0;
+ while ((int)*(src + i) != 0) {
+ *(dest + (n + i)) = *(src + i);
+ i += (size_t)1;
+ }
+ *(dest + (n + i)) = (char)0;
+ return dest;
+}
+
+/*@ requires valid_nstring_src: valid_read_nstring(src, n);
+ requires valid_string_dest: valid_string(dest);
+ ensures result_ptr: \result ≡ \old(dest);
+ assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n)), \result;
+ assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n))
+ \from *(src + (0 .. n));
+ assigns \result \from dest;
+
+ behavior complete:
+ assumes
+ valid_string_src_fits: valid_read_string(src) ∧ strlen(src) ≤ n;
+ requires
+ room_string: \valid((dest + strlen(dest)) + (0 .. strlen(src)));
+ ensures
+ sum_of_lengths:
+ strlen(\old(dest)) ≡ \old(strlen(dest) + strlen(src));
+ assigns *(dest +
+ (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src))),
+ \result;
+ assigns
+ *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src)))
+ \from *(src + (0 .. strlen{Old}(src)));
+ assigns \result \from dest;
+
+ behavior partial:
+ assumes
+ valid_string_src_too_large:
+ ¬(valid_read_string(src) ∧ strlen(src) ≤ n);
+ requires room_string: \valid((dest + strlen(dest)) + (0 .. n));
+ ensures
+ sum_of_bounded_lengths:
+ strlen(\old(dest)) ≡ \old(strlen(dest)) + \old(n);
+ assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n)),
+ \result;
+ assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n))
+ \from *(src + (0 .. strlen{Old}(src)));
+ assigns \result \from dest;
+ */
+char *strncat(char *dest, char const *src, size_t n)
+{
+ size_t i;
+ size_t dest_len = strlen((char const *)dest);
+ i = (unsigned int)0;
+ while (i < n) {
+ if ((int)*(src + i) == 0) break;
+ *(dest + (dest_len + i)) = *(src + i);
+ i += (size_t)1;
+ }
+ *(dest + (dest_len + i)) = (char)0;
+ return dest;
+}
-/*@ requires
- valid_s1:
- valid_read_or_empty((void *)s1, (unsigned int)(sizeof(wchar_t) * n));
- requires
- valid_s2:
- valid_read_or_empty((void *)s2, (unsigned int)(sizeof(wchar_t) * n));
- requires initialization: s1: \initialized(s1 + (0 .. n - 1));
- requires initialization: s2: \initialized(s2 + (0 .. n - 1));
- requires
- danglingness: s1:
- non_escaping((void *)s1, (unsigned int)(sizeof(wchar_t) * n));
+/*@ requires valid_string_src: valid_read_string(src);
+ requires room_string: \valid(dest + (0 .. strlen(src)));
requires
- danglingness: s2:
- non_escaping((void *)s2, (unsigned int)(sizeof(wchar_t) * n));
- assigns \result;
- assigns \result
- \from (indirect: *(s1 + (0 .. n - 1))),
- (indirect: *(s2 + (0 .. n - 1))), (indirect: n);
+ separation:
+ \separated(dest + (0 .. strlen(src)), src + (0 .. strlen(src)));
+ ensures equal_contents: strcmp(\old(dest), \old(src)) ≡ 0;
+ ensures result_ptr: \result ≡ \old(dest);
+ assigns *(dest + (0 .. strlen{Old}(src))), \result;
+ assigns *(dest + (0 .. strlen{Old}(src)))
+ \from *(src + (0 .. strlen{Old}(src)));
+ assigns \result \from dest;
*/
-extern int wmemcmp(wchar_t const *s1, wchar_t const *s2, size_t n);
+char *strcpy(char *dest, char const *src)
+{
+ size_t i;
+ i = (unsigned int)0;
+ while ((int)*(src + i) != 0) {
+ *(dest + i) = *(src + i);
+ i += (size_t)1;
+ }
+ *(dest + i) = (char)0;
+ return dest;
+}
-wchar_t *wmemcpy(wchar_t *dest, wchar_t const *src, size_t n);
+/*@ requires valid_string_src: valid_read_string(src);
+ requires room_string: \valid(dest + (0 .. strlen(src)));
+ requires
+ separation:
+ \separated(dest + (0 .. strlen(src)), src + (0 .. strlen(src)));
+ ensures equal_contents: strcmp(\old(dest), \old(src)) ≡ 0;
+ ensures points_to_end: \result ≡ \old(dest) + strlen(\old(dest));
+ assigns *(dest + (0 .. strlen{Old}(src))), \result;
+ assigns *(dest + (0 .. strlen{Old}(src)))
+ \from *(src + (0 .. strlen{Old}(src)));
+ assigns \result \from dest;
+ */
+char *stpcpy(char *dest, char const *src)
+{
+ char *__retres;
+ size_t i;
+ i = (unsigned int)0;
+ while ((int)*(src + i) != 0) {
+ *(dest + i) = *(src + i);
+ i += (size_t)1;
+ }
+ *(dest + i) = (char)0;
+ __retres = dest + i;
+ return __retres;
+}
-/*@ requires valid_src: \valid_read(src + (0 .. n - 1));
- requires valid_dest: \valid(dest + (0 .. n - 1));
+/*@ requires valid_nstring_src: valid_read_nstring(src, n);
+ requires room_nstring: \valid(dest + (0 .. n - 1));
+ requires separation: \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
ensures result_ptr: \result ≡ \old(dest);
+ ensures initialization: \initialized(\old(dest) + (0 .. \old(n) - 1));
assigns *(dest + (0 .. n - 1)), \result;
- assigns *(dest + (0 .. n - 1))
- \from *(src + (0 .. n - 1)), (indirect: src), (indirect: n);
+ assigns *(dest + (0 .. n - 1)) \from *(src + (0 .. n - 1));
assigns \result \from dest;
+
+ behavior complete:
+ assumes src_fits: strlen(src) < n;
+ ensures equal_after_copy: strcmp(\old(dest), \old(src)) ≡ 0;
+
+ behavior partial:
+ assumes src_too_long: n ≤ strlen(src);
+ ensures
+ equal_prefix:
+ memcmp{Post, Post}(\old(dest), \old(src), \old(n)) ≡ 0;
*/
-extern wchar_t *wmemmove(wchar_t *dest, wchar_t const *src, size_t n);
-
-wchar_t *wmemset(wchar_t *dest, wchar_t val, size_t len);
-
-wchar_t *wcscat(wchar_t *dest, wchar_t const *src);
-
-/*@ requires valid_wstring_src: valid_read_wstring(wcs);
- ensures
- result_null_or_inside_wcs:
- \result ≡ \null ∨ \subset(\result, \old(wcs) + (0 ..));
- assigns \result;
- assigns \result \from wcs, (indirect: *(wcs + (0 ..))), (indirect: wc);
- */
-extern wchar_t *wcschr(wchar_t const *wcs, wchar_t wc);
+char *strncpy(char *dest, char const *src, size_t n)
+{
+ size_t i;
+ i = (unsigned int)0;
+ while (i < n) {
+ *(dest + i) = *(src + i);
+ if ((int)*(src + i) == 0) break;
+ i += (size_t)1;
+ }
+ while (i < n) {
+ *(dest + i) = (char)0;
+ i += (size_t)1;
+ }
+ return dest;
+}
-/*@ requires valid_wstring_s1: valid_read_wstring(s1);
- requires valid_wstring_s2: valid_read_wstring(s2);
+/*@ requires valid_string_s: valid_read_string(s);
assigns \result;
assigns \result
- \from (indirect: *(s1 + (0 ..))), (indirect: *(s2 + (0 ..)));
+ \from s, (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: c);
+
+ behavior found:
+ assumes char_found: strchr(s, c) ≡ \true;
+ ensures result_char: *\result ≡ (char)\old(c);
+ ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
+ ensures
+ result_in_length: \old(s) ≤ \result ≤ \old(s) + strlen(\old(s));
+ ensures result_valid_string: valid_read_string(\result);
+ ensures
+ result_first_occur:
+ ∀ char *p; \old(s) ≤ p < \result ⇒ *p ≢ (char)\old(c);
+
+ behavior not_found:
+ assumes char_not_found: ¬(strchr(s, c) ≡ \true);
+ ensures result_null: \result ≡ \null;
+
+ behavior default:
+ ensures
+ result_null_or_same_base:
+ \result ≡ \null ∨ \base_addr(\result) ≡ \base_addr(\old(s));
*/
-extern int wcscmp(wchar_t const *s1, wchar_t const *s2);
-
-wchar_t *wcscpy(wchar_t *dest, wchar_t const *src);
+char *strchr(char const *s, int c)
+{
+ char *__retres;
+ size_t i;
+ char const ch = (char)c;
+ i = (unsigned int)0;
+ while ((int)*(s + i) != (int)ch) {
+ if ((int)*(s + i) == 0) {
+ __retres = (char *)0;
+ goto return_label;
+ }
+ i += (size_t)1;
+ }
+ __retres = (char *)(s + i);
+ return_label: return __retres;
+}
-/*@ requires valid_wstring_wcs: valid_read_wstring(wcs);
- requires valid_wstring_accept: valid_read_wstring(accept);
+/*@ requires valid_string_s: valid_read_string(s);
assigns \result;
- assigns \result
- \from (indirect: *(wcs + (0 ..))), (indirect: *(accept + (0 ..)));
+ assigns \result \from s, *(s + (0 ..)), c;
+
+ behavior found:
+ assumes char_found: strchr(s, c) ≡ \true;
+ ensures result_char: (int)*\result ≡ \old(c);
+ ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
+ ensures result_valid_string: valid_read_string(\result);
+
+ behavior not_found:
+ assumes char_not_found: ¬(strchr(s, c) ≡ \true);
+ ensures result_null: \result ≡ \null;
+
+ behavior default:
+ ensures
+ result_null_or_same_base:
+ \result ≡ \null ∨ \base_addr(\result) ≡ \base_addr(\old(s));
*/
-extern size_t wcscspn(wchar_t const *wcs, wchar_t const *accept);
+char *strrchr(char const *s, int c)
+{
+ char *__retres;
+ char const ch = (char)c;
+ {
+ size_t tmp;
+ tmp = strlen(s);
+ size_t i = tmp + (size_t)1;
+ while (i > (size_t)0) {
+ if ((int)*(s + (i - (size_t)1)) == (int)ch) {
+ __retres = (char *)(s + (i - (size_t)1));
+ goto return_label;
+ }
+ i -= (size_t)1;
+ }
+ }
+ __retres = (char *)0;
+ return_label: return __retres;
+}
-/*@ requires valid_nwstring_src: valid_read_nwstring(src, n);
- requires valid_wstring_dest: valid_wstring(dest);
- requires
- room_for_concatenation:
- \valid(dest + (wcslen(dest) .. wcslen(dest) + \min(wcslen(src), n)));
+/*@ requires
+ valid:
+ valid_read_or_empty(s, n) ∨
+ \valid_read((unsigned char *)s + (0 .. memchr_off((char *)s, c, n)));
requires
- separation:
- \separated(
- dest + (0 .. wcslen(dest) + wcslen(src)), src + (0 .. wcslen(src))
- );
- assigns *(dest + (0 ..)), \result;
- assigns *(dest + (0 ..))
- \from *(dest + (0 ..)), (indirect: dest), *(src + (0 .. n - 1)),
- (indirect: src), (indirect: n);
- assigns \result
- \from (indirect: *(dest + (0 ..))), (indirect: *(src + (0 .. n - 1))),
- (indirect: n);
- */
-extern size_t wcslcat(wchar_t * restrict dest, wchar_t const * restrict src,
- size_t n);
-
-/*@ requires valid_wstring_src: valid_read_wstring(src);
- requires room_nwstring: \valid(dest + (0 .. n));
+ initialization:
+ \initialized((unsigned char *)s + (0 .. n - 1)) ∨
+ \initialized((unsigned char *)s + (0 .. memchr_off((char *)s, c, n)));
requires
- separation: dest: src:
- \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
- assigns *(dest + (0 .. n - 1)), \result;
- assigns *(dest + (0 .. n - 1))
- \from *(src + (0 .. n - 1)), (indirect: src), (indirect: n);
- assigns \result
- \from (indirect: *(dest + (0 .. n - 1))), (indirect: dest),
- (indirect: *(src + (0 .. n - 1))), (indirect: src), (indirect: n);
- */
-extern size_t wcslcpy(wchar_t *dest, wchar_t const *src, size_t n);
-
-size_t wcslen(wchar_t const *str);
-
-wchar_t *wcsncat(wchar_t *dest, wchar_t const *src, size_t n);
-
-/*@ requires valid_wstring_s1: valid_read_wstring(s1);
- requires valid_wstring_s2: valid_read_wstring(s2);
+ danglingness:
+ non_escaping(s, n) ∨
+ non_escaping(s, (unsigned int)(memchr_off((char *)s, c, n) + 1));
assigns \result;
- assigns \result
- \from (indirect: *(s1 + (0 .. n - 1))),
- (indirect: *(s2 + (0 .. n - 1))), (indirect: n);
+ assigns \result \from s, c, *((unsigned char *)s + (0 .. n - 1));
+
+ behavior found:
+ assumes char_found: memchr((char *)s, c, n) ≡ \true;
+ ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
+ ensures result_char: (int)*((char *)\result) ≡ \old(c);
+ ensures
+ result_in_str:
+ ∀ ℤ i;
+ 0 ≤ i < \old(n) ⇒
+ *((unsigned char *)\old(s) + i) ≡ \old(c) ⇒
+ (unsigned char *)\result ≤ (unsigned char *)\old(s) + i;
+
+ behavior not_found:
+ assumes char_not_found: ¬(memchr((char *)s, c, n) ≡ \true);
+ ensures result_null: \result ≡ \null;
*/
-extern int wcsncmp(wchar_t const *s1, wchar_t const *s2, size_t n);
+void *memchr(void const *s, int c, size_t n)
+{
+ void *__retres;
+ unsigned char const ch = (unsigned char)c;
+ unsigned char const *ss = (unsigned char const *)s;
+ {
+ size_t i = (unsigned int)0;
+ while (i < n) {
+ if ((int)*(ss + i) == (int)ch) {
+ __retres = (void *)(ss + i);
+ goto return_label;
+ }
+ i += (size_t)1;
+ }
+ }
+ __retres = (void *)0;
+ return_label: return __retres;
+}
-wchar_t *wcsncpy(wchar_t *dest, wchar_t const *src, size_t n);
+void *memrchr(void const *s, int c, size_t n)
+{
+ void *__retres;
+ unsigned char const ch = (unsigned char)c;
+ unsigned char const *ss = (unsigned char const *)s;
+ {
+ size_t i = n;
+ while (i > (size_t)0) {
+ if ((int)*(ss + (i - (size_t)1)) == (int)ch) {
+ __retres = (void *)(ss + (i - (size_t)1));
+ goto return_label;
+ }
+ i -= (size_t)1;
+ }
+ }
+ __retres = (void *)0;
+ return_label: return __retres;
+}
-/*@ requires valid_wstring_wcs: valid_read_wstring(wcs);
- requires valid_wstring_accept: valid_read_wstring(accept);
+/*@ requires valid_string_haystack: valid_read_string(haystack);
+ requires valid_string_needle: valid_read_string(needle);
ensures
- result_null_or_inside_wcs:
- \result ≡ \null ∨ \subset(\result, \old(wcs) + (0 ..));
+ result_null_or_in_haystack:
+ \result ≡ \null ∨
+ (\subset(\result, \old(haystack) + (0 ..)) ∧
+ \valid_read(\result) ∧
+ memcmp{Pre, Pre}(\result, \old(needle), strlen(\old(needle))) ≡ 0);
assigns \result;
assigns \result
- \from wcs, (indirect: *(wcs + (0 ..))), (indirect: *(accept + (0 ..)));
+ \from haystack, (indirect: *(haystack + (0 ..))),
+ (indirect: *(needle + (0 ..)));
*/
-extern wchar_t *wcspbrk(wchar_t const *wcs, wchar_t const *accept);
+char *strstr(char const *haystack, char const *needle)
+{
+ char *__retres;
+ if ((int)*(needle + 0) == 0) {
+ __retres = (char *)haystack;
+ goto return_label;
+ }
+ {
+ size_t i = (unsigned int)0;
+ while ((int)*(haystack + i) != 0) {
+ {
+ size_t j;
+ j = (unsigned int)0;
+ while ((int)*(haystack + (i + j)) != 0) {
+ if ((int)*(haystack + (i + j)) != (int)*(needle + j)) break;
+ j += (size_t)1;
+ }
+ if ((int)*(needle + j) == 0) {
+ __retres = (char *)(haystack + i);
+ goto return_label;
+ }
+ }
+ i += (size_t)1;
+ }
+ }
+ __retres = (char *)0;
+ return_label: return __retres;
+}
-/*@ requires valid_wstring_wcs: valid_read_wstring(wcs);
- ensures
- result_null_or_inside_wcs:
- \result ≡ \null ∨ \subset(\result, \old(wcs) + (0 ..));
+static int strerror___fc_strerror_init;
+/*@ ensures result_internal_str: \result ≡ __fc_p_strerror;
+ ensures result_nul_terminated: *(\result + 63) ≡ 0;
+ ensures result_valid_string: valid_read_string(\result);
assigns \result;
- assigns \result
- \from wcs, (indirect: *(wcs + (0 .. wcslen{Old}(wcs)))), (indirect: wc);
+ assigns \result \from __fc_p_strerror, (indirect: errnum);
*/
-extern wchar_t *wcsrchr(wchar_t const *wcs, wchar_t wc);
+char *strerror(int errnum)
+{
+ char *__retres;
+ if (! strerror___fc_strerror_init) {
+ Frama_C_make_unknown(__fc_strerror,(unsigned int)63);
+ __fc_strerror[63] = (char)0;
+ strerror___fc_strerror_init = 1;
+ }
+ __retres = __fc_strerror;
+ return __retres;
+}
-/*@ requires valid_wstring_wcs: valid_read_wstring(wcs);
- requires valid_wstring_accept: valid_read_wstring(accept);
+/*@ requires valid_string_s: valid_read_string(s);
assigns \result;
assigns \result
- \from (indirect: *(wcs + (0 .. wcslen{Old}(wcs)))),
- (indirect: *(accept + (0 .. wcslen{Old}(accept))));
+ \from (indirect: *(s + (0 .. strlen{Old}(s)))),
+ (indirect: __fc_heap_status);
+ allocates \result;
+
+ behavior allocation:
+ assumes can_allocate: is_allocable(strlen(s));
+ ensures allocation: \fresh{Old, Here}(\result,strlen(\old(s)));
+ ensures
+ result_valid_string_and_same_contents:
+ valid_string(\result) ∧ strcmp(\result, \old(s)) ≡ 0;
+ assigns __fc_heap_status, \result;
+ assigns __fc_heap_status \from (indirect: s), __fc_heap_status;
+ assigns \result
+ \from (indirect: *(s + (0 .. strlen{Old}(s)))),
+ (indirect: __fc_heap_status);
+
+ behavior no_allocation:
+ assumes cannot_allocate: ¬is_allocable(strlen(s));
+ ensures result_null: \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
*/
-extern size_t wcsspn(wchar_t const *wcs, wchar_t const *accept);
+char *strdup(char const *s)
+{
+ char *__retres;
+ size_t tmp;
+ tmp = strlen(s);
+ size_t l = tmp + (size_t)1;
+ char *p = malloc(l);
+ if (! p) {
+ __fc_errno = 12;
+ __retres = (char *)0;
+ goto return_label;
+ }
+ memcpy((void *)p,(void const *)s,l);
+ __retres = p;
+ return_label: return __retres;
+}
-/*@ requires valid_wstring_haystack: valid_read_wstring(haystack);
- requires valid_wstring_needle: valid_read_wstring(needle);
- ensures
- result_null_or_inside_haystack:
- \result ≡ \null ∨ \subset(\result, \old(haystack) + (0 ..));
+/*@ requires valid_string_s: valid_read_string(s);
assigns \result;
assigns \result
- \from haystack, (indirect: *(haystack + (0 ..))),
- (indirect: *(needle + (0 ..)));
- */
-extern wchar_t *wcsstr(wchar_t const *haystack, wchar_t const *needle);
-
-/*@ requires room_nwstring: \valid(ws + (0 .. n - 1));
- requires valid_stream: \valid(stream);
- ensures result_null_or_same: \result ≡ \null ∨ \result ≡ \old(ws);
- ensures
- terminated_string_on_success:
- \result ≢ \null ⇒ valid_wstring(\old(ws));
- assigns *(ws + (0 .. n - 1)), \result;
- assigns *(ws + (0 .. n - 1)) \from (indirect: n), (indirect: *stream);
- assigns \result \from ws, (indirect: n), (indirect: *stream);
+ \from (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: n),
+ (indirect: __fc_heap_status);
+ allocates \result;
+
+ behavior allocation:
+ assumes can_allocate: is_allocable(\min(strlen(s), n + 1));
+ ensures
+ allocation:
+ \fresh{Old, Here}(\result,\min(strlen(\old(s)), \old(n) + 1));
+ ensures
+ result_valid_string_bounded_and_same_prefix:
+ \valid(\result + (0 .. \min(strlen(\old(s)), \old(n)))) ∧
+ valid_string(\result) ∧ strlen(\result) ≤ \old(n) ∧
+ strncmp(\result, \old(s), \old(n)) ≡ 0;
+ assigns __fc_heap_status, \result;
+ assigns __fc_heap_status
+ \from (indirect: s), (indirect: n), __fc_heap_status;
+ assigns \result
+ \from (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: n),
+ (indirect: __fc_heap_status);
+
+ behavior no_allocation:
+ assumes cannot_allocate: ¬is_allocable(\min(strlen(s), n + 1));
+ ensures result_null: \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
*/
-extern wchar_t *fgetws(wchar_t * restrict ws, int n, FILE * restrict stream);
-
-/*@ axiomatic wformat_length {
- logic ℤ wformat_length{L}(wchar_t *format) ;
-
- }
+char *strndup(char const *s, size_t n)
+{
+ char *__retres;
+ size_t l;
+ l = (unsigned int)0;
+ while (l < n) {
+ if ((int)*(s + l) == 0) break;
+ l += (size_t)1;
+ }
+ char *p = malloc(l + (size_t)1);
+ if (! p) {
+ __fc_errno = 12;
+ __retres = (char *)0;
+ goto return_label;
+ }
+ memcpy((void *)p,(void const *)s,l);
+ *(p + l) = (char)0;
+ __retres = p;
+ return_label: return __retres;
+}
-*/
-/*@ requires valid_wstring_ws1: valid_read_wstring(ws1);
- requires valid_wstring_ws2: valid_read_wstring(ws2);
+static int strsignal___fc_strsignal_init;
+/*@ ensures result_internal_str: \result ≡ __fc_p_strsignal;
+ ensures result_nul_terminated: *(\result + 63) ≡ 0;
+ ensures result_valid_string: valid_read_string(\result);
assigns \result;
- assigns \result
- \from (indirect: *(ws1 + (0 ..))), (indirect: *(ws2 + (0 ..)));
+ assigns \result \from __fc_p_strsignal, (indirect: signum);
*/
-extern int wcscasecmp(wchar_t const *ws1, wchar_t const *ws2);
+char *strsignal(int signum)
+{
+ char *__retres;
+ if (! strsignal___fc_strsignal_init) {
+ Frama_C_make_unknown(__fc_strsignal,(unsigned int)63);
+ __fc_strsignal[63] = (char)0;
+ strsignal___fc_strsignal_init = 1;
+ }
+ __retres = __fc_strsignal;
+ return __retres;
+}
/*@ requires
valid_dest:
diff --git a/tests/libc/oracle/fc_libc.2.res.oracle b/tests/libc/oracle/fc_libc.2.res.oracle
index eca9057a10e..04c73597962 100644
--- a/tests/libc/oracle/fc_libc.2.res.oracle
+++ b/tests/libc/oracle/fc_libc.2.res.oracle
@@ -92,6 +92,7 @@ skipping share/libc/complex.h
[kernel] Parsing share/libc/setjmp.h (with preprocessing)
[kernel] Parsing share/libc/signal.h (with preprocessing)
[kernel] Parsing share/libc/stdarg.h (with preprocessing)
+[kernel] Parsing share/libc/stdatomic.h (with preprocessing)
[kernel] Parsing share/libc/stdbool.h (with preprocessing)
[kernel] Parsing share/libc/stddef.h (with preprocessing)
[kernel] Parsing share/libc/stdint.h (with preprocessing)
diff --git a/tests/libc/oracle/stdatomic_c.res.oracle b/tests/libc/oracle/stdatomic_c.res.oracle
new file mode 100644
index 00000000000..0fd40c2e892
--- /dev/null
+++ b/tests/libc/oracle/stdatomic_c.res.oracle
@@ -0,0 +1,357 @@
+[kernel] Parsing tests/libc/stdatomic_c.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
+
+[eva] computing for function test_atomic_int <- main.
+ Called from tests/libc/stdatomic_c.c:46.
+[eva] computing for function __fc_atomic_init_marker <- test_atomic_int <- main.
+ Called from tests/libc/stdatomic_c.c:6.
+[eva] Recording results for __fc_atomic_init_marker
+[eva] Done for function __fc_atomic_init_marker
+[eva] computing for function atomic_thread_fence <- test_atomic_int <- main.
+ Called from tests/libc/stdatomic_c.c:8.
+[eva] Recording results for atomic_thread_fence
+[eva] Done for function atomic_thread_fence
+[eva] computing for function atomic_signal_fence <- test_atomic_int <- main.
+ Called from tests/libc/stdatomic_c.c:9.
+[eva] Recording results for atomic_signal_fence
+[eva] Done for function atomic_signal_fence
+[eva] computing for function __fc_atomic_is_lock_free <- test_atomic_int <- main.
+ Called from tests/libc/stdatomic_c.c:10.
+[eva] computing for function Frama_C_nondet <- __fc_atomic_is_lock_free <-
+ test_atomic_int <- main.
+ Called from share/libc/stdatomic.c:35.
+[eva] using specification for function Frama_C_nondet
+[eva] Done for function Frama_C_nondet
+[eva] Recording results for __fc_atomic_is_lock_free
+[eva] Done for function __fc_atomic_is_lock_free
+[eva] computing for function __fc_atomic_store_marker <- test_atomic_int <- main.
+ Called from tests/libc/stdatomic_c.c:11.
+[eva] Recording results for __fc_atomic_store_marker
+[eva] Done for function __fc_atomic_store_marker
+[eva] computing for function __fc_atomic_store_explicit_marker <-
+ test_atomic_int <- main.
+ Called from tests/libc/stdatomic_c.c:12.
+[eva] Recording results for __fc_atomic_store_explicit_marker
+[eva] Done for function __fc_atomic_store_explicit_marker
+[eva] computing for function __fc_atomic_load <- test_atomic_int <- main.
+ Called from tests/libc/stdatomic_c.c:13.
+[eva] Recording results for __fc_atomic_load
+[eva] Done for function __fc_atomic_load
+[eva] computing for function __fc_atomic_load_explicit <- test_atomic_int <- main.
+ Called from tests/libc/stdatomic_c.c:14.
+[eva] share/libc/stdatomic.c:57:
+ Reusing old results for call to __fc_atomic_load
+[eva] Recording results for __fc_atomic_load_explicit
+[eva] Done for function __fc_atomic_load_explicit
+[eva] computing for function __fc_atomic_exchange <- test_atomic_int <- main.
+ Called from tests/libc/stdatomic_c.c:15.
+[eva] Recording results for __fc_atomic_exchange
+[eva] Done for function __fc_atomic_exchange
+[eva] computing for function __fc_atomic_exchange_explicit <- test_atomic_int <-
+ main.
+ Called from tests/libc/stdatomic_c.c:16.
+[eva] computing for function __fc_atomic_exchange <-
+ __fc_atomic_exchange_explicit <- test_atomic_int <-
+ main.
+ Called from share/libc/stdatomic.c:87.
+[eva] Recording results for __fc_atomic_exchange
+[eva] Done for function __fc_atomic_exchange
+[eva] Recording results for __fc_atomic_exchange_explicit
+[eva] Done for function __fc_atomic_exchange_explicit
+[eva] computing for function __fc_atomic_compare_exchange_strong <-
+ test_atomic_int <- main.
+ Called from tests/libc/stdatomic_c.c:17.
+[eva] computing for function memcmp <- __fc_atomic_compare_exchange_strong <-
+ test_atomic_int <- main.
+ Called from share/libc/stdatomic.c:93.
+[eva] using specification for function memcmp
+[eva] share/libc/stdatomic.c:93:
+ function memcmp: precondition 'valid_s1' got status valid.
+[eva] share/libc/stdatomic.c:93:
+ function memcmp: precondition 'valid_s2' got status valid.
+[eva] share/libc/stdatomic.c:93:
+ function memcmp: precondition 'initialization,s1' got status valid.
+[eva] share/libc/stdatomic.c:93:
+ function memcmp: precondition 'initialization,s2' got status valid.
+[eva] share/libc/stdatomic.c:93:
+ function memcmp: precondition 'danglingness,s1' got status valid.
+[eva] share/libc/stdatomic.c:93:
+ function memcmp: precondition 'danglingness,s2' got status valid.
+[eva] share/libc/string.h:63:
+ cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp
+[eva] Done for function memcmp
+[eva] share/libc/stdatomic.c:94: Call to builtin memcpy
+[eva] share/libc/stdatomic.c:94:
+ function memcpy: precondition 'valid_dest' got status valid.
+[eva] share/libc/stdatomic.c:94:
+ function memcpy: precondition 'valid_src' got status valid.
+[eva] share/libc/stdatomic.c:94:
+ function memcpy: precondition 'separation' got status valid.
+[eva] share/libc/string.h:101:
+ cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp
+[eva] share/libc/stdatomic.c:95: Call to builtin memcpy
+[eva] share/libc/stdatomic.c:95:
+ function memcpy: precondition 'valid_dest' got status valid.
+[eva] share/libc/stdatomic.c:95:
+ function memcpy: precondition 'valid_src' got status valid.
+[eva] share/libc/stdatomic.c:95:
+ function memcpy: precondition 'separation' got status valid.
+[eva] Recording results for __fc_atomic_compare_exchange_strong
+[eva] Done for function __fc_atomic_compare_exchange_strong
+[eva] computing for function __fc_atomic_compare_exchange_strong_explicit <-
+ test_atomic_int <- main.
+ Called from tests/libc/stdatomic_c.c:18.
+[eva] computing for function __fc_atomic_compare_exchange_strong <-
+ __fc_atomic_compare_exchange_strong_explicit <-
+ test_atomic_int <- main.
+ Called from share/libc/stdatomic.c:104.
+[eva] computing for function memcmp <- __fc_atomic_compare_exchange_strong <-
+ __fc_atomic_compare_exchange_strong_explicit <-
+ test_atomic_int <- main.
+ Called from share/libc/stdatomic.c:93.
+[eva] Done for function memcmp
+[eva] share/libc/stdatomic.c:94: Call to builtin memcpy
+[eva] share/libc/stdatomic.c:95: Call to builtin memcpy
+[eva] Recording results for __fc_atomic_compare_exchange_strong
+[eva] Done for function __fc_atomic_compare_exchange_strong
+[eva] Recording results for __fc_atomic_compare_exchange_strong_explicit
+[eva] Done for function __fc_atomic_compare_exchange_strong_explicit
+[eva] computing for function __fc_atomic_compare_exchange_weak <-
+ test_atomic_int <- main.
+ Called from tests/libc/stdatomic_c.c:21.
+[eva] computing for function __fc_atomic_compare_exchange_strong <-
+ __fc_atomic_compare_exchange_weak <-
+ test_atomic_int <- main.
+ Called from share/libc/stdatomic.c:110.
+[eva] computing for function memcmp <- __fc_atomic_compare_exchange_strong <-
+ __fc_atomic_compare_exchange_weak <-
+ test_atomic_int <- main.
+ Called from share/libc/stdatomic.c:93.
+[eva] Done for function memcmp
+[eva] share/libc/stdatomic.c:94: Call to builtin memcpy
+[eva] share/libc/stdatomic.c:95: Call to builtin memcpy
+[eva] Recording results for __fc_atomic_compare_exchange_strong
+[eva] Done for function __fc_atomic_compare_exchange_strong
+[eva] Recording results for __fc_atomic_compare_exchange_weak
+[eva] Done for function __fc_atomic_compare_exchange_weak
+[eva] computing for function __fc_atomic_compare_exchange_weak_explicit <-
+ test_atomic_int <- main.
+ Called from tests/libc/stdatomic_c.c:22.
+[eva] computing for function __fc_atomic_compare_exchange_strong <-
+ __fc_atomic_compare_exchange_weak_explicit <-
+ test_atomic_int <- main.
+ Called from share/libc/stdatomic.c:118.
+[eva] computing for function memcmp <- __fc_atomic_compare_exchange_strong <-
+ __fc_atomic_compare_exchange_weak_explicit <-
+ test_atomic_int <- main.
+ Called from share/libc/stdatomic.c:93.
+[eva] Done for function memcmp
+[eva] share/libc/stdatomic.c:94: Call to builtin memcpy
+[eva] share/libc/stdatomic.c:95: Call to builtin memcpy
+[eva] Recording results for __fc_atomic_compare_exchange_strong
+[eva] Done for function __fc_atomic_compare_exchange_strong
+[eva] Recording results for __fc_atomic_compare_exchange_weak_explicit
+[eva] Done for function __fc_atomic_compare_exchange_weak_explicit
+[eva] computing for function __fc_atomic_fetch_add <- test_atomic_int <- main.
+ Called from tests/libc/stdatomic_c.c:25.
+[eva] Recording results for __fc_atomic_fetch_add
+[eva] Done for function __fc_atomic_fetch_add
+[eva] computing for function __fc_atomic_fetch_add_explicit <- test_atomic_int <-
+ main.
+ Called from tests/libc/stdatomic_c.c:26.
+[eva] computing for function __fc_atomic_fetch_add <-
+ __fc_atomic_fetch_add_explicit <- test_atomic_int <-
+ main.
+ Called from share/libc/stdatomic.c:147.
+[eva] Recording results for __fc_atomic_fetch_add
+[eva] Done for function __fc_atomic_fetch_add
+[eva] Recording results for __fc_atomic_fetch_add_explicit
+[eva] Done for function __fc_atomic_fetch_add_explicit
+[eva] computing for function __fc_atomic_fetch_sub <- test_atomic_int <- main.
+ Called from tests/libc/stdatomic_c.c:27.
+[eva] Recording results for __fc_atomic_fetch_sub
+[eva] Done for function __fc_atomic_fetch_sub
+[eva] computing for function __fc_atomic_fetch_sub_explicit <- test_atomic_int <-
+ main.
+ Called from tests/libc/stdatomic_c.c:28.
+[eva] computing for function __fc_atomic_fetch_sub <-
+ __fc_atomic_fetch_sub_explicit <- test_atomic_int <-
+ main.
+ Called from share/libc/stdatomic.c:171.
+[eva] Recording results for __fc_atomic_fetch_sub
+[eva] Done for function __fc_atomic_fetch_sub
+[eva] Recording results for __fc_atomic_fetch_sub_explicit
+[eva] Done for function __fc_atomic_fetch_sub_explicit
+[eva] computing for function __fc_atomic_fetch_or <- test_atomic_int <- main.
+ Called from tests/libc/stdatomic_c.c:29.
+[eva] Recording results for __fc_atomic_fetch_or
+[eva] Done for function __fc_atomic_fetch_or
+[eva] computing for function __fc_atomic_fetch_or_explicit <- test_atomic_int <-
+ main.
+ Called from tests/libc/stdatomic_c.c:30.
+[eva] computing for function __fc_atomic_fetch_or <-
+ __fc_atomic_fetch_or_explicit <- test_atomic_int <-
+ main.
+ Called from share/libc/stdatomic.c:195.
+[eva] Recording results for __fc_atomic_fetch_or
+[eva] Done for function __fc_atomic_fetch_or
+[eva] Recording results for __fc_atomic_fetch_or_explicit
+[eva] Done for function __fc_atomic_fetch_or_explicit
+[eva] computing for function __fc_atomic_fetch_xor <- test_atomic_int <- main.
+ Called from tests/libc/stdatomic_c.c:31.
+[eva] Recording results for __fc_atomic_fetch_xor
+[eva] Done for function __fc_atomic_fetch_xor
+[eva] computing for function __fc_atomic_fetch_xor_explicit <- test_atomic_int <-
+ main.
+ Called from tests/libc/stdatomic_c.c:32.
+[eva] computing for function __fc_atomic_fetch_xor <-
+ __fc_atomic_fetch_xor_explicit <- test_atomic_int <-
+ main.
+ Called from share/libc/stdatomic.c:225.
+[eva] Recording results for __fc_atomic_fetch_xor
+[eva] Done for function __fc_atomic_fetch_xor
+[eva] Recording results for __fc_atomic_fetch_xor_explicit
+[eva] Done for function __fc_atomic_fetch_xor_explicit
+[eva] computing for function __fc_atomic_fetch_and <- test_atomic_int <- main.
+ Called from tests/libc/stdatomic_c.c:33.
+[eva] Recording results for __fc_atomic_fetch_and
+[eva] Done for function __fc_atomic_fetch_and
+[eva] computing for function __fc_atomic_fetch_and_explicit <- test_atomic_int <-
+ main.
+ Called from tests/libc/stdatomic_c.c:34.
+[eva] computing for function __fc_atomic_fetch_and <-
+ __fc_atomic_fetch_and_explicit <- test_atomic_int <-
+ main.
+ Called from share/libc/stdatomic.c:255.
+[eva] Recording results for __fc_atomic_fetch_and
+[eva] Done for function __fc_atomic_fetch_and
+[eva] Recording results for __fc_atomic_fetch_and_explicit
+[eva] Done for function __fc_atomic_fetch_and_explicit
+[eva] computing for function atomic_flag_test_and_set <- test_atomic_int <- main.
+ Called from tests/libc/stdatomic_c.c:36.
+[eva] Recording results for atomic_flag_test_and_set
+[eva] Done for function atomic_flag_test_and_set
+[eva] computing for function atomic_flag_test_and_set_explicit <-
+ test_atomic_int <- main.
+ Called from tests/libc/stdatomic_c.c:37.
+[eva] Recording results for atomic_flag_test_and_set_explicit
+[eva] Done for function atomic_flag_test_and_set_explicit
+[eva] computing for function atomic_flag_clear <- test_atomic_int <- main.
+ Called from tests/libc/stdatomic_c.c:38.
+[eva] Recording results for atomic_flag_clear
+[eva] Done for function atomic_flag_clear
+[eva] computing for function atomic_flag_clear_explicit <- test_atomic_int <- main.
+ Called from tests/libc/stdatomic_c.c:39.
+[eva] Recording results for atomic_flag_clear_explicit
+[eva] Done for function atomic_flag_clear_explicit
+[eva] Recording results for test_atomic_int
+[eva] Done for function test_atomic_int
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function __fc_atomic_exchange:
+ r ∈ [0..4294967295]
+ a ∈ [--..--]
+[eva:final-states] Values at end of function __fc_atomic_exchange_explicit:
+ a ∈ [--..--]
+[eva:final-states] Values at end of function __fc_atomic_fetch_add:
+ r ∈ [0..4294967295]
+ a ∈ [--..--]
+[eva:final-states] Values at end of function __fc_atomic_fetch_add_explicit:
+ a ∈ [--..--]
+[eva:final-states] Values at end of function __fc_atomic_fetch_and:
+ r ∈ [0..4294967295]
+ a ∈ [--..--]
+[eva:final-states] Values at end of function __fc_atomic_fetch_and_explicit:
+ a ∈ [--..--]
+[eva:final-states] Values at end of function __fc_atomic_fetch_or:
+ r ∈ [0..4294967295]
+ a ∈ [--..--]
+[eva:final-states] Values at end of function __fc_atomic_fetch_or_explicit:
+ a ∈ [--..--]
+[eva:final-states] Values at end of function __fc_atomic_fetch_sub:
+ r ∈ [0..4294967295]
+ a ∈ [--..--]
+[eva:final-states] Values at end of function __fc_atomic_fetch_sub_explicit:
+ a ∈ [--..--]
+[eva:final-states] Values at end of function __fc_atomic_fetch_xor:
+ r ∈ [0..4294967295]
+ a ∈ [--..--]
+[eva:final-states] Values at end of function __fc_atomic_fetch_xor_explicit:
+ a ∈ [--..--]
+[eva:final-states] Values at end of function __fc_atomic_init_marker:
+
+[eva:final-states] Values at end of function __fc_atomic_is_lock_free:
+ Frama_C_entropy_source ∈ [--..--]
+ __retres ∈ {0; 1}
+[eva:final-states] Values at end of function __fc_atomic_load:
+ __retres ∈ [0..4294967295]
+[eva:final-states] Values at end of function __fc_atomic_load_explicit:
+
+[eva:final-states] Values at end of function __fc_atomic_store_explicit_marker:
+
+[eva:final-states] Values at end of function __fc_atomic_store_marker:
+
+[eva:final-states] Values at end of function atomic_flag_clear:
+ flag ∈ [--..--]
+[eva:final-states] Values at end of function atomic_flag_clear_explicit:
+ flag ∈ [--..--]
+[eva:final-states] Values at end of function atomic_flag_test_and_set:
+ r ∈ {0; 1}
+ flag ∈ [--..--]
+[eva:final-states] Values at end of function atomic_flag_test_and_set_explicit:
+ r ∈ {0; 1}
+ flag ∈ [--..--]
+[eva:final-states] Values at end of function atomic_signal_fence:
+
+[eva:final-states] Values at end of function atomic_thread_fence:
+
+[eva:final-states]
+ Values at end of function __fc_atomic_compare_exchange_strong:
+ r ∈ [--..--]
+ a ∈ [--..--]
+ aa ∈ [--..--]
+ __retres ∈ {0; 1}
+[eva:final-states]
+ Values at end of function __fc_atomic_compare_exchange_strong_explicit:
+ a ∈ [--..--]
+ aa ∈ [--..--]
+[eva:final-states] Values at end of function __fc_atomic_compare_exchange_weak:
+ a ∈ [--..--]
+ aa ∈ [--..--]
+[eva:final-states]
+ Values at end of function __fc_atomic_compare_exchange_weak_explicit:
+ a ∈ [--..--]
+ aa ∈ [--..--]
+[eva:final-states] Values at end of function test_atomic_int:
+ Frama_C_entropy_source ∈ [--..--]
+ a ∈ [--..--]
+ aa ∈ [--..--]
+ c ∈ {42}
+ b1 ∈ {0; 1}
+ d ∈ [--..--]
+ e ∈ [--..--]
+ f ∈ [--..--]
+ g ∈ [--..--]
+ b2 ∈ {0; 1}
+ b3 ∈ {0; 1}
+ b4 ∈ {0; 1}
+ b5 ∈ {0; 1}
+ add1 ∈ [--..--]
+ add2 ∈ [--..--]
+ sub1 ∈ [--..--]
+ sub2 ∈ [--..--]
+ or1 ∈ [--..--]
+ or2 ∈ [--..--]
+ xor1 ∈ [--..--]
+ xor2 ∈ [--..--]
+ and1 ∈ [--..--]
+ and2 ∈ [--..--]
+ flag ∈ [--..--]
+ b6 ∈ {0; 1}
+ b7 ∈ {0; 1}
+[eva:final-states] Values at end of function main:
+ Frama_C_entropy_source ∈ [--..--]
diff --git a/tests/libc/stdatomic_c.c b/tests/libc/stdatomic_c.c
new file mode 100644
index 00000000000..2c05a027f5d
--- /dev/null
+++ b/tests/libc/stdatomic_c.c
@@ -0,0 +1,47 @@
+#include "stdatomic.c"
+
+void test_atomic_int() {
+ atomic_int a = ATOMIC_VAR_INIT(42);
+ int aa = 51;
+ atomic_init(&a, 42);
+ int c = kill_dependency(a);
+ atomic_thread_fence(memory_order_relaxed);
+ atomic_signal_fence(memory_order_consume);
+ _Bool b1 = atomic_is_lock_free(&a);
+ atomic_store(&a, 43);
+ atomic_store_explicit(&a, 43, memory_order_release);
+ int d = atomic_load(&a);
+ int e = atomic_load_explicit(&a, memory_order_acquire);
+ int f = atomic_exchange(&a, 44);
+ int g = atomic_exchange_explicit(&a, 44, memory_order_acq_rel);
+ _Bool b2 = atomic_compare_exchange_strong(&a, &aa, 45);
+ _Bool b3 = atomic_compare_exchange_strong_explicit(&a, &aa, 46,
+ memory_order_seq_cst,
+ memory_order_relaxed);
+ _Bool b4 = atomic_compare_exchange_weak(&a, &aa, 47);
+ _Bool b5 = atomic_compare_exchange_weak_explicit(&a, &aa, 48,
+ memory_order_consume,
+ memory_order_relaxed);
+ int add1 = atomic_fetch_add(&a, 60);
+ int add2 = atomic_fetch_add_explicit(&a, 61, memory_order_acquire);
+ int sub1 = atomic_fetch_sub(&a, 62);
+ int sub2 = atomic_fetch_sub_explicit(&a, 63, memory_order_acquire);
+ int or1 = atomic_fetch_or(&a, 64);
+ int or2 = atomic_fetch_or_explicit(&a, 65, memory_order_acquire);
+ int xor1 = atomic_fetch_xor(&a, 66);
+ int xor2 = atomic_fetch_xor_explicit(&a, 67, memory_order_acquire);
+ int and1 = atomic_fetch_and(&a, 68);
+ int and2 = atomic_fetch_and_explicit(&a, 69, memory_order_acquire);
+ atomic_flag flag = ATOMIC_FLAG_INIT;
+ _Bool b6 = atomic_flag_test_and_set(&flag);
+ _Bool b7 = atomic_flag_test_and_set_explicit(&flag, memory_order_relaxed);
+ atomic_flag_clear(&flag);
+ atomic_flag_clear_explicit(&flag, memory_order_relaxed);
+}
+
+void test_atomic_pointer() {
+}
+
+void main() {
+ test_atomic_int();
+}
--
GitLab