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 0743447d9..82c792ea4 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 7ec8687a7..8c2a1581d 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 0ded46b42..57b3fe6f5 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 f4820193b..1c293cdd0 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 07326dd09..fcfb22654 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 fb464a07a..4df95b6a9 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 0429eff02..8ce792e4b 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 9c2bb0a62..c32cea645 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 14a59edab..c835f4db5 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 8ae873a9c..bf867f541 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 67db343cf..df4690d40 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 5f967c9b0..07a025ae3 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 0e8ee841c..fba11513d 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 6984993df..c56a764ec 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 b2df1375b..83644b9c2 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 a88d47290..4c4f5d762 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 285d933ef..6909c51ba 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 f579e5ff2..b2d909047 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 c4cde39fa..503614a9c 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 c98c3fbee..cedcde127 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 3eb8ec3d8..1a4d021ee 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 000000000..6b7d81821 --- /dev/null +++ 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 deleted file mode 100644 index bc30e9ebe..000000000 --- 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) 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 aaf335b50..000000000 --- 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") )