Pretty printing removes array indices

[Himeshi]

When pretty printing the error expressions which contain array indices, only the array name without the indexed element is shown in the final expression.

[domainexpert]

@Himeshi Is this in the context of basic/array_test2.c of fp-examples?

[domainexpert]

@Himeshi Please note, however, sometimes we don't want array indices, for example, for a primitive-typed variable such as int, char, etc. The standard way of printing those in KLEE is to use array of chars, but you would probably want to avoid using arrays in those cases, whereas you would want to have the indices printed for real arrays.

[Himeshi]

@domainexpert yes, this is in the context of basic/array_test2.c of fp-examples.

In that case how can do we identify which ones are of primitive type and which ones are actually arrays?

[domainexpert]

@Himeshi Say v is the pointer to the LLVM value of the global array (with type llvm::Value *), you can now if it's an array or a pointer to primitive by the return value of v->getType()->isArrayTy().

[domainexpert]

Resolved via #34 . Array is detected via user naming of symbolic values, such as in the following example:

#include <klee/klee.h>
#include <stdio.h>

void test_array(char *x);

char arr[5], answer;

int main() {

  klee_make_symbolic(arr, sizeof arr, "__arr8__arr");
  klee_track_error(arr, "__arr8__arr_error");

  test_array(arr);

  klee_bound_error(arr[0], 1.3);
  return 0;
}

void test_array(char *x) {
  // x[0] = (x[1] + x[2]) * (x[3] - x[4]);
  x[0] = x[1] + x[2];
}

Results in the following error expression:

Line 18 of /home/dcsandr/software/fp-examples/basic/array_test1.c (main): 
Output Error: (((arr_error[1] * arr[1]) + (arr_error[2] * arr[2])) / (arr[1] + arr[2]))
Absolute Bound: 1.300000e+00