Difference between revisions of "C generic Team1 (E-ACSL) Benchmark1"
(→Benchmark Data) |
(→Benchmark Data) |
||
| Line 12: | Line 12: | ||
==== Informal Description ==== | ==== Informal Description ==== | ||
| − | |||
| − | |||
The benchmark provides a simple implementation of a utility that prints the contents of a file given by two C strings that store the directory the file is located in and the base name of that file. The lengths of the strings are given as separate arguments. | The benchmark provides a simple implementation of a utility that prints the contents of a file given by two C strings that store the directory the file is located in and the base name of that file. The lengths of the strings are given as separate arguments. | ||
Revision as of 10:02, 5 June 2016
Contents
Benchmark Data
This benchmark is located in crv.liflab.ca@/home/e-acsl/crv16_benchmarks/c-generic-track/integer-overflow
The Trace Part
E-ACSL has no notion of trace
The Property Part
Given integers A and B check if the sum of these integers is less than some integer C. This check should take into account the fact that expression (A + B) can overflow.
Informal Description
The benchmark provides a simple implementation of a utility that prints the contents of a file given by two C strings that store the directory the file is located in and the base name of that file. The lengths of the strings are given as separate arguments.
The scenario explored by this example is as follows. The strings representing a directory and a file name are concatenated in a fixed-size buffer. The concatenation is guarded by a conditional statement that adds the lengths of the strings and immediately returns if the sum of of the lengths is greater than the size of the buffer. The aim of the guard is to prevent writing past the bounds of the fixed-size buffer.
The design of the guard is flawed: large enough values of string lengths may cause the addition to overflow and wrap around to a low number allowing to bypass the check and lead to buffer overflow during the concatenation.
The final step reads data from a file (via fopen) and output its contents to the standard output stream via putchar.
Demonstration Traces
Formal Specification
The formal property is given using the ACSL
/*@ assert (a + b) <= max; */
where a, b and max of of integer types
