Hi KLEE developer group members:
I am new to KLEE; These days I want to do some experiments on Cloud9 (build
based on KLEE), when I run a program as following:
#include<klee/klee.h>
int main(){
int a;
klee_make_symbolic(...);
if(a>0)
return 1;
else
return -1;
}
I found the generated .ll file will not show an expected br instruction for
the branching point;
the actual llvm instruction for the branching point in the .ll file is:
%. = select i1 %cmp,
i32 1, i32 -1;
what's more, only one test case generated for this program;
The developer of Cloud9 told me this might be due to KLEE compiler
optimization or some other reason. Is anybody can tell me why?
Is there any way I can stop this optimization?
Best Regards.
Bing
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev