ld linking error while compiling z3

2020-07-24 05:37发布

问题:

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

Thank you very much!

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

回答1:

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

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



标签: linker ld z3