Z3 테스트 예제를 컴파일하면 빌드 오류가 발생합니다.

코드 플렉스의 소스에서 Z3을 컴파일했습니다. 구성 세부 정보 :Z3 테스트 예제를 컴파일하면 빌드 오류가 발생합니다.

운영 시스템 데비안 5.0 (레니)
GLIBC 2.7
GCC 4.4.3
OpenMP의 4.3.4 (패키지 버전)

내가 빌드하려고 예를 들면 다음과 같습니다.

../../lib/libz3.so: undefined reference to `std::ctype<char>::_M_widen_init() [email protected]_3.4.11'

부이 예를 들어 내가 얻은 C++ 예제 :

../../lib/libz3.so: undefined reference to `[email protected]_3.0' 
../../lib/libz3.so: undefined reference to `[email protected]_3.0' 
../../lib/libz3.so: undefined reference to `[email protected]_3.0' 
../../lib/libz3.so: undefined reference to `[email protected]_3.0'.

예는 앞서 Z3 웹 사이트에서 다운로드했습니다. 소스 코드와 함께 제공되는 test_capi 예제를 빌드 할 때 위의 오류 메시지가 결합되어 있습니다.

문제점의 본질은 무엇입니까? Z3을 사용하기위한 시스템의 전제 조건이 있습니까?

다른 데비안 6.0 시스템에서는 모든 것이 원활하게 진행됩니다. 미리 감사드립니다.

출처

2012-11-01 Egbert

공식 src 릴리스 또는 마스터 분기를 사용하고 있다고 가정합니다. 그렇다면 test_capi 디렉토리에서 test_capi을 사용하여 컴파일하려고 할 수 있습니까? 명령에

gcc -o test_capi -I ../lib test_capi.c -L ../bin/external -lz3 -lstdc++ -lgomp

우리가 명시 적으로 C++ 표준 및 OMP 라이브러리와 링크 gcc을 말하고있다 위. C++ 예제의 경우, g ++가 기본적으로 C++ 표준 라이브러리와 연결되므로 -lgomp을 포함하면됩니다. 당신은 ldd를 사용하여 다른없는 종속성을 찾을 수 있습니다

, 나는 Z3를위한 새로운 빌드 시스템에서 일하고 있어요 말했다되고 그건

ldd ../bin/external/libz3.o

, 당신은 CodePlex의에서 unstable 분기를 얻어서 그것을 시도 할 수 있습니다. 시도해 줄 수 있니? 빌드가 더 많은 플랫폼에서 원활하게 진행될 수 있도록 의견을 보내 주시면 감사하겠습니다.

출처

2012-11-01 17:26:02

감사합니다. 플래그 -lstdC++ -lgomp이 나를 위해 일했습니다! 발견 된 또 다른 해결 방법은 LD_LIBRARY_PATH에서/usr/lib를 제외하는 것이 었습니다. 런타임에 다른 버전의 libstdC++가 GCC 4.4.3에서 제공 한 것보다 사용 된 것으로 보입니다. 그 기계에는 구형 GCC 버전이 설치되어 있기 때문입니다. – Egbert

불안정한 지점의 경우 빌드가 성공적이지 않았습니다. 레니에 사용 된 파이썬은 2.5이고 (http://wiki.debian.org/Python을 참고하십시오), 새로운 버전이 필요합니다 : [...] 'src/api/dotnet/Enumerations.cs'생성 [ ...] 파일 "scripts/update_api.py", 줄 663 예를 제외하고 예외 : SyntaxError : 잘못된 구문 – Egbert

불안정한 분기를 사용해 주셔서 감사합니다. 나는 파이썬 2.5를 지원하려고 노력할 것이다. –

Z3 테스트 예제를 컴파일하면 빌드 오류가 발생합니다.

답변

관련 문제