[klee-dev] Range analysis using Klee

[Oscar Soria Dustmann]

Hi Radu,

we're currently working on something very related to this. However, you
can already have klee tell you the closure of the admissible range for a
given expression. Could you send us the code that doesn't work for you?
For one thing, are you talking about running code that calls special
functions or did you modify klee itself? In order to help you out it
would be helpful to see the code.

Cheers, Oscar

On 24/06/14 11:27, Radu Stoenescu wrote:
> 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
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>