問題タブ [cbmc]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
c - cbmcはcヘッダーでどのように機能しますか?
複数の関数を含む ac ファイルがあり、(gcc を使用して) 前処理されたバージョンのプログラムで z3 ソルバーを使用して cbmc を実行したい場合、ヘッダー セクションに他のファイル (c ファイル) がいくつかあります。cbmc はこれらのファイルをどのように認識しますか? 私はそれを実行しようとしましたが、彼はいくつかの変数について、それがどこにあるか宣言されていないというエラーを出しました。実際、それらはヘッダーファイルの1つで宣言されています。
誰かがこれがどのように機能するか説明できますか?
アップデート：
まず、gcc を使用してプログラムを前処理します。
次に、pycparser でプログラムを解析します
次に、計器 (4 の後に print ステートメントを追加して、x の値を確認します)
次に、インストルメント化されたバージョンのファイルで cbmc を実行したところ、次のエラーが発生しました: 関数 `sqrt' は宣言されていません
c - `__CPROVER_fence()` 引数
Linux RCU テストや CBMC 分析用の pthread ラッパー__CPROVER_fence("RRfence", "RWfence");などのプロジェクトで使用されているようなコードを目にします。オンライン ドキュメントを見ましたが、この CBMC 関数に送信された文字列に関するテキストは見つかりませんでした。
に使用できるパラメータは何__CPROVER_fenceですか?
私の見解では、実際の実装によって実行されるバリア/フェンスを示すのは注釈/機能です。つまり、実際の機能の分析スタブです。明らかに、パラメータはバリアのタイプを示していますが、実際のパラメータと対応するバリア タイプへの参照は見つかりませんでした。つまり、「RRFence」は読み取りフェンスです。これは、この時点より前の読み取りが、この時点以降の読み取りの前に完了することを意味します (推測として)。