frama-c.byte - クラウド上のオンライン

プログラム：

NAME

frama-c [.byte] -Cプログラム用の静的アナライザー

frama-c-gui [.byte] -frama-cのグラフィカルインターフェイス

SYNOPSIS

フレームc [ オプション ] ファイル

DESCRIPTION

フレームc は、Cで記述されたソースコードの分析専用のツールスイートです。
単一のコラボレーションフレームワークにいくつかの静的分析手法を収集します。 この
フレームワークは、に配置された追加のプラグインによって拡張できます。 $ FRAMAC_PLUGIN ディレクトリにあります。
コマンド

frame-c -ヘルプ

現在インストールされているプラ​​グインの完全なリストを提供します。

frame-c-gui のグラフィカルユーザーインターフェイスです フレームc。 それはと同じオプションを備えています
コマンドラインバージョン。

フレーム c.byte & frame-c-gui.byte コマンドラインのocamlバイトコードバージョンであり、
それぞれグラフィカルユーザーインターフェイス。

デフォルトでは、Frama-Cは認識します .c 前処理が必要なCファイルとしてのファイルと .i ファイルとして
Cファイルはすでに前処理されています。 一部のプラグインは、認識されたリストを拡張する場合があります
ファイル。 前処理は、 -cpp-コマンド & -cpp-extra-args
オプション。

OPTIONS

構文

追加のパラメータをとるオプションは、フォームの下に書くこともできます

-オプション=パラメータ

このオプションは、次の場合に必須です。 パラメータ ダッシュ（ '-'）で始まります

パラメータをとらないほとんどのオプションには、対応するオプションがあります

-番号-オプション

逆の効果を持つオプション。

カスタマーサービス オプション

-助けて 短い使用通知とインストールされているプラ​​グインのリストを提供します。

-カーネルヘルプ
Frama-Cのカーネルによって認識されるオプションのリストを出力します

-詳細 n
詳細レベルを設定します（デフォルトは1）。 0に設定すると、出力が少なくなります
メッセージ。 このレベルは、ごとに設定することもできます プラグイン 基本、オプション付き -プラグイン-
詳細 n。 カーネルの詳細レベルはオプションで制御できます
-カーネル-verbose n.

-デバッグ n
デバッグレベルを設定します（デフォルトは0で、デバッグメッセージがないことを意味します）。 このオプション
プラグイン（およびカーネル）ごとの専門分野は -詳細.

-静かな 詳細度とデバッグレベルを0に設定します。

オプション 制御 Frama-Cの kernel

-絶対有効範囲
範囲内のすべての数値アドレスが 最小-最大 有効です。 境界は
ocaml整数定数として解析されます。 デフォルトでは、すべての数値アドレスは
無効と見なされます。

-パスを追加 p1 [、p2 [...、pn]]
ディレクトリを追加します 　 プラグインが存在するディレクトリのリストへ
検索

[-いいえ]-重複を許可する
テストとループの正規化中に小さなブロックを複製できます。
それ以外の場合、正規化ではラベルとgotoを使用します。 より大きなブロックと非
些細な制御フローが複製されることはありません。 デフォルトはyesです。

[-いいえ]-アノ
ACSLアノテーションを読み取ります。 これがデフォルトです。 注釈はによって前処理されません
ディフォルト。 使用する -pp-アノ そのために。

-big-ints-hex マックス
より大きい整数 マックス XNUMX進数で表示されます（デフォルトでは、すべての整数は
XNUMX進数で表示）

-小切手 内部ASTで整合性チェックを実行します（開発者のみ）。

[-no] -collapse-call-cast
関数によって返される値とそれがある左辺値の間の暗黙のキャストを許可します
に割り当てられた。 それ以外の場合は、一時変数が使用され、キャストが明示的になります。
デフォルトはyesです。

[-いいえ]-構成
分析の前に、コード内のすべての構文定数式を折りたたむ。 デフォルト
いいえ。

[-no] -continue-annot-error
注釈を分析する場合、デフォルトの動作（ -番号 このオプションのバージョン）
タイプチェックエラーが発生した場合は、の場合のようにソースファイルを拒否します
Cコード内のタイプチェックエラー。 このオプションをオンにすると、タイプチェッカーは
警告を出力して注釈を破棄するだけですが、タイプチェックは続行されます
（ただし、Cコードのエラーは依然として致命的です）。

-cpp-コマンド CMD
あなたが使用します CMD Cファイルを前処理するコマンドとして。 デフォルトは CPP 環境
変数または

gcc -C -E-I。

設定されていない場合。 ACSL注釈を保持するために、プリプロセッサは保持する必要があります
コメント（ -C gccのオプション）。 %1 & %2 で使用できます CMD を示すために
それぞれ元のソースファイルと前処理されたファイル

