1

此函数模拟一个函数，该函数返回一个持续上升的值，直到发生溢出。这就像millis()Arduino 中的函数。

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

有没有办法让 WP 忽略 assigns 子句？

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. 我认为幽灵变量完全独立于程序实现。这有什么特殊原因吗？

4

1 回答 1

3

我假设您的static变量是要被调用的milliseconds，而不是microseconds现在这样。

您对幽灵变量的假设确实是错误的：幽灵代码不应该干扰真实代码，反之亦然（请注意，此时 Frama-C 并未强制执行）。因此，如果您声明milliseconds为ghost，则对它的任何分配都应该发生在ghost代码中。assigns但是从规范的角度来看，这样的赋值仍然是需要在条款中提及的副作用。

于 2018-11-19T15:38:30.660 回答