[libc] add experimental support for <stdatomic.h>

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

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"

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"

share/libc/stdatomic.c

+/**************************************************************************/
+/*                                                                        */
+/*  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

share/libc/stdatomic.h

+/**************************************************************************/
+/*                                                                        */
+/*  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

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"

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"

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)

tests/libc/oracle/stdatomic_c.res.oracle

+[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 ∈ [--..--]

tests/libc/stdatomic_c.c

+#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();
+}