Difference between revisions of "C implicit Team1 (E-ACSL) Benchmark3"
m (E-acsl moved page C implicit Team1 Benchmark3 to C implicit Team1 (E-ACSL) Benchmark3) |
(→Benchmark Data) |
||
| Line 10: | Line 10: | ||
==== 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 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. | ||
==== Demonstration Traces ==== | ==== Demonstration Traces ==== | ||
| Line 16: | Line 20: | ||
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] | ||
| + | |||
| + | /*@ assert \base_addr(p) == \base_addr(p + i); */ | ||
| + | |||
| + | where '''p''' is of pointer type and '''i''' is of integral type. | ||
==== A FO-LTL Specification ==== | ==== A FO-LTL Specification ==== | ||
Revision as of 17:15, 3 June 2016
Contents
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 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 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.
Demonstration Traces
Formal Specification
The formal property is given using the ACSL
/*@ assert \base_addr(p) == \base_addr(p + i); */
where p is of pointer type and i is of integral type.
