問題タブ [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.
frama-c - メイン関数を持たない C ファイルに対して Frama-C で値解析を実行できますか?
main 関数なしで C ファイルに対して Frama-C を実行すると、エラーが発生しました。そのような C ファイルで Frama-C 値解析を実行するオプションはありますか?
macos - Mac OS X に Frama-C をインストールする
現在の Frama-C リリースとその前提条件を Mac にインストールするにはどうすればよいですか?
Mac OS X 10.6.8 を実行するラップトップと、ソフトウェアをインストールできる Mac OS X 10.7.5 を実行するデスクトップがあります。また、Mac OS X 10.8 を実行しているマシンのラボにもアクセスできます。質問があれば、技術サポート担当者がそれらにインストールします。
私には、プログラム分析に興味を持っている学生がいて、何かを理解したり追加したりできる何かを必要としています。私は Frama-C を知っていましたが、別の大学の同僚がそれを勧めました。
以前に Frama-C をインストールしようとしたことがあり、惨めに失敗しました。同僚は、自分も同じ経験をしたとコメントした。さて、時代は変わります。そこで私は Frama-C の Web サイトにアクセスし、これまで以上に感銘を受け、それを手に入れたいと強く思い、取り掛かりました。
frama-c.com のダウンロード ページには、どのプラットフォームの現在の (Flourine 3) リリースのバイナリへのリンクもありません。インストール手順へのリンクをクリックすると、自動インストーラーをダウンロードするように指示されたページに移動します。どの自動インストーラー？
古いバージョンの Mac OS X 用の手順がありますが、それに従ってもうまくいきませんでした。指示に従って前提条件の 1 つのセットをロードすると、次の前提条件 (gtksourceview) がインストールされない状態が生成されました。
もちろん、以前のリリースを確認したところ、Mac OS X Leopard 用の Nitrogen バージョンがあることがわかりましたが、「/ でルートとしてアーカイブを解凍してください」と、不可能なことを実行するよう求められます。私は root アカウントを持っておらず、今後も与えられることはありません (マシンはすべて大学のものです)。gcc と clang を好きな場所にインストールすることは完全に可能です。なぜ Frama-C は / に入りたいのですか?
frama-c - Frama-C ロジック ラベルについて
デフォルトのロジック ラベル LoopEntry と LoopCurrent を使用しようとすると、問題が発生します。これは、私が使用するさまざまな証明者 (alt-ergo、coq、cvc3、z3) が証明できない簡単な例です。
特に、1 番目と 2 番目の不変条件は証明されていません (他は問題ありません)。ここで、i の宣言/定義の後にラベル「label」を追加してこの単純な例を変更し、そのラベルを参照して、ここで LoopCurrent を変更すると (このスニペットが得られます:
)
これですべてが証明されました。
Acsl のデフォルト ロジック ラベルに関するドキュメントは非常に理解しやすく、最初の例が 2 番目の例として証明されることを期待していました。問題がどこから来るのか説明していただけますか?
ロー
PS1 : ループ句で Pre が使用される場合、Pre は何を参照しますか? 最初のループ反復または前の反復の前の状態??
PS2 : Frama-C Fluorine を使用していますが、マイナー アップデートごとにアップグレードしていない可能性があります。
c - 型チェックとコード パターン検出、Frama-C
私は Frama-C ソフトウェアを発見しました。ダブル if テストや、特定の関数の呼び出しの後に常に別の関数が続くなどのコード パターンを検出できるかどうか疑問に思っていました。
または、変数名を使用する何か、たとえば、特定の接頭辞が付いた名前の変数が特定のタイプに属しているかどうかを確認するなどです。
Frama-C で (ACSL を使用するか、新しいモジュールを開発することによって) 可能だと思いますか?
どうもありがとう =)
frama-c - ACSL の PreCondition または PostCondtion
ACSL では、さまざまな前提条件と事後条件を区別できません。私が知っているように、require、terminate、および想定は前提条件であり、post-condition で保証および割り当てます。しかし、減少などの休憩はどのセットにありますか??
理解するのを手伝ってくれる体はありますか?? 前もって感謝します
slice - スライス プラグインの開発に最適な Frama-C のバージョンはどれですか?
Frama-C を調べて、アサーション ベースのスライス (ACSL 表記を使用) を適用したいと考えています。Frama-C にはいくつかの異なる機能を備えたいくつかの異なるバージョンがあることがわかりました。私の質問は、Frama-C へのスライシング プラグインを開発し、Frama-C によって作成された AST を操作するのに最適なバージョンはどれかということです。