Почему Frama-C предупреждает о «доступе к неинициализированному левому значению» в базовом примере?

Question

Frama-C считает приведенный ниже код правильным (без предупреждения, без ошибок):

#include <stdio.h>
#include <stdlib.h>

int *p;

int main() {

        p = malloc(sizeof(int));
        if (p!=NULL) {
                *p = 9;
                printf("*p = %d\n",(int) (*p));
        }
        return(1);
}

Но, если я немного изменю код, разделив if-then-else:

#include <stdio.h>
#include <stdlib.h>

int *p;

int main() {

        p = malloc(sizeof(int));
        if (p!=NULL) {
                *p = 9;
        }
        if (p!=NULL) {
                printf("*p = %d\n",(int) (*p));
        }
        return(1);
}

Я получаю сообщение:

test6.c:13:[value] warning: accessing uninitialized left-value. assert \initialized(p);

И вопрос в том, почему Frama-C считает, что p может получить доступ к неинициализированному левому значению? Чего мне не хватает?

Я вызываю Frama-C с помощью команды:

 frama-c-gui -val test.c

Answer 1

Абстрактные интерпретаторы ограничивают сложность их анализа, выполняя абстракции («соединения»), когда встречаются два пути потока управления. Вот что происходит в вашем втором примере: после окончания первого if объединяются абстракции для двух ветвей. В полученной абстракции связь между p и инициализацией *p потеряна.

В Frama-C / Eva возможно , а не , чтобы выполнять соединения, когда встречаются несколько путей потока управления, вместо этого распространяя наборы состояний параллельно. Максимальная мощность этих наборов определяется параметром -slevel. Здесь -slevel 2 достаточно, чтобы доказать ваш второй пример.