[klee-dev] How to show (get) the negative values returned in klee's .pc files?

[General Email]

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
-------------- next part --------------
HTML attachment scrubbed and removed