-cpp-extra-args 引数
プリプロセッサに追加の引数を与えます。 これは次の場合にのみ役立ちます
-前処理-アノ が設定されています。 注釈の前処理は、XNUMXつの別々の前処理で行われます。
処理段階。 最初のものは、マクロを保持するCコードの通常のパスです。
定義。 これらは、注釈が行われるXNUMX番目のパスで使用されます。
前処理済み。 引数 最初のパスにのみ使用されるため、
XNUMX回使用しないでください（追加のincludeディレクティブやマクロなど）
定義）したがって、代わりにそこに行く必要があります -cpp-コマンド.

[-いいえ] -dynlink
オンの場合、検索パスで見つかったすべての動的プラグインをロードします（を参照） -印刷プラグイン-
path デフォルトの検索パスの詳細については）。 それ以外の場合は、プラグインのみ
に要求された -ロードモジュール ロードされます。 デフォルトの動作はオンです。

-列挙型 再現する
列挙型の表現を決定する方法を選択します。 フレームc
-列挙型 助けます 利用可能なオプションのリストを提供します。 デフォルトは gcc-列挙型

-浮動小数点桁 n
浮動小数点数を出力する場合は、 n 数字。 デフォルトは12です。

-float-flush-to-zero
浮動小数点演算はゼロにフラッシュします

-float-hex
XNUMX進数でフロートを表示します

-フロート-通常
標準のOcamlルーチンでフロートを表示する

-フロート相対
フロート間隔を[として表示 下界++幅 ]

[-no] -force-rl-arg-eval
関数呼び出しの引数の評価順序を右から左に強制します。 さもないと
C規格のように、評価順序は指定されていません。 デフォルトはnoです。

-ジャーナル無効
現在のセッションのジャーナルを出力しません。 見る -ジャーナル対応.

-ジャーナル対応
デフォルトでは、現在の間に実行されたすべてのアクションのジャーナルをダンプします
で再生できるocamlスクリプト形式のFrama-Cセッション -負荷-
スクリプト。 スクリプトの名前は、 -ジャーナル名 オプションを選択します。

-ジャーナル名 名
ジャーナルファイルの名前を設定します（ .ml 拡大）。 デフォルトは
frama_c_journal。

-初期化されたパディング-ローカル
ローカルの暗黙的な初期化により、パディングビットが0に設定されます。falseの場合、パディングビット
初期化されないままになります（デフォルトはyes）。

[-no] -keep-comments
ソースコードをきれいに印刷するときにコメントを保持しようとします（デフォルトはno）。

[-no] -keep-switch
日時 -単純化-cfg が設定され、switchステートメントを保持します。 デフォルトはnoです。

-未使用の指定された関数を保持する
見る -削除-未使用-指定-関数

[-no] -lib-entry
プログラムの実行中にエントリポイントが呼び出されることを示します。 これは、
特に、グローバル変数が初期値を持つと想定することはできません。
デフォルトは -no-lib-entry：エントリポイントは、の開始点でもあります。
プログラムとグローバルには初期値があります。

-負荷 file
に含まれる（以前に保存された）状態をロードします file.

-ロードモジュール m1 [、m2 [...、mn]]
ocamlモジュールをロードします 　 。 これらのモジュールは .cmxsのファイル
Frama-cのネイティブコードバージョンと .cmoor.cmaバイトコードバージョンのファイル（を参照）
詳細については、OcamlマニュアルのDynlinkセクションを参照してください）。 であるすべてのモジュール
プラグイン検索パスに存在するものは自動的にロードされます。

-ロードスクリプト s1 [、s2、[...、sn]]
ocamlスクリプトをロードします 　 。 スクリプトは次のようにする必要があります .mlファイル。 彼ら
Ocaml標準ライブラリとFrama-CのAPIのみに依存してコンパイル可能である必要があります。 もしも
いくつかのカスタムコンパイル手順が必要です。Frama-Cの外部でコンパイルして使用してください。
-ロードモジュール を代わりにお使いください。

-macdep 機械
使用されます 機械 現在のマシン依存構成として（さまざまなサイズ
整数型、endiandness、...）。 現在サポートされているマシンのリストは次のとおりです。
から入手可能 -macdep 助けます オプション。 デフォルトは x86_32

-メイン f
セット f 分析のエントリポイントとして。 デフォルトは「main」です。 デフォルトでは、
分析中のプログラムの開始点と見なされます。 使用する -lib エントリ if f
実行の途中で呼び出されることになっています。

-難読化
コードの難読化されたバージョンを出力します（元の識別子が置き換えられます）
意味のないものによって）そして終了します。 オリジナルと新規の対応表
記号は結果の先頭に保持されます。

-ocode file
きれいに印刷されたコードをにリダイレクトします file 標準出力の代わりに。

[-no] -orig-name
正規化フェーズ中に、一部の変数は異なる場合に名前が変更される場合があります
同じ名前の変数が共存できます（例：グローバル変数と正式な変数）
パラメータ）。 このオプションがオンの場合、これが発生するたびにメッセージが出力されます。
デフォルトはnoです。

[-いいえ]-警告-署名済み-ダウンキャスト
署名されたダウンキャストが宛先範囲を超える可能性がある場合にアラームを生成します（デフォルトは
ない）。

[-いいえ]-警告-署名済み-オーバーフロー
オーバーフローした署名付き操作のアラームを生成します（デフォルトはyes）。

