Difference between revisions of "C implicit Team1 (E-ACSL) Benchmark2"
From CRV
m (E-acsl moved page C implicit Team1 Benchmark2 to C implicit Team1 (E-ACSL) Benchmark2) |
(→Benchmark Data) |
||
Line 10: | Line 10: | ||
==== Informal Description ==== | ==== 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: | ||
+ | # A block of memory is allocated on a program's heap via a call to '''malloc'''. | ||
+ | # The first four bytes of the allocated block are initialized. | ||
+ | # 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. | ||
+ | # 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. | ||
==== Demonstration Traces ==== | ==== Demonstration Traces ==== | ||
Line 16: | Line 26: | ||
The formal property is given using the [http://frama-c.com/acsl.html ACSL] | The formal property is given using the [http://frama-c.com/acsl.html ACSL] | ||
+ | |||
+ | /*@ assert \initialized(p); */ | ||
+ | |||
+ | where '''p''' is of pointer type. | ||
==== A FO-LTL Specification ==== | ==== A FO-LTL Specification ==== |
Revision as of 17:13, 3 June 2016
Contents
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:
- A block of memory is allocated on a program's heap via a call to malloc.
- The first four bytes of the allocated block are initialized.
- 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.
- 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.
Demonstration Traces
Formal Specification
The formal property is given using the ACSL
/*@ assert \initialized(p); */
where p is of pointer type.