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 <[email protected]>
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
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
