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

[Andrew Santosa]

Dear Javier,
I believe the straight answer is no.
I think Z3, which is now supported by KLEE, supports uninterpreted functions, so itseems possible to implement this feature, but the question is why should C functionbe mathematical function? What if the C function has side effects?

However, a possible workaround to your problem that I could think ofmight be the following:
foo(int a){  int ret_boo = boo(a);
  klee_make_symbolic(&ret_boo, sizeof(ret_boo), "boo(a)");
  if (ret_boo > 0)      return 0;  else      return 1;}
Best,Andrew
 

    On Wednesday, 14 December 2016, 21:29, Javier Godoy <j.godoy277 at gmail.com> wrote:
 

 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! :)
_______________________________________________
klee-dev mailing list
klee-dev at imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


   
-------------- next part --------------
HTML attachment scrubbed and removed