Documentation

Supported Ada Pragmas

Polyspace® software provides verification support for many standard Ada or GNAT compiler pragmas.

PragmaHow Polyspace Software Processes Pragma
Import, Import_Function, and Import_ProcedureStubs function or procedure
Interface and Interface_NameStubs function or procedure
Inspection_PointProvides information about possible values for the variable. May display a range.
VolatileVariable becomes full-range
Volatile_Components

If you specify Polyspace for Ada95, you get the same results as with the pragma Volatile. However, in this case, the pragma applies to arrays.

AssertProduces a user assertion check, ASRT. See User Assertion: ASRT.
RestrictionsIgnored for standard Ada or GNAT compiler restrictions. Other restriction pragmas produce a warning.
Ada_83 and Ada_95Polyspace option -lang overwrites this pragma (option set by default to Ada95 when you use polyspace-ada).
PureApplies requirement that package has cross-dependencies only with other Pure packages. If requirement is not met, generates compilation errors.

You can remove requirement by inserting pragma Not_Elaborated within package body. For example:

package System is 
pragma Pure;
pragma Not_Elaborated; 

... 
end System;

Prelaborate, Elaborate Elaborate_All, and Elaborate_Body

Provides order of elaboration and verification of packages by Polyspace
Storage_UnitPolyspace option -storage_unit overwrites this pragma

    Note:   If your code contains an unsupported pragma, Polyspace ignores the pragma and continues the verification. At the end of the compilation phase, Polyspace displays a message:

    The following pragmas have been ignored... 

Was this topic helpful?