Handle multiple klee_make_symbolic on the same object

[paulmar]

Reported by Alexander Kampmann on the mailing list

The output of the ktest-tool is:

ktest file : 'klee-out-5/test000004.ktest'
args : ['main.bc']
num objects: 3
object 0: name: 'model_version'
object 0: size: 4
object 0: data: '\x01\x00\x00\x00'
object 1: name: 'var2'
object 1: size: 6
object 1: data: '\x00\x00\x00\x00\x00\x00'
object 2: name: 'var2'
object 2: size: 6
object 2: data: '\x01\x01\x01\x00\x00\x00'

As you can see, there are two objects named 'var2' and no object named
'var1'. The c code is:

#include <string.h>
#include <stdlib.h>

int main(int argc, char **argv) {
       char *var1 = "Hallo";
       char *var2 = "Hallo";
       klee_make_symbolic(var1, 6*sizeof(char), "var1");
       klee_assume(var1[5] == 0);
       klee_make_symbolic(var2, 6*sizeof(char), "var2");
       klee_assume(var2[5] == 0);

       for(int i=0;i<strlen(var1);i++) {
               if(var1[i] != var2[i]) {
                       return 1;
               }
       }
       return 0;
}

It has 'var1' and 'var2', and makes both of them symbolic. The loop is
merely to give klee some branches to work with. 'var1' is missing in the
ktest-tool output. I am compiling with

clang -c -g -emit-llvm main.c

and running klee with

klee --libc=uclibc --posix-runtime -max-time=30 main.bc

[andreamattavelli]

I ran in the same problem in an off-line discussion by helping running KLEE on a similar example.
It seems like that KLEE gets confused by the fact that var1 and var2 are aliases of the same memory address ("Hallo" is compiled by clang to a global variable @str). In fact, by changing one of the two strings everything works fine.