Merge pull request #1126 from AdaCore/describe_where_gnatcheck_rules_come_from

gusthoff · web-flow · commit 3d303381be50 · 2024-10-18T10:40:01.000+02:00
Describe where gnatcheck rules come from
diff --git a/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/guidelines/concurrency/con01_use_the_ravenscar_profile.rst b/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/guidelines/concurrency/con01_use_the_ravenscar_profile.rst
@@ -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
 
diff --git a/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/guidelines/concurrency/con02_use_the_jorvik_profile.rst b/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/guidelines/concurrency/con02_use_the_jorvik_profile.rst
@@ -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
 
diff --git a/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/guidelines/concurrency/con03_avoid_shared_variables_for_inter-task_communication.rst b/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/guidelines/concurrency/con03_avoid_shared_variables_for_inter-task_communication.rst
@@ -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
diff --git a/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/guidelines/exception_usage/exu01_dont_raise_language-defined_exceptions.rst b/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/guidelines/exception_usage/exu01_dont_raise_language-defined_exceptions.rst
@@ -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
diff --git a/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/guidelines/exception_usage/exu02_no_unhandled_application-defined_exceptions.rst b/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/guidelines/exception_usage/exu02_no_unhandled_application-defined_exceptions.rst
@@ -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
diff --git a/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/guidelines/exception_usage/exu03_no_exception_propagation_beyond_name_visibility.rst b/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/guidelines/exception_usage/exu03_no_exception_propagation_beyond_name_visibility.rst
@@ -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
diff --git a/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/guidelines/object_oriented_programming/oop03_limit_inheritance_hierarchy_depth.rst b/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/guidelines/object_oriented_programming/oop03_limit_inheritance_hierarchy_depth.rst
@@ -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
diff --git a/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/guidelines/object_oriented_programming/oop04_limit_statically-dispatched_calls_to_primitive_operations.rst b/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/guidelines/object_oriented_programming/oop04_limit_statically-dispatched_calls_to_primitive_operations.rst
@@ -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
diff --git a/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/guidelines/object_oriented_programming/oop05_use_explicit_overriding_annotations.rst b/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/guidelines/object_oriented_programming/oop05_use_explicit_overriding_annotations.rst
@@ -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
diff --git a/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/guidelines/object_oriented_programming/oop06_use_class-wide_pre-post_contracts.rst b/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/guidelines/object_oriented_programming/oop06_use_class-wide_pre-post_contracts.rst
@@ -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
diff --git a/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/guidelines/robust_programming_practice/rpp01_no_use_of_others_in_case_constructs.rst b/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/guidelines/robust_programming_practice/rpp01_no_use_of_others_in_case_constructs.rst
@@ -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
diff --git a/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/guidelines/robust_programming_practice/rpp02_no_enumeration_ranges_in_case_constructs.rst b/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/guidelines/robust_programming_practice/rpp02_no_enumeration_ranges_in_case_constructs.rst
@@ -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
diff --git a/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/guidelines/robust_programming_practice/rpp03_limited_use_of_others_in_aggregates.rst b/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/guidelines/robust_programming_practice/rpp03_limited_use_of_others_in_aggregates.rst
@@ -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
diff --git a/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/guidelines/robust_programming_practice/rpp04_no_unassigned_mode-out_procedure_parameters.rst b/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/guidelines/robust_programming_practice/rpp04_no_unassigned_mode-out_procedure_parameters.rst
@@ -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
diff --git a/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/guidelines/robust_programming_practice/rpp05_no_use_of_others_in_exception_handlers.rst b/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/guidelines/robust_programming_practice/rpp05_no_use_of_others_in_exception_handlers.rst
@@ -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
diff --git a/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/guidelines/robust_programming_practice/rpp07_functions_only_have_mode_in.rst b/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/guidelines/robust_programming_practice/rpp07_functions_only_have_mode_in.rst
@@ -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
diff --git a/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/guidelines/robust_programming_practice/rpp12_no_recursion.rst b/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/guidelines/robust_programming_practice/rpp12_no_recursion.rst
@@ -20,7 +20,7 @@ Goal
 **Remediation** :math:`\rightarrow` Low
 
 **Verification Method** :math:`\rightarrow` GNATcheck rule:
-:rule:`Recursive_Subprograms`
+:rule:`Recursive_Subprograms` (builtin rule)
 
 +++++++++++
 Reference
diff --git a/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/guidelines/robust_programming_practice/rpp13_no_reuse_of_standard_typemarks.rst b/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/guidelines/robust_programming_practice/rpp13_no_reuse_of_standard_typemarks.rst
@@ -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
diff --git a/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/guidelines/robust_programming_practice/rpp14_use_symbolic_constants_for_literal_values.rst b/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/guidelines/robust_programming_practice/rpp14_use_symbolic_constants_for_literal_values.rst
@@ -20,7 +20,7 @@ Goal
 **Remediation** :math:`\rightarrow` Low
 
 **Verification Method** :math:`\rightarrow` GNATcheck rule:
-:rule:`Numeric_Literals`
+:rule:`Numeric_Literals` (builtin rule)
 
 +++++++++++
 Reference
diff --git a/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/guidelines/software_engineering/swe04_hide_implementation_artifacts.rst b/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/guidelines/software_engineering/swe04_hide_implementation_artifacts.rst
@@ -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
diff --git a/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/introduction.rst b/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/chapters/introduction.rst
@@ -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,
diff --git a/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/rules/lkql/README.md b/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/rules/lkql/README.md
@@ -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
diff --git a/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/rules/lkql/has_restriction.lkql b/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/rules/lkql/has_restriction.lkql
diff --git a/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/rules/lkql/no_pre_post_contracts.lkql b/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/rules/lkql/no_pre_post_contracts.lkql
