[klee-dev] Range analysis using Klee

[Radu Stoenescu]

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