C implicit Team1 (E-ACSL) Benchmark2

Benchmark Data

This benchmark is located in crv.liflab.ca@/home/e-acsl/crv16_benchmarks/c-implicit-track/realloc-init

The Trace Part

E-ACSL has no notion of trace

The Property Part

Informal Description

The benchmark relates to memory safety and more specifically to reading from a heap-allocated memory block that has not been fully initialised by a previous write.

This benchmark has been derived from the use of the realloc memory allocation function used to increase or decrease the size of a given heap-allocated memory block.

This benchmark explores the following scenario:

1. A block of memory is allocated on a program's heap via a call to malloc.
2. The first four bytes of the allocated block are initialized.
3. The same memory block is then partially de-allocated and then re-allocated again (via realloc). This renders the last byte of the block uninitialised.
4. The same memory block is then used in a print statement that potentially reads from an properly allocated location that has not been fully initialized.

Formal Specification

The formal specification is given using ACSL

/*@ assert \initialized(p); */

where p is of pointer type.