The path constraint is in the KQuery language ( see http://klee.llvm.org/KQuery.html#ReadLSB_expr ). The stuff in the square brackets are the constraints which can be understood to mean
2880154532 == (array X concatenated together). X was simply an integer in your case so this concatenation is just concatenating 4bytes together the integer. Decimal constants (such as 2880154532 ) used in this way as far as I know represent the unsigned interpretation of a bitvector. Assuming that a two-complement representation for signed integers you can use gdb to quickly calculate what the decimal representation of the signed integer x is. $ gdb (gdb) print /t 2880154532 $1 = 10101011101010111010101110100100 # The most significant bit is 1 so we know the number is negative. We can invert the bits and add 1 to find the absolute value ( see http://en.wikipedia.org/wiki/Two%27s_complement#The_most_negative_number ) (gdb) print ~(2880154532) + 1 $2 = 1414812764 (gdb) exit So this tells you that the decimal value of integer x is -1414812764 in the constraints you showed. Hope that helps. On 1 May 2013 17:16, General Email <[email protected]> wrote: > 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 [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
