4

現在の Frama-C リリースとその前提条件を Mac にインストールするにはどうすればよいですか?

Mac OS X 10.6.8 を実行するラップトップと、ソフトウェアをインストールできる Mac OS X 10.7.5 を実行するデスクトップがあります。また、Mac OS X 10.8 を実行しているマシンのラボにもアクセスできます。質問があれば、技術サポート担当者がそれらにインストールします。

私には、プログラム分析に興味を持っている学生がいて、何かを理解したり追加したりできる何かを必要としています。私は Frama-C を知っていましたが、別の大学の同僚がそれを勧めました。

以前に Frama-C をインストールしようとしたことがあり、惨めに失敗しました。同僚は、自分も同じ経験をしたとコメントした。さて、時代は変わります。そこで私は Frama-C の Web サイトにアクセスし、これまで以上に感銘を受け、それを手に入れたいと強く思い、取り掛かりました。

frama-c.com のダウンロード ページには、どのプラットフォームの現在の (Flourine 3) リリースのバイナリへのリンクもありません。インストール手順へのリンクをクリックすると、自動インストーラーをダウンロードするように指示されたページに移動します。どの自動インストーラー？

古いバージョンの Mac OS X 用の手順がありますが、それに従ってもうまくいきませんでした。指示に従って前提条件の 1 つのセットをロードすると、次の前提条件 (gtksourceview) がインストールされない状態が生成されました。

もちろん、以前のリリースを確認したところ、Mac OS X Leopard 用の Nitrogen バージョンがあることがわかりましたが、「/ でルートとしてアーカイブを解凍してください」と、不可能なことを実行するよう求められます。私は root アカウントを持っておらず、今後も与えられることはありません (マシンはすべて大学のものです)。gcc と clang を好きな場所にインストールすることは完全に可能です。なぜ Frama-C は / に入りたいのですか?

4

3 に答える 3

5

Pascal の回答に加えて、OCaml アプリケーションのソース パッケージ マネージャーであるopamも参照できます。MacOS X で動作するようで、Frama-C の Oxygen と Fluorine 用のパッケージがあります。

于 2013-08-08T12:56:56.953 に答える
4

すべての Frama-C バイナリ パッケージは、/ (正確には /usr/local/Frama-C) にインストールする必要があります。これは、Frama-C が GTK+ およびさまざまな GTK+ 関連ライブラリを使用するためです。これらのライブラリは、固定された場所以外から実行するようには設計されていません。これらは、コンパイル時にハードコードされたパスから構成ファイルとリソースをロードします。GCC と Clang は GTK+ に依存しないため、どこにでもインストールできます。それらと同様に、Frama-C のコマンド ライン バージョンは、ここにリストされているさまざまな環境変数を介して再配置できます。

バイナリ パッケージを利用するには、/usr/local/Frama-C から実際にファイルを抽出した場所を指すシンボリック リンクが 1 つだけ必要であることに注意してください (管理者が許可している場合)。バイナリ パッケージは、1 つの OS X バージョンでのみ機能します。公式 Web サイトから入手できるパッケージの場合、このバージョンは通常 10.6 (Snow Leopard) です。

Frama-C バイナリ パッケージの作成を中止した理由は 2 つあります。

  1. 過去 2 回の OS X リリースのそれぞれでハードウェア構成の機能とサポートを削除することで、Apple は OS X のランドスケープを細分化し、私には対処する時間がありません。質問で10.6、10.7、および10.8について言及しています。また、10.6、10.7、および 10.8 のそれぞれを実行している Mac もあります。それらはすべて互換性がありません (コンパイラを含むソフトウェア パッケージをビルドしようとした場合)。
  2. Frama-C ベースの静的解析を関心のある産業ユーザーに提供するスタートアップ企業の設立に参加しているため、今は利用できる時間がはるかに少なくなっています。

とはいえ、オープンソースの高度な研究プロトタイプである Frama-C は引き続き開発および維持されており、実験するための優れたテストベッドであり続けています。すでに試しました：

  1. コマンドライン バージョンのみをインストールします。次に、唯一の依存関係は OCaml コンパイラの最近のバージョンです。Frama-C の configure は、GTK ライブラリがないことを検出し、それらを使用しようとしません。最近の OCaml + 最新の Frama-C の場合、インストールには最大 20 分かかります。
  2. 仮想マシンに最新の Linux ディストリビューションをインストールします。そのディストリビューションのパッケージ マネージャーを使用して、すべての GTK+ 依存関係を取得します。ディストリビューションの OCaml パッケージが十分に新しい場合は、それを使用してから lablgtk-2 パッケージを使用します。そうでない場合は、OCaml をコンパイルしてからソースから lablgtk-2 をコンパイルします。次に Frama-C をコンパイルします。

Fluorine の場合、サポートされている最も古い OCaml バージョンは 3.12.1 です。

于 2013-08-08T06:33:41.293 に答える
1

Macports を使用:

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
于 2014-04-12T13:59:08.260 に答える