7. Requirements Concerning Tool Switches

For designated tools, this section specifies which tool switches must be provided, and which tool switches must not be provided, when using the tools per this process.

This section does not specify switches for tools not prescribed by this process, such as the assembler, the binder, and the linker. These tools are out of the scope of this process.

7.1. Requirements Concerning Compiler Warning Switches

This section specifies which compiler warning switches must be provided, and which compiler warning switches must not be provided, when compiling SPARK or Ada software per this process. Mandatory compiler warning switches must be specified in the Compiler package of each project file (unless the project sets Source_Files to ()). Prohibited compiler warning switches must not be specified in the Compiler package of any project file.

This section also provides a rationale for why each warning switch is required, prohibited, or neither.

This section covers every compiler warning switch documented in [GUG], section Warning Message Control.

Required Compiler Warning Switches

Switch	Rationale for requiring
-gnatwa -Wall	Enables warnings that are not “controversial”. Note: The use of -Wall includes all the effects of -gnatwa, but this process requires both options so as to be explicit.
-gnatw.d	Expected to provide greater clarity to warnings. (Also, other compilers do this by default.)
-gnatwe -Werror	Treating warnings as errors results in warnings being taken seriously and results in cleaner build output Note: The use of -Werror includes all the effects of -gnatwe, but this process requires both options so as to be explicit.
-gnatwh	Implicitly-hidden declarations are a potential source of confusion when reading code. Note: The Ada/SPARK Guidelines document is expected to provide guidance on how to mitigate the risk that adding a declaration to a package will cause another package to fail to compile due to warnings enabled by -gnatwh.
-gnatw.h	Record representation clauses should be complete and fully specify the layout, and that a hole might be an indication of an error.
-gnatw.j	Tucker Taft, the chief designer of Ada 95, states that Ada “should have disallowed … adding visible operations to a tagged type after deriving a private extension from it” due to the confusion created. The capability also does not appear to add value to the language.
-gnatw.k	As warned by AdaCore, redefining names in package Standard could lead to confusion.
-gnatwl	This warning appears to prevent elaboration problems that could lead to exceptions
-gnatw.o	This switch enables warnings that are a straightforward extension of warnings enabled by -gnatwu/-gnatwa. For consistency, enable these warnings.
-gnatw_r	Record representation clauses should be structurally consistent with the associated record type definitions to ensure a complete consideration of the constraints on representation.
-gnatw.s	Record representation clauses should not contradict the associated record type definitions.
-gnatwt	It is expected that every code path within a compilation unit will be reachable without modification of the compilation unit so that every code path can be tested using the same object code as what ships to customers
-gnatw.w	Enables useful warnings about misuse of Warnings Off pragmas.
-gnatw.X	Necessary when using pragma Restrictions (No_Exception_Propagation) to avoid spurious warnings compiling SPARK code.

Prohibited Compiler Warning Switches

Switch	Rationale for prohibiting
-gnatwA -gnatw.A -gnatw_A -gnatwB -gnatw.B -gnatwC -gnatw.C -gnatw_C -gnatwF -gnatwG -gnatwI -gnatw.I -gnatwJ -gnatwK -gnatwM -gnatw.M -gnatwP -gnatw.P -gnatw_P -gnatwQ -gnatwR -gnatw.R -gnatw.T -gnatwU -gnatwV -gnatw.V -gnatwW -gnatwX -gnatwY -gnatwZ -gnatw.Z	Would suppress warnings enabled by -gnatwa
-gnatw.D	Would suppress effects of -gnatw.d
-gnatwH	Would suppress effects of -gnatwh
-gnatw.H	Would suppress effects of -gnatw.h
-gnatw.J	Would suppress effects of -gnatw.j
-gnatw.K	Would suppress effects of -gnatw.k
-gnatwL	Would suppress effects of -gnatwl
-gnatwn	Would suppress effects of -gnatwe
-gnatwO	Would disable some warnings that are enabled by default
-gnatw.O	Would suppress effects of -gnatw.o
-gnatw_R	Would suppress effects of -gnatw_r
-gnatws	Would disable all warnings
-gnatw.S	Would suppress effects of -gnatw.s
-gnatwT	Would suppress effects of -gnatwt
-gnatw.W	Would suppress effects of -gnatw.w
-gnatw.x	Would undo effects of -gnatw.X
-w	Would undo effects of -Wall

(Informative) Optional Compiler Warning Switches

