frama-c - 在 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在正确的部分使用吗？\frompNULL

Answer 1

是的你可以。的右侧部分from指示哪些位置可能对 的值有贡献\result，但f不需要从中读取*p来计算（当然，如果是的\result话，最好避免使用它）。作为旁注，问题也可能针对行为条款提出，正如C中没有暗示的那样。pNULLassignsp_not_nullp!=\null\valid(p)

然而，没有行为的合同比有行为的合同稍微不那么精确，它规定当p是NULL一个常量值时返回，当p不为空时，只使用的内容*p（assigns没有行为的条款允许返回例如*p+(int)p，或甚至(int)p）。