Плагин frama-c wp не может проверить функцию подкачки из руководства

Question

Как сделать frama-c -wp проверить пример из руководства wp - тривиально swap функция (swap.c):

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

void swap(int * a, int * b) {
    int tmp = * a;
    *a = *b;
    *b = tmp;
    return ;
}

Вызов

$ frama-c -wp -wp-rte swap.c

дает:

[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing swap.c (with preprocessing)
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[rte] annotating function swap
[wp] 4 goals scheduled
[wp] [Alt-Ergo] Goal typed_swap_assert_rte_mem_access_4 : Unknown (174ms)
[wp] [Alt-Ergo] Goal typed_swap_assert_rte_mem_access_2 : Unknown (160ms)
[wp] [Alt-Ergo] Goal typed_swap_assert_rte_mem_access : Unknown (154ms)
[wp] [Alt-Ergo] Goal typed_swap_assert_rte_mem_access_3 : Unknown (220ms)
[wp] Proved goals:    0 / 4
     Alt-Ergo:        0  (unknown: 4)

интересно, почему

1. количество голов отличается (4 против 9) в моей попытке по сравнению с руководством?
2. Альт-Эрго (и на самом деле, ни один из cvc3, gappa, simplify, verit, yices, z3) не был в состоянии отказаться от любого из этих 4 доказательств обязательств?

Я использую последнюю установку OPAM:

• frama-c: Натрий-20150201
• alt-ergo: 0.95.2 (из основного пакета репозитория ubuntu 14.04) alt-ergo)
• why3: 0.86.1

Пример доказательства обязательств, переданных alt-ergo от wp:

goal swap_assert_rte_mem_access:
  forall t : int farray.
  forall a_1,a : addr.
  linked(t) ->
  (region(a.base) <= 0) ->
  (region(a_1.base) <= 0) ->
  valid_rd(t, a, 1)

Answer 1

Вы сделали ошибку, когда скопировали спецификацию swap из руководства WP. (В следующей версии будет использоваться шрифт, позволяющий вставлять копии.) Между началом комментария C и текстом не должно быть пробела. @ в спецификациях ACSL; в противном случае комментарий интерпретируется как простой комментарий. Таким образом, вы эффективно пытаетесь доказать

void swap(int * a, int * b);

void swap(int * a, int * b) {
    int tmp = * a;
    *a = *b;
    *b = tmp;
    return ;
}

что, конечно, невозможно, потому что a а также b не может быть действительными указателями.

Правильная спецификация

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

При использовании Frama-C на небольших примерах вы, вероятно, должны использовать интерфейс GUI (frama-c-gui). Таким образом, вы увидите ваш исходный код после нормализации, какие RTE были добавлены и т. Д.