Ошибка синтаксиса плагина frama-c wp при использовании CVC4 prover - PullRequest
Новая
       24

Ошибка синтаксиса плагина frama-c wp при использовании CVC4 prover

0 голосов
/ 02 ноября 2018

С примером файла 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.

...