Hi, When sending replies please CC the mailing list.
klee_assume() is a "special function" that adds constraints to the current path being explored (if the resulting path is possible). See SpecialFunctionHandler::handleAssume() in SpecialFunctionHandler.cpp SpecialFunctionHandler::handleAssume() receives std::vector<ref<Expr> > &arguments as one of its arguments which will be an expression tree describing the constraint that was passed into klee_assume(). klee_assert() is a macro defined in klee.h that will call the special function __assert_fail() if the assertion is false. This special function is handled by SpecialFunctionHandler::handleAssertFail() this will terminate the path currently being explored. On 1 May 2013 20:29, General Email <[email protected]> wrote: > Thanks Daniel, > > This is very helpful. > So, my next question is how does klee generate such a condition based on the > following set of commands?! > > klee_assume(!(0<(x+5))); > klee_assume(y==x+7); > klee_assert(y<0); > > I would appreciate if you provide me with some guidance of how klee_assume > and klee_assert work. > Again thank you so much for your help. > ________________________________ > From: Daniel Liew <[email protected]> > To: General Email <[email protected]> > Cc: klee-dev <[email protected]> > Sent: Wednesday, May 1, 2013 1:01 PM > Subject: Re: [klee-dev] How to show (get) the negative values returned in > klee's .pc files? > > 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
