Hardened Booleans (GNAT Reference Manual)

### 19.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).