問題タブ [acsl]

他の正式な仕様でセットのカーディナリティをよく使用しますが、WP frama-c プラグインを使用して ACSL で使用できるかどうか疑問に思っています。

たとえば、書く assumes card({*a, *b, *c}) == 3 よりも 書く方が明確に思えます。assumes *a != *b && *a != *c && *b != *c

問題の説明

スライシング プラグインをライブラリとして使用して、自動生成されたコードの未使用部分を削除する frama-c プラグインを開発しています。残念ながら、スライシング プラグインは、実際に使用される一連のスタック値をドロップします。これらは、それらのアドレスが抽象的な外部関数に渡される構造体に含まれている限り使用されます。

簡単な例

これは、私が持っているのと同じ一般的な構造をモデル化した、より単純な例です。

この例をスライスするとframa-c-gui -slice-calls some_function experiment_slicing.c(GUI を使用せずにコマンド ラインを呼び出したときにスライス出力を表示する方法がわかりません)、宣言int *a[];と への呼び出し以外はすべて削除されsome_functionます。

試みられた修正

ACSL アノテーションを追加して修正してみました。しかし、私が賢明な仕様 (以下を参照) であると信じていたものは機能しませんでした

次に、目的の動作をする割り当て (以下を参照) を試しました。ただし、関数が実際にポインターに書き込むことはなく、正しい機能のためにそれを読み取る必要があるため、これは正しい仕様ではありません。このような誤った仕様で進めば、後で奇妙な問題が発生するのではないかと心配しています。