問題タブ [frama-c]
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 - Frama-C で基本的な算術型のサイズを制御する方法は?
Frama-Cでは、基本型のサイズを自由に指定することはできますか?
私のターゲットである TMS320F2808 DSP には 16 ビットのバイトがあります。char、short、int 型はすべて 1 バイトで、long 型は 2 バイトです。
Frama-C にこれらのサイズを指定する方法が、可能であればまだわかりません。
ocaml - データ型を Cil_types から Cil に変換する方法
Fram-c を使用してパーサーを作成する場合。Ast.get() が Cil_types.file 型を返すという問題が発生しましたが、今後使用するために Cil.file が必要です。実際には同じフィールドがありますが、ocaml コンパイラは Cil_types.file から Cil.file への直接代入を許可しません。これを行うのに役立つ Ocaml の型キャスト関数はありますか。
Ps: Cil_types.file の各フィールドを Cil.file に割り当てようとしましたが、同じ問題が再帰的に発生します (Cil.file.* = Cil_types.file.* を許可しないでください)。本当にありがとうございます！</p>
frama-c - VC 生成中に frama-c jessie が殺される
顧客からの独自のセーフティ クリティカル システムのモジュールに frama-c/jessie を適用しようとしています。分析中の関数は非常に大きく (コメントなしの 700 行の画像)、多くの条件ステートメントと複雑なステートメント (&&、|| など) があります。
Ubuntu VM 64 ビット マシンで実行すると、このエラー メッセージが表示されました。エラー 137 はメモリ サイズなどに関連しているようですが、よくわかりません。
このエラーに対処する方法についての提案は大歓迎です。
[
frama-c - WP プラグイン: Alt-Ergo 構文エラー
以下の C 関数では、最新バージョンの Frama-c の Alt-Ergo から構文エラーが発生します。
この生成された行の何が問題なのかわかりません:
解析中の C 関数
frama-c - Alt-Ergo を使用した WP プラグイン - 証明できませんか?
かなり複雑な関数で Alt-Ergo を使用して WP プラグインをテストしようとしています。残念ながら、以下に示す「基本的な」動作の何が問題なのかを理解できません。
最初の条件文のelseセクション以外にtenumRModeが更新される場所がないため、この動作は正しいはずです。
奇妙なことは、いくつかの行を任意にコメントすると、Alt-ergo から常に「有効」になることです。
コメントはありますか？
frama-c - frama-c から C ファイル名を取得するには?
Cil_types を使用して、frama-c でプラグインを開発しています。このプラグインは、デフォルトで C プログラムの AST (Cil_types.file) を入力として受け取ります。このファイルの名前を取得したいのですが、Cil_types を使用するとできませんでした。他の方法でこの情報を取得できますか?
windows - Windows 7 での frama-c の使用
frame-c Web サイトhttp://frama-c.com/download.htmlから Windows インストーラーの Boron バージョンをインストールしました。
val プラグインを実行しようとすると、プリプロセッサ変数 CPP が次のように設定されていないというエラーが表示されます。
-cpp-command を使用すると、次のエラーが表示されます。
手がかり/提案はありますか？