Hi,
I made a simple program to produce even number for any symbolic input x.
#include <assert.h>
int even(int x) {
if( (x % 2) == 0) x = x + 2;
else x = x + 1;
assert(x % 2 == 0);
return x;
}
int main() {
int x;
klee_make_symbolic(&x, sizeof(x), "x");
return even(x);
}
I tried to understand how KLEE able to reason about x whether x is even
or not.
My question is, how the operation of addition of x is store? and later
use for reasoning
about x in the assertion formula.
I have printed the query used by the solver, such as:
array x[4] : w32 -> w8 = symbolic
(query [(Eq 0
(And w32 (ReadLSB w32 0 x)
1))]
false []
[x])
# OK -- Elapsed: 2.598763e-05
# Solvable: true
# x = [0,0,0,0]
But, the query is quite general and does not further describe the
constraint of x.
I expect reasoning something like x%2 == 0 implies x == x+ 2 then x
should be even.
Where in the code I should find the reasoning like this?
Thank you very much.
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
