 *modified "Mon Dec 14 10:00:20 2015" *by "Paul E. Black"

This directory has a program to extract all the warnings from the two
Frama-C result files and classify each one.  This is a single script
for all classes, instead of a script for each class, to insure that
each warning is assigned to exactly one class.

$ make

The script still misclassifies many warnings.  For instance, many
warnings that are labeled read or write buffer overflow are really
null pointer dereference warnings.  Since our goal is to check if
Frama-C satisfies the STAE V Ockham Criteria, not to classify
warnings, we improved the code until we were satisfied.


Some warnings are excluded from automatic processing.
EXCLUDE-A
    72 files with unintentional flaw: read after end of buffer -
constant string SRC_STR.  Here is the problem code (memmove in half):
        memcpy(structCharVoid.charFirst, SRC_STR, sizeof(structCharVoid));
SRC_STR is 20 bytes, but sizeof() yields 24 bytes.  Thus memcpy() or
memmove() reads after the end of the buffer holding the constant
string.
    Frama-C correctly warned about these.  We decided not to take the
time to change code to process these automatically.

EXCLUDE-B
    76 test cases, including a total of 112 files, are excluded
because they use RAND32.  Frama-C's model results in any execution
using RAND32 to be undefined, and Frama-C stops processing in some
instances.
    Since we can't easily determine what occurs in the control flow
before RAND32 is used, we decided to exclude these test cases
altogether.

EXCLUDE-C
    2101 warnings referred to signed integer overflow due to Frama-C's
interpretation of left bitwise shift (for more than 16 bits) as integer
overflow. Those warnings did not fit Ockham's definition of an integer
overflow site.

EXCLUDE-D
    152 warnings about invalid memory access by calloc() when memory
allocation fails.  I doubt that actual code really tries to clear
memory in these cases.  So we discount these as model artifacts.

EXCLUDE-E
    623 "overflow in conversion occurs" when a floating point value is
assigned to an integer, but the value may be larger than can be
represented by an integer.  This may be a side effect of a potential
divide-by-zero condition.
    605 "passing INT_MIN to standard function abs()" is not covered in
the SATE V Ockham Criteria.

EXCLUDE-F
    440 "invalid arguments to library function" warnings come from
lines like the following:
        SNPRINTF(data, 100, L"%s", source);
Additional comments in the warning include "Too many arguments for
format".  The source code has a conditional macro that defines
SNPRINTF as _snwprintf in a Windows environment or as snprintf.  L"%s"
is a wide character string.  The warning may be because snprintf()
takes a regular character (char *) string for the format, not a wide
character (wchar_t *) string.
