[klee-dev] Question on Ktest tool

[Yi Zhang]

Dear all,
   I'm now using KLEE to generate test cases for patch validation
purpose.I'd like to know how to use Ktest tool to interpret result when I
symbolic execute more complext structure like INT array, struct than
primitive type.For example, when I symbolic execute an INT array in the
matrix muliplication program as below:
  int main(int argc, char** argv){
     int m =2;
     int *matrix1, *matrix2;
     matrix1 = (int *) malloc(m * m * sizeof(int));
     matrix2 = (int *) malloc(m * m * sizeof(int));
     InitializeMatrix(matrix1);
     klee_make_symbolic(matrix2, m*m*sizeof(int), "matrix2"); //only
symbolic matrix2

    //do matrix mutiplication and check some property
    .....
   }

Part of the result is
  ktest file : 'klee-last/test000001.ktest'
  args : ['sym.bc']
  num objects: 2
  object 0: name: 'model_version'
  object 0: size: 4
  object 0: data: 1
  object 1: name: 'matrix2'
  object 1: size: 16
  object 1: data:
'\xf9W\x19\xed\x00\x00\x00\x00k\xa8\xe6\x12\x00\x00\x00\x00'

As you can see, the result data is shown in a series of hexadecimal numbers
even if I try the --write-ints flag in ktest tool. I'd like to know how to
make the result easier to read.(Like concrete value of each element of the
array in the form of decimal numbers)

Best,

Yi
-------------- next part --------------
HTML attachment scrubbed and removed