Difference between revisions of "C implicit Team1 (E-ACSL) Benchmark1"
(→Informal Description) |
(→Informal Description) |
||
| Line 15: | Line 15: | ||
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 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 | + | 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 ==== | ==== Demonstration Traces ==== | ||
Latest revision as of 10:15, 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 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.