[-いいえ]-警告-署名なし-ダウンキャスト
署名されていないダウンキャストが宛先範囲を超える可能性がある場合にアラームを生成します（デフォルト
いいえ）。

[-no]-警告-符号なし-オーバーフロー
オーバーフローする符号なし操作のアラームを生成します（デフォルトはno）。

[-no] -pp-annot
注釈を前処理します。 これは現在、gcc（またはGNU）を使用している場合にのみ可能です。
cpp）プリプロセッサ。 デフォルトでは、注釈を前処理しません。

[-いいえ]-印刷
pretty-CILで正規化されたソースコードを出力します（デフォルトはno）。

-print-libpath
Frama-Cカーネルライブラリがインストールされているディレクトリを出力します

-印刷パス
のエイリアス -印刷共有パス

-印刷プラグインのパス
Frama-Cがプラグインを検索するディレクトリを出力します（
FRMAC_PLUGIN 変数と -パスを追加 オプション）

-印刷共有パス
Frama-Cがデータを保存するディレクトリを出力します（
FRMAC_SHARE 変数）

-削除-未使用-指定-関数
ACSL仕様はあるが、で使用されていない関数プロトタイプを保持します。
コード。 これがデフォルトです。 属性を持つ関数 FRMAC_BUILTIN いつも
維持。

-セーフ配列
多次元配列または構造体内のフィールドである配列の場合、
すべてのアクセスはバインドされている必要があります（デフォルトで設定されています）。 反対のオプションは -安全ではない-
アレイ

-保存する file
Frama-Cの状態をに保存します file 分析が行われた後。

[-no] -simplify-cfg
分析前にbreak、continue、switchステートメントを削除します。 デフォルトはnoです。

-それから 分析を作成することができます：Frama-Cの最初の実行はオプションで発生します
-それから XNUMX回目の実行は、後のオプションを使用して行われます。 -それから
最初の実行からの現在のプロジェクト。

-その後-オン prj
そして -それから XNUMX回目の実行がプロジェクトで実行されることを除いて prj そのようなものがない場合
プロジェクトが存在する場合、Frama-Cはエラーで終了します。

-時間 file
指定されたユーザーの時刻と日付を追加します file Frama-Cが終了したとき。

-タイプチェック
ソースファイルのタイプチェックを強制します。 このオプションは、それ以上ない場合にのみ関連します
分析が要求されます（タイプチェックは分析の前に暗黙的に行われるため）
が起動されます）。

-ulevel n
構文的にループを展開します n 分析前の回数。 これは非常にコストがかかる可能性があります
一部のプラグイン（値分析など）は、より効率的な実行方法を提供します
同じこと。 詳細については、それぞれのマニュアルを参照してください。 これもできます
を介してループごとにアクティブ化されます ループ プラグマ 広げる 指令。 A
の負の値 n そのようなプラグマを抑制します。

[-no]-ユニコード
utf8文字を使用してACSL式を出力します。 これがデフォルトです。 与えられたとき
-ユニコードなし オプションの場合、Frama-Cは代わりにASCIIバージョンを使用します。 ACSLのマニュアルを参照してください
対応のために。

-安全でない配列
-セーフ配列

[-いいえ]-詳細不明-アクセス
読み取り/書き込みアクセスが不特定の順序で発生していることを確認します（Cによる）
標準のシーケンスポイントの概念）は、別々の場所で実行されます。 と
-指定なし-アクセスは、常に当てはまると想定しています（これがデフォルトです）。

-バージョン
Frama-Cのバージョン文字列を出力します

-警告-XNUMX進浮動小数点
浮動小数点定数を正確に表すことができない場合に警告します（例：0.1）。
のXNUMXつになることができます なし, かつてまたは を

[-いいえ]-警告-宣言されていない-呼び出し先
関数が宣言される前に呼び出されたときに警告します（デフォルトで設定されています）。
フラマC

プラグイン 特定の オプション

それぞれについて、 プラグイン、 コマンド

frama-c-プラグイン-助けて

プラグインに固有のオプションのリストが表示されます。

EXIT ステータス

0 正常に実行

1 無効なユーザー入力

2 ユーザーの中断（killまたは同等のもの）

3 実装されていない機能

4 5 6 内部エラー

125 不明なエラー

終了ステータスが2より大きい場合は、バグ（またはケースの機能要求）と見なすことができます。
終了ステータス3）であり、Frama-CのBTSで報告される場合があります（以下を参照）。

ENVIRONMENT 変数

Frama-Cがファイルを探す場所を制御することが可能です。
次の変数。

FRMAC_LIB
カーネルのコンパイル済みインターフェースがインストールされているディレクトリ

FRMAC_PLUGIN
Frama-Cが標準プラグインを見つけることができるディレクトリ。 プラグインが必要な場合
いくつかの場所で、 -パスを追加 を代わりにお使いください。

FRMAC_SHARE
Frama-Cデータがインストールされているディレクトリ。

onworks.net サービスを使用してオンラインで frama-c.byte を使用する