Difference between revisions of "C implicit Team1 (E-ACSL) Benchmark1"
(→Formal Specification) |
(→Informal Description) |
||
| Line 13: | Line 13: | ||
This benchmark relates to a property of memory safety and more specifically to a violation involving writing past the bounds of a heap-allocated memory block. | This benchmark relates to a property of memory safety and more specifically to a violation involving writing past the bounds of a heap-allocated memory block. | ||
| − | The main aim of this benchmark to evaluate performance of | + | The main aim of this benchmark to evaluate performance of an online verification tool in the presence of intensive memory allocation for a memory safety property involving the legality of writes to heap-allocated memory locations. |
The scenario explored by this benchmark is as follows. Allocate a number of memory blocks on a program's heap and write to every byte of the allocated memory (potentially writing past the bounds of allocated memory). Deallocate heap memory. Repeat. | The scenario explored by this benchmark is as follows. Allocate a number of memory blocks on a program's heap and write to every byte of the allocated memory (potentially writing past the bounds of allocated memory). Deallocate heap memory. Repeat. | ||
Revision as of 10:14, 5 June 2016
Contents
Benchmark Data
This benchmark is located in crv.liflab.ca@/home/e-acsl/crv16_benchmarks/c-implicit-track/heap-performance
The Trace Part
E-ACSL has no notion of trace
The Property Part
Informal Description
This benchmark relates to a property of memory safety and more specifically to a violation involving writing past the bounds of a heap-allocated memory block.
The main aim of this benchmark to evaluate performance of an online verification tool in the presence of intensive memory allocation for a memory safety property involving the legality of writes to heap-allocated memory locations.
The scenario explored by this benchmark is as follows. Allocate a number of memory blocks on a program's heap and write to every byte of the allocated memory (potentially writing past the bounds of allocated memory). Deallocate heap memory. Repeat.
Demonstration Traces
Formal Specification
The formal specification is given using ACSL
/*@ assert \valid(p); */
where p is of pointer type.
