forked from klee/klee
-
Notifications
You must be signed in to change notification settings - Fork 11
Closed
Description
Then run KLEE on alias with uclibc function it fail
Example
size_t variable_length(size_t len) {
return 0;
}
size_t variable_length_alias(size_t len)
__attribute__((alias ("variable_length")));utbot@03457909ca26:~/test_proj$ klee -libc=uclibc -entry-point=variable_length_alias a.bc
klee: ../lib/Runner/run_klee.cpp:1189: void createLibCWrapper(std::vector<std::unique_ptr<llvm::Module> > &, llvm::StringRef, llvm::StringRef): Assertion `userMainFn && "unable to get user main"' failed.
#0 0x0000000001cb296a llvm::sys::PrintStackTrace(llvm::raw_ostream&) (/utbot_distr/klee/bin/klee+0x1cb296a)
#1 0x0000000001cb08c4 llvm::sys::RunSignalHandlers() (/utbot_distr/klee/bin/klee+0x1cb08c4)
#2 0x0000000001cb0a08 SignalHandler(int) (/utbot_distr/klee/bin/klee+0x1cb0a08)
#3 0x00007ff9f0330980 __restore_rt (/lib/x86_64-linux-gnu/libpthread.so.0+0x12980)
#4 0x00007ff9ef5a8e87 raise (/lib/x86_64-linux-gnu/libc.so.6+0x3ee87)
#5 0x00007ff9ef5aa7f1 abort (/lib/x86_64-linux-gnu/libc.so.6+0x407f1)
#6 0x00007ff9ef59a3fa (/lib/x86_64-linux-gnu/libc.so.6+0x303fa)
#7 0x00007ff9ef59a472 (/lib/x86_64-linux-gnu/libc.so.6+0x30472)
#8 0x0000000000522e40 createLibCWrapper(std::vector<std::unique_ptr<llvm::Module, std::default_delete<llvm::Module> >, std::allocator<std::unique_ptr<llvm::Module, std::default_delete<llvm::Module> > > >&, llvm::StringRef, llvm::StringRef) /home/utbot/klee/build/../lib/Runner/run_klee.cpp:0:3
#9 0x0000000000522e40 linkWithUclibc(llvm::StringRef, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::vector<std::unique_ptr<llvm::Module, std::default_delete<llvm::Module> >, std::allocator<std::unique_ptr<llvm::Module, std::default_delete<llvm::Module> > > >&) /home/utbot/klee/build/../lib/Runner/run_klee.cpp:1261:3
#10 0x0000000000522e40 run_klee(int, char**, char**) /home/utbot/klee/build/../lib/Runner/run_klee.cpp:1700:5
#11 0x00007ff9ef58bc87 __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21c87)
#12 0x0000000000519c6a _start (/utbot_distr/klee/bin/klee+0x519c6a)
Aborted (core dumped)Expected KLEE not fail same as libc=klee
utbot@03457909ca26:~/test_proj$ klee -libc=klee -entry-point=variable_length_alias a.bc
KLEE: output directory is "/home/utbot/test_proj/klee-out-12"
KLEE: Using Z3 solver backend
KLEE: Using Z3 bitvector builder
WARNING: this target does not support the llvm.stacksave intrinsic.
KLEE: ERROR: Entry function 'variable_length_alias' not found in module.Maybe it should generate tests for alias funcution or give more info.
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
No labels