これは、Ubuntu Online、Fedora Online、Windows オンライン エミュレータ、MAC OS オンライン エミュレータなどの複数の無料オンライン ワークステーションの XNUMX つを使用して、OnWorks の無料ホスティング プロバイダで実行できるコマンド goto-cc です。
プログラム：
NAME
cbmc - C/C++ および Java プログラム用の境界モデル チェッカー
SYNOPSIS
CBMC [ - 財産 プロパティID] ファイル.c ...
CBMC [--プロパティを表示] ファイル.c ...
CBMC [--すべてのプロパティ] ファイル.c ...
goto-cc [-私 インクルードパス] [-NS] ファイル.c [-または outfile.o]
goto-instrument ファイル内 アウトファイル
最も便利なオプションのみがここにリストされています。 残りについては、以下を参照してください。
DESCRIPTION
CBMC アサーションがどのように違反されるかを示すトレースを生成するか、
指定されたループ反復回数内ではアサーションに違反することはできません。 CBMCは読み取ることができます
ソースコードを直接、または goto-cc によって生成された goto-binary。 Java プログラムは次のように与えられます。
クラスファイル。 それ以上のオプションを指定しないと、cbmc はすべてのプロパティをチェックします (自動的に
生成またはユーザー指定) がプログラム内で見つかりました。 いずれかのプロパティが可能であれば、
違反した場合は反例が出力され、分析は中止されます。 分析できるのは、
--property オプションを使用すると、特定のプロパティに制限されます。 検証結果
すべてのプロパティは --all-properties オプションを使用して取得できます。
goto-cc ソースコードを読み取り、goto-binary を生成します。 そのコマンドラインインターフェイスは次のとおりです。
を模倣するように設計されています gccの(1)。 特に注意してください goto-cc 区別する
gcc と同様に、コンパイルとリンクのフェーズ。 CBMC goto-バイナリを期待しています。
リンクが完了しました。
goto-instrument goto-バイナリを読み取り、指定されたプログラム変換を実行してから、
結果のプログラムを goto-binary としてディスクに書き込みます。
通常の流れは、(1) goto-cc を使用してソースを goto-binary に変換し、次に (2)
goto-instrument でインストルメンテーションを実行し、最後に (3) で分析を実行します。
cbmc。
OPTIONS
FRONTEND OPTIONS (cbmc & goto-cc)
-Iパス
インクルードパスの設定 (C/C++)
-Dマクロ
プリプロセッサ マクロの定義 (C/C++)
-前処理
前処理後に停止
--show-シンボルテーブル
シンボルテーブルを表示
--show-goto-functions
gotoプログラムを表示
建築 OPTIONS (cbmc & goto-cc)
CBMC デフォルトでは、マシンのアーキテクチャ設定と一致するアーキテクチャ設定が使用されます。 CBMC is
つまり、以下の設定は、次のソフトウェアを検証する場合にのみ必要です。
異なるアーキテクチャまたは OS 上で実行することを目的としています。 goto-cc の goto バイナリを生成します。
特定のアーキテクチャ。つまり、goto-binary が実行された後はアーキテクチャを変更できません。
生成された。
--16、-32、-64
int の幅を設定する
--LP64、--ILP64、-LLP64、--ILP32、--LP32
int、long、ポインタの幅を設定する
-リトルエンディアン
リトルエンディアンのワードバイト変換を許可する
-ビッグエンディアン
ビッグエンディアンのワードバイト変換を許可する
--unsigned-char
デフォルトで「char」を署名なしにする
--arch ターゲット アーキテクチャを設定します
--os ターゲット オペレーティング システムを設定します
--アーチなし
アーキテクチャをセットアップしないでください
--ライブラリなし
組み込みの抽象 C ライブラリを無効にする
--round-to-nearest、--round-to-plus-inf、--round-to-minus-inf、--round-to-zero
プログラムの開始時に使用する IEEE 浮動小数点丸めモード (デフォルトはround)
最も近いところへ）。 検証中のプログラムは、たとえば次のようにしてこの設定をオーバーライドできます。
フェセットラウンドとします。
プログラム 計装 OPTIONS (cbmc & goto-instrument)
両方 CBMC & goto-instrument 特定の一般的なエラーをキャッチするアサーションを生成できます。
以下に示すように。
-- 境界チェック
配列境界チェックを有効にする
--div-by-zero-check
ゼロ除算チェックを有効にする
--ポインタチェック
ポインタチェックを有効にする
--signed-overflow-check
符号付き整数演算のオーバーフローおよびアンダーフローの算術チェックを有効にする
-- unsigned-overflow-check
符号なし整数演算のオーバーフローおよびアンダーフローの算術チェックを有効にする
--ナンチェック
NaN の浮動小数点計算をチェックする
-アサーションなし
ユーザー指定のアサーションを無視する
-- 仮定なし
ユーザーが提供した仮定を無視する
--error-label ラベル
指定されたラベルが到達不能であることを確認する
プログラム 計装 OPTIONS (goto-instrument のみ）
goto-instrument さらに複雑なプログラム変換をサポートします。
--非デット揮発性
揮発性変数からの読み取りを非決定的にする
--isr関数
指定された名前で割り込みサービス ルーチンをインストルメントします。
--mmio 計測器のメモリマップ I/O
--nondet-static
静的な有効期間を持つ変数は非決定的に初期化されます
--ダンプ-c
goto バイナリの代わりに ANSI-C ソース コードを出力します。
BMC OPTIONS (CBMC)
--すべてのプロパティ
すべてのプロパティのステータスをレポートする
--show-プロパティ
プロパティのみを表示
--show-loops
プログラム内のループを表示する
--cover-assertions
どのアサーションが到達可能であるかを確認する
--関数名
メイン関数名を設定する
--プロパティID
指定された識別子を持つ特定のプロパティのみをチェックします
--プログラムのみ
プログラム式のみを表示
--深さ番号
検索の深さを制限する
--巻き戻し番号
ループをn回ほど巻き戻す
--unwindset L:B,...
ループ L を B の境界で巻き戻します (ループ ID を取得するには --show-loops を使用します)
--show-vcc
検証条件を表示する
--スライス式
プロパティに関係のない割り当てを削除する
--no-unwinding-assertions
アンワインド アサーションを生成しない
--きれいな名前はありません
識別子を単純化しないでください
バックエンド OPTIONS (CBMC)
--dimacs
外部 SAT ソルバーで使用するために CNF を DIMACS 形式で生成します
--beautify-貪欲
反例を美しくする (貪欲なヒューリスティック)
--smt1 SMT1 構文でサブゴールを出力します (実験的)
--smt2 SMT2 構文でサブゴールを出力します (実験的)
--boolector
Boolector を使用する (実験的)
--マスサット
MathSAT を使用する (実験的)
--cvc CVC3 を使用します (実験的)
--そうだね
Yices を使用する (実験的)
--z3 Z3 を使用します (実験的)
- リファイン
改良手順を使用する (実験的)
--outfile ファイル名
指定されたファイルに数式を出力する
--arrays-uf-never
配列を解釈されていない関数にしないでください
--arrays-uf-always
常に配列を解釈されない関数に変換する
ENVIRONMENT
すべてのツールは、一時ファイルを生成するときに TMPDIR 環境変数を尊重します。
ディレクトリ。 さらに、CBMC によって使用されるプリプロセッサは環境を使用することに注意してください。
ヘッダー ファイルを見つけるための変数。 GOTO-CC は、次のすべての環境変数を受け入れることを目的としています。
GCC はそうします。
COPYRIGHT
2001～2014年、ダニエル・クローニング、エドモンド・クラーク
onworks.net サービスを使用してオンラインで goto-cc を使用する
