To summarize: I guess what I am asking is - In klee source code, is there a way to find if "Array" and "ConstantExpr" alias each other... (i.e an array and a pointer expression)
On 28 April 2015 at 21:49, Anitha B Gollamudi <[email protected]> wrote: > 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 -- Anitha _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
