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는 \result을 계산 *p에서 읽을 필요가 없다 (그리고 p 물론 NULL 경우가 더 잘 피해야한다). 측면 참고로, 질문도 이

그럼에도 불구하고 C로 \valid(p)을 의미하지는 않습니다 p!=\null 같이 p_not_null 행동의 assigns 조항에 대해 제기 될 수 있었다, 행동없이 계약과 함께보다 약간 덜 정확 0으로 설정하면 p이 NULL 일 때 상수 값이 반환되고 p이 null이 아닌 경우 *p의 내용 만 사용됩니다 (동작이없는 assigns 절은 예 : *p+(int)p 또는 (int)p을 반환 할 수 있음).