[klee-dev] Adding Symbolic Arrays and Solver's Data structure to map

[Anitha B Gollamudi]

Hopefully someone can answer this.

I am experimenting klee with special function handling. I'll try to
pose a simple question (please feel free to ask me further question if
it is unclear). Lets say we have a simple testcase as follows where
myspecialfunc(char *c) is handled in SpecialFunctionHandler.h/cpp


int foo(char *c) {

  ...
 if (myspecialfunc(c)  == 0)
     return 0;
 else
    return 1;
}

int main() {

 char myarray[10];
 klee_make_symbolic(myarray, 10, "myarray-print");

 return foo(myarray);
}


myspecialfunc() generates some constraints (say c == 0 for simplicity)
which are successfully checked by underlying SMT solver ( am using
metaSMT). Now I want to read_value(c) of the successful SAT model.

Here is the problem: While generating constraint from myspecialfunc(),
I should add the newly created solver's data structure corresponding
to "myarray" to the "constructed" map. (Please refer to the step:
constructed.insert(....) in STPBuilder::construct())

But the expression tree generated in myspecialfunc() uses
"ConstantExpr" to represent "c". So I am losing the fact that 'c' is
actually the array "myarray". How can I access "myarray" so that I can
add to constructed.insert()

(My apologies, the problem description is only representative of the
actual problem. So the motivation can seem obscure.)








-- 
 Anitha