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

[Liu, Mingyi]

Hi Frank,

Thanks for your reply but that doesn't answer the question. Yes, this line "printf("%s%s%n\n", &a, &b, &c);" plays a significant role here, as it should write 2 to c even if it was not constrained when a = 2 and b = 3 from my understanding.


I checked three testcases and that was the reason why I just used testcase #3 for verification.


Thanks,

Mingyi




________________________________
From: klee-dev-bounces at imperial.ac.uk <klee-dev-bounces at imperial.ac.uk> on behalf of Frank Busse <f.busse at imperial.ac.uk>
Sent: Friday, April 2, 2021 6:36 AM
Cc: klee-dev at imperial.ac.uk <klee-dev at imperial.ac.uk>
Subject: Re: [klee-dev] question on different outputs when running under klee and with ktest file

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://nam12.safelinks.protection.outlook.com/?url=https%3A%2F%2Fklee.github.io%2Fdocs%2Ftools%2F%23ktest-tool&amp;data=04%7C01%7Cmingyiliu%40gatech.edu%7C555803863efa4a4e93af08d8f5c358e9%7C482198bbae7b4b258b7a6d7f32faa083%7C0%7C0%7C637529566664761472%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&amp;sdata=mpKqsEsNEhQzK16%2BZHgXsBJT1kLHxRdnKsWlcwG6S00%3D&amp;reserved=0

_______________________________________________
klee-dev mailing list
klee-dev at imperial.ac.uk
https://nam12.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmailman.ic.ac.uk%2Fmailman%2Flistinfo%2Fklee-dev&amp;data=04%7C01%7Cmingyiliu%40gatech.edu%7C555803863efa4a4e93af08d8f5c358e9%7C482198bbae7b4b258b7a6d7f32faa083%7C0%7C0%7C637529566664761472%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&amp;sdata=2F3qBSkBcVP6KQljZ3hVc6zZcs7XHeh30MzIdKY7Yfk%3D&amp;reserved=0
-------------- next part --------------
HTML attachment scrubbed and removed