C implicit Team1 (E-ACSL) Benchmark1

From CRV
Jump to: navigation, search

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.

A FO-LTL Specification