[klee-dev] question on different outputs when running under klee and with ktest file

[Frank Busse]

Hi,


On Thu, 1 Apr 2021 22:15:57 +0000
"Liu, Mingyi" <mingyiliu at gatech.edu> wrote:

>     printf("%s%s%n\n", &a, &b, &c);

Is this bogus line relevant?

> To be specific, I used the following commands and got three
> paths/testcases as expected. What I am confused about is the output
> for the c value ("after: a = 2 b = 3 c = 0"), should that be 2? Why
> it is 0 here?

Am I missing something? c is completely unconstrained in your example.
When I run your program without the line above I get three test cases:

a,b,c
0,0,0
2,0,0
2,3,0

Replaying those cases results in the same output. You can inspect your
.ktest files with ktest-tool[1].


Kind regards,

Frank


[1] https://klee.github.io/docs/tools/#ktest-tool