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

From CRV
Jump to: navigation, search
(Created page with "== 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 not...")
 
(Informal Description)
 
(4 intermediate revisions by the same user not shown)
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 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 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 to unallocated locations). Deallocate heap memory. Repeat.
  
 
==== Demonstration Traces ====
 
==== Demonstration Traces ====
Line 21: Line 21:
 
==== Formal Specification ====
 
==== Formal Specification ====
  
The formal property is given using the [http://frama-c.com/acsl.html ACSL]
+
The formal specification is given using [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 ====

Latest revision as of 10:15, 5 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 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