Why is Frama-C warning about 'accessing uninitialized left-value' in basic example?

Question

Frama-C considers the code below correct (no warning, no error) :

#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);
}

But, if I change slightly the code by splitting the 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);
}

I get the message :

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

And the question is, why is Frama-C considering that p might access an uninitialized left-value? What am I missing?

I invoke Frama-C using the command:

 frama-c-gui -val test.c

Answer 1

Abstract interpreters limit the complexity of their analysis by performing abstractions ("joins") when two control-flow paths meet. This is what happens on your second example: after the end of the first if, the abstractions for the two branches are joined. In the resulting abstraction, the relationship between p and the initialization of *p is lost.

In Frama-C/Eva, it is possible not to perform joins when multiple control-flow paths meet, instead propagating sets of states in parallel. The maximum cardinality of those sets is governed by the parameter -slevel. Here -slevel 2 is sufficient to prove your second example.