SMT prover yields 'unknown' despite strong

问题:

Suppose we have the following C annotated code:

#define L  3
int a[L] = {0};
/*@ requires \valid(a+(0..(L - 1)));
    ensures \forall int j; 0 <= j < L ==> (a[j] == j); */
int main() {
        int i = 0;
        /*@ loop assigns i, a[0..(i-1)];
            loop invariant inv1: 0 <= i <= L;
            loop invariant inv2:
                        \forall int k; 0 <= k < i ==> a[k] == k; 
        */
        while (i < L) {
          a[i] = i;
          i++;
        }
        /*@ assert final_progress:
               \forall int k; 0 < k < L ==> a[k] == a[k-1] + 1; 
            assert final_c: 
               a[2] == a[1] - 1; */
        return 0;
}

Why Alt-Ergo/Z3 yields "unknown" or timeouts for final_c assertion despite the fact that final_progress statement was proven? I would definitely like to see "Not valid" for such obviously (from user point of view) invalid statements.

$ frama-c -wp -wp-rte -wp-prover z3 test2.c
..
[wp] [z3] Goal typed_main_assert_final_c : Unknown (455ms)

$ frama-c -wp -wp-rte -wp-prover alt-ergo test2.c 
..
[wp] [Alt-Ergo] Goal typed_main_assert_final_c : Timeout

回答1:

The WP plugin does not support marking properties (preconditions, postconditions, user assertions) as invalid. As documented in section 2.2 of the WP plugin manual, the status is one of:

1. — No proof attempted.

2. — The property has not been validated.

   This status means that a proof could not be found. This might be because the property is actually invalid.

3. — The property is valid but has dependencies.

   You will see this status applied to a property if the WP plugin is able to prove the property assuming one or more properties are fully valid.

4. — The property and all its dependencies are fully valid.

Although the WP plugin does not support marking properties as invalid, you can use the trick of asserting \false at the end of the function:

#define L  3
int a[L] = {0};
/*@ requires \valid(a+(0..(L - 1)));
    ensures \forall int j; 0 <= j < L ==> (a[j] == j); */
int main()
{
    int i = 0;
    /*@ loop assigns i, a[0..(i-1)];
        loop invariant inv1: 0 <= i <= L;
        loop invariant inv2: \forall int k; 0 <= k < i ==> a[k] == k; 
    */
    while (i < L) {
        a[i] = i;
        i++;
    }
    //@ assert final_progress: \forall int k; 0 < k < L ==> a[k] == a[k-1] + 1;
    //@ assert final_c: a[2] == a[1] - 1;
    //@ assert false: \false;
    return 0;
}

Running the WP plugin on this code results in:

...
[wp] [Alt-Ergo] Goal typed_main_assert_false : Valid (114ms) (97)
...

If the WP plugin marks assert \false valid (in the GUI it will show as valid-but-has-dependencies) then you know that there is an invalid property.