Как доказать это присваивает пункт, часть 2?

Question

Я не могу придумать ни одной идеи, чтобы получить утверждение о присвоении foo. Я пробовал assigns var;, поскольку foo() косвенно изменяет глобальную переменную var, но она не работает. Есть ли способ получить предложение assigns для локальной переменной p или возвращение местоположения из a()? Вот код:

int var;
//@ assigns \nothing;
int *a(){
    return &var;
}
//@ assigns *p;
void b(int* p){
  *p = 1;
}
//@ assigns \nothing;
void foo(){
   int *p = a();
   b(p);
}
//@ assigns var;
void main(){
    var = 0;
    foo();
    return;
}

команда frama-c:

frama-c -wp test.c

[kernel] Parsing test.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 10 goals scheduled
[wp] [Alt-Ergo] Goal typed_foo_assign_normal_part3 : Unknown (103ms)
[wp] [Alt-Ergo] Goal typed_foo_assign_exit_part3 : Unknown (Qed:4ms) (102ms)
[wp] Proved goals:    8 / 10
  Qed:             8 
  Alt-Ergo:        0  (unknown: 2)

Answer 1

Как вы уже догадались, foo действительно присваивает что-то, а assigns \nothing является недопустимым предложением для этой функции. Правильный пункт действительно assigns var. В предложении assigns вы должны перечислить все глобальные переменные, которые были изменены, а также все переменные, которые являются локальными для вызывающей стороны и на которые можно ссылаться посредством формальности.

Теперь, почему не проверяется вариант с assigns var? Ну, как написано в foo, WP не может угадать, куда указывает p, так как он не может знать, что на самом деле он равен &a. Вы должны добавить эту информацию в спецификацию функции a. С этой модификацией доказательство немедленно.

Полный код:

int var;

/*@ assigns \nothing;
    ensures \result == &var; */
int *a(){
    return &var;
}

//@ assigns *p;
void b(int* p){
  *p = 1;
}

//@ assigns var;
void foo(){
   int *p = a();
   b(p);
}

//@ assigns var;
void main(){
    var = 0;
    foo();
    return;
}