David

Using constrained types in C

When writing critical software, one of the advantages cited for using Ada rather than C is that Ada lets you define constrained types, like this:

type Percentage is Integer range 0 .. 100;

The Ada compiler inserts a run-time check whenever the program assigns a value to a variable of type Percentage that might be less than 0 or greater than 100, and in other similar situations such as when passing parameters.

C doesn’t support constrained types. Fortunately, there are ways round this. One is to use eCv’s constrained typedef syntax:

typedef int invariant(0 <= value; value <= 100) Percentage;

We met the invariant macro in an earlier post – it expands to nothing when your program is compiled, making the constraint invisible to a regular C or C++ compiler. So you won’t get run-time checking of the constraint. However, eCv will try to prove that the constraint is obeyed. For example, the following function:

void foo(bool b, Percentage *score) {
if (b) { *score = 200; }
  else { *score += 1; }
}

gives rise to these verification errors:

c:\escher\ecvtest\ecvtest7.c (13,23): Error! Refuted: Type constraint satisfied
    (defined at c:\escher\ecvtest\ecvtest7.c (9,39)),
     cannot prove: 200 <= 100.

c:\escher\ecvtest\ecvtest7.c (14,16): Warning! Unable to prove:
    Type constraint for ‘Percentage’ satisfied,
    suggestion available (see c:\escher\ecvtest\ecvtest7_unproven.htm#1),
    cannot prove: (1 + *score) <= 100.

and if you follow the suggestion link in the second message, it suggests a suitable function precondition.

If you want run-time checking of constraints, then the best way is to use a C++ class:

class Percentage {
  int value;

public:
  Percentage(int arg) : value(arg) {
    if (arg < 0 || arg > 100) { ... }
  }

  Percentage& operator = (int arg) {
    if (arg < 0 || arg > 100) { ... }
    value = arg;
  }
  operator int() const { return value; }
}

I’ve made Percentage type-compatible with int, but ensured that any attempt to assign or convert an int to a Percentage is subject to a range check (replace “...” with whatever you want to do when a range check fails).

If your C++ compiler supports templates, then you can define a class template with selectable minimum and maximum values. This makes it trivial to introduce new types like Percentage with a simple typedef.

ARTICLES   List of Articles     TOPTOP