[klee-dev] Errors Detected by KLEE-2.1

[Frank Busse]

Hi Mohit,


On Tue, 1 Jun 2021 17:08:20 +0530 (IST)
kmohit <kmohit at cdac.in> wrote:

> But is it possible to find the same error in Klee without using the
> Klee api's (Klee_make_symbolic) which you are using in that example,
> instead of Klee api if we make Klee symbolic via command line
> argument ( --sym-stdin).

I just used the symbolic variable to generate all three errors in one
run. Just drop the switch (or switch on a symbolic argv[]) for the case
you're interested in.

> I am not getting the same error (ptr.err).
> So could you help me out with any example or any explanations. Here,
> the code
> 
> #include<stdlib.h>
> 
> int global[3];
> 
> int main()
> {
>  free(global);
> }

I'm a little confused - you're using the free.err example to generate a
ptr.err?


Kind regards,

Frank