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

Hi Yude, Others would probably have a better idea, but I think replacing calls to libm functions may not cause (many) false positives. I agree this may reduce the number of tests for the same coverage. You may also want to have a look at the paper

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

Hi Andrew, Good from you too! I've never thought about the problem in terms of non-determinism. Yes, our work is related to using summaries, but I actually want to discuss some thing more general here. My understanding of KLEE is that it doesn't do over-approximation. It's either precise or

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

Hi Yude, Good to hear from you! I guess you are replacing function calls with their symbolic summary under the weakest semantics. (What I meant by weakest semantics here can even be nondeterministic, so this is more general than uninterpreted function: In your approach, sequence of f(5) calls

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

Hi Javier, On 14 December 2016 at 13:28, Javier Godoy 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

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

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

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

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