[ 0:01] compiling /home/xrockai/src/divine/nightly/test/libcxx/deque/types.pass.cpp
[ 0:01] 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.10/_klee_out"
[ 0:05] KLEE: Using Z3 solver backend
[ 0:05] WARNING: this target does not support the llvm.stacksave intrinsic.
[ 0:05] 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:06] 
[ 0:06] KLEE: WARNING: undefined reference to function: __dios_tainted_init
[ 0:08] KLEE: WARNING: undefined reference to function: klee_free
[ 0:08] KLEE: WARNING: undefined reference to function: klee_malloc
[ 0:08] i:1
[ 0:09] KLEE: WARNING ONCE: Alignment of memory from call "klee_malloc" is not modelled. Using alignment of 8.
[ 0:09] about to __boot:0
[ 0:09] about to run the scheduler:0
[ 0:09] KLEE: WARNING ONCE: calling external: __dios_tainted_init() at /dios/libc/sys/start.cpp:49 5
[ 0:09] KLEE: ERROR: /dios/libc/sys/start.cpp:87: failed external call: __dios_tainted_init
[ 0:09] KLEE: NOTE: now ignoring this error at this location
[ 0:09] KLEE: ERROR: EXITING ON ERROR:
[ 0:09] Error: failed external call: __dios_tainted_init
[ 0:09] File: /dios/libc/sys/start.cpp
[ 0:09] Line: 87
[ 0:09] assembly.ll line: 33989
[ 0:09] Stack: 
[ 0:09] 	#000033989 in __dios_start (l=0, argc=1, argv=94401802236424, envp=94401802305544) at /dios/libc/sys/start.cpp:87
[ 0:09] 	#100010015 in _ZN6__dios10sched_nullINS_5ClockINS_10NondetKleeINS_4BaseEEEEEE13run_schedulerINS_7ContextEEEvv () at /dios/sys/sched_null.hpp:163
[ 0:09] 	#200042254 in klee_boot (argc=2, argv=94401775794944) at /dios/arch/klee/boot.c:41
[ 0:09] 
[ 0:09] 
[ 0:09]      1	/* TAGS: c++ */
[ 0:09]      2	/* VERIFY_OPTS: -o nofail:malloc */
[ 0:09]      3	//===----------------------------------------------------------------------===//
[ 0:09]      4	//
[ 0:09]      5	//                     The LLVM Compiler Infrastructure
[ 0:09]      6	//
[ 0:09]      7	// This file is dual licensed under the MIT and the University of Illinois Open
[ 0:09]      8	// Source Licenses. See LICENSE.TXT for details.
[ 0:09]      9	//
[ 0:09]     10	//===----------------------------------------------------------------------===//
[ 0:09]     11	
[ 0:09]     12	// <deque>
[ 0:09]     13	
[ 0:09]     14	// Test nested types and default template args:
[ 0:09]     15	
[ 0:09]     16	// template <class T, class Allocator = allocator<T> >
[ 0:09]     17	// class deque
[ 0:09]     18	// {
[ 0:09]     19	// public:
[ 0:09]     20	//     typedef T                                        value_type;
[ 0:09]     21	//     typedef Allocator                                allocator_type;
[ 0:09]     22	//     typedef typename allocator_type::reference       reference;
[ 0:09]     23	//     typedef typename allocator_type::const_reference const_reference;
[ 0:09]     24	//     typedef implementation-defined                   iterator;
[ 0:09]     25	//     typedef implementation-defined                   const_iterator;
[ 0:09]     26	//     typedef typename allocator_type::size_type       size_type;
[ 0:09]     27	//     typedef typename allocator_type::difference_type difference_type;
[ 0:09]     28	//     typedef typename allocator_type::pointer         pointer;
[ 0:09]     29	//     typedef typename allocator_type::const_pointer   const_pointer;
[ 0:09]     30	//     typedef std::reverse_iterator<iterator>          reverse_iterator;
[ 0:09]     31	//     typedef std::reverse_iterator<const_iterator>    const_reverse_iterator;
[ 0:09]     32	// };
[ 0:09]     33	
[ 0:09]     34	#include <deque>
[ 0:09]     35	#include <iterator>
[ 0:09]     36	#include <type_traits>
[ 0:09]     37	
[ 0:09]     38	#include "test_allocator.h"
[ 0:09]     39	#include "Copyable.h"
[ 0:09]     40	#include "min_allocator.h"
[ 0:09]     41	
[ 0:09]     42	template <class T, class Allocator>
[ 0:09]     43	void
[ 0:09]     44	test()
[ 0:09]     45	{
[ 0:09]     46	    typedef std::deque<T, Allocator> C;
[ 0:09]     47	
[ 0:09]     48	    static_assert((std::is_same<typename C::value_type, T>::value), "");
[ 0:09]     49	    static_assert((std::is_same<typename C::value_type, typename Allocator::value_type>::value), "");
[ 0:09]     50	    static_assert((std::is_same<typename C::allocator_type, Allocator>::value), "");
[ 0:09]     51	    static_assert((std::is_same<typename C::size_type, typename Allocator::size_type>::value), "");
[ 0:09]     52	    static_assert((std::is_same<typename C::difference_type, typename Allocator::difference_type>::value), "");
[ 0:09]     53	    static_assert((std::is_same<typename C::reference, typename Allocator::reference>::value), "");
[ 0:09]     54	    static_assert((std::is_same<typename C::const_reference, typename Allocator::const_reference>::value), "");
[ 0:09]     55	    static_assert((std::is_same<typename C::pointer, typename Allocator::pointer>::value), "");
[ 0:09]     56	    static_assert((std::is_same<typename C::const_pointer, typename Allocator::const_pointer>::value), "");
[ 0:09]     57	    static_assert((std::is_same<
[ 0:09]     58	        typename std::iterator_traits<typename C::iterator>::iterator_category,
[ 0:09]     59	        std::random_access_iterator_tag>::value), "");
[ 0:09]     60	    static_assert((std::is_same<
[ 0:09]     61	        typename std::iterator_traits<typename C::const_iterator>::iterator_category,
[ 0:09]     62	        std::random_access_iterator_tag>::value), "");
[ 0:09]     63	    static_assert((std::is_same<
[ 0:09]     64	        typename C::reverse_iterator,
[ 0:09]     65	        std::reverse_iterator<typename C::iterator> >::value), "");
[ 0:09]     66	    static_assert((std::is_same<
[ 0:09]     67	        typename C::const_reverse_iterator,
[ 0:09]     68	        std::reverse_iterator<typename C::const_iterator> >::value), "");
[ 0:09]     69	}
[ 0:09]     70	
[ 0:09]     71	int main()
[ 0:09]     72	{
[ 0:09]     73	    test<int, test_allocator<int> >();
[ 0:09]     74	    test<int*, std::allocator<int*> >();
[ 0:09]     75	    test<Copyable, test_allocator<Copyable> >();
[ 0:09]     76	    static_assert((std::is_same<std::deque<char>::allocator_type,
[ 0:09]     77	                                std::allocator<char> >::value), "");
[ 0:09]     78	#if __cplusplus >= 201103L
[ 0:09]     79	    {
[ 0:09]     80	        typedef std::deque<short, min_allocator<short>> C;
[ 0:09]     81	        static_assert((std::is_same<C::value_type, short>::value), "");
[ 0:09]     82	        static_assert((std::is_same<C::allocator_type, min_allocator<C::value_type> >::value), "");
[ 0:09]     83	        static_assert((std::is_same<C::reference, C::value_type&>::value), "");
[ 0:09]     84	        static_assert((std::is_same<C::const_reference, const C::value_type&>::value), "");
[ 0:09]     85	        static_assert((std::is_same<C::pointer, min_pointer<C::value_type>>::value), "");
[ 0:09]     86	        static_assert((std::is_same<C::const_pointer, min_pointer<const C::value_type>>::value), "");
[ 0:09]     87	//  min_allocator doesn't have a size_type, so one gets synthesized
[ 0:09]     88	        static_assert((std::is_same<C::size_type, std::make_unsigned<C::difference_type>::type>::value), "");
[ 0:09]     89	        static_assert((std::is_same<C::difference_type, std::ptrdiff_t>::value), "");
[ 0:09]     90	    }
[ 0:09]     91	#endif
[ 0:09]     92	}
[ 0:09] # no errors were expected but one was found anyway