Может ли ACSL обозначать, что назначение должно быть скрыто?

Question

Эта функция проверяет функцию, которая возвращает непрерывно растущее значение, пока не произойдет переполнение. Это как 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;
}

Я попытался сделать это с переменными-призраками, и заметил, что функция, которая назначает переменную-призрака, не может быть assigns \nothing, Я думал, что переменные-призраки полностью независимы от реализации программы. Есть ли для этого особая причина?

Answer 1

Я полагаю, ваш static переменная должна называться milliseconds и не microseconds как сейчас.

Ваше предположение о переменных-призраках действительно неверно: код-призрак не должен мешать реальному коду и наоборот (обратите внимание, что на данный момент Frama-C не применяет его). Следовательно, если вы объявите milliseconds как ghostлюбое присвоение ему должно происходить внутри ghost код. Но с точки зрения спецификации, такие присвоения, тем не менее, являются побочными эффектами, которые должны быть упомянуты в assigns пункт.