[klee-dev] Klee Symbolic Pointers

[Frank Busse]

Hi,


On Fri, 28 Jun 2019 16:07:44 -0400
Charles Noble <charlesddnoble at gmail.com> wrote:

> PATH 2:
> [ (1 == sym_len),
>   !(0 == sym_src) ]
> 
> SYM MEMORY:
> sym_dest = sym_src[0]
> sym_src = sym_src[0]
> 
> From what I understand of KLEE, if the src pointer is not symbolic then
> there will only be a single path and if the src pointer is symbolic, then
> KLEE will generate many paths when it is derefenced due to the not knowing
> the which address that the symbolic pointer points to. Is there any way
> that I run KLEE to generate both paths while avoiding the pointer
> resolution issue?

could you elaborate a little bit? In the second case KLEE selects
possible memory objects, that's why it forks (once in L: src == NULL
and n times in the load for L: *d++ = *s++).

How should KLEE know where the pointer might point to (there is no
allocation for src)? If it concretises src, it probably will return
nullptr and dest as possible values. If you add a malloc of size 1 it
should add this object as another path.


Kind regards,

Frank