FRAMA-C/WP Цели не подтверждаются

Question

Я пытаюсь доказать упрощенную версию примера из руководства по WP, но постоянно получаю сообщение об ошибке для одного из условий обеспечения.

Вот мой код:

      /*@ requires \valid(a) && \valid(b);
@ ensures A: *a == \old(*b) ;
@ ensures B: *b == \old(*a) ;
@ assigns *a,*b ;
@*/
void swap(int *a,int *b)
{
    int tmp = *a;
    *a = *b;
    *b = tmp;
}

Когда я бегуframa-c -wp -wp-rte swap.c, я получаю следующую ошибку:

      [kernel] Parsing main_wp.c (with preprocessing)
[rte] annotating function swap
Collecting axiomatic usagewarning: [Warning] cannot load an editor: missing field 'options'

warning: [Warning] cannot load an editor: missing field 'options'

warning: [Warning] cannot load an editor: missing field 'options'

warning: [Warning] cannot load an editor: missing field 'options'

warning: [Warning] cannot load an editor: missing field 'options'

[wp] 8 goals scheduled
[wp] [Alt-Ergo 2.0.0] Goal typed_swap_ensures_A : Failed
[wp] [Cache] found:3
[wp] Proved goals:    7 / 8
  Qed:               5  (1ms-2ms-4ms)
  Alt-Ergo 2.0.0:    2  (12ms-15ms) (22) (cached: 3) (failed: 1)

Мне было интересно, делаю ли я что-то не так, или это проблема с проверщиками, поскольку я сталкивался с аналогичными ошибками с Alt-Ergo при тестировании файлов из больших кодовых баз.

Я использую Frama-C 24.0 и Alt-Ergo 2.0.0.