Switch	Rationale for not requiring
-gnatw.a -gnatw_a -gnatwb -gnatw.b -gnatwc -gnatw.c -gnatw_c -gnatwf -gnatwg -gnatwi -gnatw.i -gnatwj -gnatwk -gnatwm -gnatw.m -gnatwp -gnatw.p -gnatw_p -gnatwq -gnatwr -gnatw.r -gnatw.t -gnatwu -gnatwv -gnatw.v -gnatww -gnatwx -gnatwy -gnatwz -gnatw.z	Would have no effect (already enabled by required switch -gnatwa)
-gnatwd -gnatwD	Enabling the warnings would disallow a common idiom in Ada that is prevalent even among Ada examples
-gnatwE	All warnings enabled by this switch are already enabled by -gnatwe
-gnatw.e	AdaCore documentation warns that this switch is “almost certain” to cause “large numbers of useless warnings”
-gnatw.g	Entirely redundant with other warning options, and AdaCore warns that its effect may change in the future without advanced notice
-gnatw.l -gnatw.L	This switch merely causes the compiler to emit a list of aspects that are inherited, which is purely informational, rather than a list of things that are wrong.
-gnatw.n -gnatw.N	Enabling the warning would interfere with the use of Atomic variables, which some lower-level software needs to use
-gnatwo	Warnings enabled by this switch are enabled by default
-gnatw.q -gnatw.Q	Warnings enabled by this switch concern performance and space efficiency but not code correctness.
-gnatw.u -gnatw.U	Using comparisons of enumerated values is a common idiom for determining whether a given enumerated value is within a certain range of enumerated values. It should not be required that this be explicitly allowed in the definition of the enumerated type.
-gnatw.y -gnatw.Y	This switch controls verbose informational messages that typically do not indicate errors
-Wunused -Wuninitialized	Entities that are declared but not referenced, or uninitialized, from a back end perspective but not from a front end perspective are more likely to be indicative of the effects of optimizations than real errors

7.2. Requirements Concerning Non-Warning-Related Compiler Switches

This section specifies which non-warning-related compiler switches must be provided, and which non-warning-related compiler switches must not be provided, when compiling SPARK or Ada software per this process. Mandatory non-warning-related compiler switches must be specified in the Compiler package of each project file. Prohibited non-warning-related compiler warning switches must not be specified in the Compiler package of any project file.

This section also provides a rationale for why certain compiler switches are required, prohibited, or neither.

Generally, switches that have been safety-qualified can be used where their semantics match the requirements of a given project. Rationales for permitting certain switches are listed below. Consult your safety manual for a full list.

Required Compiler Switches

Switch	Rationale for requiring
-fcallgraph-info=su,da	Necessary to ensure that GNATstack produces correct output in the Check_Stack_Usage step.
-gnatyr	Unique IDs (see section Traceability Model) are case sensitive and built from local IDs sometimes derived from identifiers. To remove ambiguity concerning the correct local ID (and thus the correct unique ID) for a comment or syntactic construct, all references to the same entity must agree about the case of the associated identifiers.

Prohibited Compiler Switches

Switch	Rationale for prohibiting
-gnata (except for non-production builds)	This switch causes contracts to be executed at runtime, and contracts and ghost code are permitted to use Ada 2022, but Ada 2022 is not safety qualified for production use.
–RTS	The runtime should be set at project level.
-c -o <file> -I <path> -x -S	Will be added by gprbuild.
All non-warning-related compiler switches not explicitly listed in the compiler safety manual as having been safety qualified	These compiler switches are not safety-qualified.

(Informative) Optional Compiler Switches

Switch	Rationale for not requiring
-gnato -gnaton -gnatomn	The -gnato family of switches is permitted but not recommended. The -gnato0 switch suppresses overflow checks (except where explicitly unsuppressed in the code, such as for all non-SPARK code). Overflow checks are just one of the kinds of checks suppressed by the -gnatp switch. The -gnato0 switch is permitted for the same reasons that the -gnatp switch is permitted. However, for performance reasons, it is preferable to use the -gnatp switch instead, as it suppresses more unnecessary checks. The -gnato, -gnato1, and -gnato11 switches all have the effect of enabling overflow checking (even in SPARK code), without changing the overflow mode from the default (STRICT both inside and outside of contracts). This can undo the beneficial performance effects of -gnatp. The -gnato2, -gnato3, -gnato12, -gnato13, -gnato21, -gnato22, -gnato23, and -gnato33 switches unnecessarily widen intermediate subexpressions in SPARK code (where GNATprove already formally verifies the absence of overflow even without the widening), potentially hurting performance of SPARK code. These switches can also make it more difficult to determine whether a non-SPARK Ada code computation will complete successfully or trigger a language-defined check, reducing the clarity of non-SPARK Ada code. Note: The Verify_Dynamic_Assumptions and Run_Integration_Tests steps require rebuilding tests without the -gnato0 switch.
-gnatp (except for non-production builds)	The -gnatp switch disables unnecessary language-defined checks in SPARK code and may thereby improve the performance of SPARK code. The checks are unnecessary because GNATprove formally verifies that SPARK code never violates any of the properties checked by the language-defined checks. This switch is not required, but it is recommended by this process for performance reasons. Note: This process requires all non-SPARK code to be contained within pragma Unsuppress(All_Checks) regions. Therefore, in software units that comply with this process, non-SPARK code is not affected by the presence or absence of the -gnatp switch. Note: The Verify_Dynamic_Assumptions and Run_Integration_Tests steps require rebuilding tests without the -gnatp switch.

