Hi, I need to understand how to use klee_assume and klee_assert. I tried to implement the following assumptions (in the function listed below) which assumed that if a symbolic variable x satisfies the condition !(0<(x+5)) and that if another variable y is set to x+7, I want to check whether y is < 0 or not. ------------------------------------------------------------------
void main() { int x,y; klee_make_symbolic(&x, sizeof(x), "x"); klee_assume(!(0<(x+5))); klee_assume(y==x+7); klee_assert(y<0); } ------------------------------------------------------------------ The result from klee showed that the assersion is satisfiable based on the following path constraint which I couldn't understand. array x[4] : w32 -> w8 = symbolic (query [(Eq 2880154532 (ReadLSB w32 0 x))] false) Also how to get the equivelant negative value of the number 2880154532? Would you please advise? Thanks
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev