Repository navigation
CBMC does not recognize pointer initializations outside functions #8593
Description
We observed that CBMC does not recognize pointers that are initialized within a C file but outside a function.
It marks these pointers as INVALID-X where X is an integer.
For example, in the code below
#define PACKETBUF_SIZE 128
static uint32_t packetbuf_aligned[(PACKETBUF_SIZE + 3) / 4];
// Initializing a pointer outside a function causes CBMC to misbehave
uint8_t *packetbuf = (uint8_t *)packetbuf_aligned;
void harness() {
uint16_t channelId;
uint8_t *data = packetbuf;
memcpy(&channelId, data, 2);
}packetbuf is initialized to point to the statically allocated packetbuf_aligned array.
However, when data is defined to point to packetbuf, CBMC sees the packetbuf pointer as invalid and subsequently, makes data invalid.
As a result, an error is reported in the memcpy line where data is accessed.
We tested this with CBMC v6.3.1
Activity
AmPaschal commentedon Apr 2, 2025
Hi
Please, I am just following up if there is an update on this issue?
Fix static lifetime pointer initialization dependency ordering
Fix static lifetime pointer initialization dependency ordering
Fix static lifetime pointer initialization dependency ordering
Fix static lifetime pointer initialization dependency ordering
Fix static lifetime pointer initialization dependency ordering
Fix static lifetime pointer initialization dependency ordering