7.3. Requirements Concerning GNATprove Switches

This section specifies which GNATprove switches must be provided, and which GNATprove switches must not be provided, when verifying SPARK software per this process. Mandatory GNATprove switches must be specified in the Prove package of each project file passed to GNATprove or must be specified on each gnatprove command line. Prohibited GNATprove switches must not be specified in the Prove package of any project file passed to GNATprove and must not be specified on the gnatprove command line.

This section also provides a rationale for why each GNATprove switch is required, prohibited, or neither.

Note that this section has no bearing on the use of GNATprove outside of the official verification of SPARK software per this process. As part of normal development, it is permissible to use GNATprove with prohibited switches and/or without mandatory switches, as long as final verification is performed using switches consistent with this section. Final verification refers to the gnatprove run in the Verify Project step.

This section is intended to cover every GNATprove switch that is documented in [SUG], section Command Line Invocation, or documented via the output of gnatprove –help, excluding some switches identified via the gnatprove –help output as “advanced switches”.

Any switch not listed here shall be assumed to be prohibited.

Required GNATprove Switches

Switch	Rationale for requiring
–checks-as-errors=on	In this process, GNATprove check messages are reviewed via diagnostic justifications, not via gnatprove output. This switch ensures that any check message will result in gnatprove not exiting without an error code.
–warnings=error	Some GNATprove warnings are used to identify potential violations of GNATprove assumptions, each of which requires manual review to ensure the violations will not lead to GNATprove false negatives. This switch ensures that any such potential violation will result in gnatprove not exiting without an error code.
-P <project-file.gpr>	The use of -P is part of every documented method for specifying which compilation units to analyze.
-U	Without -U, GNATprove will not necessarily analyze all the units that are part of the project. GNATprove specifically behaves as follows when invoked without -U: If specific source files are identified on the command line, then GNATprove will only analyze the units containing those source files, even if source files from other units are included in the project file. (GNATprove will additionally analyze their dependencies if also invoked with -u, but this still leaves open the possibility that some of the units will be missed). If specific source files are not identified on the command line, then GNATprove will only analyze main units and the units they depend on.

Prohibited GNATprove Switches

Switch	Rationale for prohibiting
–assumptions	This switch is not safety-qualified.
–clean	This switch directs GNATprove not to attempt to prove anything. NOTE: This switch is required, not prohibited, during the cleaning part of the Verify_Project step.
–cwe	This switch is not safety-qualified.
–help -h	This switch is not safety-qualified.
–list-categories	This switch prevents GNATprove from fulfilling its intended function. This switch is also not safety-qualified.
–mode=bronze –mode=check –mode=check_all –mode=flow –mode=prove –mode=stone	–mode=check would partially disable checks that SPARK_Mode => On packages and subprograms are within the SPARK subset of Ada. –mode=check, –mode=check_all, –mode=prove, and –mode=stone would partially or fully disable flow analysis, which is needed to verify initialization of variables before use and compliance with some contracts. –mode=flow and –mode=bronze would disable verification of functional contracts and of the absence of run-time errors. These switches are also not safety-qualified.
–mode=gold –mode=silver	Though these switches are equivalent to –mode=all, they are not safety-qualified (where –mode=all is safety-qualified).
–limit-line=… –limit-region=… –limit-subp=… –no-subprojects	With any of these options, GNATprove will not necessarily analyze all of the code within each analyzed unit. These switches are also not safety-qualified.
–output-msg-only	This switch is not safety-qualified.
–proof	This switch is not safety-qualified.
–prover=colibri (or any superset of this)	GNATprove’s use of the Colibri prover is not safety-qualified.
–replay	This switch is not safety-qualified.
–RTS=<dir>	Per the Create_Project_File step, a safety-qualified runtime is already specified in the project file using the Runtime(“Ada”) attribute. This ensures the various tools use a consistent runtime.
–subdirs=…	This switch is not safety-qualified.
–version	This switch prevents GNATprove from fulfilling its intended function. This switch is also not safety-qualified.
–warnings=off –warnings=continue	This switch would interfere with the effect of -warnings=error. These switches are also not safety-qualified.
-aP=…	This switch is not safety-qualified.
-f	This switch is not safety-qualified. Note that this switch is not needed to ensure correct results.
-gnateT=<target.atp>	This switch could result in an inconsistency between the target configuration used by the compiler and the target configuration used by GNATprove.
-k	This switch is not safety-qualified.
-m	This switch is not safety-qualified.
-q	This switch is not safety-qualified. (Note however that a synonym, –quiet, is safety-qualified.)
-u	Would conflict with -U. This switch is also not safety-qualified.
-v	This switch is not safety-qualified. (Note however that a synonym, –verbose, is safety-qualified.)
All switches not covered in this section	These switches are not safety-qualified.

