2

Frama-Cがポインタに関連付けられたある種の型チェックを実装しているかどうか知りたいです。たとえば、次のことを考慮してください。

int x[10];
void * v = x;

//@ assert isOfTypeInt(x, 10)
//@ assert isOfTypeInt(v, 10)

上記に似た精神的なものはありますか？

ACSLのマニュアルを見ると、メモリとポインタの使用を確認する方法はたくさんあります（その一部はFrama-C Oxygenに実装されています）。ただし、型情報を処理するための一般的なサポートは見つかりませんでした。この目的で使用できるframa-cプラグインはありますか？

ありがとう、エドゥアルド

4

1 に答える 1

2

ACSLには確かにそのようなことはありません。実際、Cのメモリ位置には、実際にはタイプ情報が関連付けられていません。潜在的なアラインメント制約を無視すると、4バイトの任意のブロックを使用して32ビット整数を格納できます。

とはいえ、Frama-Cは拡張可能なプラットフォームであり、特定のニーズに合わせてプラグインを作成することはいつでも可能です。あなたの例のようなプレーン変数の場合、宣言された型は、ASTの対応するフィールドからx直接アクセスできます。のようなポインタの場合、Valueの結果を利用して、それらがどこを指しているかを確認し、これを使用して適切な型情報を導き出すことができるはずです（主な問題は、Valueが不正確であり、いくつかの潜在的な場所を提供する場合に何をすべきかを決定することです。他の種類）。vtypevarinfov

于 2012-11-15T08:42:51.613 に答える