[ 0:01] compiling /home/xrockai/src/divine/nightly/test/libcxx/atomic/integral.pass.cpp
[ 0:01] In file included from /home/xrockai/src/divine/nightly/test/libcxx/atomic/integral.pass.cpp:91:
[ 0:01] In file included from /dios/libcxx/include/atomic:550:
[ 0:01] In file included from /dios/libcxx/include/cstddef:44:
[ 0:01] In file included from /dios/include/stddef.h:10:
[ 0:01] In file included from /dios/include/_PDCLIB/int.h:16:
[ 0:01] /dios/include/_PDCLIB/cdefs.h:69:10: warning: Unsupported _ _cplusplus (__cplusplus) (too new) (supported: ISO/IEC 14882:1997, ISO/IEC 14882:2011).
[ 0:01]         #warning Unsupported _ _cplusplus (__cplusplus) (too new) (supported: ISO/IEC 14882:1997, ISO/IEC 14882:2011).
[ 0:01]          ^
[ 0:01] 1 warning generated.
[ 0:02] compiling /dios/lib/config/seqklee.bc
[ 0:02] setting up pass: functionmeta, options = 
[ 0:03] setting up pass: fuse-ctors, options = 
[ 0:03] KLEE: output directory is "/var/obj/divine-nightly/semidbg/test/__test_work_dir.15/_klee_out"
[ 0:07] KLEE: Using Z3 solver backend
[ 0:07] WARNING: this target does not support the llvm.stacksave intrinsic.
[ 0:07] warning: Linking two modules of different target triples: klee_div_zero_check.bc' is 'x86_64-unknown-linux-gnu' whereas 'klee.bc' is 'x86_64-unknown-none-elf'
[ 0:07] 
[ 0:07] KLEE: WARNING: undefined reference to function: __dios_tainted_init
[ 0:13] KLEE: WARNING: undefined reference to function: klee_free
[ 0:13] KLEE: WARNING: undefined reference to function: klee_malloc
[ 0:13] i:1
[ 0:13] KLEE: WARNING ONCE: Alignment of memory from call "klee_malloc" is not modelled. Using alignment of 8.
[ 0:13] about to __boot:0
[ 0:13] about to run the scheduler:0
[ 0:13] KLEE: WARNING ONCE: calling external: __dios_tainted_init() at /dios/libc/sys/start.cpp:49 5
[ 0:13] KLEE: ERROR: /dios/libc/sys/start.cpp:87: failed external call: __dios_tainted_init
[ 0:13] KLEE: NOTE: now ignoring this error at this location
[ 0:13] KLEE: ERROR: EXITING ON ERROR:
[ 0:13] Error: failed external call: __dios_tainted_init
[ 0:13] File: /dios/libc/sys/start.cpp
[ 0:13] Line: 87
[ 0:13] assembly.ll line: 151792
[ 0:13] Stack: 
[ 0:13] 	#000151792 in __dios_start (l=2, argc=1, argv=94329169515016, envp=94329169592328) at /dios/libc/sys/start.cpp:87
[ 0:13] 	#100127801 in _ZN6__dios10sched_nullINS_5ClockINS_10NondetKleeINS_4BaseEEEEEE13run_schedulerINS_7ContextEEEvv () at /dios/sys/sched_null.hpp:163
[ 0:13] 	#200160040 in klee_boot (argc=2, argv=94329092724736) at /dios/arch/klee/boot.c:41
[ 0:13] 
[ 0:13] 
[ 0:13]      1	/* TAGS: c++ fin */
[ 0:13]      2	/* CC_OPTS: -std=c++2a */
[ 0:13]      3	/* VERIFY_OPTS: -o nofail:malloc */
[ 0:13]      4	//===----------------------------------------------------------------------===//
[ 0:13]      5	//
[ 0:13]      6	// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
[ 0:13]      7	// See https://llvm.org/LICENSE.txt for license information.
[ 0:13]      8	// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
[ 0:13]      9	//
[ 0:13]     10	//===----------------------------------------------------------------------===//
[ 0:13]     11	//
[ 0:13]     12	// UNSUPPORTED: libcpp-has-no-threads
[ 0:13]     13	
[ 0:13]     14	// <atomic>
[ 0:13]     15	
[ 0:13]     16	// template <>
[ 0:13]     17	// struct atomic<integral>
[ 0:13]     18	// {
[ 0:13]     19	//     bool is_lock_free() const volatile;
[ 0:13]     20	//     bool is_lock_free() const;
[ 0:13]     21	//     void store(integral desr, memory_order m = memory_order_seq_cst) volatile;
[ 0:13]     22	//     void store(integral desr, memory_order m = memory_order_seq_cst);
[ 0:13]     23	//     integral load(memory_order m = memory_order_seq_cst) const volatile;
[ 0:13]     24	//     integral load(memory_order m = memory_order_seq_cst) const;
[ 0:13]     25	//     operator integral() const volatile;
[ 0:13]     26	//     operator integral() const;
[ 0:13]     27	//     integral exchange(integral desr,
[ 0:13]     28	//                       memory_order m = memory_order_seq_cst) volatile;
[ 0:13]     29	//     integral exchange(integral desr, memory_order m = memory_order_seq_cst);
[ 0:13]     30	//     bool compare_exchange_weak(integral& expc, integral desr,
[ 0:13]     31	//                                memory_order s, memory_order f) volatile;
[ 0:13]     32	//     bool compare_exchange_weak(integral& expc, integral desr,
[ 0:13]     33	//                                memory_order s, memory_order f);
[ 0:13]     34	//     bool compare_exchange_strong(integral& expc, integral desr,
[ 0:13]     35	//                                  memory_order s, memory_order f) volatile;
[ 0:13]     36	//     bool compare_exchange_strong(integral& expc, integral desr,
[ 0:13]     37	//                                  memory_order s, memory_order f);
[ 0:13]     38	//     bool compare_exchange_weak(integral& expc, integral desr,
[ 0:13]     39	//                                memory_order m = memory_order_seq_cst) volatile;
[ 0:13]     40	//     bool compare_exchange_weak(integral& expc, integral desr,
[ 0:13]     41	//                                memory_order m = memory_order_seq_cst);
[ 0:13]     42	//     bool compare_exchange_strong(integral& expc, integral desr,
[ 0:13]     43	//                                 memory_order m = memory_order_seq_cst) volatile;
[ 0:13]     44	//     bool compare_exchange_strong(integral& expc, integral desr,
[ 0:13]     45	//                                  memory_order m = memory_order_seq_cst);
[ 0:13]     46	//
[ 0:13]     47	//     integral
[ 0:13]     48	//         fetch_add(integral op, memory_order m = memory_order_seq_cst) volatile;
[ 0:13]     49	//     integral fetch_add(integral op, memory_order m = memory_order_seq_cst);
[ 0:13]     50	//     integral
[ 0:13]     51	//         fetch_sub(integral op, memory_order m = memory_order_seq_cst) volatile;
[ 0:13]     52	//     integral fetch_sub(integral op, memory_order m = memory_order_seq_cst);
[ 0:13]     53	//     integral
[ 0:13]     54	//         fetch_and(integral op, memory_order m = memory_order_seq_cst) volatile;
[ 0:13]     55	//     integral fetch_and(integral op, memory_order m = memory_order_seq_cst);
[ 0:13]     56	//     integral
[ 0:13]     57	//         fetch_or(integral op, memory_order m = memory_order_seq_cst) volatile;
[ 0:13]     58	//     integral fetch_or(integral op, memory_order m = memory_order_seq_cst);
[ 0:13]     59	//     integral
[ 0:13]     60	//         fetch_xor(integral op, memory_order m = memory_order_seq_cst) volatile;
[ 0:13]     61	//     integral fetch_xor(integral op, memory_order m = memory_order_seq_cst);
[ 0:13]     62	//
[ 0:13]     63	//     atomic() = default;
[ 0:13]     64	//     constexpr atomic(integral desr);
[ 0:13]     65	//     atomic(const atomic&) = delete;
[ 0:13]     66	//     atomic& operator=(const atomic&) = delete;
[ 0:13]     67	//     atomic& operator=(const atomic&) volatile = delete;
[ 0:13]     68	//     integral operator=(integral desr) volatile;
[ 0:13]     69	//     integral operator=(integral desr);
[ 0:13]     70	//
[ 0:13]     71	//     integral operator++(int) volatile;
[ 0:13]     72	//     integral operator++(int);
[ 0:13]     73	//     integral operator--(int) volatile;
[ 0:13]     74	//     integral operator--(int);
[ 0:13]     75	//     integral operator++() volatile;
[ 0:13]     76	//     integral operator++();
[ 0:13]     77	//     integral operator--() volatile;
[ 0:13]     78	//     integral operator--();
[ 0:13]     79	//     integral operator+=(integral op) volatile;
[ 0:13]     80	//     integral operator+=(integral op);
[ 0:13]     81	//     integral operator-=(integral op) volatile;
[ 0:13]     82	//     integral operator-=(integral op);
[ 0:13]     83	//     integral operator&=(integral op) volatile;
[ 0:13]     84	//     integral operator&=(integral op);
[ 0:13]     85	//     integral operator|=(integral op) volatile;
[ 0:13]     86	//     integral operator|=(integral op);
[ 0:13]     87	//     integral operator^=(integral op) volatile;
[ 0:13]     88	//     integral operator^=(integral op);
[ 0:13]     89	// };
[ 0:13]     90	
[ 0:13]     91	#include <atomic>
[ 0:13]     92	#include <new>
[ 0:13]     93	#include <cassert>
[ 0:13]     94	
[ 0:13]     95	#include "cmpxchg_loop.h"
[ 0:13]     96	
[ 0:13]     97	#include "test_macros.h"
[ 0:13]     98	
[ 0:13]     99	template <class A, class T>
[ 0:13]    100	void
[ 0:13]    101	do_test()
[ 0:13]    102	{
[ 0:13]    103	    A obj(T(0));
[ 0:13]    104	    assert(obj == T(0));
[ 0:13]    105	    std::atomic_init(&obj, T(1));
[ 0:13]    106	    assert(obj == T(1));
[ 0:13]    107	    std::atomic_init(&obj, T(2));
[ 0:13]    108	    assert(obj == T(2));
[ 0:13]    109	    bool b0 = obj.is_lock_free();
[ 0:13]    110	    ((void)b0); // mark as unused
[ 0:13]    111	    obj.store(T(0));
[ 0:13]    112	    assert(obj == T(0));
[ 0:13]    113	    obj.store(T(1), std::memory_order_release);
[ 0:13]    114	    assert(obj == T(1));
[ 0:13]    115	    assert(obj.load() == T(1));
[ 0:13]    116	    assert(obj.load(std::memory_order_acquire) == T(1));
[ 0:13]    117	    assert(obj.exchange(T(2)) == T(1));
[ 0:13]    118	    assert(obj == T(2));
[ 0:13]    119	    assert(obj.exchange(T(3), std::memory_order_relaxed) == T(2));
[ 0:13]    120	    assert(obj == T(3));
[ 0:13]    121	    T x = obj;
[ 0:13]    122	    assert(cmpxchg_weak_loop(obj, x, T(2)) == true);
[ 0:13]    123	    assert(obj == T(2));
[ 0:13]    124	    assert(x == T(3));
[ 0:13]    125	    assert(obj.compare_exchange_weak(x, T(1)) == false);
[ 0:13]    126	    assert(obj == T(2));
[ 0:13]    127	    assert(x == T(2));
[ 0:13]    128	    x = T(2);
[ 0:13]    129	    assert(obj.compare_exchange_strong(x, T(1)) == true);
[ 0:13]    130	    assert(obj == T(1));
[ 0:13]    131	    assert(x == T(2));
[ 0:13]    132	    assert(obj.compare_exchange_strong(x, T(0)) == false);
[ 0:13]    133	    assert(obj == T(1));
[ 0:13]    134	    assert(x == T(1));
[ 0:13]    135	    assert((obj = T(0)) == T(0));
[ 0:13]    136	    assert(obj == T(0));
[ 0:13]    137	    assert(obj++ == T(0));
[ 0:13]    138	    assert(obj == T(1));
[ 0:13]    139	    assert(++obj == T(2));
[ 0:13]    140	    assert(obj == T(2));
[ 0:13]    141	    assert(--obj == T(1));
[ 0:13]    142	    assert(obj == T(1));
[ 0:13]    143	    assert(obj-- == T(1));
[ 0:13]    144	    assert(obj == T(0));
[ 0:13]    145	    obj = T(2);
[ 0:13]    146	    assert((obj += T(3)) == T(5));
[ 0:13]    147	    assert(obj == T(5));
[ 0:13]    148	    assert((obj -= T(3)) == T(2));
[ 0:13]    149	    assert(obj == T(2));
[ 0:13]    150	    assert((obj |= T(5)) == T(7));
[ 0:13]    151	    assert(obj == T(7));
[ 0:13]    152	    assert((obj &= T(0xF)) == T(7));
[ 0:13]    153	    assert(obj == T(7));
[ 0:13]    154	    assert((obj ^= T(0xF)) == T(8));
[ 0:13]    155	    assert(obj == T(8));
[ 0:13]    156	
[ 0:13]    157	    {
[ 0:13]    158	        TEST_ALIGNAS_TYPE(A) char storage[sizeof(A)] = {23};
[ 0:13]    159	        A& zero = *new (storage) A();
[ 0:13]    160	        assert(zero == 0);
[ 0:13]    161	        zero.~A();
[ 0:13]    162	    }
[ 0:13]    163	}
[ 0:13]    164	
[ 0:13]    165	template <class A, class T>
[ 0:13]    166	void test()
[ 0:13]    167	{
[ 0:13]    168	    do_test<A, T>();
[ 0:13]    169	    do_test<volatile A, T>();
[ 0:13]    170	}
[ 0:13]    171	
[ 0:13]    172	
[ 0:13]    173	int main(int, char**)
[ 0:13]    174	{
[ 0:13]    175	    test<std::atomic_char, char>();
[ 0:13]    176	    test<std::atomic_schar, signed char>();
[ 0:13]    177	    test<std::atomic_uchar, unsigned char>();
[ 0:13]    178	    test<std::atomic_short, short>();
[ 0:13]    179	    test<std::atomic_ushort, unsigned short>();
[ 0:13]    180	    test<std::atomic_int, int>();
[ 0:13]    181	    test<std::atomic_uint, unsigned int>();
[ 0:13]    182	    test<std::atomic_long, long>();
[ 0:13]    183	    test<std::atomic_ulong, unsigned long>();
[ 0:13]    184	    test<std::atomic_llong, long long>();
[ 0:13]    185	    test<std::atomic_ullong, unsigned long long>();
[ 0:13]    186	#ifndef _LIBCPP_HAS_NO_UNICODE_CHARS
[ 0:13]    187	    test<std::atomic_char16_t, char16_t>();
[ 0:13]    188	    test<std::atomic_char32_t, char32_t>();
[ 0:13]    189	#endif  // _LIBCPP_HAS_NO_UNICODE_CHARS
[ 0:13]    190	    test<std::atomic_wchar_t, wchar_t>();
[ 0:13]    191	
[ 0:13]    192	    test<std::atomic_int8_t,    int8_t>();
[ 0:13]    193	    test<std::atomic_uint8_t,  uint8_t>();
[ 0:13]    194	    test<std::atomic_int16_t,   int16_t>();
[ 0:13]    195	    test<std::atomic_uint16_t, uint16_t>();
[ 0:13]    196	    test<std::atomic_int32_t,   int32_t>();
[ 0:13]    197	    test<std::atomic_uint32_t, uint32_t>();
[ 0:13]    198	    test<std::atomic_int64_t,   int64_t>();
[ 0:13]    199	    test<std::atomic_uint64_t, uint64_t>();
[ 0:13]    200	
[ 0:13]    201	    test<volatile std::atomic_char, char>();
[ 0:13]    202	    test<volatile std::atomic_schar, signed char>();
[ 0:13]    203	    test<volatile std::atomic_uchar, unsigned char>();
[ 0:13]    204	    test<volatile std::atomic_short, short>();
[ 0:13]    205	    test<volatile std::atomic_ushort, unsigned short>();
[ 0:13]    206	    test<volatile std::atomic_int, int>();
[ 0:13]    207	    test<volatile std::atomic_uint, unsigned int>();
[ 0:13]    208	    test<volatile std::atomic_long, long>();
[ 0:13]    209	    test<volatile std::atomic_ulong, unsigned long>();
[ 0:13]    210	    test<volatile std::atomic_llong, long long>();
[ 0:13]    211	    test<volatile std::atomic_ullong, unsigned long long>();
[ 0:13]    212	#ifndef _LIBCPP_HAS_NO_UNICODE_CHARS
[ 0:13]    213	    test<volatile std::atomic_char16_t, char16_t>();
[ 0:13]    214	    test<volatile std::atomic_char32_t, char32_t>();
[ 0:13]    215	#endif  // _LIBCPP_HAS_NO_UNICODE_CHARS
[ 0:13]    216	    test<volatile std::atomic_wchar_t, wchar_t>();
[ 0:13]    217	
[ 0:13]    218	    test<volatile std::atomic_int8_t,    int8_t>();
[ 0:13]    219	    test<volatile std::atomic_uint8_t,  uint8_t>();
[ 0:13]    220	    test<volatile std::atomic_int16_t,   int16_t>();
[ 0:13]    221	    test<volatile std::atomic_uint16_t, uint16_t>();
[ 0:13]    222	    test<volatile std::atomic_int32_t,   int32_t>();
[ 0:13]    223	    test<volatile std::atomic_uint32_t, uint32_t>();
[ 0:13]    224	    test<volatile std::atomic_int64_t,   int64_t>();
[ 0:13]    225	    test<volatile std::atomic_uint64_t, uint64_t>();
[ 0:13]    226	
[ 0:13]    227	  return 0;
[ 0:13]    228	}
[ 0:13] # no errors were expected but one was found anyway