Frama-C
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2026/09/22 12:33 UTC 版)
|
この記事には大規模言語モデル（生成AI）による文章が転載されている可能性があります。 (2026年9月)
|
|
 |
|
| 開発元 | Commissariat à l'Énergie Atomique (CEA-List) and Inria |
|---|---|
| リポジトリ | |
| プログラミング 言語 |
OCaml, C |
| 対応OS | Linux, macOS, FreeBSD, OpenBSD, NetBSD, Microsoft Windows.[1] |
| 対応言語 | English |
| 種別 | Formal verification, Static code analysis |
| ライセンス | mostly LGPL, some parts under BSD licenses |
| 公式サイト | frama-c |
Frama-Cは、C言語のプログラムを対象とした相互運用可能なプログラム解析ツール群である。名称の「Frama-C」は Framework for Modular Analysis of C programs（Cプログラムのためのモジュール式解析フレームワーク）の略である。フランスの原子力・代替エネルギー庁（CEA-List）とInria（フランス国立情報学自動制御研究所）によって開発されており、Core Infrastructure Initiativeからの資金提供も受けている。Frama-Cは静的解析ツールでありプログラムを実行せずに検査する。名称は似ているが、フランスのプロジェクトであるフラーマソフトとは無関係である。
アーキテクチャ
Frama-Cは、EclipseやGIMPと同様のモジュール式プラグインアーキテクチャを採用している。
Frama-Cは、CIL（C Intermediate Language）を用いて抽象構文木を生成する。この抽象構文木は、ANSI/ISO C Specification Language（ACSL）で記述された注釈（アノテーション）に対応している。
いくつかのモジュールは抽象構文木を操作し、ACSLの注釈を追加することができる。よく使われるプラグインには次のようなものがある。
- Value analysis：プログラム中の各変数について、その値、または取りうる値の集合を計算する。抽象解釈の手法を用いており、他の多くのプラグインがその解析結果を利用している。
- Jessie：性質を演繹的に検証する。WhyまたはWhy3をバックエンドとして用い、証明責務（proof obligation）をZ3、Simplify、Alt-Ergoなどの自動定理証明器や、Rocq（旧称Coq）、Whyなどの対話型定理証明器に送ることができる。Jessieを使うと、バブルソートの実装や簡易的な電子投票システムが、それぞれの仕様を満たすことを証明できる。また、分離論理に着想を得た分離メモリモデルを採用している。
- WP（Weakest Precondition、最弱事前条件）：Jessieと同様に、性質を演繹的に検証する。Jessieと異なり、メモリモデルを切り替えられるようにパラメータ化することに重点を置いている。また、Cプログラムを直接Why言語に変換するJessieと違い、WPはValue analysisなど他のFrama-Cプラグインと連携するよう設計されている。オプションでWhy3プラットフォームを利用すれば、他の多くの自動証明器や対話型証明器を呼び出すこともできる。
- E-ACSL（Executable ACSL）：プログラムに計装を施し、性質の実行時検証を行う。Value analysisやWPなど他のプラグインを補う形で使うこともできる（例えば、他のプラグインで静的に検証できなかった性質について、アサーションを実行時に検査する）。
- Impact analysis（影響解析）：Cソースコードへの変更が及ぼす影響を明示する。
- Slicing（スライシング）：プログラムスライシングを行う。与えられた性質を保ったまま、より小さな新しいCプログラムを生成できる。
- Spare code：Cプログラムから不要なコードを取り除く。
その他のプラグイン:
- Dominators：各文の支配節点（dominator）と後支配節点（postdominator）を計算する。
- From analysis：関数的依存関係を計算する。
機能
Frama-Cは次のような目的に利用できる。
- 他人が書いたCコードを理解する。特に、取りうる値の集合を観察したり、プログラムをより短いプログラムにスライスしたり、プログラム内を移動しながら読み進めたりできる。
- コードの形式的な性質を証明する。ACSLで記述した仕様を用いることで、起こりうるあらゆる振る舞いについて、コードの性質を保証できる。浮動小数点数も扱うことができる。
- 独自のプラグインを用いて、Cソースコードにコーディング規約を適用する。
- 特定のセキュリティ上の欠陥への対策として、Cコードに計装を施す。
関連項目
脚注
- ↑ “opam - Install”. opam.ocaml.org. 2026年7月4日閲覧。
- ↑ “Lessons Learned from Verifying Actual C Code with Frama-C”. YouTube (2021年7月11日). 2026年9月22日閲覧。
- ↑ Baudin (2024年2月26日). “The dogged pursuit of bug-free C programs: The Frama-C Software Analysis Platform”. cea.hal.science. 2025年8月16日時点のオリジナルよりアーカイブ。2026年3月17日閲覧。
外部リンク
- 公式ウェブサイト
- Frama-C discussion list Archived 2008-12-30 at the Wayback Machine.
- Frama-C Bug Tracking System
- Frama-Cのページへのリンク
