[ 0:00] compiling /home/xrockai/src/divine/nightly/test/svcomp/bitvector/byte_add_2_true.c [ 0:00] compiling /dios/lib/config/seqklee.bc [ 0:00] 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.17/_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:05] [ 0:05] 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] about to __boot:0 [ 0:07] KLEE: WARNING ONCE: Alignment of memory from call "klee_malloc" is not modelled. Using alignment of 8. [ 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: 34524 [ 0:07] Stack: [ 0:07] #000034524 in __dios_start (l=0, argc=1, argv=94483802415112, envp=94483802433544) at /dios/libc/sys/start.cpp:87 [ 0:07] #100010535 in _ZN6__dios10sched_nullINS_5ClockINS_10NondetKleeINS_4BaseEEEEEE13run_schedulerINS_7ContextEEEvv () at /dios/sys/sched_null.hpp:163 [ 0:07] #200042874 in klee_boot (argc=1, argv=94483789432896) at /dios/arch/klee/boot.c:41 [ 0:07] [ 0:07] [ 0:07] 1 /* VERIFY_OPTS: --symbolic --sequential */ [ 0:07] 2 /* TAGS: sym c */ [ 0:07] 3 #include [ 0:07] 4 extern void __VERIFIER_assert(int);/* emulates multi-precision addition */ [ 0:07] 5 [ 0:07] 6 extern unsigned int __VERIFIER_nondet_uint(void); [ 0:07] 7 [ 0:07] 8 unsigned int mp_add(unsigned int a, unsigned int b) [ 0:07] 9 { [ 0:07] 10 unsigned char a0, a1, a2, a3; [ 0:07] 11 unsigned char b0, b1, b2, b3; [ 0:07] 12 unsigned char r0, r1, r2, r3; [ 0:07] 13 [ 0:07] 14 unsigned short carry; [ 0:07] 15 unsigned short partial_sum; [ 0:07] 16 unsigned int r; [ 0:07] 17 unsigned char i; [ 0:07] 18 unsigned char na, nb; [ 0:07] 19 [ 0:07] 20 a0 = a; [ 0:07] 21 a1 = a >> 8; [ 0:07] 22 a2 = a >> 16U; [ 0:07] 23 a3 = a >> 24U; [ 0:07] 24 [ 0:07] 25 b0 = b; [ 0:07] 26 b1 = b >> 8U; [ 0:07] 27 b2 = b >> 16U; [ 0:07] 28 b3 = b >> 24U; [ 0:07] 29 [ 0:07] 30 na = (unsigned char)4; /* num of components of a */ [ 0:07] 31 if (a3 == (unsigned char)0) { [ 0:07] 32 na = na - 1; [ 0:07] 33 if (a2 == (unsigned char)0) { [ 0:07] 34 na = na - 1; [ 0:07] 35 if (a1 == (unsigned char)0) { [ 0:07] 36 na = na - 1; [ 0:07] 37 } [ 0:07] 38 } [ 0:07] 39 } [ 0:07] 40 [ 0:07] 41 nb = (unsigned char)4; /* num of components of b */ [ 0:07] 42 if (b3 == (unsigned char)0) { [ 0:07] 43 nb = nb - 1; [ 0:07] 44 if (b2 == (unsigned char)0) { [ 0:07] 45 nb = nb - 1; [ 0:07] 46 if (b1 == (unsigned char)0) { [ 0:07] 47 nb = nb - 1; [ 0:07] 48 } [ 0:07] 49 } [ 0:07] 50 } [ 0:07] 51 [ 0:07] 52 carry = (unsigned short)0; [ 0:07] 53 i = (unsigned char)0; [ 0:07] 54 while ((i < na) || (i < nb) || (carry != (unsigned short)0)) { [ 0:07] 55 partial_sum = carry; [ 0:07] 56 carry = (unsigned short)0; [ 0:07] 57 [ 0:07] 58 if (i < na) { [ 0:07] 59 if (i == (unsigned char)0) { partial_sum = partial_sum + a0; } [ 0:07] 60 if (i == (unsigned char)1) { partial_sum = partial_sum + a1; } [ 0:07] 61 if (i == (unsigned char)2) { partial_sum = partial_sum + a2; } [ 0:07] 62 if (i == (unsigned char)3) { partial_sum = partial_sum + a3; } [ 0:07] 63 } [ 0:07] 64 if (i < nb) { [ 0:07] 65 if (i == (unsigned char)0) { partial_sum = partial_sum + b0; } [ 0:07] 66 if (i == (unsigned char)1) { partial_sum = partial_sum + b1; } [ 0:07] 67 if (i == (unsigned char)2) { partial_sum = partial_sum + b2; } [ 0:07] 68 if (i == (unsigned char)3) { partial_sum = partial_sum + b3; } [ 0:07] 69 } [ 0:07] 70 if (partial_sum > ((unsigned char)255)) { [ 0:07] 71 partial_sum = partial_sum & ((unsigned char)255); [ 0:07] 72 carry = (unsigned short)1; [ 0:07] 73 } [ 0:07] 74 [ 0:07] 75 if (i == (unsigned char)0) { r0 = (unsigned char)partial_sum; } [ 0:07] 76 if (i == (unsigned char)1) { r1 = (unsigned char)partial_sum; } [ 0:07] 77 if (i == (unsigned char)2) { r2 = (unsigned char)partial_sum; } [ 0:07] 78 if (i == (unsigned char)3) { r3 = (unsigned char)partial_sum; } [ 0:07] 79 [ 0:07] 80 i = i + (unsigned char)1; [ 0:07] 81 } [ 0:07] 82 [ 0:07] 83 while (i < (unsigned char)4) { [ 0:07] 84 if (i == (unsigned char)0) { r0 = (unsigned char)0; } [ 0:07] 85 if (i == (unsigned char)1) { r1 = (unsigned char)0; } [ 0:07] 86 if (i == (unsigned char)2) { r2 = (unsigned char)0; } [ 0:07] 87 if (i == (unsigned char)3) { r3 = (unsigned char)0; } [ 0:07] 88 [ 0:07] 89 i = i + (unsigned char)1; [ 0:07] 90 } [ 0:07] 91 [ 0:07] 92 r = r0 | (r1 << 8U) | (r2 << 16U) | (r3 << 24U); [ 0:07] 93 [ 0:07] 94 return r; [ 0:07] 95 } [ 0:07] 96 [ 0:07] 97 [ 0:07] 98 int main() [ 0:07] 99 { [ 0:07] 100 unsigned int a = __VERIFIER_nondet_uint(); [ 0:07] 101 unsigned int b, r; [ 0:07] 102 [ 0:07] 103 b = 234770789; [ 0:07] 104 [ 0:07] 105 r = mp_add(a, b); [ 0:07] 106 [ 0:07] 107 __VERIFIER_assert(r == a + b); [ 0:07] 108 [ 0:07] 109 return 0; [ 0:07] 110 } [ 0:07] # no errors were expected but one was found anyway