Hello,
I have two naive questions.
I thought KLEE relies on SMT solver on the theory of linear arithmetics 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?
Thanks for your ideas.
Zhoulai
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
