Difference between revisions of "C generic Team1 (E-ACSL) Benchmark1"

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-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 benchmark 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. This allows to bypass the check and lead to a buffer overflow during string concatenation.

The final step reads data from a file and output its contents to the standard output stream.

Demonstration Traces

Formal Specification

The formal specification is given using ACSL

/*@ assert (a + b) <= max; */

where a, b and max are of integral types.

A FO-LTL Specification