frama-c - Frama-C ロジック ラベルについて

Question

デフォルトのロジック ラベル LoopEntry と LoopCurrent を使用しようとすると、問題が発生します。これは、私が使用するさまざまな証明者 (alt-ergo、coq、cvc3、z3) が証明できない簡単な例です。

/*@ requires n > 0;*/
void f(int n){
    int i = 0;
    /*@ loop invariant \at(i,LoopEntry) == 0;
      @ loop invariant \at(i,LoopCurrent) >= \at(i,LoopEntry);
      @ loop invariant 0 <= i <= n;
      @ loop assigns i;
      @ loop variant n-i;
    */
    while(i < n){
        i++;
    }
}

特に、1 番目と 2 番目の不変条件は証明されていません (他は問題ありません)。ここで、i の宣言/定義の後にラベル「label」を追加してこの単純な例を変更し、そのラベルを参照して、ここで LoopCurrent を変更すると (このスニペットが得られます:

/*@ requires n > 0;*/
void f(int n){
    int i = 0;
    label : ;
    /*@ loop assigns i;
      @ loop invariant \at(i,label) == 0;
      @ loop invariant \at(i,Here) >= \at(i,label);
      @ loop invariant 0 <= i <= n;
      @ loop variant n-i;
    */
    while(i < n){
        i++;
    }
}

)

これですべてが証明されました。

Acsl のデフォルト ロジック ラベルに関するドキュメントは非常に理解しやすく、最初の例が 2 番目の例として証明されることを期待していました。問題がどこから来るのか説明していただけますか?

ロー

PS1 : ループ句で Pre が使用される場合、Pre は何を参照しますか? 最初のループ反復または前の反復の前の状態??

PS2 : Frama-C Fluorine を使用していますが、マイナー アップデートごとにアップグレードしていない可能性があります。