問題タブ [cbmc]

Python から CBMC を呼び出す方法はありますか、またはそのためのラッパーまたは API はありますか?

私の問題は次のとおりです。Python で C 関数を自動的に作成し (これは非常にうまく機能します)、それらを Python から CBMC に送信して、関数が正常かどうかを確認し、フィードバックを得たいと考えています。

Visual Express なしでスタンドアロンとして CBMC を実行することは可能ですか? 再コンパイルする必要がありますか、それとも別のトリックがありますか?

関数を CNF に定期的に変換するために CBMC を使用するだけでよいので、関数名で呼び出し、cnf ファイルをディスクに書き込んで、最初からやり直します。Visual Studio を使用したくありません。

私は、条件を満たすb[4][4]場所だけが 1 で、残りが 0 になるようにテーブルを制約しようとしています。i>=j(stored[i] & stored[j]) == stored[i]

なぜこれが機能しないのですか？

CProver は、b[i][j] == 1を意味するはずの効果を得ようとしていると想定しstored[i]& stored[j] == stored[i]ます。しかし、出力にはこの効果はありません。どうしたの？私はCBMCとCも初めてです。

私は、CBMC (C 境界モデル チェッカー) で「正確に 1 回」のプロパティを記述するためのより良い解決策を思いつくために一生懸命努力しています。つまり、行内の 1 つの要素の位置が値 1 (またはブール値 true としてチェックできる任意の正の数) を持つ必要があり、残りはすべてゼロでなければなりません。

M = 4 の場合

それ以上のMは大問題です。M = 8 としましょう。次のようなことをしなければなりません:

違反を 1 回だけチェックするのは簡単ですが、それを述べるのは簡単ではありません。もう 1 つのオプションがあります。2 次元配列の問題を 1 次元のビットベクトルの問題に記述してから、スマート xor を実行することです。しかし、私は現在それについて確信が持てません。

誰にも問題のより良い解決策がありますか?

ハミルトニアン パスを持つ合計ノード 6 のグラフを取得しようとしているだけです。これは上記のコードでうまく機能します。しかし、len ie total no.of edge を使用しようとすると、 cbmc run で無限の巻き戻しが発生します。

上記のコードは、 len を使用して反復しない限りうまく機能します。cbmc の実行が無限の巻き戻しに入る ?? 誰でもそれを説明できますか。

C と C++ の両方のプログラムに対して、Ubuntu でCBMC Bounded Model Checkerを使用しようとしています。gcc (4.9 v) および g++ (4.9 v) コンパイラをダウンロードし、端末から CBMC をインストールしました。

C プログラムを検証でき、以下の手順を使用しても問題は発生しません。

Α .c ファイルの名前file2.c:

端末タイプ:

出力：

次の .cpp ファイルを実行しようとすると、エラーが発生します。

sum_num.cppファイル：

ターミナルに次のように入力します。

出力 - エラー:

次のコード スニペットがあります。

このコードでは、1 バイトのメモリをポインターに割り当てています。次に、メモリが割り当てられてから20ユニット後のメモリ位置にアクセスしています。そのポインターを逆参照すると、メモリ アクセス違反エラーやセグメンテーション フォールトなどのエラーが発生することが予想されます。そのようなエラーは発生しません。

これが未定義の動作のケースであると仮定しましょう。そこで、よく知られたモデルチェッカーであるCBMCを使って、以下のコマンドでこのプログラムを検証してみました。

CBMC は、プログラムが安全であることを報告しています。それはCBMCの問題ですか、それとも何か不足していますか?

GitHub のオープンソース C プロジェクトでCBMC (C Bounded Model Checking: https://www.cprover.org/cbmc/ )を使用しようとしています。この質問のために、次のプロジェクトを考えてみましょう: https://github.com/reubenhwk/radvd

プロジェクトをgccでコンパイルすると問題が発生します。cbmc を呼び出す実行可能ファイルを取得できます

しかし、次のエラー メッセージが表示されます。

その理由は、goto-cc の代わりに gcc を使用したため (ここで説明されているように: http://www.cprover.org/cprover-manual/goto-cc.html )、ファイルを認識できない可能性があるためです。また、前のリンクとhttp://www.cprover.org/goto-cc/examples/nanosat.htmlのような例で説明したように、goto-cc を使用しようとしました。ただし、これらはガイド付きの例であるため、cbmc を機能させるのは簡単なようです。リンクされたプロジェクト（radvd）などの他のプロジェクトで同じプロセスを実行し、gcc の代わりに goto-cc を使用すると、make CC=goto-ccコマンド の実行時に次のメッセージが表示されます。

現在、仮想 Linux マシン (Ubuntu 17.10) でバージョン 5.8 の cbmc を使用しています。

それを機能させる方法について何か考えはありますか？

ありがとうございました