Hi John, On 24.01.12 22:18, John Regehr wrote: > While writing this up I discovered that when "i" is symbolic Klee cannot > find a value for i that makes this code access an OOB array element:
Could you please paste the complete source code you're running? On my machine, KLEE immediately discovers the OBB error saying that i=6: KLEE: output directory = "klee-out-2" KLEE: WARNING: undefined reference to function: puts KLEE: ERROR: memory error: out of bound pointer KLEE: NOTE: now ignoring this error at this location KLEE: WARNING: calling external: puts(23821840) Error Error KLEE: done: total instructions = 56 KLEE: done: completed paths = 4 KLEE: done: generated tests = 4 $ ktest-tool --write-int klee-last/test000001.ktest ktest file : 'klee-last/test000001.ktest' args : ['obb.o'] num objects: 1 object 0: name: 'i' object 0: size: 4 object 0: data: 6 - Raimondas _______________________________________________ klee-dev mailing list [email protected] http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