(Informative) Optional GNATprove Switches

Switch	Rationale for not requiring
–counterexamples	Though this switch is not safety-qualified with the on setting, its use is nevertheless permitted because this switch cannot lead to false negatives in verification results. In a worst-case scenario, verification does not complete successfully and a faulty counterexample is provided that does not explain the verification failure. This scenario still does not have a safety impact.
–info	This switch can provide additional information but its presence or absence cannot lead to false negatives in verification results.
-j	This switch affects proof performance, but its presence or absence cannot lead to false negatives in verification results.
–level	This switch can control when GNATprove determines that it is unable to complete verification, but cannot lead to false negatives in verification results. This switch can control which provers are used, but cannot be used to select a non-safety-qualified prover. This switch can control whether counterexamples are produced, but see above for why that is not of concern.
–quiet	This switch hides some output but will not mask a verification failure.
–memlimit –steps –timeout	These switches can control when GNATprove determines that it is unable to complete verification, but these switches cannot lead to false negatives in verification results.
–mode=all	This switch requests the default behavior of GNATprove, which is to do full checking for compliance with SPARK restrictions, full flow analysis, and full proof.
–output	This switch affects the format of the output but will not mask a verification failure.
–prover=altergo,cvc5,z3 (or any subset of these)	GNATprove’s use of the Alt-Ergo, CVC5, and Z3 provers is safety-qualified, and GNATprove does not use any other provers unless specifically directed to do so with the –prover=… switch.
–verbose	This switch reports some additional output but will not mask a verification failure.

7.4. Requirements Concerning GNATcheck Switches and Rules

This section specifies which GNATcheck switches [GCRM] must be provided, and which GNATcheck switches must not be provided, when verifying SPARK software per this process. Mandatory GNATcheck switches must be specified in the Check package of each project file passed to GNATcheck or on the gnatcheck command line. Any switch not explicitly allowed here must not be specified in the Check package of any project file passed to GNATcheck, and must not be passed on the gnatcheck command line.

This section also provides a rationale for why each GNATcheck switch is required, or optional.

Note that this section has no bearing on the use of GNATcheck outside of the official verification of SPARK software per this process. As part of normal development, it is permissible to use GNATcheck with prohibited switches and/or without mandatory switches, as long as final verification is performed using switches consistent with this section.

Note: The Ada/SPARK Guidelines may mandate the use of additional GNATcheck rules. This section is not intended to specify all desirable GNATcheck rules, but rather is intended to specify what is minimally required by this process. This section is not intended to specify a coding standard.

Required GNATcheck Switches

Switch	Rationale for requiring
–check-redefinition	Detects errors in rule set that could cause unexpected suppression of rules.
-rules -from=<rule_option_filename>	This options must be provided in the GPR file to enable the rules required in the Table of Required GNATcheck Rules. Note: Entries of the form -R<rule> must not exist in any rule option file specified via -from=<rule_option_filename>, whether specified on the command line or inside another rule option file.
-P <project-file.gpr>	The use of -P ensures that switches passed via the Check package of the project file are effective.
-U	Without -U, GNATcheck will not necessarily analyze all the units that are part of the project.

(Informative) Optional GNATcheck Switches

Switch	Rationale for not requiring
-Xname=value	Configuration data is allowed.
-o <report_file>	Has no effect on reporting of rule violations on stdout / stderr.
–show-rule	Has no effect on whether the number of rule violations reported on stdout / stderr is zero or non-zero.
–include-file=<file>	Has no effect on reporting of rule violations on stdout / stderr.
–no-objects-dir	The GNATcheck output files are not significant to this process, since the existence of rule violations is reported on the command line.
–no-subprojects	This switch does not control the processing of ADS/ADB files from the project specified with -P (the “argument project”). This switch only controls the processing of ADS/ADB files from other projects recursively included in the argument project.
–rules-dir=<dir>	This is a valid way to specify the locations of custom rules.
-j	Has no effect on reporting of rule violations.

