[C-safe-secure-studygroup] analyzer requirements for false positives

Martin Sebor msebor at gmail.com
Tue Jul 10 20:55:30 BST 2018


On our last call I agreed to put in writing my proposal to have
analyzers issue two kinds of diagnostics: one for true positives
and another for possible violations of undecidable rules that
cannot be ruled out to be false positives.  Below is the first
draft of this proposal.

The text makes two changes to TS 17961: a) it requires analyzers
to avoid false positives or negatives for Decidable rules, and
b) requires them to clearly differentiate between true positives
and possible false positives for Undecidable rules.

It stops short of requiring analyzers to provide a switch such
as a command line option to let users control which kind of
diagnostics to request.  I think that's best left to the QoI:
a quality implementation will make the distinction clear enough
to search for using tools like grep, and so let users do
the filtering afterwards. (It doesn't preclude the switch
either.)

The Recommended practice section outlines a non-normative
encouragement for analyzer implementers (i.e., it's not
a part of the conformance requirement).  It's widely used
in the C standard.

Martin

In section 2 Conformance, replace the paragraph:

   For each rule, the analyzer shall document whether its analysis
   is guaranteed to report all violations of that rule and shall
   document its accuracy with respect to avoiding false positives
   and false negatives.

withe the following text:

   The analyzer shall be both complete and sound in diagnosing
   violations of all Decidable rules (xref Completeness and
   Soundness, xref Decidability of Rules).
   For each Undecidable rule, the analyzer shall issue diagnostics
   for certain violations (true positives) that are distinct from
   those for possible but not certain violations (those that may
   be false positives).

   Recommended practice:
   The distinction between the diagnostics of certain and possible
   violations should make it clear when the former is a true positive
   and latter may be a false positive, and the degree of likelihood
   that the latter is a true positive.

   Example:
   Function f below inevitably violates rule [accfree] and so
   a diagnostic is required.

   void f (int n)
   {
     void *p = malloc (n);
     if (p)
       free (p);
     // ...
     memset (p, 0, n);               // diagnostic required
   }

   warning: memset accessing freed memory on line 7 [accfree]

   Function g below violates rule [accfree] only if the value
   of the first byte of the storage allocated by malloc is
   zero.  Whether that condition is satisfied is undecidable.
   An analyzer is required to diagnose the possible violation
   by a distinct message.

   void g (int n)
   {
     void *p = malloc (n);
     if (rand () % 10)               // undecidable
       free (p);
     // ...
     memset (p, 0, n);               // diagnostic required
   }

   warning: memset may access freed memory on line 7 with 90%
   probability [accfree]




More information about the C-safe-secure-studygroup mailing list