Каково значение и назначение столбца "после" в EVA-плагине Frama-C

Question

В уроке по EVA я нашел этот скриншот: с объяснением:"Точное значение, которое вызвало это, показано в столбце c5: -1. Стандарт C рассматривает сдвиг влево отрицательного числа как неопределенное поведение. Поскольку -1 - единственно возможное значение в этом стеке вызовов, сокращение вызванный тревогой приводит к пост-состоянию, которое есть ".

Итак, я хочу спросить:

Каково значение и назначение столбца "после" в EVA-плагине Frama-C?

Есть ли какой-либо более подробный документ для понимания терминов "сокращение" и "пост-состояние", используемых в EVA?

Answer 1

Когда вы выбираете заявление s в графическом интерфейсе есть два состояния памяти, которые имеют отношение к s (также называемый предварительным состоянием), и тот, который после побочных эффектов s было сделано (также называется пост-состояние). Вот почему у вас есть две колонки в Values tab для каждого lval, который вас интересует. Понятие pre и post-state довольно стандартно при верификации программы и в основном восходит к Hoare Logic.

Термин "сокращение" относится к тому факту, что после подачи тревоги EVA будет пытаться удалить из своего абстрактного состояния элементы, которые соответствуют конкретным состояниям, которые определенно приведут к неопределенному поведению. Действительно, предполагается, что абстрактное состояние представляет собой чрезмерное приближение всех конкретных состояний, которые могут достичь утверждения, не вызвав заранее неопределенного поведения: если что-то не получалось раньше sнет смысла рассуждать о том, что может произойти при оценке s, В приведенном вами примере мы имеем конкретный случай, когда все возможные конкретные состояния приводят к ошибке. Следовательно, мы в конечном итоге с BOTTOM абстрактное состояние, представляющее пустой набор конкретных состояний, и анализ этой ветви заканчивается.