[klee-dev] Problems with Klee Docker Image

[Paris Tamiolakis]

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 at 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 at 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 		
	

 		 	   		  
-------------- next part --------------
HTML attachment scrubbed and removed