Thx Daniel. Got that (the three states); my question is why does
your State 3 need to exist at all? This doesn not seem like an
error to me.
Guo,Shengjian <[email protected]> writes:
Hi,
To my understanding, KLEE will maintain three states in handling
a symbolic-size memory allocation:
State 1 -- tries to allocate a concrete size buffer, which is
128 by default.
State 2 (forked from State 1) -- assigns a NULL return value to
the "calloc" function call.
State 3 (forked from State 2) -- the "concretized symbolic size"
error state, as you witnessed.
Daniel.
On 2/13/21, 11:10, "[email protected] on behalf of
Michael" <[email protected] on behalf of
[email protected]> wrote:
Hi,
I'm using klee for the first time and am seeing it stop with
the
following error:
KLEE: ERROR: EXITING ON ERROR:
Error: concretized symbolic size
File: libc/misc/dirent/opendir.c
Line: 74
assembly.ll line: 37501
State: 48
Stack:
#000037501 in opendir (=94123719640632) at
libc/misc/dirent/opendir.c:74
#100027688 in apprentice_load (=94123697244416,
=94123719640632, =0) at
../../src/apprentice.c:1394
#200027566 in apprentice_1 (=94123697244416,
=94123719640632, =0) at ../../src/apprentice.c:465
#300027427 in file_apprentice (=94123697244416,
=94123719026688, =0) at ../../src/apprentice.c:716
#400033959 in magic_load (=94123697244416,
=94123719026688) at ../../src/magic.c: 302
#500002320 in load (=94123719026688, =0) at
../../src/file.c:479
#600002034 in __klee_posix_wrapped_main (=4,
=94123719649200) at ../../src/file.c:401
#700037208 in __user_main (=7, =94123690168064,
=94123690168128) at
runtime/POSIX/klee_init_env.c:245
#800001460 in __uClibc_main (=7, =94123690168064)
at
libc/misc/internals/__uClibc_main.c:401
#900001626 in main (=7, =94123690168064)
I *think* I understand what's happening. The code is calling
calloc with a size argument that it read from the (symbolic)
file
system. Reading Executor::initializeGlobalAlias, klee
correctly
sees that this could be a very large number causing the
allocation to fail.
My question is: so what if it fails? In ths particular case,
the
code under test would detect that & handle it. Would it not
be
better for klee to assume allocation failure, return nil to
the
caller & let the chips fall where they may?
Or am I missing something?
Thanks for this great tool, BTW.
--
Michael <[email protected]>
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
--
Michael <[email protected]>
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
