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] 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 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") )