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

From CRV
Jump to: navigation, search
(Informal Description)
 
(2 intermediate revisions by the same user not shown)
Line 10: Line 10:
  
 
==== Informal Description ====
 
==== Informal Description ====
 +
 +
The benchmark relates to memory safety and more specifically to reading from a heap-allocated memory block that has not been fully initialised by a previous write.
 +
 +
This benchmark explores the following scenario:
 +
# A block of memory is allocated on a program's heap via a call to '''malloc'''.
 +
# The first four bytes of the allocated block are initialized.
 +
# The same memory block is then partially de-allocated and then re-allocated again (via '''realloc'''). This renders the last byte of the block uninitialised.
 +
# The same memory block is then used in a print statement that potentially reads from a properly allocated location that has not been fully initialized.
  
 
==== Demonstration Traces ====
 
==== Demonstration Traces ====
Line 15: Line 23:
 
==== 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]
 +
 
 +
/*@ assert \initialized(p); */
 +
 
 +
where '''p''' is of pointer type.
  
 
==== A FO-LTL Specification ====
 
==== A FO-LTL Specification ====

Latest revision as of 10:17, 5 June 2016

Benchmark Data

This benchmark is located in crv.liflab.ca@/home/e-acsl/crv16_benchmarks/c-implicit-track/realloc-init

The Trace Part

E-ACSL has no notion of trace

The Property Part

Informal Description

The benchmark relates to memory safety and more specifically to reading from a heap-allocated memory block that has not been fully initialised by a previous write.

This benchmark explores the following scenario:

  1. A block of memory is allocated on a program's heap via a call to malloc.
  2. The first four bytes of the allocated block are initialized.
  3. The same memory block is then partially de-allocated and then re-allocated again (via realloc). This renders the last byte of the block uninitialised.
  4. The same memory block is then used in a print statement that potentially reads from a properly allocated location that has not been fully initialized.

Demonstration Traces

Formal Specification

The formal specification is given using ACSL

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

where p is of pointer type.

A FO-LTL Specification