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: [email protected] <[email protected]> on
behalf of Frank Busse <[email protected]>
Sent: Friday, April 2, 2021 6:36 AM
Cc: [email protected] <[email protected]>
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" <[email protected]> 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&data=04%7C01%7Cmingyiliu%40gatech.edu%7C555803863efa4a4e93af08d8f5c358e9%7C482198bbae7b4b258b7a6d7f32faa083%7C0%7C0%7C637529566664761472%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=mpKqsEsNEhQzK16%2BZHgXsBJT1kLHxRdnKsWlcwG6S00%3D&reserved=0
_______________________________________________
klee-dev mailing list
[email protected]
https://nam12.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmailman.ic.ac.uk%2Fmailman%2Flistinfo%2Fklee-dev&data=04%7C01%7Cmingyiliu%40gatech.edu%7C555803863efa4a4e93af08d8f5c358e9%7C482198bbae7b4b258b7a6d7f32faa083%7C0%7C0%7C637529566664761472%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=2F3qBSkBcVP6KQljZ3hVc6zZcs7XHeh30MzIdKY7Yfk%3D&reserved=0
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
