[ 0:01] compiling /home/xrockai/src/divine/nightly/test/svcomp/bitvector/byte_add_false.c [ 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.23/_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: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] 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: 34538 [ 0:07] Stack: [ 0:07] #000034538 in __dios_start (l=0, argc=1, argv=94792304235016, envp=94792304312328) at /dios/libc/sys/start.cpp:87 [ 0:07] #100010557 in _ZN6__dios10sched_nullINS_5ClockINS_10NondetKleeINS_4BaseEEEEEE13run_schedulerINS_7ContextEEEvv () at /dios/sys/sched_null.hpp:163 [ 0:07] #200042888 in klee_boot (argc=2, argv=94792278833920) at /dios/arch/klee/boot.c:41 [ 0:07] [ 0:07] [ 0:07] 1 /* TAGS: error c sym */ [ 0:07] 2 /* VERIFY_OPTS: --symbolic --sequential -o nofail:malloc */ [ 0:07] 3 extern void __VERIFIER_error() __attribute__ ((__noreturn__)); [ 0:07] 4 [ 0:07] 5 extern unsigned int __VERIFIER_nondet_uint(void); [ 0:07] 6 void __VERIFIER_assert(int cond) { [ 0:07] 7 if (!(cond)) { [ 0:07] 8 ERROR: __VERIFIER_error(); [ 0:07] 9 } [ 0:07] 10 return; [ 0:07] 11 } [ 0:07] 12 /* emulates multi-precision addition */ [ 0:07] 13 #include [ 0:07] 14 [ 0:07] 15 unsigned int mp_add(unsigned int a, unsigned int b) [ 0:07] 16 { [ 0:07] 17 unsigned char a0, a1, a2, a3; [ 0:07] 18 unsigned char b0, b1, b2, b3; [ 0:07] 19 unsigned char r0, r1, r2, r3; [ 0:07] 20 [ 0:07] 21 unsigned short carry; [ 0:07] 22 unsigned short partial_sum; [ 0:07] 23 unsigned int r; [ 0:07] 24 unsigned char i; [ 0:07] 25 unsigned char na, nb; [ 0:07] 26 [ 0:07] 27 a0 = a; [ 0:07] 28 a1 = a >> 8; [ 0:07] 29 a2 = a >> 16U; [ 0:07] 30 a3 = a >> 24U; [ 0:07] 31 [ 0:07] 32 b0 = b; [ 0:07] 33 b1 = b >> 8U; [ 0:07] 34 b2 = b >> 16U; [ 0:07] 35 b3 = b >> 24U; [ 0:07] 36 [ 0:07] 37 na = (unsigned char)4; /* num of components of a */ [ 0:07] 38 if (a3 == (unsigned char)0) { [ 0:07] 39 na = na - 1; [ 0:07] 40 if (a2 == (unsigned char)0) { [ 0:07] 41 na = na - 1; [ 0:07] 42 if (a1 == (unsigned char)0) { [ 0:07] 43 na = na - 1; [ 0:07] 44 } [ 0:07] 45 } [ 0:07] 46 } [ 0:07] 47 [ 0:07] 48 nb = (unsigned char)4; /* num of components of b */ [ 0:07] 49 if (b3 == (unsigned char)0) { [ 0:07] 50 nb = nb - 1; [ 0:07] 51 if (b2 == (unsigned char)0) { [ 0:07] 52 nb = nb - 1; [ 0:07] 53 if (b1 == (unsigned char)0) { [ 0:07] 54 nb = nb - 1; [ 0:07] 55 } [ 0:07] 56 } [ 0:07] 57 } [ 0:07] 58 [ 0:07] 59 carry = (unsigned short)0; [ 0:07] 60 i = (unsigned char)0; [ 0:07] 61 while ((i < na) || (i < nb) || (carry != (unsigned short)0)) { [ 0:07] 62 partial_sum = carry; [ 0:07] 63 carry = (unsigned short)0; [ 0:07] 64 [ 0:07] 65 if (i < na) { [ 0:07] 66 if (i == (unsigned char)0) { partial_sum = partial_sum + a0; } [ 0:07] 67 if (i == (unsigned char)1) { partial_sum = partial_sum + a1; } [ 0:07] 68 if (i == (unsigned char)2) { partial_sum = partial_sum + a2; } [ 0:07] 69 if (i == (unsigned char)3) { partial_sum = partial_sum + a3; } [ 0:07] 70 } [ 0:07] 71 if (i < nb) { [ 0:07] 72 if (i == (unsigned char)0) { partial_sum = partial_sum + b0; } [ 0:07] 73 if (i == (unsigned char)1) { partial_sum = partial_sum + b1; } [ 0:07] 74 if (i == (unsigned char)2) { partial_sum = partial_sum + b2; } [ 0:07] 75 if (i == (unsigned char)3) { partial_sum = partial_sum + b3; } [ 0:07] 76 } [ 0:07] 77 if (partial_sum > ((unsigned char)254)) { [ 0:07] 78 partial_sum = partial_sum & ((unsigned char)255); [ 0:07] 79 carry = (unsigned short)1; [ 0:07] 80 } [ 0:07] 81 [ 0:07] 82 if (i == (unsigned char)0) { r0 = (unsigned char)partial_sum; } [ 0:07] 83 if (i == (unsigned char)1) { r1 = (unsigned char)partial_sum; } [ 0:07] 84 if (i == (unsigned char)2) { r2 = (unsigned char)partial_sum; } [ 0:07] 85 if (i == (unsigned char)3) { r3 = (unsigned char)partial_sum; } [ 0:07] 86 [ 0:07] 87 i = i + (unsigned char)1; [ 0:07] 88 } [ 0:07] 89 [ 0:07] 90 while (i < (unsigned char)4) { [ 0:07] 91 if (i == (unsigned char)0) { r0 = (unsigned char)0; } [ 0:07] 92 if (i == (unsigned char)1) { r1 = (unsigned char)0; } [ 0:07] 93 if (i == (unsigned char)2) { r2 = (unsigned char)0; } [ 0:07] 94 if (i == (unsigned char)3) { r3 = (unsigned char)0; } [ 0:07] 95 [ 0:07] 96 i = i + (unsigned char)1; [ 0:07] 97 } [ 0:07] 98 [ 0:07] 99 // (r3 << 24U) is undefined behavior if r3 > 127, because [ 0:07] 100 // r3 gets promoted to int and r3<<24U will exceed INT_MAX [ 0:07] 101 // (see ISO/IEC 9899:2011 6.5.7#4) [ 0:07] 102 r = r0 | (r1 << 8U) | (r2 << 16U) | (r3 << 24U); [ 0:07] 103 [ 0:07] 104 return r; [ 0:07] 105 } [ 0:07] 106 [ 0:07] 107 [ 0:07] 108 int main() [ 0:07] 109 { [ 0:07] 110 unsigned int a, b, r; [ 0:07] 111 [ 0:07] 112 a = __VERIFIER_nondet_uint(); [ 0:07] 113 b = __VERIFIER_nondet_uint(); [ 0:07] 114 [ 0:07] 115 r = mp_add(a, b); [ 0:07] 116 [ 0:07] 117 __VERIFIER_assert(r == a + b); /* ERROR */ [ 0:07] 118 [ 0:07] 119 return 0; [ 0:07] 120 } [ 0:07] # expected error to be found at /home/xrockai/src/divine/nightly/test/svcomp/bitvector/byte_add_false.c:117, but it was not