Hello, I am trying to use Klee for performing a very trivial range analysis: I would like to see what is the set of possible values of a given symbol just before existing a function call.
After some more convoluted attempts I settled for the following approach: In the *framePopped *method of StatsTracker I am trying to find the symbol in the AddressSpace pertaining to the current ExecutionState and if the symbol is found I invoke the *read* method of the corresponding ObjectSpace instance. Finally this expression is passed to the *getRange *of the currently employed solver, along with the ExecutionState (which carries the constraints currently in place). The trouble is that my above approach doesn't seem to work, even in the simplest example: an unsigned integer multiplied by 2. No matter what I do - the range is 0 - 2^32-1 (no constraints or mutations seem to affect this output). Is this the bad way of doing things or am I just a poor coder and I messed things up along the way ? Many thanks, Radu.
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
