Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Compilation error #4

Open
davidtr1037 opened this issue Jul 22, 2020 · 4 comments
Open

Compilation error #4

davidtr1037 opened this issue Jul 22, 2020 · 4 comments

Comments

@davidtr1037
Copy link

davidtr1037 commented Jul 22, 2020

The compilation fails on 7.0.0-dev branch (when STP is enabled).
I have the following error:

/lib/Solver/STPSolver.cpp:177:31: error: no matching function for call to ‘klee::Assignment::Assignment(std::vector<const klee::Array*>&, std::vector<std::vector<unsigned char> >&)’
   Assignment a(objects, values);
@mchalupa
Copy link
Member

Hi,

yes, STP is not supported on 7.0.0 branch. Our symbolic-size allocations extension needs some features that STP does not provide, so we use Z3. Sorry that it is not documented anywhere.

lzaoral added a commit to lzaoral/klee that referenced this issue Apr 20, 2021
Fixes:
$ cat test.c
int main(void) {}
$ clang -m32 -emit-llvm -c test.c -o test.bc
$ klee test.bc
 KLEE: output directory is "/home/lukas/klee/klee-out-9"
 KLEE: Using Z3 solver backend
 LLVM ERROR: 64-bit code requested on a subtarget that doesn't support it!
  #0 0x00007fb59688bbf6 llvm::sys::PrintStackTrace(llvm::raw_ostream&, int) (/lib64/libLLVM-12.so+0xc07bf6)
  staticafi#1 0x00007fb596889ae4 llvm::sys::RunSignalHandlers() (/lib64/libLLVM-12.so+0xc05ae4)
  staticafi#2 0x00007fb596889c69 (/lib64/libLLVM-12.so+0xc05c69)
  staticafi#3 0x00007fb595772310 __restore_rt (/lib64/libc.so.6+0x3d310)
  staticafi#4 0x00007fb595772292 raise (/lib64/libc.so.6+0x3d292)
  staticafi#5 0x00007fb59575b8a4 abort (/lib64/libc.so.6+0x268a4)
  staticafi#6 0x00007fb5967d7b5e llvm::report_fatal_error(llvm::Twine const&, bool) (/lib64/libLLVM-12.so+0xb53b5e)
  staticafi#7 0x00007fb5967d7c8e (/lib64/libLLVM-12.so+0xb53c8e)
  staticafi#8 0x00007fb5990e1b26 (/lib64/libLLVM-12.so+0x345db26)
  staticafi#9 0x00007fb5990e2120 (/lib64/libLLVM-12.so+0x345e120)
 staticafi#10 0x00007fb5990e5ac4 (/lib64/libLLVM-12.so+0x3461ac4)
 staticafi#11 0x00000000004919ed klee::RaiseAsmPass::runOnModule(llvm::Module&) /home/lukas/klee/build/../lib/Module/RaiseAsm.cpp:102:31
 staticafi#12 0x00007fb5969b1d02 llvm::legacy::PassManagerImpl::run(llvm::Module&) (/lib64/libLLVM-12.so+0xd2dd02)
 staticafi#13 0x0000000000486cac klee::KModule::instrument(klee::Interpreter::ModuleOptions const&) /home/lukas/klee/build/../lib/Module/KModule.cpp:237:23
 staticafi#14 0x000000000043562f klee::Executor::setModule(std::vector<std::unique_ptr<llvm::Module, std::default_delete<llvm::Module> >, std::allocator<std::unique_ptr<llvm::Module, std::default_delete<llvm::Module> > > >&, klee::Interpreter::ModuleOptions const&) /home/lukas/klee/build/../lib/Core/Executor.cpp:537:23
 staticafi#15 0x0000000000417dd5 main /home/lukas/klee/build/../tools/klee/main.cpp:1411:46
 staticafi#16 0x00007fb59575cb75 __libc_start_main (/lib64/libc.so.6+0x27b75)
 staticafi#17 0x0000000000424d6e _start (build/bin/klee+0x424d6e)
@tareq97-zz
Copy link

I want to use only klee part from symbiotic is there a way to bypass this issues and build klee.

@mchalupa
Copy link
Member

mchalupa commented Dec 8, 2021

If you use Z3 as the solver, there should not be this problem.

@tareq97-zz
Copy link

@mchalupa Thanks for the update. Got it.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants