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

From CRV
Jump to: navigation, search
(Formal Specification)
(Informal Description)
 
Line 11: Line 11:
 
==== Informal Description ====
 
==== Informal Description ====
  
The property explored by this benchmark relates to memory safety and more specifically to a spatial error on a program's stack where a pointer '''P''' to an allocated memory block '''A''' is used to read from a properly allocated memory location which address does not belong to '''A'''.
+
The property explored by this benchmark relates to memory safety and more specifically to a spatial error on a program's stack where pointer '''P''' to an allocated memory block '''A''' is used to read from a properly allocated memory location which address does not belong to '''A'''.
  
The scenario explored by this benchmark is as follows. Two character arrays are allocated on a program's stack. The arrays are filled with data and the difference between their start addresses is computed. This difference is then used to print the contents of the second buffer using a pointer to the first buffer.
+
The scenario explored by this benchmark is as follows. Two character arrays are allocated on a program's stack. The arrays are filled with data and the difference between their start addresses is computed. This difference is then used to print the contents of the second array using a pointer to the first array.
  
 
==== Demonstration Traces ====
 
==== Demonstration Traces ====

Latest revision as of 10:18, 5 June 2016

Benchmark Data

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

The Trace Part

E-ACSL has no notion of trace

The Property Part

Informal Description

The property explored by this benchmark relates to memory safety and more specifically to a spatial error on a program's stack where pointer P to an allocated memory block A is used to read from a properly allocated memory location which address does not belong to A.

The scenario explored by this benchmark is as follows. Two character arrays are allocated on a program's stack. The arrays are filled with data and the difference between their start addresses is computed. This difference is then used to print the contents of the second array using a pointer to the first array.

Demonstration Traces

Formal Specification

The formal specification is given using ACSL

/*@ assert \base_addr(p) == \base_addr(p + i); */

where p is of pointer type and i is of integral type.

A FO-LTL Specification