Выполните предположения, сделанные моделью памяти WP во Frama-C

Question

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

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

/*@ requires \valid(a) && \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(&a, &a);
  //@ assert a == 1;
  //@ assert a == 2;
  return 0;
}

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

Answer 1

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

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

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