Я пытаюсь проверить следующий фрагмент кода, используя frama-c
/*@ ensures \result != \null;
@ assigns \nothing;
@*/
extern int *new_value();
//@ assigns *p;
void f(int* p){
*p = 8;
}
//@ assigns \nothing;
int main(void){
int *p = new_value();
f(p);
}
Доказывающая сторона не может доказать, что main ничего не присваивает, что имеет смысл, поскольку main присваивает *p через функцию f. Однако как мне указать это в предложении \assigns, поскольку p является локальной переменной и к ней нельзя получить доступ в аннотации.
