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

[Anitha B Gollamudi]

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 <anitha.boyapati at gmail.com> 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