编译z3时ld链接错误 [英] ld linking error while compiling z3

问题描述

我在编译z3时遇到以下错误.对于ld来说似乎是错误的.我想知道如何做才能使其编译.这是git中opt分支的问题.我在使用OS X 10.9.2(13C1021)的iMac上 我使用的xcode版本5.1.1(5B1008)的xcode-select工具安装到版本2333.我使用的端口版本是2.2.1，安装了ld. 该问题似乎是一个链接问题.我将链接加载器用作:ld64 @ 136_2 + llvm33(正在活动) 我的gcc是gcc(MacPorts gcc48 4.8.2_0)4.8.2

I met the following error while compiling z3. It seems to be an error for ld. I wonder what I can do to make it compile. It is a problem from the opt branch in git. I am on iMac with OS X 10.9.2 (13C1021) I am with xcode Version 5.1.1 (5B1008) with xcode-select tools installed to version 2333. I use port with version 2.2.1 with ld installed. The problem seems to be a linking problem. I am using link loader as: ld64 @136_2+llvm33 (active) My gcc is gcc (MacPorts gcc48 4.8.2_0) 4.8.2

非常感谢！

g++ -o z3  shell/datalog_frontend.o shell/dimacs_frontend.o 
 shell/gparams_register_modules.o shell/install_tactic.o shell/main.o     
shell/mem_initializer.o shell/smtlib_frontend.o shell/z3_log_frontend.o api/api.a opt/opt.a parsers/smt/smtparser.a tactic/portfolio/portfolio.a tactic/ufbv/ufbv_tactic.a tactic/smtlogics/smtlogic_tactics.a muz/fp/fp.a muz/duality/duality_intf.a muz/bmc/bmc.a muz/tab/tab.a muz/clp/clp.a muz/pdr/pdr.a muz/rel/rel.a muz/transforms/transforms.a muz/base/muz.a duality/duality.a qe/qe.a tactic/sls/sls_tactic.a smt/tactic/smt_tactic.a tactic/fpa/fpa.a tactic/bv/bv_tactics.a smt/user_plugin/user_plugin.a smt/smt.a smt/proto_model/proto_model.a smt/params/smt_params.a ast/rewriter/bit_blaster/bit_blaster.a ast/pattern/pattern.a ast/macros/macros.a ast/simplifier/simplifier.a ast/proof_checker/proof_checker.a parsers/smt2/smt2parser.a cmd_context/extra_cmds/extra_cmds.a cmd_context/cmd_context.a interp/interp.a solver/solver.a tactic/aig/aig_tactic.a math/subpaving/tactic/subpaving_tactic.a nlsat/tactic/nlsat_tactic.a tactic/arith/arith_tactics.a sat/tactic/sat_tactic.a tactic/core/core_tactics.a math/euclid/euclid.a math/grobner/grobner.a parsers/util/parser_util.a ast/substitution/substitution.a tactic/tactic.a model/model.a ast/normal_forms/normal_forms.a ast/rewriter/rewriter.a ast/ast.a math/subpaving/subpaving.a math/realclosure/realclosure.a math/interval/interval.a math/simplex/simplex.a math/hilbert/hilbert.a nlsat/nlsat.a sat/sat.a math/polynomial/polynomial.a util/util.a  -lpthread  -fopenmp
0  0x1079c1a68  __assert_rtn + 144
1  0x107a3bccd  mach_o::relocatable::Parser<x86_64>::parse(mach_o::relocatable::ParserOptions const&) + 1039
2  0x107a2b899  mach_o::relocatable::Parser<x86_64>::parse(unsigned char const*, unsigned long long, char const*, long, ld::File::Ordinal, mach_o::relocatable::ParserOptions const&) + 313
3  0x107a290f0  mach_o::relocatable::parse(unsigned char const*, unsigned long long, char const*, long, ld::File::Ordinal, mach_o::relocatable::ParserOptions const&) + 208
4  0x107a18797  archive::File<x86_64>::makeObjectFileForMember(archive::File<x86_64>::Entry const*) const + 795
5  0x107a182b3  archive::File<x86_64>::justInTimeforEachAtom(char const*, ld::File::AtomHandler&) const + 139
6  0x1079c5d46  ld::tool::InputFiles::searchLibraries(char const*, bool, bool, bool, ld::File::AtomHandler&) const + 210
7  0x107a0b772  ld::tool::Resolver::resolveUndefines() + 200
8  0x107a0d6e1  ld::tool::Resolver::resolve() + 75
9  0x1079c1d44  main + 370
A linker snapshot was created at:
/tmp/z3-2014-03-25-110931.ld-snapshot
ld: Assertion failed: (cfiStartsArray[i] != cfiStartsArray[i-1]), function parse, file src/ld/parsers/macho_relocatable_file.cpp, line 1555.
collect2: error: ld returned 1 exit status
make: *** [z3] Error 1

推荐答案

这是因为我们使用了port并安装了gcc和ld等软件包.

It is because we used port and installed gcc and ld and other packages.

另一种可能性是ld取决于llvm 3.3而不是llvm 3.4.更新ld后，问题得以解决.

Another possibility is that ld was depend on llvm 3.3 rather than llvm 3.4. The problem was solved after updating ld.

这篇关于编译z3时ld链接错误的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！