Next: , Previous: Stack Related Facilities, Up: Top

23 Verifying properties using gnatcheck

The gnatcheck tool is an ASIS-based utility that checks properties of Ada source files according to a given set of semantic rules.

In order to check compliance with a given rule, gnatcheck has to semantically analyze the Ada sources. Therefore, checks can only be performed on legal Ada units. Moreover, when a unit depends semantically upon units located outside the current directory, the source search path has to be provided when calling gnatcheck, either through a specified project file or through gnatcheck switches as described below.

The project support for gnatcheck is provided by the gnat driver.

Several rules are already implemented in gnatcheck. The list of such rules can be obtained with option -h as described in the next section. A user can add new rules by modifying the gnatcheck code and rebuilding the tool. For adding a simple rule making some local checks, a small amount of straightforward ASIS-based programming is usually needed.

gnatcheck has the command-line interface of the form

     $ gnatcheck [switches]  {filename}  [-files={arg_list_filename}]
           [-cargs gcc_switches] [-rules rule_options]


Either a filename or an arg_list_filename needs to be supplied.