Почему плагин Eva из Frama-c возвращает неизвестное, когда фактически обнаружил контрпример к утверждению

Question

Я пытаюсь вставить утверждение внутри функции.Вот что я сделал:

void foo(int a) {
    //@ assert a == 1;
}

void main() {
   foo(1);
   foo(2);
}

Я ожидаю получить недопустимый результат, но Frama-C возвращает неизвестный результат, в то время как может предоставить контрпример с стеком вызовов.

Вотснимок экрана, когда я запускаю свой пример с Frama-C:

Answer 1

Ева указывает, что статус неизвестен, поскольку он обнаружил стек вызовов, где утверждение было действительным, а другое - недействительным.Однако, поскольку плагин выполняет чрезмерные приближения (ну, не здесь, поскольку ваша программа тривиальна, но в общем случае будет), он не может быть уверен, что оба могут произойти в конкретном исполнении: одинветви (или утверждение, или подтверждение) может быть невозможно достичь в конкретном мире, из-за условий, недоступных абстракциям, которые использует Ева.Следовательно, единственная надежная возможность, которая охватывает все возможности, - это поставить здесь статус Unknown.

Вы также можете увидеть, что такая же проблема возникает, если вы закомментируете вызов foo(1).Затем Ева сообщит, что утверждение недействительно, но только , при условии, что оно действительно может быть достигнуто .

Наконец, аннотации такого типа действительно те, которые вы обычно хотите исследовать в первую очередь (в отличие от аннотаций с «простым» неизвестным состоянием) и в более новых версиях Frama-C (начиная с версии 17.0), у вас есть дополнительная панель Red Alarms, в которой перечислены свойства, которые недопустимы по крайней мере для одного стека вызовов.