Difference between revisions of "C implicit Team1 (E-ACSL) Benchmark1"

From CRV
Jump to: navigation, search
(Benchmark Data)
Line 23: Line 23:
 
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]
  
Let '''p''' be a term of a pointer type, then:
+
/*@ assert \valid(p); */
  
/*@ assert \valid(p); */
+
where '''p''' is of pointer type.
  
 
==== A FO-LTL Specification ====
 
==== A FO-LTL Specification ====

Revision as of 17:17, 3 June 2016

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 a dynamic 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 property is given using the ACSL

/*@ assert \valid(p); */

where p is of pointer type.

A FO-LTL Specification