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
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
