[klee-dev] KLEE compiler optimization?

[bing liu]

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
-------------- next part --------------
HTML attachment scrubbed and removed