ACSL是否可以表示任务应该被隐藏？

Question

此函数模拟一个函数，该函数返回一个不断上升的值，直到发生溢出。它类似于Arduino中的millis()函数。

为了证明实现，我需要增加(因此，赋值)静态变量，以保持调用之间的状态。但是，调用mock_millis()的函数仍然能够实现assign \nothing。

有没有办法让WP忽略赋值条款？

static int64_t milliseconds = 0;

/*@ assigns milliseconds;

    behavior normal:
      assumes milliseconds < INT64_MAX;
      ensures \result == \old(milliseconds) + 1;
      ensures milliseconds == \old(milliseconds) + 1;
    behavior overflow:
      assumes milliseconds == INT64_MAX;
      ensures \result == 0;
      ensures milliseconds == 0;

    complete behaviors normal, overflow;
    disjoint behaviors normal, overflow;
*/
int64_t mock_millis() {
    if (milliseconds < INT64_MAX) {
        milliseconds++;
    } else {
        milliseconds = 0;
    }
    return milliseconds;
}

我试着用ghost变量来做这件事，并且注意到分配ghost变量的函数不能是assigns \nothing。我认为幽灵变量完全独立于程序的实现。有什么特别的原因吗？

Answer 1

我假设您的static变量应该被称为milliseconds，而不是现在的microseconds。

关于鬼变量的假设确实是错误的:鬼代码不应该干扰真正的代码，反之亦然(请注意，这一点不是由Frama强制执行的)。因此，如果您将milliseconds声明为ghost，那么对它的任何分配都应该发生在ghost代码中。但从规范的角度来看，这种分配仍然是副作用，需要在assigns条款中提及。