Hello everyone,
My name is Paris Tamiolakis. I am a student of informatics and I am having
problems with an assignment concerning Klee. I am trying to run klee from a
docker image but having problems when my code includes the function
klee_make_symbolic. The code that I use is the same as the gentlemans in the
link below.
https://github.com/klee/klee/issues/285
The results that I end with are the following:
After compilation:
klee@4f6d6445f44b:~$ clang -emit-llvm -g -c test4.c -o test4.bc
test4.c:3:3: warning: implicit declaration of function 'klee_make_symbolic' is
invalid in C99 [-Wimplicit-function-declaration]
klee_make_symbolic(&a, sizeof(a), a);
^
1 warning generated.
After run:
klee@4f6d6445f44b:~$ klee --libc=uclibc test4.bc
KLEE: NOTE: Using klee-uclibc :
/home/klee/klee_build/klee/Release+Asserts/lib/klee-uclibc.bca
KLEE: output directory is "/home/klee/klee-out-6"
Using STP solver backend
KLEE: WARNING: undefined reference to function: fcntl
KLEE: WARNING: undefined reference to function: fstat
KLEE: WARNING: undefined reference to function: ioctl
KLEE: WARNING: undefined reference to function: open
KLEE: WARNING: undefined reference to function: write
KLEE: WARNING ONCE: calling external: ioctl(0, 21505, 63609152)
KLEE: WARNING ONCE: calling __user_main with extra arguments.
klee: /home/klee/klee_src/lib/Core/SpecialFunctionHandler.cpp:242: std::string
klee::SpecialFunctionHandler::readStringAtAddress(klee::ExecutionState &,
ref<klee::Expr>): Assertion `0 && "XXX out of bounds / multiple resolution
unhandled"' failed.
0 klee 0x0000000000dcab02 llvm::sys::PrintStackTrace(_IO_FILE*) +
34
1 klee 0x0000000000dca8f4
2 libpthread.so.0 0x00002b2ba020a340
3 libc.so.6 0x00002b2ba26aecc9 gsignal + 57
4 libc.so.6 0x00002b2ba26b20d8 abort + 328
5 libc.so.6 0x00002b2ba26a7b86
6 libc.so.6 0x00002b2ba26a7c32
7 klee 0x000000000059dab9
8 klee 0x00000000005a0675
klee::SpecialFunctionHandler::handleMakeSymbolic(klee::ExecutionState&,
klee::KInstruction*, std::vector<klee::ref<klee::Expr>,
std::allocator<klee::ref<klee::Expr> > >&) + 117
9 klee 0x000000000059d665
klee::SpecialFunctionHandler::handle(klee::ExecutionState&, llvm::Function*,
klee::KInstruction*, std::vector<klee::ref<klee::Expr>,
std::allocator<klee::ref<klee::Expr> > >&) + 197
10 klee 0x000000000057ddb8
klee::Executor::callExternalFunction(klee::ExecutionState&,
klee::KInstruction*, llvm::Function*, std::vector<klee::ref<klee::Expr>,
std::allocator<klee::ref<klee::Expr> > >&) + 88
11 klee 0x000000000057d067
klee::Executor::executeCall(klee::ExecutionState&, klee::KInstruction*,
llvm::Function*, std::vector<klee::ref<klee::Expr>,
std::allocator<klee::ref<klee::Expr> > >&) + 119
12 klee 0x000000000058135f
klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*)
+ 4751
13 klee 0x0000000000589ccc
klee::Executor::run(klee::ExecutionState&) + 1180
14 klee 0x000000000058ce17
klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 2039
15 klee 0x0000000000573b34 main + 13860
16 libc.so.6 0x00002b2ba2699ec5 __libc_start_main + 245
17 klee 0x000000000056c859
Aborted (core dumped)
If u have any idea what is the problem, or how I could fix it, I would very
much appreciate it. Thank you in advance.
Yours sincerely,Paris Tamiolakis
Το παρόν email στάλθηκε από ασφαλή υπολογιστή που προστατεύεται
από το Avast. www.avast.com
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
