は、私は、以下の機能を持っていると仮定すると：frama-cにバッファアクセス節を指定することはできますか？
void process_data(uint32_t * data, size_t length) {
for (size_t i = 0; i < length; i++) {
foo(data[i]);
}
}
は、どのように私は、「この機能はdata[i]条件を満たすi < lengthへのすべてのアクセスを保証します」FRAMA-Cを伝えることができますか？私が理解する限り、dataというコードのすべての行の近くにアサーションを置くことができますが、より良い方法がありますか？
無効なメモリアクセスを防止するには、少なくともlength要素を読み取ることができるdataポインタでこの関数が常に呼び出されることを確認する必要があります。だから、前提条件を記述する必要があります。
//@ requires \valid_read (data + (0 .. length-1));
void process_data(uint32_t * data, size_t length) {
このプロパティが有効であることを確認することができますのであれば、それはあなたが任意の無効なメモリアクセスを持っていないことを保証します。
おそらく私はこれを説明するにはあまりにも明確ではない、申し訳ありません。 'process_data'関数が' length'次元の外で 'data'に潜在的にアクセスできるときに、frama-c wpが特定のチェックに失敗するようにします。たとえば、 'process_data'に' uint32_t a = data [length + 1] 'という文が含まれていれば、チェックは失敗します。 –
@ジョン・ドー私は、あなたのFrama-Cの使用に依存しているのではないかと心配しています。たとえばWPで '-wp-rte'を使う場合、Anneのアノテーションは本当に必要なものです.WPはrequireに書かれているものしか知っていないので、' length'より大きいインデックスにアクセスしようとすると、 RTE注釈の状態が不明です。代わりにValueを使用し、 'process_data'が' length'より大きいサイズのバッファで呼び出された場合は、より具体的な注釈が必要になります。注釈は自分自身（またはカスタムスクリプトを通して）で提供する必要があります。適切な回答を提供できるよう、質問を自由に修正してください。 – Virgile
これで説明します。私はrequire節が価値分析にのみ影響すると思った、ありがとう。 –
あなたの質問 - 絶対に保証されていますか？ 'data'はNULLではなく、' uint32_t'のコレクションを指していますか？おそらく 'for'ループに入る前にアサーションが必要でしょうか？ – t0mm13b
はい、 'data'は' \ valid'で、uint32_tの配列を指しています。 –
「この関数によって保証される」とはどういう意味ですか？ 「この関数が必要です」と言いたいのですが（それ以外の場合は無効なメモリアクセスがあります）、そうですか？ – Anne