Skip to content

Commit

Permalink
Merge pull request #1126 from AdaCore/describe_where_gnatcheck_rules_…
Browse files Browse the repository at this point in the history
…come_from

Describe where gnatcheck rules come from
  • Loading branch information
gusthoff authored Oct 18, 2024
2 parents 46eafbc + 017f0d0 commit 3d30338
Show file tree
Hide file tree
Showing 24 changed files with 49 additions and 41 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ Goal
**Remediation** :math:`\rightarrow` High

**Verification Method** :math:`\rightarrow` GNATcheck rule:
:rule:`uses_profile:ravenscar`
:rule:`uses_profile:ravenscar` (supplied with document)

**Mutually Exclusive** :math:`\rightarrow` CON02

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ Goal
**Remediation** :math:`\rightarrow` High

**Verification Method** :math:`\rightarrow` GNATcheck rule:
:rule:`uses_profile:jorvik`
:rule:`uses_profile:jorvik` (supplied with document)

**Mutually Exclusive** :math:`\rightarrow` CON01

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ Goal
**Remediation** :math:`\rightarrow` High

**Verification Method** :math:`\rightarrow` GNATcheck rule:
:rule:`Volatile_Objects_Without_Address_Clauses`
:rule:`Volatile_Objects_Without_Address_Clauses` (builtin rule)

+++++++++++
Reference
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ Goal
**Remediation** :math:`\rightarrow` Low

**Verification Method** :math:`\rightarrow` GNATcheck rule:
:rule:`Raising_Predefined_Exceptions`
:rule:`Raising_Predefined_Exceptions` (builtin rule)

+++++++++++
Reference
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ Goal
**Remediation** :math:`\rightarrow` Low

**Verification Method** :math:`\rightarrow` GNATcheck rule:
:rule:`Unhandled_Exceptions`
:rule:`Unhandled_Exceptions` (supplied with document)

+++++++++++
Reference
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ Goal
**Remediation** :math:`\rightarrow` Low

**Verification Method** :math:`\rightarrow` GNATcheck rule:
:rule:`Non_Visible_Exceptions`
:rule:`Non_Visible_Exceptions` (builtin rule)

+++++++++++
Reference
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ Goal
**Remediation** :math:`\rightarrow` High

**Verification Method** :math:`\rightarrow` GNATcheck rule:
:rule:`Deep_Inheritance_Hierarchies:2`
:rule:`Deep_Inheritance_Hierarchies:2` (builtin rule)

+++++++++++
Reference
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ Goal
bug)

**Verification Method** :math:`\rightarrow` GNATcheck rule:
:rule:`Direct_Calls_To_Primitives`
:rule:`Direct_Calls_To_Primitives` (builtin rule)

+++++++++++
Reference
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,8 @@ Goal

**Remediation** :math:`\rightarrow` Low

**Verification Method** :math:`\rightarrow` GNATcheck rule: :rule:`Style_Checks:O`
**Verification Method** :math:`\rightarrow` GNATcheck rule:
:rule:`Style_Checks:O` (builtin rule)

+++++++++++
Reference
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ Goal
**Remediation** :math:`\rightarrow` Low

**Verification Method** :math:`\rightarrow` GNATcheck rule:
:rule:`Specific_Pre_Post`
:rule:`Specific_Pre_Post` (builtin rule)

+++++++++++
Reference
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ Goal
**Remediation** :math:`\rightarrow` Low

**Verification Method** :math:`\rightarrow` GNATcheck rule:
:rule:`OTHERS_In_CASE_Statements`
:rule:`OTHERS_In_CASE_Statements` (builtin rule)

+++++++++++
Reference
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ Goal
**Remediation** :math:`\rightarrow` Low

**Verification Method** :math:`\rightarrow` GNATcheck rule:
:rule:`Enumeration_Ranges_In_CASE_Statements`
:rule:`Enumeration_Ranges_In_CASE_Statements` (builtin rule)

+++++++++++
Reference
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ Goal
**Remediation** :math:`\rightarrow` Low

**Verification Method** :math:`\rightarrow` GNATcheck rule:
:rule:`OTHERS_In_Aggregates`
:rule:`OTHERS_In_Aggregates` (builtin rule)

+++++++++++
Reference
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ Goal
**Remediation** :math:`\rightarrow` High

**Verification Method** :math:`\rightarrow` GNATcheck rule:
:rule:`Unassigned_OUT_Parameters`
:rule:`Unassigned_OUT_Parameters` (builtin rule)

+++++++++++
Reference
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ Goal
**Remediation** :math:`\rightarrow` Low

**Verification Method** :math:`\rightarrow` GNATcheck rule:
:rule:`OTHERS_In_Exception_Handlers`
:rule:`OTHERS_In_Exception_Handlers` (builtin rule)

+++++++++++
Reference
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ Goal
**Remediation** :math:`\rightarrow` Low

**Verification Method** :math:`\rightarrow` GNATcheck rule:
:rule:`function_out_parameters`
:rule:`function_out_parameters` (supplied with document)

+++++++++++
Reference
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ Goal
**Remediation** :math:`\rightarrow` Low

**Verification Method** :math:`\rightarrow` GNATcheck rule:
:rule:`Recursive_Subprograms`
:rule:`Recursive_Subprograms` (builtin rule)

+++++++++++
Reference
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ Goal
**Remediation** :math:`\rightarrow` Low

**Verification Method** :math:`\rightarrow` GNATcheck rule:
:rule:`overrides_standard_name`
:rule:`overrides_standard_name` (supplied with document)

+++++++++++
Reference
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ Goal
**Remediation** :math:`\rightarrow` Low

**Verification Method** :math:`\rightarrow` GNATcheck rule:
:rule:`Numeric_Literals`
:rule:`Numeric_Literals` (builtin rule)

+++++++++++
Reference
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ Goal
**Remediation** :math:`\rightarrow` High, as retrofit can be extensive

**Verification Method** :math:`\rightarrow` GNATcheck rule:
:rule:`Visible_Components`
:rule:`Visible_Components` (builtin rule)

+++++++++++
Reference
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,11 @@ detection and enforcement. For example, the language restriction identifier
The advantage of GNATcheck over the compiler is that all generated messages
will be collected in the GNATcheck report that can be used as evidence of the
level of adherence to the coding standard. In addition, GNATcheck provides a
mechanism to deal with accepted exemptions.
mechanism to deal with accepted exemptions. Note that, when the verification
method indicates a GNATcheck rule could be used, the rule will note whether
it is part of the atandard GNATcheck rule set, or has been provided as-is
within the document repository, located
`here. <https://github.com/AdaCore/learn/tree/master/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/rules>`_

In some cases the enforcement mechanism is the SPARK language and analyzer.
Many of the guidelines (and more) are implicit in the design of SPARK and are,
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
The rules in this folder where specifically created for the
Guidelines for Safe and Secure Ada/SPARK.

Some of these rules are in the process of being added into the GNATcheck tool
itself, while some of them are more related to this particular coding standard.
The document is being updated (2024-10-08) to indicate which rules are built-in
to GNATcheck, and which rules are specic to this document

* function_out_parameters

* will be added to GNATcheck

* overrides_standard_name

* will be added to GNATcheck

* unhandled_exceptions

* will remain as guideline-specific

* uses_profile

* will remain as guideline-specific

This file was deleted.

This file was deleted.

0 comments on commit 3d30338

Please sign in to comment.