Mac OS X에서 Frama-C를 설치하십시오

Question

Mac에 현재 Frama-C 릴리스 및 해당 사전 설치 소프트웨어를 설치하려면 어떻게합니까?

저는 소프트웨어를 설치할 수있는 Mac OS X 10.6.8 및 Mac OS X 10.7.5 을 실행하는 노트북이 있습니다. 또한 Mac OS X 10.8을 실행하는 컴퓨터 실험실 에 액세스 할 수 있습니다. 기술 지원 담당자가 에 물건을 설치할 예정입니다.

나는 프로그램 분석에 관심이 있고 우리가 이해하고 추가 할 수있는 싸움의 기회를 가지고있는 이 필요한 학생이 있습니다. 나는 이미 Frama-C를 알고 있었고, 다른 대학의 동료가 그것을 추천했다.

이전에 Frama-C를 설치하려고 시도했지만 비참하게 실패했습니다. 동료 도 같은 경험을했다는 의견을 냈습니다. 음, 시간이 바뀝니다. 그래서 나는 Frama-C 웹 사이트 을 방문했고, 그 어느 때보 다 더 감동적이고 예민했으며, 그것에 대해 을 설정했습니다.

frama-c.com 다운로드 페이지에는 모든 플랫폼의 현재 (Flourine 3) 릴리스에 대한 바이너리로의 링크가 없습니다. 설치 설치에 대한 링크를 통해 자동 설치 프로그램을 다운로드하라는 페이지로 이동합니다. 자동 설치 프로그램이란 무엇입니까?

이전 버전의 Mac OS X에 대한 지침이 있지만 그 뒤를 따르는 이 작동하지 않습니다. 지침에 따라 일련의 전제 조건을로드하면 다음 필수 조건 (gtksourceview)이 설치되지 않는 상태 인 상태가 생성되었습니다. 물론

나는 이전 버전을 확인하고, 나는 거기에 맥 OS X 레오파드에 대한 질소 버전하지만 은 불가능을 수행하는 나에게 묻습니다 "에서/root로 압축 파일을 압축을 풀어야하시기 바랍니다"것을 알 수있다. 나는 루트 계정이없고 (컴퓨터가 모두 대학에 속함)을 제공하지 않을 것입니다. gcc와 clang을 완벽하게 설치할 수있는 곳은 입니다. 왜 Frama-C가 /에 들어가고 싶어?

Answer 1

모든 Frama-C 바이너리 패키지는/(정확하게/usr/local/Frama-C)에 설치하려고합니다. Frama-C는 GTK +와 다른 GTK + 관련 라이브러리를 사용하기 때문에 고정 된 위치. 컴파일시 하드 코딩 된 경로에서 구성 파일과 리소스를로드합니다. GCC와 Clang은 GTK +에 의존하지 않기 때문에 어디서나 설치됩니다. 이들과 마찬가지로, Frama-C의 명령 행 버전은 here으로 나열된 다양한 환경 변수를 통해 재배치 될 수 있습니다.

바이너리 패키지를 이용하려면/usr/local/Frama-C에서 파일을 추출한 위치로 심볼 링크가 하나 필요합니다. 관리자가 귀하에게 권한을 부여 할 수 있다면 그. 바이너리 패키지는 하나의 OS X 버전에서만 작동합니다. 공식 웹 사이트에서 제공되는 패키지의 경우이 버전은 대개 10.6 (Snow Leopard)입니다.

---

나는 두 가지 이유 FRAMA-C 바이너리 패키지을 중단 한 : 기능과 마지막 두 OS X의 출시 각각의 하드웨어 구성에 대한 지원을 제거하여

1. , 애플은 OS X 세분화했다 나는 방식으로 조경 할 시간이 없다. 귀하의 질문에 10.6, 10.7 및 10.8을 언급합니다. 나는 또한 맥을 각각 10.6, 10.7, 10.8로 돌리고있다.그것들은 모두 호환되지 않습니다 (컴파일러가 포함 된 소프트웨어 패키지를 만들려고 할 때).
2. 관심있는 산업 사용자에게 Frama-C 기반 정적 분석을 제공하는 신생 기업 창립에 참여할 수있게되어서 시간이 훨씬 단축되었습니다.

이것은 오픈 소스 고급 연구 프로토 타입 인 Frama-C가 계속 개발되고 유지되며 실험을 계속할 수있는 훌륭한 테스트 베드가됩니다. Mac에서 루트 액세스없이 Frama-C를 설치할 수 있습니다. 이미 시도한 것과 다른 두 가지 방법 :

1. 명령 줄 버전 만 설치하십시오. 그렇다면 유일한 의존성은 OCaml 컴파일러의 최신 버전입니다. Frama-C의 configure는 여러분이 GTK 라이브러리를 가지고 있지 않으며 그것들을 사용하려고 시도하지 않을 것임을 탐지 할 것입니다. 최신 OCaml + 최신 Frama-C의 경우 설치시 최대 20 분이 걸립니다.
2. 가상 컴퓨터에 최근 Linux 배포를 설치합니다. 해당 배포판의 패키지 관리자를 사용하여 모든 GTK + 종속성을 확보하십시오. 배포판의 OCaml 패키지가 최신 버전이면, 그 패키지를 사용하고 lablgtk-2 패키지를 사용하십시오. 그렇지 않으면 소스에서 OCaml을 컴파일 한 다음 lablgtk-2를 컴파일하십시오. 그런 다음 Frama-C를 컴파일합니다.

불소의 경우 지원되는 가장 오래된 OCaml 버전은 3.12.1입니다.

Answer 2

파스칼의 대답 외에도 OCaml 응용 프로그램의 소스 패키지 관리자 인 opam을 살펴볼 수도 있습니다. MacOS X에서 실행되는 것으로 보이며 Frama-C의 Oxygen 및 Fluorine 패키지가 있습니다. MacPorts를 가진

Answer 3

:

export PKG_CONFIG_PATH=/opt/local/lib/pkgconfig 
sudo port install opam 
opam init 
    Y 
eval `opam config env` 
sudo port install gtksourceview2 lablgtk2 ocaml-ocamlgraph 
opam install frama-c