ユーザーヒントなしでループで拡張を実行する方法を探しています。例を使って説明します：
int z;
void main(void) {
int r = Frama_C_interval(0, MAX_INT);
z = 0;
for (int y=0; y<r; y++)
z++;
}
このコードで frama-c 値解析を実行すると、グローバル変数zは間隔 [--,--] を受け取ります。z がゼロに設定され、ループがインクリメンタル演算子で構成されているため、自動拡張メソッドは、より正確な間隔が [0, --] であると推定できるはずです。Frama-Cでこれを行うことは可能ですか?