On 25/07/15 17:59, Zhoulai wrote:
Hello,
Hi,
I have two naive questions.
I thought KLEE relies on SMT solver on the theory of linear arithmetics
No, it relies on the theory of bitvectors and arrays.
and therefore, it should be unable to explore path involving non-linear
relation. But I am surprised by the results from testing a program with
a simple polynomial constraint:
/#include <klee/klee.h>
#include <stdio.h>
int foo(int x) {
int y = x*x*x+x*x+x;
if (y == 1110){
.......
}
/
/ return 0;
/
/}
int main() {
int a;
klee_make_symbolic(&a, sizeof(a), "a");
return foo(a);
}
/
KLEE successfully triggers the branch 'y==1110', Why?
*Another question:* I got a warning from symbolically executing the
program above:
/
KLEE: WARNING ONCE: calling external: puts(169520648)/
What does the warning mean?
The function puts is not instrumented.
Best,
Cristian
Thanks for your ideas.
Zhoulai
_______________________________________________
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
