Hi all, Could anyone help me understand the following differences?
Thanks, Mingyi ________________________________ From: klee-dev-boun...@imperial.ac.uk <klee-dev-boun...@imperial.ac.uk> on behalf of Liu, Mingyi <mingyi...@gatech.edu> Sent: Thursday, April 1, 2021 6:15 PM To: klee-dev@imperial.ac.uk <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 [cid:4493b7ad-e1f8-433a-acfd-1f0477862675] 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 [cid:10eb545b-fc10-4eaf-95ef-062b4f7247f4] 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 https://mailman.ic.ac.uk/mailman/listinfo/klee-dev