Radu Stoenescu

2014-06-24 10:27:42 UTC

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.

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.