C implicit Team1 (E-ACSL) Benchmark1
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 to unallocated locations). Deallocate heap memory. Repeat.
Demonstration Traces
Formal Specification
The formal specification is given using ACSL
/*@ assert \valid(p); */
where p is of pointer type.
