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.

Sign up for GitHub

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

Jump to bottom

Build problem #7

Closed
hxm-cpp opened this issue May 27, 2023 · 7 comments
Closed

Build problem #7

hxm-cpp opened this issue May 27, 2023 · 7 comments

Comments

@hxm-cpp
Copy link

hxm-cpp commented May 27, 2023 

5>LLVMParser.obj : error LNK2019: unresolved external symbol "bool __cdecl prove(class z3::expr)" (?prove@@YA_NVexpr@z3@@@Z) referenced in function "private: bool __cdecl LSiMBA::LLVMParser::verify(class llvm::SmallVectorImpl<struct LSiMBA::BFSEntry> &,class std::basic_string<char,struct std::char_traits<char>,class std::allocator<char> > &,class llvm::SmallVectorImpl<class llvm::Value *> &)" (?verify@LLVMParser@LSiMBA@@AEAA_NAEAV?$SmallVectorImpl@UBFSEntry@LSiMBA@@@llvm@@AEAV?$basic_string@DU?$char_traits@D@std@@V?$allocator@D@2@@std@@AEAV?$SmallVectorImpl@PEAVValue@llvm@@@4@@Z)
6>SiMBA++.vcxproj -> Z:\SiMBA-\build\RelWithDebInfo\SiMBA++.exe
5>Simplifier.obj : error LNK2019: unresolved external symbol "bool __cdecl proveReplacement(class std::basic_string<char,struct std::char_traits<char>,class std::allocator<char> > &,class std::basic_string<char,struct std::char_traits<char>,class std::allocator<char> > &,int,class std::vector<class std::basic_string<char,struct std::char_traits<char>,class std::allocator<char> >,class std::allocator<class std::basic_string<char,struct std::char_traits<char>,class std::allocator<char> > > > &)" (?proveReplacement@@YA_NAEAV?$basic_string@DU?$char_traits@D@std@@V?$allocator@D@2@@std@@0HAEAV?$vector@V?$basic_string@DU?$char_traits@D@std@@V?$allocator@D@2@@std@@V?$allocator@V?$basic_string@DU?$char_traits@D@std@@V?$allocator@D@2@@std@@@2@@2@@Z) referenced in function "private: bool __cdecl LSiMBA::Simplifier::verify_mba_unsat(class std::basic_string<char,struct std::char_traits<char>,class std::allocator<char> > &,class std::basic_string<char,struct std::char_traits<char>,class std::allocator<char> > &)" (?verify_mba_unsat@Simplifier@LSiMBA@@AEAA_NAEAV?$basic_string@DU?$char_traits@D@std@@V?$allocator@D@2@@std@@0@Z)
5>Z:\SiMBA-\build\RelWithDebInfo\SiMBAPass.dll : fatal error LNK1120: 2 unresolved externals
5>Done building project "SiMBAPass.vcxproj" -- FAILED.

What version of z3 you are using ?
llvm was compiled with LLVM_ENABLE_Z3_SOLVER=ON support and the z3 lib is linked.
@pgarba
Copy link
Owner

pgarba commented May 27, 2023 via email

@hxm-cpp
Copy link
Author

hxm-cpp commented May 27, 2023

i installed z3 using vcpkg. why would i need to add Z3Prover.cpp.

@pgarba
Copy link
Owner

pgarba commented May 27, 2023

https://github.com/pgarba/SiMBA-/blob/main/Z3Prover.cpp is part of the project and its not getting compiled on your side.

This file implements the functions prove and proveReplacement

@hxm-cpp
Copy link
Author

hxm-cpp commented May 27, 2023

yes i fixed it, but there is anohter problem, why on the first llvm::cl::ParseCommandLineOptions(argc, argv) i get

>	SiMBA++.exe!HandleAbort(int Sig) Line 419	C++
 	[External Code]	
 	SiMBA++.exe!llvm::report_fatal_error(const llvm::Twine & Reason, bool GenCrashDiag) Line 123	C++
 	SiMBA++.exe!llvm::report_fatal_error(const char * Reason, bool GenCrashDiag) Line 83	C++
 	SiMBA++.exe!`anonymous namespace'::CommandLineParser::addOption(llvm::cl::Option * O, llvm::cl::SubCommand * SC) Line 240	C++
 	SiMBA++.exe!llvm::cl::Option::addArgument() Line 445	C++
 	[Inline Frame] SiMBA++.exe!llvm::cl::opt<bool,1,llvm::cl::parser<bool>>::done() Line 1466	C++
 	[Inline Frame] SiMBA++.exe!llvm::cl::opt<bool,1,llvm::cl::parser<bool>>::{ctor}(const char[6] &) Line 1490	C++
 	SiMBA++.exe!`anonymous namespace'::CreateDebug::call() Line 87	C++
 	SiMBA++.exe!llvm::ManagedStaticBase::RegisterManagedStatic(void *(*)() Creator, void(*)(void *) Deleter) Line 36	C++
 	[Inline Frame] SiMBA++.exe!llvm::ManagedStatic<llvm::cl::opt<bool,1,llvm::cl::parser<bool>>,`anonymous namespace'::CreateDebug,llvm::object_deleter<llvm::cl::opt<bool,1,llvm::cl::parser<bool>>>>::operator*() Line 89	C++
 	SiMBA++.exe!llvm::initDebugOptions() Line 146	C++
 	SiMBA++.exe!initCommonOptions() Line 2674	C++
 	SiMBA++.exe!llvm::cl::ParseCommandLineOptions(int argc, const char * const * argv, llvm::StringRef Overview, llvm::raw_ostream * Errs, const char * EnvVar, bool LongOptionsUseDoubleDash) Line 1452	C++
 	SiMBA++.exe!main(int argc, char * * argv) Line 140	C++
 	[External Code]

@hxm-cpp
Copy link
Author

hxm-cpp commented May 27, 2023 

: CommandLine Error: Option 'debug' registered more than once!
LLVM ERROR: inconsistency in registered CommandLine options

#llvm-config --version
17.0.0git

@pgarba
Copy link
Owner

pgarba commented May 28, 2023

Try with llvm 15

@pgarba
Copy link
Owner

pgarba commented Jun 2, 2023

Closing this as no feedback provided

@pgarba pgarba closed this as completed Jun 2, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@pgarba @hxm-cpp