[klee-dev] Same variable twice in ktest-tool output

[Alexander Kampmann]

hey,

For my test input, the ktest-tool outputs the same object name twice and
skips another object.

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

I guess this is related to the string constants, if I use a malloc
instead, the problem disappears. Is this a bug in klee or is this
intended? My initial guess was, that some inlining just makes var1 and
var2 the same pointer (they have the same value), but then, why does
klee have different values for those objects?

Cheers,
Alex

PS: Just in case you need this: "klee --version" outputs

KLEE 0.2.0 (https://klee.github.io)
  Built Jun  3 2015 (15:16:42)
  Build mode: Debug+Asserts
  Build revision: 6118403fa4315388946babd25be38a9524a5e2c5

LLVM (http://llvm.org/):
  LLVM version 3.4.2
  DEBUG build with assertions.
  Built Jun  3 2015 (14:39:50).
  Default target: x86_64-unknown-linux-gnu
  Host CPU: core-avx-i