Difference between revisions of "C implicit Team1 (E-ACSL) Benchmark1"
m (E-acsl moved page C implicit Team0 Benchmark1 to C implicit Team1 (E-ACSL) Benchmark1) |
(→Informal Description) |
||
| (3 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 | + | 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 ==== | ||
| Line 21: | Line 21: | ||
==== Formal Specification ==== | ==== Formal Specification ==== | ||
| − | The formal | + | The formal specification is given using [http://frama-c.com/acsl.html ACSL] |
| − | + | /*@ 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
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.
