frama-c

1熱

1答えて

mallocが割り当てられたバッファを正常に返すと仮定してプログラムを分析したいと思います。 #include <stdlib.h> int main(){ char * test = malloc(10); test[0] = 'a'; } は、私は次のような出力が得られます：私はこの単純なプログラムにコマンド /Users/philippeantoine/.opam

5熱

2答えて

符号なし整数オーバーフローに依存するコードの証明はありますか？

いくつかの非効率性を避けるために、モジュラ算術に依存する次のようなコードの正確性を証明するにはどうすればよいですか？ #include <stdint.h> uint32_t my_add(uint32_t a, uint32_t b) { uint32_t r = a + b; if (r < a) return UINT32_MAX; return

1熱

1答えて

Frama-Cプラグインの開発：価値分析の結果を得る

私は、価値分析を使ってFrama-Cのためのプラグインを開発しています。私は単に各ステートメントの後に変数（値）の状態を出力したい（私は解決策は簡単だと思いますが、わかりませんでした）。訪問者のvstmt_auxメソッドでDb.Value.get_stmt_stateの現在の状態を取得しました。どのように変数の値を取得できますか？ PS：私はこの記事を見つけたが、それは助けにはならなかった、

0熱

1答えて

Frama-C：ステートメントの値を取得する

私は現在のステートメントの値を取得するFrama-C-Pluginを開発したいと思います。 Frama-C Plugin development: Getting result of value-analysis私はステートメントの値を印刷することができましたが、必要な方法でポインタが表示されませんでした。コメントの助けを借りて、私は状態全体（文の変数だけでなく）を印刷することができました。私

0熱

1答えて

Frama-C：プラグインで注釈を追加

私はFrama-C-pluginを書いています。このプラグインでは、関数に注釈を追加したいと考えています（たとえば、関数名= "test"の場合、パラメータ== 1と言うrequire句を追加します）。 Annotations.add_requiresという関数が見つかりましたが、パラメータの一部（Emitter.t、Identified_predicates）がわかりません。 string-pa

0熱

1答えて

Frama-CコードスライサーがCファイルをロードしていません

教授が書いた10個の数学アルゴリズムを持つ1000行のCファイルがあります。1000個の行から9個の数学関数とすべての依存関係を削除する必要があります。 Frama-C Boron windowsバイナリインストーラを使用してください。ここでは、最も単純なexample.cファイルはロードされません...私はソースファイルを選択し、何もロードしません。ボロン版は2010年のものですので、後でF

0熱

1答えて

Frama-C WPプラグインが扱える一時変数の数はいくつですか？

私は、合計44個の一時変数が存在する特定のプログラムの弱い前提条件を生成しようとしていました。 2つの一時変数の値が仮定されます。他のすべての変数は、これらの2つの変数から導出されます。また、2つの入力変数があります。ここに私のコードのセグメントです。 void main(int err1_10, int err2_10){ int x_mkfirm1,x_mkfirm2; i

2熱

1答えて

Coqインタラクティブ定理証明書でFrama-c WPプラグインを実行するには？

スワップの例のフォームWPプラグインのチュートリアルです。 /*@ requires \valid(a) && \valid(b); @ ensures A: *a == \old(*b) ; @ ensures B: *b == \old(*a) ; @ assigns *a,*b ; @*/ void swap(int *a, int *b) { int tmp;

0熱

1答えて

Frama-C-Plugin：ポインタをポインタに解決する

ポインタの値（ポインターのアドレスではなく、そのアドレスの値）を取得する、frama-c-pluginを開発しています。単純なポインタでこれまでの動作です。今私はポインタへのポインタを扱いたい。例えば： int k=12; int *l=&k; int **m = &l; int ***n = &m; 私の実際のバージョンでこのコードを分析し、私は値を取得： k=12 l=12

1熱

1答えて

Frama-Cの値Builtins

私はちょうどOpamのパッケージマネージャからインストールしてビルドしました。frama-cウェブサイトのチュートリアルのバリュー分析の使い方を学んでいます。私は現在、builtin.cファイルを使用することができません。共有フォルダにはありません。また、-val-builtin（それが適切であれば）を使用する方法を理解することはできません。これを行う方法に関するアイデアはありますか？ Fram