[ 0:00] compiling /home/xrockai/src/divine/nightly/test/lang-c/global-memset-overflow.c [ 0:00] /home/xrockai/src/divine/nightly/test/lang-c/global-memset-overflow.c:5:5: warning: implicitly declaring library function 'memset' with type 'void *(void *, int, unsigned long)' [ 0:00] memset( array, 1, 3 * sizeof( int ) ); /* ERROR */ [ 0:00] ^ [ 0:00] /home/xrockai/src/divine/nightly/test/lang-c/global-memset-overflow.c:5:5: note: include the header or explicitly provide a declaration for 'memset' [ 0:00] 1 warning generated. [ 0:00] compiling /dios/lib/config/seq.bc [ 0:00] setting up pass: functionmeta, options = [ 0:01] setting up pass: fuse-ctors, options = [ 0:01] KLEE: output directory is "/var/obj/divine-nightly/semidbg/test/__test_work_dir.12/_klee_out" [ 0:02] KLEE: Using Z3 solver backend [ 0:02] WARNING: this target does not support the llvm.stacksave intrinsic. [ 0:02] warning: Linking two modules of different target triples: klee_div_zero_check.bc' is 'x86_64-pc-linux-gnu' whereas 'klee.bc' is 'x86_64-unknown-none-elf' [ 0:02] [ 0:02] KLEE: WARNING: undefined reference to function: klee_free [ 0:02] KLEE: WARNING: undefined reference to function: klee_malloc [ 0:02] about to __boot:0 [ 0:02] KLEE: WARNING ONCE: Alignment of memory from call "klee_malloc" is not modelled. Using alignment of 8. [ 0:02] about to run the scheduler:0 [ 0:02] [ 0:02] KLEE: done: total instructions = 14976 [ 0:02] KLEE: done: completed paths = 1 [ 0:02] KLEE: done: generated tests = 0 [ 0:02] 1 /* TAGS: error min c segv */ [ 0:02] 2 int array[2]; [ 0:02] 3 int main() [ 0:02] 4 { [ 0:02] 5 memset( array, 1, 3 * sizeof( int ) ); /* ERROR */ [ 0:02] 6 return 0; [ 0:02] 7 } [ 0:02] # expected error to be found at /home/xrockai/src/divine/nightly/test/lang-c/global-memset-overflow.c:5, but it was not