为什么在基本示例中frama-c警告“访问未初始化的左值”?

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