[C-safe-secure-studygroup] Choices in between Soundness and Completeness

[Fulvio Baccaglini]

During the meeting Aaron submitted another example for consideration, I
cannot remember its exact details, but it was along the lines of
function 'f1' in this example:

~~~~~~~~>
#include <stdio.h>

unsigned int f1 (void)
{
  unsigned int x;
  printf ("Enter an integer between 0 and 2 ");
  scanf ("%d", & x);
  return 1000 / x; // possible division by zero - external source
}

unsigned int f2 (void)
{
  // adopted binary code
  extern unsigned int g2 (unsigned int n);

  unsigned int x = g2 (4);
  return 1000 / x; // possible division by zero - lack of information
}

unsigned int g3 (unsigned int x)
{
  // this function is self-contained, implements a well defined and
  // constant mapping from parameter x to function result, and its
  // source code is fully available, however it is so complex that no
  // existing tool can figure out whether g3 (4) == 0

  // ...
}

unsigned int f3 (void)
{
  unsigned int x = g3 (4);
  return 1000 / x; // possible division by zero - complexity
}
<~~~~~~~~

I feel that 'f1' could also be in a different category of 'possible'
with respect to 'f2' and 'f3': for 'f1' an instance of 'program +
input' can be identified where the malfunction occurs, while for 'f2'
and 'f3' it is possible that there is no instance of 'program + input'
where a malfunction occurs.

Fulvio