I have following code snippet.
#include<stdio.h>
#include<stdlib.h>
int main()
{
char *c = malloc(1);
printf("%p\n", c);
c = c + 20;
printf("%p\n", c);
printf("%d\n", *c);
free(c - 20);
return 0;
}
In this code, I'm allocating 1 byte of memory to a pointer. Then I'm accessing a memory location which 20 unit after allocated memory. When I dereference that pointer, I'm expected to get a Memory Access Violation error or Segmentation Fault or something like that. I'm not getting any such error.
Let us assume this is a case of undefined behaviour. So I tried to verify this program using CBMC, a well known model checker using following command.
cbmc test01.c --pointer-check
CBMC is reporting that program is safe. Is it an issue with CBMC or am I missing something?
As you said in your question, the statement
printf("%d\n", *c);exposes undefined behaviour. Being undefined, any expectation you might have against it is false. This includes getting a specific error or any error at all.The C runtime library doesn't check the way your program accesses the memory. If it would do it, the program would run much, much slower. Regarding the heap, the C runtime library does some basic checks; for example, it puts a certain value at address
0during the program startup and checks if the value is still there when the program ends. If the value changed then a null pointer was de-referenced for writing and it can warn you about this.After
c = c + 20;,cmost probably points to a block of memory that belongs to your program. It can be a free area on the heap, it can be inside the data structures used by the heap manager to handle the heap, but there are big chances that it is still on the same memory page.If you have (bad) luck and
c + 20lands outside the memory page that storescthen an exceptional situation happens that is handled by the operating system. It terminates the program and displays an error message similar with the one you listed in the question (the idea is the same, the words and the presentation differ on each OS).Update
Allocating memory is not some kind of magic. The program starts with a block of memory (called "heap") that is assigned by the OS to the program for this purpose.
The C runtime library contains code that manages the heap. This code uses a small part of this memory for its bookkeeping. A common implementation uses double-linked lists, the payload of each node from the list being a block of memory "allocated" by the program using the functions declared in
<memory.h>(malloc(),calloc()etc). When a call tomalloc()happens, this code runs, creates a new node in the list and returns the address of the node's payload (an address inside the heap).The program uses this pointer as it wants. Your program is free to write at
c-1, for example. In fact, insidemalloc()it actually wrote information there. Aftermalloc()returnsc, your code can also write atc-1. From theOSpoint of view, there is no difference between these two write operations. And becauseCis not a managed or interpreted language, there is no code included in your program that watches what the code you wrote does or hold its hand to not write in the wrong place.If you write at
c-1there is a big chance that you corrupt the data structures used by the heap manager. Nothing wrong happens immediately. No error message is displayed and your program continues to run apparently normal. But on the next call to a function that handles the heap (be it a memory allocation or a release) the program will start wreaking havoc. The heap data structures being corrupt anything could happen.Regarding CBMC, I don't know how it works. Maybe it cannot detect such situations. Or maybe it reports your program as being safe because it doesn't write at
cafter it was incremented.