[klee-dev] Symbolizing a struct with a std::string and a std::vector

[Alberto Garcia]

Hi,
I've read every tutorial in the documentation and the external resources
but I've not found any information on symbolizing C++ containers.
What would be the best approach to symbolize a struct containing a
std::string and a std::vector?
Here is some quick code I wrote to demonstrate what I'm trying to do?

struct A{
  std::string str;
  std::vector<int> vec;
  bool flag;
};


void test(struct A myStruct){
  if(str.size()>4 && str[3] == 'A'){
    printf("Winer");
   }
   else {
    printf("Losser");
  }

int main(){
  struct A myStruct;
  myStruct.str = std::string("test"); // Just so there is some memory
allocated at myStruct.str
  myStruct.vec= {1,2,3,4}; // To create a std::vector of 4 elements

  klee_make_symbolic(&myStruct.str[0], myStruct.str.size(), "my string");

  for(int i= 0; i<myStruct.vec.size(); i++ ){
    klee_make_symbolic(&myStruct.vec[i], sizeof(int), "my int vector
item"); // I may have to not give the same name to every item in
vector
  }
  test(myStruct);
  return 0;
}

Is this the correct way to symbolize a std::string and a std::vector? How
can I make the size of either of them symbolic?

Thank you.

-- 
Alberto García Illera

GPG Public Key <https://goo.gl/yshdwh>
-------------- next part --------------
HTML attachment scrubbed and removed