Question

[Surbhi Goel]

Hi!

I'm using KLEE to generate test cases for simple programs. For some reason
it always generates 0 (in case I take an int) and if 0 satisfies a
particular path, it will check that and not put this condition through to
STP. I wish to change that. How can I?

[Urmas Repinski]

Hello, Surbhi.

Can you paste the code of the simple program and KLEE instrumentation for the variables, that the value is generated by the KLEE for?
There possibly syntax errors in the code for test generation.

Another reason is that variable, that the value if generated for, is not used anywhere future in the code.
In this case value 0 will activate all possible paths, as in any other paths for program execution variable does not exist.
In this case error in the C program, as this is meaningless program, where input is provided but not used anywhere.

Check program code, klee instrumentation code, and paste instrumented simple program to the list please if there is no syntax errors,
Urmas Repinski

Date: Thu, 20 Jun 2013 13:58:29 -0400
From: surbhi18-***@public.gmane.org
To: klee-dev-AQ/***@public.gmane.org
Subject: [klee-dev] Question

Hi!
I'm using KLEE to generate test cases for simple programs. For some reason it always generates 0 (in case I take an int) and if 0 satisfies a particular path, it will check that and not put this condition through to STP. I wish to change that. How can I?