[klee-dev] KLEE with Non-linear integer constraint; warning about the external 'put'

[Cristian Cadar]

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