[klee-dev] concretized symbolic size

[Michael]

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 <sp1ff at pobox.com>