[ 0:01] compiling /home/xrockai/src/divine/nightly/test/libcxx/forwardlist/remove.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.19/_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:11] KLEE: WARNING: undefined reference to function: __dios_tainted_init [ 0:11] KLEE: WARNING: undefined reference to function: klee_free [ 0:11] KLEE: WARNING: undefined reference to function: klee_malloc [ 0:11] KLEE: WARNING ONCE: Using zero size array fix for landingpad instruction filter [ 0:12] i:1 [ 0:12] KLEE: WARNING ONCE: Alignment of memory from call "klee_malloc" is not modelled. Using alignment of 8. [ 0:12] about to __boot:0 [ 0:12] about to run the scheduler:0 [ 0:12] KLEE: WARNING ONCE: calling external: __dios_tainted_init() at /dios/libc/sys/start.cpp:49 5 [ 0:12] KLEE: ERROR: /dios/libc/sys/start.cpp:87: failed external call: __dios_tainted_init [ 0:12] KLEE: NOTE: now ignoring this error at this location [ 0:12] KLEE: ERROR: EXITING ON ERROR: [ 0:12] Error: failed external call: __dios_tainted_init [ 0:12] File: /dios/libc/sys/start.cpp [ 0:12] Line: 87 [ 0:12] assembly.ll line: 76280 [ 0:12] Stack: [ 0:12] #000076280 in __dios_start (l=0, argc=1, argv=94503280743944, envp=94503280837640) at /dios/libc/sys/start.cpp:87 [ 0:12] #100024109 in _ZN6__dios10sched_nullINS_5ClockINS_10NondetKleeINS_4BaseEEEEEE13run_schedulerINS_7ContextEEEvv () at /dios/sys/sched_null.hpp:163 [ 0:12] #200084860 in klee_boot (argc=2, argv=94503246802304) at /dios/arch/klee/boot.c:41 [ 0:12] [ 0:12] [ 0:12] 1 /* TAGS: c++ */ [ 0:12] 2 /* VERIFY_OPTS: -o nofail:malloc */ [ 0:12] 3 //===----------------------------------------------------------------------===// [ 0:12] 4 // [ 0:12] 5 // The LLVM Compiler Infrastructure [ 0:12] 6 // [ 0:12] 7 // This file is dual licensed under the MIT and the University of Illinois Open [ 0:12] 8 // Source Licenses. See LICENSE.TXT for details. [ 0:12] 9 // [ 0:12] 10 //===----------------------------------------------------------------------===// [ 0:12] 11 [ 0:12] 12 // [ 0:12] 13 [ 0:12] 14 // void remove(const value_type& v); [ 0:12] 15 [ 0:12] 16 #include [ 0:12] 17 #include [ 0:12] 18 #include [ 0:12] 19 [ 0:12] 20 #include "min_allocator.h" [ 0:12] 21 [ 0:12] 22 struct S { [ 0:12] 23 S(int i) : i_(new int(i)) {} [ 0:12] 24 S(const S &rhs) : i_(new int(*rhs.i_)) {} [ 0:12] 25 S& operator = (const S &rhs) { *i_ = *rhs.i_; return *this; } [ 0:12] 26 ~S () { delete i_; i_ = NULL; } [ 0:12] 27 bool operator == (const S &rhs) const { return *i_ == *rhs.i_; } [ 0:12] 28 int get () const { return *i_; } [ 0:12] 29 int *i_; [ 0:12] 30 }; [ 0:12] 31 [ 0:12] 32 [ 0:12] 33 int main() [ 0:12] 34 { [ 0:12] 35 { [ 0:12] 36 typedef int T; [ 0:12] 37 typedef std::forward_list C; [ 0:12] 38 const T t1[] = {0, 5, 5, 0, 0, 0, 5}; [ 0:12] 39 const T t2[] = {5, 5, 5}; [ 0:12] 40 C c1(std::begin(t1), std::end(t1)); [ 0:12] 41 C c2(std::begin(t2), std::end(t2)); [ 0:12] 42 c1.remove(0); [ 0:12] 43 assert(c1 == c2); [ 0:12] 44 } [ 0:12] 45 { [ 0:12] 46 typedef int T; [ 0:12] 47 typedef std::forward_list C; [ 0:12] 48 const T t1[] = {0, 0, 0, 0}; [ 0:12] 49 C c1(std::begin(t1), std::end(t1)); [ 0:12] 50 C c2; [ 0:12] 51 c1.remove(0); [ 0:12] 52 assert(c1 == c2); [ 0:12] 53 } [ 0:12] 54 { [ 0:12] 55 typedef int T; [ 0:12] 56 typedef std::forward_list C; [ 0:12] 57 const T t1[] = {5, 5, 5}; [ 0:12] 58 const T t2[] = {5, 5, 5}; [ 0:12] 59 C c1(std::begin(t1), std::end(t1)); [ 0:12] 60 C c2(std::begin(t2), std::end(t2)); [ 0:12] 61 c1.remove(0); [ 0:12] 62 assert(c1 == c2); [ 0:12] 63 } [ 0:12] 64 { [ 0:12] 65 typedef int T; [ 0:12] 66 typedef std::forward_list C; [ 0:12] 67 C c1; [ 0:12] 68 C c2; [ 0:12] 69 c1.remove(0); [ 0:12] 70 assert(c1 == c2); [ 0:12] 71 } [ 0:12] 72 { [ 0:12] 73 typedef int T; [ 0:12] 74 typedef std::forward_list C; [ 0:12] 75 const T t1[] = {5, 5, 5, 0}; [ 0:12] 76 const T t2[] = {5, 5, 5}; [ 0:12] 77 C c1(std::begin(t1), std::end(t1)); [ 0:12] 78 C c2(std::begin(t2), std::end(t2)); [ 0:12] 79 c1.remove(0); [ 0:12] 80 assert(c1 == c2); [ 0:12] 81 } [ 0:12] 82 { // LWG issue #526 [ 0:12] 83 typedef int T; [ 0:12] 84 typedef std::forward_list C; [ 0:12] 85 int t1[] = {1, 2, 1, 3, 5, 8, 11}; [ 0:12] 86 int t2[] = { 2, 3, 5, 8, 11}; [ 0:12] 87 C c1(std::begin(t1), std::end(t1)); [ 0:12] 88 C c2(std::begin(t2), std::end(t2)); [ 0:12] 89 c1.remove(c1.front()); [ 0:12] 90 assert(c1 == c2); [ 0:12] 91 } [ 0:12] 92 { [ 0:12] 93 typedef S T; [ 0:12] 94 typedef std::forward_list C; [ 0:12] 95 int t1[] = {1, 2, 1, 3, 5, 8, 11, 1}; [ 0:12] 96 int t2[] = { 2, 3, 5, 8, 11 }; [ 0:12] 97 C c; [ 0:12] 98 for(int *ip = std::end(t1); ip != std::begin(t1);) [ 0:12] 99 c.push_front(S(*--ip)); [ 0:12] 100 c.remove(c.front()); [ 0:12] 101 C::const_iterator it = c.begin(); [ 0:12] 102 for(int *ip = std::begin(t2); ip != std::end(t2); ++ip, ++it) { [ 0:12] 103 assert ( it != c.end()); [ 0:12] 104 assert ( *ip == it->get()); [ 0:12] 105 } [ 0:12] 106 assert ( it == c.end ()); [ 0:12] 107 } [ 0:12] 108 #if __cplusplus >= 201103L [ 0:12] 109 { [ 0:12] 110 typedef int T; [ 0:12] 111 typedef std::forward_list> C; [ 0:12] 112 const T t1[] = {0, 5, 5, 0, 0, 0, 5}; [ 0:12] 113 const T t2[] = {5, 5, 5}; [ 0:12] 114 C c1(std::begin(t1), std::end(t1)); [ 0:12] 115 C c2(std::begin(t2), std::end(t2)); [ 0:12] 116 c1.remove(0); [ 0:12] 117 assert(c1 == c2); [ 0:12] 118 } [ 0:12] 119 { [ 0:12] 120 typedef int T; [ 0:12] 121 typedef std::forward_list> C; [ 0:12] 122 const T t1[] = {0, 0, 0, 0}; [ 0:12] 123 C c1(std::begin(t1), std::end(t1)); [ 0:12] 124 C c2; [ 0:12] 125 c1.remove(0); [ 0:12] 126 assert(c1 == c2); [ 0:12] 127 } [ 0:12] 128 { [ 0:12] 129 typedef int T; [ 0:12] 130 typedef std::forward_list> C; [ 0:12] 131 const T t1[] = {5, 5, 5}; [ 0:12] 132 const T t2[] = {5, 5, 5}; [ 0:12] 133 C c1(std::begin(t1), std::end(t1)); [ 0:12] 134 C c2(std::begin(t2), std::end(t2)); [ 0:12] 135 c1.remove(0); [ 0:12] 136 assert(c1 == c2); [ 0:12] 137 } [ 0:12] 138 { [ 0:12] 139 typedef int T; [ 0:12] 140 typedef std::forward_list> C; [ 0:12] 141 C c1; [ 0:12] 142 C c2; [ 0:12] 143 c1.remove(0); [ 0:12] 144 assert(c1 == c2); [ 0:12] 145 } [ 0:12] 146 { [ 0:12] 147 typedef int T; [ 0:12] 148 typedef std::forward_list> C; [ 0:12] 149 const T t1[] = {5, 5, 5, 0}; [ 0:12] 150 const T t2[] = {5, 5, 5}; [ 0:12] 151 C c1(std::begin(t1), std::end(t1)); [ 0:12] 152 C c2(std::begin(t2), std::end(t2)); [ 0:12] 153 c1.remove(0); [ 0:12] 154 assert(c1 == c2); [ 0:12] 155 } [ 0:12] 156 #endif [ 0:12] 157 } [ 0:12] # no errors were expected but one was found anyway