17.4 Hardened Booleans ¶

Ada has built-in support for introducing boolean types with alternative representations, using representation clauses:

type HBool is new Boolean;
for HBool use (16#5a#, 16#a5#);
for HBool'Size use 8;

When validity checking is enabled, the compiler will check that variables of such types hold values corresponding to the selected representations.

There are multiple strategies for where to introduce validity checking (see -gnatV options). Their goal is to guard against various kinds of programming errors, and GNAT strives to omit checks when program logic rules out an invalid value, and optimizers may further remove checks found to be redundant.

For additional hardening, the hardbool Machine_Attribute pragma can be used to annotate boolean types with representation clauses, so that expressions of such types used as conditions are checked even when compiling with -gnatVT:

pragma Machine_Attribute (HBool, "hardbool");

function To_Boolean (X : HBool) returns Boolean is (Boolean (X));

is compiled roughly like:

function To_Boolean (X : HBool) returns Boolean is
begin
  if X not in True | False then
    raise Constraint_Error;
  elsif X in True then
    return True;
  else
    return False;
  end if;
end To_Boolean;

Note that -gnatVn will disable even hardbool testing.

Analogous behavior is available as a GCC extension to the C and Objective C programming languages, through the hardbool attribute, with the difference that, instead of raising a Constraint_Error exception, when a hardened boolean variable is found to hold a value that stands for neither True nor False, the program traps. For usage and more details on that attribute, see Using the GNU Compiler Collection (GCC).