0

使用示例 find.c 文件，我可以使用默认的 alt-ergo 证明它没有问题。但是当更改为 cvc4 时，会收到警告消息和语法错误。这里的代码：

/*@ requires 0 <= n && \valid(a+(0..n-1));
    assigns  \nothing;
    ensures  (\result == -1    && ! (\exists int i; 0<=i<n && a[i] == v))
                  || (0 <= \result < n && a[\result] == v);
*/
int find(int n,const int a[n],int v)
{
    int i;
    /*@ loop invariant 0<=i<=n;
    loop invariant \forall int j; 0<=j<i ==> a[j] != v;
    loop assigns i;
    loop variant n - i;
    */
    for (i=0; i<n; ++i)
        if (a[i] == v)
            return i;
        return -1;
}

int main(void)
{
    const int const a1[5] = { 9,7,8,9,6 };
    int const f1 = find(5,a1,8);
    return 0;
}

运行此命令并获取以下消息： frama-c -wp -wp-prover CVC4 -wp-out out find.c

File "out/typed/find_Why3_ide.why", line 14, characters 0-20:
warning: the keyword `import' is redundant here and can be omitted
File "out/typed/find_Why3_ide.why", line 15, characters 0-28:
warning: the keyword `import' is redundant here and can be omitted
File "out/typed/Compound.why", line 6, characters 0-20:
warning: the keyword `import' is redundant here and can be omitted
File "out/typed/Compound.why", line 7, characters 0-18:
warning: the keyword `import' is redundant here and can be omitted
File "out/typed/Compound.why", line 8, characters 0-31:
warning: the keyword `import' is redundant here and can be omitted
File "out/typed/Compound.why", line 9, characters 0-25:
warning: the keyword `import' is redundant here and can be omitted
File "out/typed/Compound.why", line 10, characters 0-18:
warning: the keyword `import' is redundant here and can be omitted
File "out/typed/Compound.why", line 12, characters 0-18:
warning: the keyword `import' is redundant here and can be omitted
File "out/typed/Compound.why", line 13, characters 0-24:
warning: the keyword `import' is redundant here and can be omitted
File "out/typed/find_Why3_ide.why", line 17, characters 60-61:
syntax error
------------------------------------------------------------
[wp] [CVC4] Goal typed_find_loop_inv_2_preserved : Failed
  Why3 exits with status 1.
[wp] [CVC4] Goal typed_find_loop_inv_preserved : Failed
  Why3 exits with status 1.
[wp] [CVC4] Goal typed_find_post : Failed
  Why3 exits with status 1.
[wp] Proved goals:   10 / 13
  Qed:            10  (4ms)
  CVC4:            0  (failed: 3)

如何摆脱警告和语法错误？我的 CVC4 是 1.6 版。

4

0 回答 0