[klee-dev] KLEE compiler optimization?

[Jonathan Neuschäfer]

On Thu, Jan 31, 2013 at 01:27:48AM -0500, bing liu wrote:
> 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;

I reckon your example is too trivial. The two branches of the "if" don't
acually do something different. If you, for example do the following,
you should get a branch instruction:

int main(int a)
{
	if (a > 0)
		return 1;
	else
		return -2*a;
}

> 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?

Is klee called with "-optimize" on the command line at some point?


HTH,
Jonathan Neuschäfer