Required GNATcheck Rules

Switch	Rationale for requiring
Ada_2022_In_Ghost_Code	Required to flag Ada 2022 code used outside of contracts, which would violate the GNAT safety manual (see step Manual_Check_Against_Safety_Manuals)
Forbidden_Attributes:Initialized	Needed to identify cases where manual review is required for GNATprove assumption [SPARK_INITIALIZED_ATTRIBUTE]
Forbidden_Pragmas:Validity_Checks	Required because pragma Validity_Checks is not safety-certified
Forbidden_Pragmas:Assertion_Policy	Required to avoid inclusion of Ada 2022 code in contracts into the production build, which would violate the GNAT safety manual (see step Manual_Check_Against_Safety_Manuals) Note: With a GNATcheck diagnostic justification annotation, pragma Assertion_Policy can still be used with the Ignore parameter as long as additional tests are specified; see the Write_Tests step). However, pragma Assertion_Policy with the Check parameter is only valid if it is known that all applicable contracts entirely refrain from using Ada 2022 features.
Forbidden_Pragmas:Ignore_Pragma	Required because pragma Ignore_Pragma can cause SPARK to be silently disabled.
Metrics_Cyclomatic_Complexity:10 (to be enforced on non-proven code only)	Required for non-proven code (code that is not SPARK_Mode => On and code that is annotated with Skip_Proof or Skip_Flow_And_Proof) for compliance with ISO 26262-6:2018, Table 1 row 1a “Enforcement of low complexity” and 8.4.5d “simplicity”. Note: This process does not enforce McCabe cyclomatic complexity limits on proven SPARK executable bodies because it is neither effective for reducing risk nor necessary for compliance with ISO 26262. The enforcement of low complexity in proven SPARK code is not effective for reducing risk because (1) the use of GNATprove on SPARK executable bodies significantly reduces the risk of complexity-induced systematic faults, (2) complexity metrics are a poor metric for comprehensibility, and (3) comprehensibility is already verified in the Inspect_Implementation step. The enforcement of low complexity in proven SPARK code is not necessary for compliance with ISO 26262 because the recommendation to enforce low complexity in programming languages is given in ISO 26262-6:2018, 5.4.3 in the context of mitigating programming language deficiencies relative to the criteria specified in ISO 26262-6:2018, 5.4.2, which SPARK largely excels at. Moreover, the aforementioned recommendation is accompanied by a footnote acknowledging “an appropriate compromise of this topic with other requirements of this document may be required” (ISO 26262-6:2018, Table 1, footnote a), and it is frequently the case that compliance with cyclomatic complexity limits actually reduces the comprehensibility of code (e.g., obfuscation of algorithms through refactoring into smaller subprograms). Note: AdaCore recommends scrutinizing executable bodies with McCabe cyclomatic complexities greater than 10 because this is the practice AdaCore uses for its own certified Ada runtime libraries.
Procedures_Without_Globals	Required to flag SPARK procedure declarations with no Global aspect (see note in Capture_Requirements step)
Restrictions:Max_Protected_Entries=>0	Needed to identify cases where manual review is necessary for GNATprove assumption [SPARK_OVERRIDING_AND_TASKING]
Restrictions:No_Floating_Point	Needed to identify cases where manual review is necessary for GNATprove assumption [SPARK_FLOATING_POINT]
Restrictions:No_Protected_Types	Needed to identify cases where manual review is necessary for GNATprove assumption [SPARK_OVERRIDING_AND_TASKING]
Restrictions:No_Specification_Of_Aspect=>Iterable	Needed to identify cases where manual review is necessary for GNATprove assumptions [SPARK_ITERABLE] and [SPARK_ITERABLE_FOR_PROOF]
Restrictions:No_Use_Of_Entity=>Ada.Task_Identification.Current_Task	Needed to identify cases where manual review is necessary for [SPARK_OVERRIDING_AND_TASKING]
Restrictions:No_Use_Of_Entity=>Synchronous_Task_Control	Needed to identify cases where manual review is necessary for [SPARK_OVERRIDING_AND_TASKING]
Goto_Statements:Only_Unconditional	Required for compliance with ISO 26262-6:2018, Table 6, row 1i “No unconditional jumps”