Hi Martin,
Thanks for your work.
I've tried but it still doesn't fix the mentioned issue which is
printf("%s%s%n\n", &a, &b, &c).
Please notice that it is %s that determines whether a or b is zero or not.
Thank you all the same!
Best,
Mingyi
________________________________
From: Nowack, Martin <[email protected]>
Sent: Tuesday, May 11, 2021 7:33 PM
To: Liu, Mingyi <[email protected]>
Cc: klee-dev <[email protected]>
Subject: Re: [klee-dev] question on different outputs when running under klee
and with ktest file
Hi Mingyi,
You’ve hit a bug in KLEE.
Thanks for your detailed description - I just opened PR based on your test case
https://github.com/klee/klee/pull/1407 that fixes the issue.
Feel free to apply those changes locally to try them out.
The test case is based on your example and works with the changes.
All the best,
Martin
On 5. Apr 2021, at 18:50, Liu, Mingyi
<[email protected]<mailto:[email protected]>> wrote:
Hi all,
Could anyone help me understand the following differences?
Thanks,
Mingyi
________________________________
From: [email protected]<mailto:[email protected]>
<[email protected]<mailto:[email protected]>> on
behalf of Liu, Mingyi <[email protected]<mailto:[email protected]>>
Sent: Thursday, April 1, 2021 6:15 PM
To: [email protected]<mailto:[email protected]>
<[email protected]<mailto:[email protected]>>
Subject: [klee-dev] question on different outputs when running under klee and
with ktest file
Hi klee-dev members,
I made a simple program below and observed different outputs when running under
klee and verifying with the ktest file.
#include <stdio.h>
#include "klee/klee.h"
int main() {
int a;
int b;
int c;
klee_make_symbolic(&a, sizeof(a), "a");
klee_make_symbolic(&b, sizeof(b), "b");
klee_make_symbolic(&c, sizeof(c), "c");
printf("before: a = %d b = %d c = %d\n", a, b, c);
if (a == 2 && b == 3) {
printf("%s%s%n\n", &a, &b, &c);
printf("after: a = %d b = %d c = %d\n", a, b, c);
}
return 0;
}
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?
command: $ clang-9 -I ../klee/include -c -emit-llvm -g -O0 logic_or.c
$ ../klee/build/bin/klee -external-calls=all logic_or.bc
<Outlook-wxucu054.png>
I then compiled the program and ran it with the third testcase above, the
results are all as expected as c is 2 this time.
command: $ gcc -I ../klee/include logic_or.c -lkleeRuntest -L ../klee/build/lib
-o logic_or
$ KTEST_FILE=klee-last/test000003.ktest ./logic_or
<Outlook-idgtlb50.png>
Could you please explain why the output values for c are different? Is it
intended?
klee version information:
KLEE 2.3-pre (https://klee.github.io)
Build mode: RelWithDebInfo (Asserts: ON)
Build revision: 36780583dd78865100114b02627a3418b2d56deb
LLVM (http://llvm.org/):
LLVM version 9.0.1
Optimized build.
Default target: x86_64-pc-linux-gnu
Host CPU: skylake
Thanks,
Mingyi
_______________________________________________
klee-dev mailing list
[email protected]<mailto:[email protected]>
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
