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 <mingyi...@gatech.edu<mailto:mingyi...@gatech.edu>> wrote: Hi all, Could anyone help me understand the following differences? Thanks, Mingyi ________________________________ From: klee-dev-boun...@imperial.ac.uk<mailto:klee-dev-boun...@imperial.ac.uk> <klee-dev-boun...@imperial.ac.uk<mailto:klee-dev-boun...@imperial.ac.uk>> on behalf of Liu, Mingyi <mingyi...@gatech.edu<mailto:mingyi...@gatech.edu>> Sent: Thursday, April 1, 2021 6:15 PM To: klee-dev@imperial.ac.uk<mailto:klee-dev@imperial.ac.uk> <klee-dev@imperial.ac.uk<mailto:klee-dev@imperial.ac.uk>> 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 klee-dev@imperial.ac.uk<mailto:klee-dev@imperial.ac.uk> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
