From a8d2d3dc0e6f299bc82a0f146764e1d04c3d105c Mon Sep 17 00:00:00 2001 From: Michael Frank <55284511+frank-at-adacore@users.noreply.github.com> Date: Mon, 7 Oct 2024 09:52:42 -0400 Subject: [PATCH 1/4] Rule is not actually used, so remove it for clarity --- .../rules/lkql/has_restriction.lkql | 14 -------------- 1 file changed, 14 deletions(-) delete mode 100644 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/has_restriction.lkql b/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/rules/lkql/has_restriction.lkql deleted file mode 100644 index bc30e9eb..00000000 --- a/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/rules/lkql/has_restriction.lkql +++ /dev/null @@ -1,14 +0,0 @@ -# Flag if provided restriction is not used - -import stdlib - -@memoize -fun find_restriction(restriction) = - (select first p@PragmaNode when p.f_id.p_name_is("Restrictions") and - p.f_args[1].p_assoc_expr() is - e@Expr and e.p_name_is(restriction)) == null - -@check(message="Required restriction not used") -fun has_restriction(node, restriction: string = "") = - node is CompilationUnit - when find_restriction(restriction) From 982e1ec046d33829b94c41c33fd963a1da904510 Mon Sep 17 00:00:00 2001 From: Michael Frank <55284511+frank-at-adacore@users.noreply.github.com> Date: Mon, 7 Oct 2024 09:58:39 -0400 Subject: [PATCH 2/4] Remove rule that is not actually used --- .../rules/lkql/no_pre_post_contracts.lkql | 6 ------ 1 file changed, 6 deletions(-) delete mode 100644 content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/rules/lkql/no_pre_post_contracts.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 deleted file mode 100644 index aaf335b5..00000000 --- a/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/rules/lkql/no_pre_post_contracts.lkql +++ /dev/null @@ -1,6 +0,0 @@ -@check -fun no_pre_post_contracts(node) = - node is (BasicSubpDecl or - BaseSubpBody(p_previous_part() is null) or - SubpBodyStub(p_previous_part() is null)) - and not ( node.p_has_aspect("Pre") and node.p_has_aspect("Post") ) From 66b4c9cb997cb14dadd0ac88f469e66eed6486be Mon Sep 17 00:00:00 2001 From: Michael Frank <55284511+frank-at-adacore@users.noreply.github.com> Date: Mon, 7 Oct 2024 10:42:17 -0400 Subject: [PATCH 3/4] Indicate which rules are builtin and which are defined in the repo --- .../con01_use_the_ravenscar_profile.rst | 2 +- .../con02_use_the_jorvik_profile.rst | 2 +- ...variables_for_inter-task_communication.rst | 2 +- ...dont_raise_language-defined_exceptions.rst | 2 +- ...handled_application-defined_exceptions.rst | 2 +- ...ion_propagation_beyond_name_visibility.rst | 2 +- ...op03_limit_inheritance_hierarchy_depth.rst | 2 +- ...spatched_calls_to_primitive_operations.rst | 2 +- ...05_use_explicit_overriding_annotations.rst | 3 ++- ...op06_use_class-wide_pre-post_contracts.rst | 2 +- ...01_no_use_of_others_in_case_constructs.rst | 2 +- ..._enumeration_ranges_in_case_constructs.rst | 2 +- ...03_limited_use_of_others_in_aggregates.rst | 2 +- ...assigned_mode-out_procedure_parameters.rst | 2 +- ...no_use_of_others_in_exception_handlers.rst | 2 +- .../rpp07_functions_only_have_mode_in.rst | 2 +- .../rpp12_no_recursion.rst | 2 +- .../rpp13_no_reuse_of_standard_typemarks.rst | 2 +- ..._symbolic_constants_for_literal_values.rst | 2 +- .../swe04_hide_implementation_artifacts.rst | 2 +- .../chapters/introduction.rst | 6 ++++- .../rules/lkql/README.md | 27 +++++++++++++++++++ 22 files changed, 53 insertions(+), 21 deletions(-) create mode 100644 content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/rules/lkql/README.md 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 index 0743447d..82c792ea 100644 --- 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 index 7ec8687a..8c2a1581 100644 --- 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 index 0ded46b4..57b3fe6f 100644 --- 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 index f4820193..1c293cdd 100644 --- 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 index 07326dd0..fcfb2265 100644 --- 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 index fb464a07..4df95b6a 100644 --- 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 index 0429eff0..8ce792e4 100644 --- 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 index 9c2bb0a6..c32cea64 100644 --- 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 index 14a59eda..c835f4db 100644 --- 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 index 8ae873a9..bf867f54 100644 --- 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 index 67db343c..df4690d4 100644 --- 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 index 5f967c9b..07a025ae 100644 --- 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 index 0e8ee841..fba11513 100644 --- 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 index 6984993d..c56a764e 100644 --- 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 index b2df1375..83644b9c 100644 --- 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 index a88d4729..4c4f5d76 100644 --- 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 index 285d933e..6909c51b 100644 --- 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 index f579e5ff..b2d90904 100644 --- 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 index c4cde39f..503614a9 100644 --- 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 index c98c3fbe..cedcde12 100644 --- 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 index 3eb8ec3d..1a4d021e 100644 --- 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. `_ 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 new file mode 100644 index 00000000..61168195 --- /dev/null +++ b/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/rules/lkql/README.md @@ -0,0 +1,27 @@ +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 + + * https://gitlab.adacore-it.com/eng/libadalang/langkit-query-language/-/issues/340 + * will be added to GNATcheck + +* overrides_standard_name + + * https://gitlab.adacore-it.com/eng/libadalang/langkit-query-language/-/issues/343 + * will be added to GNATcheck + +* unhandled_exceptions + + * https://gitlab.adacore-it.com/eng/libadalang/langkit-query-language/-/issues/344 + * will remain as guideline-specific + +* uses_profile + + * https://gitlab.adacore-it.com/eng/libadalang/langkit-query-language/-/issues/345 + * will remain as guideline-specific From 017f0d038cd130e8a6e74a51b2275b97f70f32ef Mon Sep 17 00:00:00 2001 From: Michael Frank <55284511+frank-at-adacore@users.noreply.github.com> Date: Thu, 17 Oct 2024 14:09:05 -0400 Subject: [PATCH 4/4] Remove references to gitlab issues They will not be visible to all github visitors --- .../rules/lkql/README.md | 50 +++++++++---------- 1 file changed, 23 insertions(+), 27 deletions(-) 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 index 61168195..6b7d8182 100644 --- 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 @@ -1,27 +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 - - * https://gitlab.adacore-it.com/eng/libadalang/langkit-query-language/-/issues/340 - * will be added to GNATcheck - -* overrides_standard_name - - * https://gitlab.adacore-it.com/eng/libadalang/langkit-query-language/-/issues/343 - * will be added to GNATcheck - -* unhandled_exceptions - - * https://gitlab.adacore-it.com/eng/libadalang/langkit-query-language/-/issues/344 - * will remain as guideline-specific - -* uses_profile - - * https://gitlab.adacore-it.com/eng/libadalang/langkit-query-language/-/issues/345 - * will remain as guideline-specific +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