[ 0:01] compiling /home/xrockai/src/divine/nightly/test/libcxx/atomic/types.generic.bool.pass.cpp [ 0:01] compiling /dios/lib/config/seqklee.bc [ 0:01] setting up pass: functionmeta, options = [ 0:02] setting up pass: fuse-ctors, options = [ 0:02] KLEE: output directory is "/var/obj/divine-nightly/semidbg/test/__test_work_dir.20/_klee_out" [ 0:04] KLEE: Using Z3 solver backend [ 0:04] WARNING: this target does not support the llvm.stacksave intrinsic. [ 0:04] 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:04] [ 0:04] KLEE: WARNING: undefined reference to function: __dios_tainted_init [ 0:07] KLEE: WARNING: undefined reference to function: klee_free [ 0:07] KLEE: WARNING: undefined reference to function: klee_malloc [ 0:07] i:1 [ 0:07] KLEE: WARNING ONCE: Alignment of memory from call "klee_malloc" is not modelled. Using alignment of 8. [ 0:07] about to __boot:0 [ 0:07] about to run the scheduler:0 [ 0:07] KLEE: WARNING ONCE: calling external: __dios_tainted_init() at /dios/libc/sys/start.cpp:49 5 [ 0:07] KLEE: ERROR: /dios/libc/sys/start.cpp:87: failed external call: __dios_tainted_init [ 0:07] KLEE: NOTE: now ignoring this error at this location [ 0:07] KLEE: ERROR: EXITING ON ERROR: [ 0:07] Error: failed external call: __dios_tainted_init [ 0:07] File: /dios/libc/sys/start.cpp [ 0:07] Line: 87 [ 0:07] assembly.ll line: 44780 [ 0:07] Stack: [ 0:07] #000044780 in __dios_start (l=0, argc=1, argv=93960162292232, envp=93960162361352) at /dios/libc/sys/start.cpp:87 [ 0:07] #100020789 in _ZN6__dios10sched_nullINS_5ClockINS_10NondetKleeINS_4BaseEEEEEE13run_schedulerINS_7ContextEEEvv () at /dios/sys/sched_null.hpp:163 [ 0:07] #200053028 in klee_boot (argc=2, argv=93960132605952) at /dios/arch/klee/boot.c:41 [ 0:07] [ 0:07] [ 0:07] 1 /* TAGS: c++ */ [ 0:07] 2 /* VERIFY_OPTS: -o nofail:malloc */ [ 0:07] 3 //===----------------------------------------------------------------------===// [ 0:07] 4 // [ 0:07] 5 // The LLVM Compiler Infrastructure [ 0:07] 6 // [ 0:07] 7 // This file is dual licensed under the MIT and the University of Illinois Open [ 0:07] 8 // Source Licenses. See LICENSE.TXT for details. [ 0:07] 9 // [ 0:07] 10 //===----------------------------------------------------------------------===// [ 0:07] 11 // [ 0:07] 12 // UNSUPPORTED: libcpp-has-no-threads [ 0:07] 13 [ 0:07] 14 // [ 0:07] 15 [ 0:07] 16 // template [ 0:07] 17 // struct atomic [ 0:07] 18 // { [ 0:07] 19 // bool is_lock_free() const volatile; [ 0:07] 20 // bool is_lock_free() const; [ 0:07] 21 // void store(T desr, memory_order m = memory_order_seq_cst) volatile; [ 0:07] 22 // void store(T desr, memory_order m = memory_order_seq_cst); [ 0:07] 23 // T load(memory_order m = memory_order_seq_cst) const volatile; [ 0:07] 24 // T load(memory_order m = memory_order_seq_cst) const; [ 0:07] 25 // operator T() const volatile; [ 0:07] 26 // operator T() const; [ 0:07] 27 // T exchange(T desr, memory_order m = memory_order_seq_cst) volatile; [ 0:07] 28 // T exchange(T desr, memory_order m = memory_order_seq_cst); [ 0:07] 29 // bool compare_exchange_weak(T& expc, T desr, [ 0:07] 30 // memory_order s, memory_order f) volatile; [ 0:07] 31 // bool compare_exchange_weak(T& expc, T desr, memory_order s, memory_order f); [ 0:07] 32 // bool compare_exchange_strong(T& expc, T desr, [ 0:07] 33 // memory_order s, memory_order f) volatile; [ 0:07] 34 // bool compare_exchange_strong(T& expc, T desr, [ 0:07] 35 // memory_order s, memory_order f); [ 0:07] 36 // bool compare_exchange_weak(T& expc, T desr, [ 0:07] 37 // memory_order m = memory_order_seq_cst) volatile; [ 0:07] 38 // bool compare_exchange_weak(T& expc, T desr, [ 0:07] 39 // memory_order m = memory_order_seq_cst); [ 0:07] 40 // bool compare_exchange_strong(T& expc, T desr, [ 0:07] 41 // memory_order m = memory_order_seq_cst) volatile; [ 0:07] 42 // bool compare_exchange_strong(T& expc, T desr, [ 0:07] 43 // memory_order m = memory_order_seq_cst); [ 0:07] 44 // [ 0:07] 45 // atomic() = default; [ 0:07] 46 // constexpr atomic(T desr); [ 0:07] 47 // atomic(const atomic&) = delete; [ 0:07] 48 // atomic& operator=(const atomic&) = delete; [ 0:07] 49 // atomic& operator=(const atomic&) volatile = delete; [ 0:07] 50 // T operator=(T) volatile; [ 0:07] 51 // T operator=(T); [ 0:07] 52 // }; [ 0:07] 53 // [ 0:07] 54 // typedef atomic atomic_bool; [ 0:07] 55 [ 0:07] 56 #include [ 0:07] 57 #include [ 0:07] 58 #include [ 0:07] 59 [ 0:07] 60 #include "cmpxchg_loop.old.h" [ 0:07] 61 [ 0:07] 62 int main() [ 0:07] 63 { [ 0:07] 64 { [ 0:07] 65 volatile std::atomic _; [ 0:07] 66 volatile std::atomic obj(true); [ 0:07] 67 assert(obj == true); [ 0:07] 68 std::atomic_init(&obj, false); [ 0:07] 69 assert(obj == false); [ 0:07] 70 std::atomic_init(&obj, true); [ 0:07] 71 assert(obj == true); [ 0:07] 72 bool b0 = obj.is_lock_free(); [ 0:07] 73 (void)b0; // to placate scan-build [ 0:07] 74 obj.store(false); [ 0:07] 75 assert(obj == false); [ 0:07] 76 obj.store(true, std::memory_order_release); [ 0:07] 77 assert(obj == true); [ 0:07] 78 assert(obj.load() == true); [ 0:07] 79 assert(obj.load(std::memory_order_acquire) == true); [ 0:07] 80 assert(obj.exchange(false) == true); [ 0:07] 81 assert(obj == false); [ 0:07] 82 assert(obj.exchange(true, std::memory_order_relaxed) == false); [ 0:07] 83 assert(obj == true); [ 0:07] 84 bool x = obj; [ 0:07] 85 assert(cmpxchg_weak_loop(obj, x, false) == true); [ 0:07] 86 assert(obj == false); [ 0:07] 87 assert(x == true); [ 0:07] 88 assert(obj.compare_exchange_weak(x, true, [ 0:07] 89 std::memory_order_seq_cst) == false); [ 0:07] 90 assert(obj == false); [ 0:07] 91 assert(x == false); [ 0:07] 92 obj.store(true); [ 0:07] 93 x = true; [ 0:07] 94 assert(cmpxchg_weak_loop(obj, x, false, [ 0:07] 95 std::memory_order_seq_cst, [ 0:07] 96 std::memory_order_seq_cst) == true); [ 0:07] 97 assert(obj == false); [ 0:07] 98 assert(x == true); [ 0:07] 99 x = true; [ 0:07] 100 obj.store(true); [ 0:07] 101 assert(obj.compare_exchange_strong(x, false) == true); [ 0:07] 102 assert(obj == false); [ 0:07] 103 assert(x == true); [ 0:07] 104 assert(obj.compare_exchange_strong(x, true, [ 0:07] 105 std::memory_order_seq_cst) == false); [ 0:07] 106 assert(obj == false); [ 0:07] 107 assert(x == false); [ 0:07] 108 x = true; [ 0:07] 109 obj.store(true); [ 0:07] 110 assert(obj.compare_exchange_strong(x, false, [ 0:07] 111 std::memory_order_seq_cst, [ 0:07] 112 std::memory_order_seq_cst) == true); [ 0:07] 113 assert(obj == false); [ 0:07] 114 assert(x == true); [ 0:07] 115 assert((obj = false) == false); [ 0:07] 116 assert(obj == false); [ 0:07] 117 assert((obj = true) == true); [ 0:07] 118 assert(obj == true); [ 0:07] 119 } [ 0:07] 120 { [ 0:07] 121 std::atomic _; [ 0:07] 122 std::atomic obj(true); [ 0:07] 123 assert(obj == true); [ 0:07] 124 std::atomic_init(&obj, false); [ 0:07] 125 assert(obj == false); [ 0:07] 126 std::atomic_init(&obj, true); [ 0:07] 127 assert(obj == true); [ 0:07] 128 bool b0 = obj.is_lock_free(); [ 0:07] 129 (void)b0; // to placate scan-build [ 0:07] 130 obj.store(false); [ 0:07] 131 assert(obj == false); [ 0:07] 132 obj.store(true, std::memory_order_release); [ 0:07] 133 assert(obj == true); [ 0:07] 134 assert(obj.load() == true); [ 0:07] 135 assert(obj.load(std::memory_order_acquire) == true); [ 0:07] 136 assert(obj.exchange(false) == true); [ 0:07] 137 assert(obj == false); [ 0:07] 138 assert(obj.exchange(true, std::memory_order_relaxed) == false); [ 0:07] 139 assert(obj == true); [ 0:07] 140 bool x = obj; [ 0:07] 141 assert(cmpxchg_weak_loop(obj, x, false) == true); [ 0:07] 142 assert(obj == false); [ 0:07] 143 assert(x == true); [ 0:07] 144 assert(obj.compare_exchange_weak(x, true, [ 0:07] 145 std::memory_order_seq_cst) == false); [ 0:07] 146 assert(obj == false); [ 0:07] 147 assert(x == false); [ 0:07] 148 obj.store(true); [ 0:07] 149 x = true; [ 0:07] 150 assert(cmpxchg_weak_loop(obj, x, false, [ 0:07] 151 std::memory_order_seq_cst, [ 0:07] 152 std::memory_order_seq_cst) == true); [ 0:07] 153 assert(obj == false); [ 0:07] 154 assert(x == true); [ 0:07] 155 x = true; [ 0:07] 156 obj.store(true); [ 0:07] 157 assert(obj.compare_exchange_strong(x, false) == true); [ 0:07] 158 assert(obj == false); [ 0:07] 159 assert(x == true); [ 0:07] 160 assert(obj.compare_exchange_strong(x, true, [ 0:07] 161 std::memory_order_seq_cst) == false); [ 0:07] 162 assert(obj == false); [ 0:07] 163 assert(x == false); [ 0:07] 164 x = true; [ 0:07] 165 obj.store(true); [ 0:07] 166 assert(obj.compare_exchange_strong(x, false, [ 0:07] 167 std::memory_order_seq_cst, [ 0:07] 168 std::memory_order_seq_cst) == true); [ 0:07] 169 assert(obj == false); [ 0:07] 170 assert(x == true); [ 0:07] 171 assert((obj = false) == false); [ 0:07] 172 assert(obj == false); [ 0:07] 173 assert((obj = true) == true); [ 0:07] 174 assert(obj == true); [ 0:07] 175 } [ 0:07] 176 { [ 0:07] 177 std::atomic_bool _; [ 0:07] 178 std::atomic_bool obj(true); [ 0:07] 179 assert(obj == true); [ 0:07] 180 std::atomic_init(&obj, false); [ 0:07] 181 assert(obj == false); [ 0:07] 182 std::atomic_init(&obj, true); [ 0:07] 183 assert(obj == true); [ 0:07] 184 bool b0 = obj.is_lock_free(); [ 0:07] 185 (void)b0; // to placate scan-build [ 0:07] 186 obj.store(false); [ 0:07] 187 assert(obj == false); [ 0:07] 188 obj.store(true, std::memory_order_release); [ 0:07] 189 assert(obj == true); [ 0:07] 190 assert(obj.load() == true); [ 0:07] 191 assert(obj.load(std::memory_order_acquire) == true); [ 0:07] 192 assert(obj.exchange(false) == true); [ 0:07] 193 assert(obj == false); [ 0:07] 194 assert(obj.exchange(true, std::memory_order_relaxed) == false); [ 0:07] 195 assert(obj == true); [ 0:07] 196 bool x = obj; [ 0:07] 197 assert(cmpxchg_weak_loop(obj, x, false) == true); [ 0:07] 198 assert(obj == false); [ 0:07] 199 assert(x == true); [ 0:07] 200 assert(obj.compare_exchange_weak(x, true, [ 0:07] 201 std::memory_order_seq_cst) == false); [ 0:07] 202 assert(obj == false); [ 0:07] 203 assert(x == false); [ 0:07] 204 obj.store(true); [ 0:07] 205 x = true; [ 0:07] 206 assert(cmpxchg_weak_loop(obj, x, false, [ 0:07] 207 std::memory_order_seq_cst, [ 0:07] 208 std::memory_order_seq_cst) == true); [ 0:07] 209 assert(obj == false); [ 0:07] 210 assert(x == true); [ 0:07] 211 x = true; [ 0:07] 212 obj.store(true); [ 0:07] 213 assert(obj.compare_exchange_strong(x, false) == true); [ 0:07] 214 assert(obj == false); [ 0:07] 215 assert(x == true); [ 0:07] 216 assert(obj.compare_exchange_strong(x, true, [ 0:07] 217 std::memory_order_seq_cst) == false); [ 0:07] 218 assert(obj == false); [ 0:07] 219 assert(x == false); [ 0:07] 220 x = true; [ 0:07] 221 obj.store(true); [ 0:07] 222 assert(obj.compare_exchange_strong(x, false, [ 0:07] 223 std::memory_order_seq_cst, [ 0:07] 224 std::memory_order_seq_cst) == true); [ 0:07] 225 assert(obj == false); [ 0:07] 226 assert(x == true); [ 0:07] 227 assert((obj = false) == false); [ 0:07] 228 assert(obj == false); [ 0:07] 229 assert((obj = true) == true); [ 0:07] 230 assert(obj == true); [ 0:07] 231 } [ 0:07] 232 { [ 0:07] 233 typedef std::atomic A; [ 0:07] 234 _ALIGNAS_TYPE(A) char storage[sizeof(A)] = {1}; [ 0:07] 235 A& zero = *new (storage) A(); [ 0:07] 236 assert(zero == false); [ 0:07] 237 zero.~A(); [ 0:07] 238 } [ 0:07] 239 } [ 0:07] # no errors were expected but one was found anyway