Hi, I'm using klee with gnat-llvm generated bytecodes (to execute symbolically Ada programs) and I have some problems.
When executing the program there are done some runtime checks, that are done by calling to GNAT external functions, such as __gnat_rcheck_CE_Overflow_Check. By running klee with option --external-calls=none the call to external functions are disallowed but an error is raised which caused that the path is not completed: KLEE: output directory is "/home/mario/automatic_ada_symbolic_execution/klee-out-15" KLEE: Using STP solver backend KLEE: WARNING: undefined reference to function: __gnat_rcheck_CE_Overflow_Check KLEE: WARNING ONCE: String not terminated by \0 passed to one of the klee_ functions KLEE: WARNING: Disallowed call to external function: __gnat_rcheck_CE_Overflow_Check *KLEE: ERROR: (location information missing) external calls disallowedKLEE: NOTE: now ignoring this error at this locationKLEE: WARNING: Disallowed call to external function: __gnat_rcheck_CE_Overflow_Check* KLEE: ERROR: (location information missing) external calls disallowed KLEE: NOTE: now ignoring this error at this location KLEE: WARNING: Disallowed call to external function: __gnat_rcheck_CE_Overflow_Check KLEE: ERROR: (location information missing) external calls disallowed KLEE: NOTE: now ignoring this error at this location KLEE: WARNING: Disallowed call to external function: __gnat_rcheck_CE_Overflow_Check KLEE: done: total instructions = 129 KLEE: done: completed paths = 4 *KLEE: done: partially completed paths = 4* KLEE: done: generated tests = 7 There are any option to skip this error and complete the path? In addition, I have a bytecode with all the gnat libraries, but linking with it gives some errors while executing some instructions (the module is broken, so I have to switch the option --disable-verify=true): *klee: /home/mario/klee/include/klee/ADT/Bits.h:79: uint64_t klee::bits64::truncateToNBits(uint64_t, unsigned int): Assertion `N > 0 && N <= 64' failed.* #0 0x00000000028dd261 llvm::sys::PrintStackTrace(llvm::raw_ostream&, int) /home/mario/llvm-project-13.0.0.src/llvm/lib/Support/Unix/Signals.inc:565:22 #1 0x00000000028dd324 PrintStackTraceSignalHandler(void*) /home/mario/llvm-project-13.0.0.src/llvm/lib/Support/Unix/Signals.inc:632:1 #2 0x00000000028db1ba llvm::sys::RunSignalHandlers() /home/mario/llvm-project-13.0.0.src/llvm/lib/Support/Signals.cpp:97:20 #3 0x00000000028dcc99 SignalHandler(int) /home/mario/llvm-project-13.0.0.src/llvm/lib/Support/Unix/Signals.inc:407:1 #4 0x00007f24b69b2140 __restore_rt (/lib/x86_64-linux-gnu/libpthread.so.0+0x14140) #5 0x00007f24b647bce1 raise (/lib/x86_64-linux-gnu/libc.so.6+0x3bce1) #6 0x00007f24b6465537 abort (/lib/x86_64-linux-gnu/libc.so.6+0x25537) #7 0x00007f24b646540f (/lib/x86_64-linux-gnu/libc.so.6+0x2540f) #8 0x00007f24b6474662 (/lib/x86_64-linux-gnu/libc.so.6+0x34662) #9 0x0000000000429f8d /home/mario/klee/include/klee/ADT/Bits.h:79:7 #10 0x000000000044d389 klee::ConstantExpr::create(unsigned long, unsigned int) /home/mario/klee/include/klee/ADT/Ref.h:93:7 #11 0x00000000004554f7 klee::Executor::evalConstant(llvm::Constant const*, klee::KInstruction const*) /home/mario/klee/lib/Core/ExecutorUtil.cpp:63:73 #12 0x0000000000455752 llvm::StructLayout::getElementOffset(unsigned int) const /usr/local/include/llvm/IR/DataLayout.h:635:5 #13 0x0000000000455752 llvm::StructLayout::getElementOffsetInBits(unsigned int) const /usr/local/include/llvm/IR/DataLayout.h:640:28 #14 0x0000000000455752 klee::Executor::evalConstant(llvm::Constant const*, klee::KInstruction const*) /home/mario/klee/lib/Core/ExecutorUtil.cpp:84:59 #15 0x000000000043985e klee::ref<klee::Expr>& klee::ref<klee::Expr>::operator=<klee::ConstantExpr>(klee::ref<klee::ConstantExpr>&&) /home/mario/klee/include/klee/ADT/Ref.h:188:5 #16 0x000000000043985e klee::Executor::bindModuleConstants() /home/mario/klee/lib/Core/Executor.cpp:3384:49 #17 0x0000000000449efc klee::Executor::run(klee::ExecutionState&) /home/mario/klee/lib/Core/Executor.cpp:3446:15 #18 0x000000000044b048 std::__uniq_ptr_impl<klee::PTree, std::default_delete<klee::PTree> >::reset(klee::PTree*) /usr/local/include/c++/12.0.1/bits/unique_ptr.h:179:16 #19 0x000000000044b048 std::unique_ptr<klee::PTree, std::default_delete<klee::PTree> >::reset(klee::PTree*) /usr/local/include/c++/12.0.1/bits/unique_ptr.h:460:12 #20 0x000000000044b048 std::unique_ptr<klee::PTree, std::default_delete<klee::PTree> >::operator=(std::nullptr_t) /usr/local/include/c++/12.0.1/bits/unique_ptr.h:401:7 #21 0x000000000044b048 klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) /home/mario/klee/lib/Core/Executor.cpp:4437:17 #22 0x0000000000414be7 main /home/mario/klee/tools/klee/main.cpp:1532:5 #23 0x00007f24b6466d0a __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x26d0a) #24 0x0000000000421d6a _start (/usr/local/bin/klee+0x421d6a) Aborted (core dumped) Why is this error due to? Is a problem with the bytecode or it can be solved any way? Thank you in advance. Regards.
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
