2014-04-25 5 views
2

z3을 컴파일하는 동안 다음 오류가 발생했습니다. ld에서 오류가있는 것 같습니다. 나는 그것이 컴파일되도록하기 위해 무엇을 할 수 있는지 궁금해. git의 opt 브랜치에서 문제가된다. OS X 10.9.2 (13C1021)로 iMac에 있습니다. xcode 버전 5.1.1 (5B1008)과 xcode-select 도구를 버전 2333에 설치했습니다. ld가 설치된 버전 2.2.1의 포트를 사용합니다. 문제가 연결 문제 인 것 같습니다. 내가 같이 링크 로더를 사용하고 있습니다 : ld64를 136_2 + llvm33 @ (활성) 내 GCC는 (MacPorts를가 4.8.2_0을 gcc48) z3을 컴파일하는 동안 ld 연결 오류가 발생했습니다.

4.8.2

매우 감사 GCC입니다!

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 
+0

관련 : https://github.com/Z3Prover/z3/issues/7 –

+0

이 나타나지만 관련성이 없습니다. 'gcc'가 아닌 'clang'을 사용하기 때문에 관련이 없습니다 : https://github.com/Z3Prover/ z3/issues/142 –

답변

1

우리가 포트를 사용하고 gcc와 ld 및 다른 패키지를 설치했기 때문입니다.

또 다른 가능성은 ld가 llvm 3.4보다는 llvm 3.3에 의존한다는 것입니다. 문제는 ld를 업데이트 한 후에 해결되었습니다.

+0

''ld'를 업데이트 한 후에 무슨 뜻입니까? 'ld64'라는 뜻입니까? [그것은 보인다] (http://stackoverflow.com/questions/1608009/how-to-install-gnu-ld-on-mac-os-x-10-6) GNU'ld'를 사용할 수 없다. MacPorts'gcc '가'ld'를 호출하기 때문에 이런 문제를 일으키는 OS X. –

+0

네 말이 맞아. –

관련 문제