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: [email protected]
To: [email protected]
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?


_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev                              
          
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Reply via email to