Decision Coverage Loves Ada Enumerations

A key feature of Ada is its strong typing, and one area that is a lot stronger than in many other imperative languages is enumerations. An enumeration type is simply a collection of distinct symbols. A variable of that type can have any one of those symbols as its value. Here we're looking at how it's easier to monitor decision coverage for Ada than C, in part because of the handling of enumerations.

The Ada View

If your code uses a case-statement to select different blocks according to the values of an enumeration, you will need to obtain decision coverage for the decision. In the case of Ada, we know that the compiler (in this case, GNAT) will typically not allow the code to compile unless every case is accounted for:

  type horizontal_alignment_t is ( left, center, right, justified );
  halign: horizontal_alignment_t;
  ragged: Boolean := False;
 ...
  halign := justified;
 ...
  case halign is
  when left|center|right => ragged := True;
  -- compiler error: missing case for "justified"
  end case;

When we monitor this for decision coverage, we can be confident that exactly one of those branches should be entered (we report an error if you go from before the case to after the case without hitting one of the branches in between).

The C View

When we do the same thing in C, we find that it's legal to enter a switch-statement with a value that is not covered by any case, because the enumeration type in C is treated as a numeric type.

  enum horizontal_alignment_t { HALIGN_LEFT, HALIGN_CENTER, 
           HALIGN_RIGHT, HALIGN_JUSTIFIED };
  enum horizontal_alignment_t halign;
  unsigned char ragged = 0;
 ...
  do_case( unsigned int halign )
 ...
    switch( halign )
    {
    case HALIGN_LEFT:
    case HALIGN_CENTER:
    case HALIGN_RIGHT:
      ragged = 1;
      break;
    case HALIGN_JUSTIFIED:
      break;
    }
 ...
  }

In this code, the compiler gives no warning that the switch might be entered with a value that is outside of the established cases (static analysis tools can help to find this case, though). This is why, when we monitor C code, we try to check whether the "default" case would have been entered instead by adding such a case into the code that we monitor.

The Upshot

In Ada, the strictness of the enumeration type makes it easier to determine what to monitor for decision coverage, it simplifies the analysis, and it reduces the testing effort needed by your verification team. Conversely, for C, we find that rules for what to monitor are more complex and our analysis needs to be similarly complex. A specific concern is the generation of out-of-range test data to exercise default cases, which may be buried deep in the call hierarchy for a C program but which could be caught much higher in the validation logic of an Ada program.