GNATcheck - Coding Standard Verification Tool

GNATcheck is an extensible rule-based tool with an easy-to-use interface. It lets you completely define a coding standard (referred to as a "Software Code Standard" in DO-178B/C) as a set of rules, for example a subset of permitted language features. GNATcheck verifies the source code's conformance with the specified rules and helps demonstrate the system’s compliance with respect to standards such as DO-178B/C.

The Ada language's strong typing and compile-time checking offer significant benefits to developers of safety-critical systems, but it may still be useful or necessary to restrict the usage of certain features in the interest of facilitating certification. Ada's pragma Restrictions is one way to do this; GNATcheck gives you  additional control by letting you specify restrictions at a finer granularity.  GNATcheck can thus help satisfy Objective 4 in Table A-5 of DO-178B/C: "Source Code conforms to standards".

Qualification

Qualification material is available for GNATcheck for certain coding standards, and we can supply additional materials based on customer request. For more information please contact info@adacore.com

Key Features

  • An integrated Ada Restrictions mechanism for banning specific features from an application. This can be used to restrict features such as tasking, exceptions, dynamic allocation, fixed point or floating point, input/output and unchecked conversions.
  • GNAT Pro-specific Restrictions, which complement the set of Ada predefined restrictions. GNAT Pro restrictions include banning the generation of implicit loops or conditionals in the object code, and banning the generation of elaboration code.
  • Additional rules based on Ada semantics. Based on customer input, these include the ordering of parameters, normalized naming of entities, and subprograms with multiple returns.
  • Easy-to-use interface for creating and using a complete coding standard.
  • Generation of project-wide reports, including evidence of the level of compliance with a given coding standard.
  • Over 30 compile-time warnings from GNAT Pro that detect typical error situations. Examples are the use of local variables before being initialized, incorrect assumptions about array lower bounds, infinite recursion, incorrect data alignment, and accidental hiding of names.
  • Style checks that allow developers to control indentation, casing, comment style, and nesting level.