Использовать возможно неверный указатель в зависимостях ACSL

Question

Мне нужно написать спецификацию ACSL для зависимостей функции, которая принимает указатель как входной, и использует его содержимое, когда указатель не равен NULL. Я думаю, что данная спецификация является правильным:

/*@ behavior p_null: 
     assumes p == \null; 
     assigns \result from \nothing; 
    behavior p_not_null: 
     assumes p != \null; 
     assigns \result from *p; 
*/ 
int f (int * p); 

, но я предпочел бы избежать поведения, но я не знаю, если это правильно (и эквивалент):

//@ assigns \result from p, *p; 
int f (int * p); 

Могу ли я использовать *p в правой части \from, даже если p может быть NULL?

Answer 1

Да, вы можете. правая часть from указывает, какие места может способствовать стоимости \result, но f не нужно читать от *p вычислить \result (и она должна лучше избегать его, если p это NULL конечно). Как примечание стороны, вопрос мог бы также был поднят для предложения о p_not_null поведения assigns как p!=\null делает не означает \valid(p) в С.

Тем не менее, контракт без поведения немного менее точен, чем тот, с поведения, в котором говорится, что, когда p является NULL постоянное значение возвращается, и когда p не равно нулю, только содержание *p используется (оговорка assigns без поведения позволяет возвращать например *p+(int)p, или даже (int)p).