[ 0:01] compiling /home/xrockai/src/divine/nightly/test/libcxx/forwardlist/member_swap.pass.cpp [ 0:01] compiling /dios/lib/config/seqklee.bc [ 0:02] setting up pass: functionmeta, options = [ 0:04] setting up pass: fuse-ctors, options = [ 0:04] KLEE: output directory is "/var/obj/divine-nightly/semidbg/test/__test_work_dir.21/_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: _Z10klee_abortv [ 0:12] KLEE: WARNING: undefined reference to function: __dios_tainted_init [ 0:12] KLEE: WARNING: undefined reference to function: klee_free [ 0:12] KLEE: WARNING: undefined reference to function: klee_malloc [ 0:12] KLEE: WARNING ONCE: Using zero size array fix for landingpad instruction filter [ 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: 90499 [ 0:13] Stack: [ 0:13] #000090499 in __dios_start (l=0, argc=1, argv=93906467672584, envp=93906467741704) at /dios/libc/sys/start.cpp:87 [ 0:13] #100038501 in _ZN6__dios10sched_nullINS_5ClockINS_10NondetKleeINS_4BaseEEEEEE13run_schedulerINS_7ContextEEEvv () at /dios/sys/sched_null.hpp:163 [ 0:13] #200099079 in klee_boot (argc=2, argv=93906436372864) at /dios/arch/klee/boot.c:41 [ 0:13] [ 0:13] [ 0:13] 1 /* TAGS: c++ */ [ 0:13] 2 /* VERIFY_OPTS: -o nofail:malloc */ [ 0:13] 3 //===----------------------------------------------------------------------===// [ 0:13] 4 // [ 0:13] 5 // The LLVM Compiler Infrastructure [ 0:13] 6 // [ 0:13] 7 // This file is dual licensed under the MIT and the University of Illinois Open [ 0:13] 8 // Source Licenses. See LICENSE.TXT for details. [ 0:13] 9 // [ 0:13] 10 //===----------------------------------------------------------------------===// [ 0:13] 11 [ 0:13] 12 // [ 0:13] 13 [ 0:13] 14 // void swap(forward_list& x); [ 0:13] 15 [ 0:13] 16 #include [ 0:13] 17 #include [ 0:13] 18 [ 0:13] 19 #include "test_allocator.h" [ 0:13] 20 #include "min_allocator.h" [ 0:13] 21 [ 0:13] 22 int main() [ 0:13] 23 { [ 0:13] 24 { [ 0:13] 25 typedef int T; [ 0:13] 26 typedef test_allocator A; [ 0:13] 27 typedef std::forward_list C; [ 0:13] 28 const T t1[] = {0, 1, 2, 3, 4, 5}; [ 0:13] 29 C c1(std::begin(t1), std::end(t1), A(1)); [ 0:13] 30 const T t2[] = {10, 11, 12}; [ 0:13] 31 C c2(std::begin(t2), std::end(t2), A(2)); [ 0:13] 32 c1.swap(c2); [ 0:13] 33 [ 0:13] 34 assert(distance(c1.begin(), c1.end()) == 3); [ 0:13] 35 assert(*next(c1.begin(), 0) == 10); [ 0:13] 36 assert(*next(c1.begin(), 1) == 11); [ 0:13] 37 assert(*next(c1.begin(), 2) == 12); [ 0:13] 38 assert(c1.get_allocator() == A(1)); [ 0:13] 39 [ 0:13] 40 assert(distance(c2.begin(), c2.end()) == 6); [ 0:13] 41 assert(*next(c2.begin(), 0) == 0); [ 0:13] 42 assert(*next(c2.begin(), 1) == 1); [ 0:13] 43 assert(*next(c2.begin(), 2) == 2); [ 0:13] 44 assert(*next(c2.begin(), 3) == 3); [ 0:13] 45 assert(*next(c2.begin(), 4) == 4); [ 0:13] 46 assert(*next(c2.begin(), 5) == 5); [ 0:13] 47 assert(c2.get_allocator() == A(2)); [ 0:13] 48 } [ 0:13] 49 { [ 0:13] 50 typedef int T; [ 0:13] 51 typedef test_allocator A; [ 0:13] 52 typedef std::forward_list C; [ 0:13] 53 const T t1[] = {0, 1, 2, 3, 4, 5}; [ 0:13] 54 C c1(std::begin(t1), std::end(t1), A(1)); [ 0:13] 55 C c2(A(2)); [ 0:13] 56 c1.swap(c2); [ 0:13] 57 [ 0:13] 58 assert(distance(c1.begin(), c1.end()) == 0); [ 0:13] 59 assert(c1.get_allocator() == A(1)); [ 0:13] 60 [ 0:13] 61 assert(distance(c2.begin(), c2.end()) == 6); [ 0:13] 62 assert(*next(c2.begin(), 0) == 0); [ 0:13] 63 assert(*next(c2.begin(), 1) == 1); [ 0:13] 64 assert(*next(c2.begin(), 2) == 2); [ 0:13] 65 assert(*next(c2.begin(), 3) == 3); [ 0:13] 66 assert(*next(c2.begin(), 4) == 4); [ 0:13] 67 assert(*next(c2.begin(), 5) == 5); [ 0:13] 68 assert(c2.get_allocator() == A(2)); [ 0:13] 69 } [ 0:13] 70 { [ 0:13] 71 typedef int T; [ 0:13] 72 typedef test_allocator A; [ 0:13] 73 typedef std::forward_list C; [ 0:13] 74 C c1(A(1)); [ 0:13] 75 const T t2[] = {10, 11, 12}; [ 0:13] 76 C c2(std::begin(t2), std::end(t2), A(2)); [ 0:13] 77 c1.swap(c2); [ 0:13] 78 [ 0:13] 79 assert(distance(c1.begin(), c1.end()) == 3); [ 0:13] 80 assert(*next(c1.begin(), 0) == 10); [ 0:13] 81 assert(*next(c1.begin(), 1) == 11); [ 0:13] 82 assert(*next(c1.begin(), 2) == 12); [ 0:13] 83 assert(c1.get_allocator() == A(1)); [ 0:13] 84 [ 0:13] 85 assert(distance(c2.begin(), c2.end()) == 0); [ 0:13] 86 assert(c2.get_allocator() == A(2)); [ 0:13] 87 } [ 0:13] 88 { [ 0:13] 89 typedef int T; [ 0:13] 90 typedef test_allocator A; [ 0:13] 91 typedef std::forward_list C; [ 0:13] 92 C c1(A(1)); [ 0:13] 93 C c2(A(2)); [ 0:13] 94 c1.swap(c2); [ 0:13] 95 [ 0:13] 96 assert(distance(c1.begin(), c1.end()) == 0); [ 0:13] 97 assert(c1.get_allocator() == A(1)); [ 0:13] 98 [ 0:13] 99 assert(distance(c2.begin(), c2.end()) == 0); [ 0:13] 100 assert(c2.get_allocator() == A(2)); [ 0:13] 101 } [ 0:13] 102 [ 0:13] 103 { [ 0:13] 104 typedef int T; [ 0:13] 105 typedef other_allocator A; [ 0:13] 106 typedef std::forward_list C; [ 0:13] 107 const T t1[] = {0, 1, 2, 3, 4, 5}; [ 0:13] 108 C c1(std::begin(t1), std::end(t1), A(1)); [ 0:13] 109 const T t2[] = {10, 11, 12}; [ 0:13] 110 C c2(std::begin(t2), std::end(t2), A(2)); [ 0:13] 111 c1.swap(c2); [ 0:13] 112 [ 0:13] 113 assert(distance(c1.begin(), c1.end()) == 3); [ 0:13] 114 assert(*next(c1.begin(), 0) == 10); [ 0:13] 115 assert(*next(c1.begin(), 1) == 11); [ 0:13] 116 assert(*next(c1.begin(), 2) == 12); [ 0:13] 117 assert(c1.get_allocator() == A(2)); [ 0:13] 118 [ 0:13] 119 assert(distance(c2.begin(), c2.end()) == 6); [ 0:13] 120 assert(*next(c2.begin(), 0) == 0); [ 0:13] 121 assert(*next(c2.begin(), 1) == 1); [ 0:13] 122 assert(*next(c2.begin(), 2) == 2); [ 0:13] 123 assert(*next(c2.begin(), 3) == 3); [ 0:13] 124 assert(*next(c2.begin(), 4) == 4); [ 0:13] 125 assert(*next(c2.begin(), 5) == 5); [ 0:13] 126 assert(c2.get_allocator() == A(1)); [ 0:13] 127 } [ 0:13] 128 { [ 0:13] 129 typedef int T; [ 0:13] 130 typedef other_allocator A; [ 0:13] 131 typedef std::forward_list C; [ 0:13] 132 const T t1[] = {0, 1, 2, 3, 4, 5}; [ 0:13] 133 C c1(std::begin(t1), std::end(t1), A(1)); [ 0:13] 134 C c2(A(2)); [ 0:13] 135 c1.swap(c2); [ 0:13] 136 [ 0:13] 137 assert(distance(c1.begin(), c1.end()) == 0); [ 0:13] 138 assert(c1.get_allocator() == A(2)); [ 0:13] 139 [ 0:13] 140 assert(distance(c2.begin(), c2.end()) == 6); [ 0:13] 141 assert(*next(c2.begin(), 0) == 0); [ 0:13] 142 assert(*next(c2.begin(), 1) == 1); [ 0:13] 143 assert(*next(c2.begin(), 2) == 2); [ 0:13] 144 assert(*next(c2.begin(), 3) == 3); [ 0:13] 145 assert(*next(c2.begin(), 4) == 4); [ 0:13] 146 assert(*next(c2.begin(), 5) == 5); [ 0:13] 147 assert(c2.get_allocator() == A(1)); [ 0:13] 148 } [ 0:13] 149 { [ 0:13] 150 typedef int T; [ 0:13] 151 typedef other_allocator A; [ 0:13] 152 typedef std::forward_list C; [ 0:13] 153 C c1(A(1)); [ 0:13] 154 const T t2[] = {10, 11, 12}; [ 0:13] 155 C c2(std::begin(t2), std::end(t2), A(2)); [ 0:13] 156 c1.swap(c2); [ 0:13] 157 [ 0:13] 158 assert(distance(c1.begin(), c1.end()) == 3); [ 0:13] 159 assert(*next(c1.begin(), 0) == 10); [ 0:13] 160 assert(*next(c1.begin(), 1) == 11); [ 0:13] 161 assert(*next(c1.begin(), 2) == 12); [ 0:13] 162 assert(c1.get_allocator() == A(2)); [ 0:13] 163 [ 0:13] 164 assert(distance(c2.begin(), c2.end()) == 0); [ 0:13] 165 assert(c2.get_allocator() == A(1)); [ 0:13] 166 } [ 0:13] 167 { [ 0:13] 168 typedef int T; [ 0:13] 169 typedef other_allocator A; [ 0:13] 170 typedef std::forward_list C; [ 0:13] 171 C c1(A(1)); [ 0:13] 172 C c2(A(2)); [ 0:13] 173 c1.swap(c2); [ 0:13] 174 [ 0:13] 175 assert(distance(c1.begin(), c1.end()) == 0); [ 0:13] 176 assert(c1.get_allocator() == A(2)); [ 0:13] 177 [ 0:13] 178 assert(distance(c2.begin(), c2.end()) == 0); [ 0:13] 179 assert(c2.get_allocator() == A(1)); [ 0:13] 180 } [ 0:13] 181 #if __cplusplus >= 201103L [ 0:13] 182 { [ 0:13] 183 typedef int T; [ 0:13] 184 typedef min_allocator A; [ 0:13] 185 typedef std::forward_list C; [ 0:13] 186 const T t1[] = {0, 1, 2, 3, 4, 5}; [ 0:13] 187 C c1(std::begin(t1), std::end(t1), A()); [ 0:13] 188 const T t2[] = {10, 11, 12}; [ 0:13] 189 C c2(std::begin(t2), std::end(t2), A()); [ 0:13] 190 c1.swap(c2); [ 0:13] 191 [ 0:13] 192 assert(distance(c1.begin(), c1.end()) == 3); [ 0:13] 193 assert(*next(c1.begin(), 0) == 10); [ 0:13] 194 assert(*next(c1.begin(), 1) == 11); [ 0:13] 195 assert(*next(c1.begin(), 2) == 12); [ 0:13] 196 assert(c1.get_allocator() == A()); [ 0:13] 197 [ 0:13] 198 assert(distance(c2.begin(), c2.end()) == 6); [ 0:13] 199 assert(*next(c2.begin(), 0) == 0); [ 0:13] 200 assert(*next(c2.begin(), 1) == 1); [ 0:13] 201 assert(*next(c2.begin(), 2) == 2); [ 0:13] 202 assert(*next(c2.begin(), 3) == 3); [ 0:13] 203 assert(*next(c2.begin(), 4) == 4); [ 0:13] 204 assert(*next(c2.begin(), 5) == 5); [ 0:13] 205 assert(c2.get_allocator() == A()); [ 0:13] 206 } [ 0:13] 207 { [ 0:13] 208 typedef int T; [ 0:13] 209 typedef min_allocator A; [ 0:13] 210 typedef std::forward_list C; [ 0:13] 211 const T t1[] = {0, 1, 2, 3, 4, 5}; [ 0:13] 212 C c1(std::begin(t1), std::end(t1), A()); [ 0:13] 213 C c2(A{}); [ 0:13] 214 c1.swap(c2); [ 0:13] 215 [ 0:13] 216 assert(distance(c1.begin(), c1.end()) == 0); [ 0:13] 217 assert(c1.get_allocator() == A()); [ 0:13] 218 [ 0:13] 219 assert(distance(c2.begin(), c2.end()) == 6); [ 0:13] 220 assert(*next(c2.begin(), 0) == 0); [ 0:13] 221 assert(*next(c2.begin(), 1) == 1); [ 0:13] 222 assert(*next(c2.begin(), 2) == 2); [ 0:13] 223 assert(*next(c2.begin(), 3) == 3); [ 0:13] 224 assert(*next(c2.begin(), 4) == 4); [ 0:13] 225 assert(*next(c2.begin(), 5) == 5); [ 0:13] 226 assert(c2.get_allocator() == A()); [ 0:13] 227 } [ 0:13] 228 { [ 0:13] 229 typedef int T; [ 0:13] 230 typedef min_allocator A; [ 0:13] 231 typedef std::forward_list C; [ 0:13] 232 C c1(A{}); [ 0:13] 233 const T t2[] = {10, 11, 12}; [ 0:13] 234 C c2(std::begin(t2), std::end(t2), A()); [ 0:13] 235 c1.swap(c2); [ 0:13] 236 [ 0:13] 237 assert(distance(c1.begin(), c1.end()) == 3); [ 0:13] 238 assert(*next(c1.begin(), 0) == 10); [ 0:13] 239 assert(*next(c1.begin(), 1) == 11); [ 0:13] 240 assert(*next(c1.begin(), 2) == 12); [ 0:13] 241 assert(c1.get_allocator() == A()); [ 0:13] 242 [ 0:13] 243 assert(distance(c2.begin(), c2.end()) == 0); [ 0:13] 244 assert(c2.get_allocator() == A()); [ 0:13] 245 } [ 0:13] 246 { [ 0:13] 247 typedef int T; [ 0:13] 248 typedef min_allocator A; [ 0:13] 249 typedef std::forward_list C; [ 0:13] 250 C c1(A{}); [ 0:13] 251 C c2(A{}); [ 0:13] 252 c1.swap(c2); [ 0:13] 253 [ 0:13] 254 assert(distance(c1.begin(), c1.end()) == 0); [ 0:13] 255 assert(c1.get_allocator() == A()); [ 0:13] 256 [ 0:13] 257 assert(distance(c2.begin(), c2.end()) == 0); [ 0:13] 258 assert(c2.get_allocator() == A()); [ 0:13] 259 } [ 0:13] 260 #endif [ 0:13] 261 } [ 0:13] # no errors were expected but one was found anyway