cwe126.0.md

title: Frama-C Analysis Report
author:
date: now

\let\underscore_ \renewcommand{_}{\discretionary{\underscore}{}{\underscore}}

Introduction {#intro}

This is a test from the Juliet test suite showing an example of buffer overflow (CWE126). The good functions should not trigger any alarm, while the bad ones have indeed an error.

Context of the analysis {#context}

Input files {#c-input}

The C source files (not including the headers .h files) that have been considered during the analysis are the following:

• tests/md/*.c

Configuration {#options}

Eva Domains {#domains}

Only the base domain (cvalue) has been used for the analysis

Stubbed Functions {#stubs}

No stubs have been used for this analysis

Coverage {#coverage}

There are 6 function definitions that are not stubbed. They represent 50 statements, of which 50 are potentially reachable through Eva, resulting in a statement coverage of 100.0% with respect to the entire application.

There were potentially 6 functions syntactically reachable from main. These functions contain 50 statements, of which 50 are potentially reachable according to Eva, resulting in a statement coverage of 100.0% with respect to the perimeter set by this entry point.

Warnings {#warnings}

The table below lists the warning that have been emitted by the analyzer. They might put additional assumptions on the relevance of the analysis results and must be reviewed carefully

Note that this does not take into account emitted alarms: they are reported in the next section

Table: Warning reported by Frama-C

Location	Description
tests/md/cwe126.c:28	out of bounds read. assert \valid_read(data + i); (emitted by eva)

Warning 0 (tests/md/cwe126.c:28) {#warn-0}

Message:

[eva] out of bounds read. assert \valid_read(data + i);

Results of the analysis {#alarms}

The table below lists the alarm that have been emitted during the analysis. Any execution starting from main in a context matching the one used for the analysis will be immune from any other undefined behavior. More information on each individual alarm is given in the remainder of this section

Table: Alarm emitted by the analysis

No	Kind	Emitter	Function	Location
0	mem_access	Eva	CWE126_Buffer_Overread__malloc_char_loop_64b_badSink	tests/md/cwe126.c:28

Alarm 0 at tests/md/cwe126.c:28 {#Alarm-0}

The following ACSL assertion must hold to avoid invalid pointer dereferencing (undefined behavior).

assert mem_access: \valid_read(data + i);

This alarm is real: Eva correctly identified the issue and did not report any spurious alarm anywhere else.