Может ли ACSL обозначать, что назначение должно быть скрыто? - PullRequest
Новая
       28

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

0 голосов
/ 19 ноября 2018

Эта функция выполняет макет функции, которая возвращает непрерывно растущее значение, пока не произойдет переполнение.Это похоже на функцию 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.Я думал, что переменные-призраки полностью независимы от реализации программы.Есть ли для этого особая причина?

1 Ответ

0 голосов
/ 19 ноября 2018

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

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

...