Как доказать это условие присваивания?

Question

/*@
  @ requires \valid(p);
  @ assigns \nothing;
*/
void foo(int *p)
{
    int *pb;
    pb = p;
    *pb = 1;
    return;
}

void main(){
    int a = 0;
    foo(&a);
    return;
}

Как я понимаю, предложение assigns для контракта функции работает только с входными переменными функции. Таким образом, я делаю предложение assigns ни к чему, но затем получаю желтый статус с -wp.

frama-c -wp test1.c
[kernel] Parsing test1.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
[wp] [Alt-Ergo] Goal typed_foo_assign_part2 : Unknown (Qed:4ms) (51ms)
[wp] Proved goals:    2 / 3
Qed:             2 
Alt-Ergo:        0  (unknown: 1)

Как доказать foo (), если присваивает \ ничего не работает?

Answer 1

Я не уверен, что вы подразумеваете под "assigns [...] работает только с входной переменной функции". Предполагается, что предложение assigns дает расширенный набор всех областей памяти, которые выделены как до, так и после состояний контракта (существуют специальные условия для обработки динамического (де) выделения) и которые могут быть изменены во время выполнение функции (или выписка по договору выписки).

В частности, ваша функция foo не может иметь предложение assigns \nothing;, поскольку оно изменяет значение местоположения, на которое указывает p: у вас должно быть что-то вроде assigns *p;, что легко подтверждается frama-c -wp.