[klee-dev] Is possible to mark a function as uninterpreted function?

[Javier Godoy]

Hi!

Is possible to mark a function as uninterpreted function in Klee?

Example i need:


foo(int a)
{
  if( boo(a) > 0)
      return 0;
  else
      return 1;
}

boo(int x) //I want to mark this as uninterpreted
{
 ...
 return x;
}

I need the PC shows "boo(a) >0" AND "boo(a) <= 0". Is posible in Klee?

I dont know any tool that do this.

Thanks! :)
-------------- next part --------------
HTML attachment scrubbed and removed