Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Describe where gnatcheck rules come from #1126

Merged
merged 4 commits into from
Oct 18, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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.

Loading