[klee-dev] Replaying KLEE generated test cases

[Giuseppe Di Guglielmo]

Dear all,
does the 'klee-replay' tool require programs whose symbolic parameters are
the
'main' function arguments?

In other words consider the example in
http://klee.llvm.org/resources/islower.c.html

int main() {
  char c;
  klee_make_symbolic(&c, sizeof(c), "input");
  return my_islower(c);
}

'c' is a symbolic variable, but it is not a parameter of the 'main'
function, i.e. argv.

Is it possible to replay the generated testbenches with such a kind of
programs? Just in case, how?

Thank you,
G.