Блог

Есть ли способ обеспечить выполнение предположений, сделанных моделью памяти WP?

Рассмотрим следующие две функции, которые необходимо проверить с помощью Frama-C:

 /*@ requires valid(a) amp;amp; valid(b);
  @ ensures A: *a == 1;
  @ ensures B: *b == 2;
  @ assigns *a, *b;
  @*/
void assign_many(int *a, int *b)
{
  *a = 1;
  *b = 2;
}


int main() {
  int a = 42;
  assign_many(amp;a, amp;a);
  //@ assert a == 1;
  //@ assert a == 2;
  return 0;
}
  

Функция assign_many не может выполнить проверку в общем случае, поскольку два аргумента могут иметь псевдонимы (как показано в main ). Однако, если вы выберете Hoare ref модель памяти, эта функция проверяет, поскольку она предполагает разделение. Но я все еще могу проверить main , даже используя Typed модель памяти. С помощью опции командной строки -wp-warn-memory-model появляется сообщение, предупреждающее вас о том, какие допущения требуются для модели памяти. Возможно ли применить эти допущения, например, добавить их в качестве предварительных условий к assign_many ?

Я боюсь, что это невозможно напрямую (т. Е. Без копирования-вставки сгенерированной спецификации в новый файл C и повторного анализа всего исходного кода: текст предупреждения, похоже, заботится о том, чтобы выразить это как действительный контракт ACSL).

Немного покопавшись в API плагина Wp, можно увидеть, что гипотезы разделения рассматриваются в MemoryContext модуле плагина, который использует свой собственный пользовательский тип данных для их представления (в отличие от предиката ACSL из стандартного AST, определенного в ядре).

Можно написать некоторый код, который будет принимать предложения, сгенерированные данной моделью для данной функции, и генерировать набор предикатов ACSL, которые затем могут быть добавлены в качестве requires предложений для этой функции (т. е. программный эквивалент копирования и вставки, упомянутого выше), но это подразумевает определенное знание Frama-C API.