I.h: C based invariant checking

This implements the C based invariant checking code and is a replacement for `assert.h'. The first two macros are the normal user interface; the remainder are used for configuring the behaviour on failure, etc.

Macro: void I (bool exprn)

The exprn should always be true if the program is correct. If the exprn is false a message will be printed, followed by core dump.(4)

Checking can be enabled and disabled by using the I_LEVEL and I_DEFAULT_GUARD macros. See the definitions below for these macros for further details.

Note that exprn should have no side-effects(5) since disabling checking shouldn't change your programs behaviour.

  I(z != 0); 
  x = y / z;

Macro: void N (bool exprn)

The opposite of `I', i.e. the expression must never ever be true if the program is working properly. It is equivelant to I(!(e)) and exists as a piece of syntactic sugar which may be helpful for complicated boolean expressions.

char* strdup(char *s) {
  N(s == NULL);
  ...;
}

Macro: int I_LEVEL

The `I_LEVEL' macro is used to globally enable and disable checking by the macros in this file. It can take on one of three values:

0

Disable all checking. Regardless of anything else no code will be generated for I, N, etc.

1

Enable checking only if the corresponding guard condition is true. The guard condition can be used to enable and disable checking at compile and run time.

2

Enable all checking regardless of guard conditions.

I_LEVEL defaults to 1.

Macro: bool I_DEFAULT_GUARD

The I_DEFAULT_GUARD is used to selectively enable or disable checking at compile or run time.

I_DEFAULT_GUARD defaults to TRUE, i.e. always enabled.

A user would typically define I_DEFAULT_GUARD to be global or local variable which is used to turn checking on or off at run--time. For example:

#define I_DEFAULT_GUARD i_guard > 0

extern int i_guard;

Macro: text I_DEFAULT_PARAMS

This is passed off to the I_DEFAULT_HANDLER and defaults to nothing, it is just some text and is intended to pass failure codes (e.g. IEH303) or requests (e.g. HW_DEAD) information off to the handler.

I_DEFAULT_PARAMS defaults to nothing.

Macro: void I_DEFAULT_HANDLER (char *exprn, char *file, int line, param)

When an error is detected the I_DEFAULT_HANDLER will be called to handle the error. The arguments are:

exprn

A string representation of the expression that has failed, e.g. "I(i>=0)".

file

The file that this error occurred in, i.e. __FILE__.

line

The line number for the error, i.e. __LINE__.

param

An optional parameter which can be passed across which defaults to I_DEFAULT_PARAMS. This can be used to pass failure codes or other information from the checking code to the handler.

All of the remaining macros are used to individually override the default values defined above. Normally these macros would be used in a system wide header file to define macros appropriate for the application. For example you might use `IH' to define different checking macros for hardware and software faults.

Macro: void I (bool e)

Macro: void IG (bool e, bool g)

Macro: void IH (bool e, Macro h)

Macro: void IP (bool e, Text p)

Macro: void IGH (bool e, bool g, Macro h)

Macro: void IGP (bool e, bool g, Text p)

Macro: void IHP (bool e, Macro h, Text p)

Macro: void IGHP (bool e, bool g, Macro h, Text p)

Macro: void N (bool e)

Macro: void NG (bool e, bool g)

Macro: void NH (bool e, Macro h)

Macro: void NP (bool e, Text p)

Macro: void NGH (bool e, bool g, Macro h)

Macro: void NGP (bool e, bool g, Text p)

Macro: void NHP (bool e, Macro h, Text p)

Macro: void NGHP (bool e, bool g, Macro h, Text p)

We also provide support for referring to previous values of variables in postconditions. The ID macro is used to create variables to save the old state in. The IS and ISG macros are to set these values.

Macro: void ID (Text decln)

Macro: void IS (Text assignment)

Macro: void ISG (Text decln, bool g)

For example:

void ex(int &r) {
  ID(int oldr = r); /* save parameter */
  g(r);
  I(oldr == r); /* check r is unchanged */
  while(more()) {
    IS(oldr = r); /* assign r to oldr */
    h(r);
    I(oldr == r * r);
  }
}

Go to the first, previous, next, last section, table of contents.