From 4d4d76dff362ffa8534a1746bbd33d00208c4d8b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Laurent=20Th=C3=A9venoux?= <thevenoux@adacore.com>
Date: Tue, 12 Sep 2023 16:19:43 +0200
Subject: [PATCH] Allow to skip `Skip_Proof` annotations in `p_is_spark`

The property `p_is_spark` can now take a boolean parameter
(`include_skip_proof_annotations`, defaults to `True`) to specify
whether the `GNATprove` `Skip_Proof` and `Skip_Flow_And_Proof`
annotations should be ignored to determine if a subprogram is in SPARK
or not.
---
 ada/ast.py                                     |  4 ++--
 .../tests/properties/is_spark/aspect/test.out  | 18 +++++++++---------
 .../tests/properties/is_spark/aspect/test.py   |  4 ++--
 .../is_spark/configuration_pragma_1/test.out   | 10 +++++++++-
 .../is_spark/configuration_pragma_1/test.py    | 12 ++++++++++--
 .../is_spark/configuration_pragma_2/test.out   |  2 +-
 .../is_spark/configuration_pragma_2/test.py    |  4 ++--
 .../is_spark/configuration_pragma_3/test.out   |  2 +-
 .../is_spark/configuration_pragma_3/test.py    |  4 ++--
 .../is_spark/configuration_pragma_4/test.out   |  2 +-
 .../is_spark/configuration_pragma_4/test.py    |  4 ++--
 .../is_spark/mixed_pragma_and_aspect/test.out  | 18 +++++++++---------
 .../is_spark/mixed_pragma_and_aspect/test.py   |  4 ++--
 .../is_spark/pkg_private_and_body/test.out     | 12 ++++++------
 .../is_spark/pkg_private_and_body/test.py      |  4 ++--
 .../tests/properties/is_spark/pragma/test.out  | 18 +++++++++---------
 .../tests/properties/is_spark/pragma/test.py   |  4 ++--
 .../is_spark/skip_flow_and_proof/test.out      |  2 +-
 .../is_spark/skip_flow_and_proof/test.py       |  4 ++--
 .../properties/is_spark/skip_proof/test.out    |  6 +++---
 .../properties/is_spark/skip_proof/test.py     |  4 ++--
 user_manual/changes/libadalang/1074.yaml       |  9 +++++++++
 22 files changed, 88 insertions(+), 63 deletions(-)
 create mode 100644 user_manual/changes/libadalang/1074.yaml

diff --git a/ada/ast.py b/ada/ast.py
index 56b9ab3dd..c6361dddf 100644
--- a/ada/ast.py
+++ b/ada/ast.py
@@ -20696,7 +20696,7 @@ def gnatprove_annotations():
         return annotations.concat(pragmas).concat(enclosing_subp_annotations)
 
     @langkit_property(public=True, return_type=Bool, memoized=True)
-    def is_spark():
+    def is_spark(include_skip_proof_annotations=(T.Bool, True)):
         """
         Return whether this subprogram body is in SPARK or not, i.e. return
         whether SPARK proofs will be applied to that subprogram or not.
@@ -20704,7 +20704,7 @@ def is_spark():
         return Cond(
             # If `Skip_Proof` or `Skip_Flow_And_Proof` has been specified, this
             # is not in SPARK.
-            Not(
+            include_skip_proof_annotations & Not(
                 Entity.gnatprove_annotations.find(
                     lambda a: a.cast(Name).name_symbol.any_of(
                         'Skip_Proof', 'Skip_Flow_And_Proof'
diff --git a/testsuite/tests/properties/is_spark/aspect/test.out b/testsuite/tests/properties/is_spark/aspect/test.out
index f9e5b68ff..29fe72dfc 100644
--- a/testsuite/tests/properties/is_spark/aspect/test.out
+++ b/testsuite/tests/properties/is_spark/aspect/test.out
@@ -1,35 +1,35 @@
-=== Analysing unit:  <AnalysisUnit 'a.adb'> """
+=== Analysing unit:  <AnalysisUnit 'a.adb'> ===
 Subprogram <NullSubpDecl ["P"] a.adb:2:4-2:24> is skipped
 Subprogram <NullSubpDecl ["Q"] a.adb:3:4-3:24> is skipped
 
-=== Analysing unit:  <AnalysisUnit 'b.adb'> """
+=== Analysing unit:  <AnalysisUnit 'b.adb'> ===
 Subprogram <NullSubpDecl ["P"] b.adb:2:4-2:24> is skipped
 Subprogram <NullSubpDecl ["Q"] b.adb:3:4-3:24> is skipped
 
-=== Analysing unit:  <AnalysisUnit 'c.adb'> """
+=== Analysing unit:  <AnalysisUnit 'c.adb'> ===
 Subprogram <NullSubpDecl ["P"] c.adb:2:4-2:24> is skipped
 Subprogram <NullSubpDecl ["Q"] c.adb:3:4-3:24> is skipped
 
-=== Analysing unit:  <AnalysisUnit 'd-p2.adb'> """
+=== Analysing unit:  <AnalysisUnit 'd-p2.adb'> ===
 Subprogram <SubpBody ["P2"] d-p2.adb:2:1-5:5> is skipped
 
-=== Analysing unit:  <AnalysisUnit 'd.adb'> """
+=== Analysing unit:  <AnalysisUnit 'd.adb'> ===
 Subprogram <NullSubpDecl ["P1"] d.adb:2:4-2:25> is skipped
 Subprogram <NullSubpDecl ["P3"] d.adb:5:4-5:25> is skipped
 
-=== Analysing unit:  <AnalysisUnit 'e-p2.adb'> """
+=== Analysing unit:  <AnalysisUnit 'e-p2.adb'> ===
 Subprogram <SubpBody ["P2"] e-p2.adb:2:1-5:5> is analyzed
 
-=== Analysing unit:  <AnalysisUnit 'e.adb'> """
+=== Analysing unit:  <AnalysisUnit 'e.adb'> ===
 Subprogram <SubpBody ["P1"] e.adb:2:4-5:11> is analyzed
 Subprogram <SubpBody ["P3"] e.adb:8:4-11:11> is skipped
 
-=== Analysing unit:  <AnalysisUnit 'f.adb'> """
+=== Analysing unit:  <AnalysisUnit 'f.adb'> ===
 Subprogram <SubpBody ["P"] f.adb:3:4-17:10> is analyzed
 Subprogram <SubpBody ["Q"] f.adb:6:7-9:13> is skipped
 Subprogram <NullSubpDecl ["R"] f.adb:14:7-14:27> is analyzed
 
-=== Analysing unit:  <AnalysisUnit 'g.adb'> """
+=== Analysing unit:  <AnalysisUnit 'g.adb'> ===
 Subprogram <NullSubpDecl ["P"] g.adb:3:7-3:27> is skipped
 Subprogram <SubpBody ["F"] g.adb:11:7-14:13> is skipped
 Subprogram <NullSubpDecl ["Q"] g.adb:16:7-16:27> is skipped
diff --git a/testsuite/tests/properties/is_spark/aspect/test.py b/testsuite/tests/properties/is_spark/aspect/test.py
index b12ee3de2..b2c577b35 100644
--- a/testsuite/tests/properties/is_spark/aspect/test.py
+++ b/testsuite/tests/properties/is_spark/aspect/test.py
@@ -13,10 +13,10 @@
     unit = context.get_from_file(filename)
     subprograms = unit.root.findall(lal.BaseSubpBody)
     if subprograms:
-        print('=== Analysing unit: ', unit, '"""')
+        print('=== Analysing unit: ', unit, '===')
         for subprogram in subprograms:
             print("Subprogram {} is {}".format(
                 subprogram,
-                "analyzed" if subprogram.p_is_spark else "skipped"
+                "analyzed" if subprogram.p_is_spark() else "skipped"
             ))
         print('')
diff --git a/testsuite/tests/properties/is_spark/configuration_pragma_1/test.out b/testsuite/tests/properties/is_spark/configuration_pragma_1/test.out
index 1e21a345a..135d885a8 100644
--- a/testsuite/tests/properties/is_spark/configuration_pragma_1/test.out
+++ b/testsuite/tests/properties/is_spark/configuration_pragma_1/test.out
@@ -1,4 +1,4 @@
-=== Analysing unit:  <AnalysisUnit 'test.adb'> """
+=== Analysing unit:  <AnalysisUnit 'test.adb'> ===
 Subprogram <NullSubpDecl ["P"] test.adb:2:4-2:24> is analyzed
 Subprogram <NullSubpDecl ["Q"] test.adb:3:4-3:24> is analyzed
 Subprogram <NullSubpDecl ["R"] test.adb:4:4-4:24> is skipped
@@ -6,3 +6,11 @@ Subprogram <NullSubpDecl ["S"] test.adb:5:4-5:24> is skipped
 Subprogram <NullSubpDecl ["T"] test.adb:6:4-6:47> is skipped
 Subprogram <NullSubpDecl ["U"] test.adb:7:4-7:46> is analyzed
 
+=== Re-analysing unit (ignoring Skip_Proof annotations):  <AnalysisUnit 'test.adb'> ===
+Subprogram <NullSubpDecl ["P"] test.adb:2:4-2:24> is analyzed
+Subprogram <NullSubpDecl ["Q"] test.adb:3:4-3:24> is analyzed
+Subprogram <NullSubpDecl ["R"] test.adb:4:4-4:24> is analyzed
+Subprogram <NullSubpDecl ["S"] test.adb:5:4-5:24> is analyzed
+Subprogram <NullSubpDecl ["T"] test.adb:6:4-6:47> is skipped
+Subprogram <NullSubpDecl ["U"] test.adb:7:4-7:46> is analyzed
+
diff --git a/testsuite/tests/properties/is_spark/configuration_pragma_1/test.py b/testsuite/tests/properties/is_spark/configuration_pragma_1/test.py
index c885577de..700152bf3 100644
--- a/testsuite/tests/properties/is_spark/configuration_pragma_1/test.py
+++ b/testsuite/tests/properties/is_spark/configuration_pragma_1/test.py
@@ -13,10 +13,18 @@
     unit = context.get_from_file(filename)
     subprograms = unit.root.findall(lal.BaseSubpBody)
     if subprograms:
-        print('=== Analysing unit: ', unit, '"""')
+        print('=== Analysing unit: ', unit, '===')
         for subprogram in subprograms:
             print("Subprogram {} is {}".format(
                 subprogram,
-                "analyzed" if subprogram.p_is_spark else "skipped"
+                "analyzed" if subprogram.p_is_spark() else "skipped"
+            ))
+        print('')
+        print('=== Re-analysing unit (ignoring Skip_Proof annotations): ',
+              unit, '===')
+        for subprogram in subprograms:
+            print("Subprogram {} is {}".format(
+                subprogram,
+                "analyzed" if subprogram.p_is_spark(False) else "skipped"
             ))
         print('')
diff --git a/testsuite/tests/properties/is_spark/configuration_pragma_2/test.out b/testsuite/tests/properties/is_spark/configuration_pragma_2/test.out
index 8ac5dbf8e..65c9dbe8b 100644
--- a/testsuite/tests/properties/is_spark/configuration_pragma_2/test.out
+++ b/testsuite/tests/properties/is_spark/configuration_pragma_2/test.out
@@ -1,4 +1,4 @@
-=== Analysing unit:  <AnalysisUnit 'test.adb'> """
+=== Analysing unit:  <AnalysisUnit 'test.adb'> ===
 Subprogram <NullSubpDecl ["P"] test.adb:2:4-2:24> is skipped
 Subprogram <NullSubpDecl ["Q"] test.adb:3:4-3:24> is skipped
 Subprogram <NullSubpDecl ["R"] test.adb:4:4-4:24> is skipped
diff --git a/testsuite/tests/properties/is_spark/configuration_pragma_2/test.py b/testsuite/tests/properties/is_spark/configuration_pragma_2/test.py
index c885577de..5c641fcbf 100644
--- a/testsuite/tests/properties/is_spark/configuration_pragma_2/test.py
+++ b/testsuite/tests/properties/is_spark/configuration_pragma_2/test.py
@@ -13,10 +13,10 @@
     unit = context.get_from_file(filename)
     subprograms = unit.root.findall(lal.BaseSubpBody)
     if subprograms:
-        print('=== Analysing unit: ', unit, '"""')
+        print('=== Analysing unit: ', unit, '===')
         for subprogram in subprograms:
             print("Subprogram {} is {}".format(
                 subprogram,
-                "analyzed" if subprogram.p_is_spark else "skipped"
+                "analyzed" if subprogram.p_is_spark() else "skipped"
             ))
         print('')
diff --git a/testsuite/tests/properties/is_spark/configuration_pragma_3/test.out b/testsuite/tests/properties/is_spark/configuration_pragma_3/test.out
index 58152ab61..961191622 100644
--- a/testsuite/tests/properties/is_spark/configuration_pragma_3/test.out
+++ b/testsuite/tests/properties/is_spark/configuration_pragma_3/test.out
@@ -1,4 +1,4 @@
-=== Analysing unit:  <AnalysisUnit 'test.adb'> """
+=== Analysing unit:  <AnalysisUnit 'test.adb'> ===
 Subprogram <NullSubpDecl ["P"] test.adb:4:4-4:24> is skipped
 Subprogram <NullSubpDecl ["Q"] test.adb:5:4-5:24> is skipped
 Subprogram <NullSubpDecl ["R"] test.adb:6:4-6:24> is skipped
diff --git a/testsuite/tests/properties/is_spark/configuration_pragma_3/test.py b/testsuite/tests/properties/is_spark/configuration_pragma_3/test.py
index c885577de..5c641fcbf 100644
--- a/testsuite/tests/properties/is_spark/configuration_pragma_3/test.py
+++ b/testsuite/tests/properties/is_spark/configuration_pragma_3/test.py
@@ -13,10 +13,10 @@
     unit = context.get_from_file(filename)
     subprograms = unit.root.findall(lal.BaseSubpBody)
     if subprograms:
-        print('=== Analysing unit: ', unit, '"""')
+        print('=== Analysing unit: ', unit, '===')
         for subprogram in subprograms:
             print("Subprogram {} is {}".format(
                 subprogram,
-                "analyzed" if subprogram.p_is_spark else "skipped"
+                "analyzed" if subprogram.p_is_spark() else "skipped"
             ))
         print('')
diff --git a/testsuite/tests/properties/is_spark/configuration_pragma_4/test.out b/testsuite/tests/properties/is_spark/configuration_pragma_4/test.out
index 4f1a43b0e..72ba90a49 100644
--- a/testsuite/tests/properties/is_spark/configuration_pragma_4/test.out
+++ b/testsuite/tests/properties/is_spark/configuration_pragma_4/test.out
@@ -1,4 +1,4 @@
-=== Analysing unit:  <AnalysisUnit 'test.adb'> """
+=== Analysing unit:  <AnalysisUnit 'test.adb'> ===
 Subprogram <NullSubpDecl ["P"] test.adb:2:4-2:24> is skipped
 Subprogram <NullSubpDecl ["Q"] test.adb:5:4-5:24> is skipped
 Subprogram <NullSubpDecl ["R"] test.adb:8:4-8:24> is skipped
diff --git a/testsuite/tests/properties/is_spark/configuration_pragma_4/test.py b/testsuite/tests/properties/is_spark/configuration_pragma_4/test.py
index b12ee3de2..b2c577b35 100644
--- a/testsuite/tests/properties/is_spark/configuration_pragma_4/test.py
+++ b/testsuite/tests/properties/is_spark/configuration_pragma_4/test.py
@@ -13,10 +13,10 @@
     unit = context.get_from_file(filename)
     subprograms = unit.root.findall(lal.BaseSubpBody)
     if subprograms:
-        print('=== Analysing unit: ', unit, '"""')
+        print('=== Analysing unit: ', unit, '===')
         for subprogram in subprograms:
             print("Subprogram {} is {}".format(
                 subprogram,
-                "analyzed" if subprogram.p_is_spark else "skipped"
+                "analyzed" if subprogram.p_is_spark() else "skipped"
             ))
         print('')
diff --git a/testsuite/tests/properties/is_spark/mixed_pragma_and_aspect/test.out b/testsuite/tests/properties/is_spark/mixed_pragma_and_aspect/test.out
index 3786370b5..5d4ee164b 100644
--- a/testsuite/tests/properties/is_spark/mixed_pragma_and_aspect/test.out
+++ b/testsuite/tests/properties/is_spark/mixed_pragma_and_aspect/test.out
@@ -1,35 +1,35 @@
-=== Analysing unit:  <AnalysisUnit 'a.adb'> """
+=== Analysing unit:  <AnalysisUnit 'a.adb'> ===
 Subprogram <NullSubpDecl ["P"] a.adb:3:4-3:24> is skipped
 Subprogram <NullSubpDecl ["Q"] a.adb:4:4-4:24> is skipped
 
-=== Analysing unit:  <AnalysisUnit 'b.adb'> """
+=== Analysing unit:  <AnalysisUnit 'b.adb'> ===
 Subprogram <NullSubpDecl ["P"] b.adb:2:4-2:24> is skipped
 Subprogram <NullSubpDecl ["Q"] b.adb:3:4-3:24> is skipped
 
-=== Analysing unit:  <AnalysisUnit 'c.adb'> """
+=== Analysing unit:  <AnalysisUnit 'c.adb'> ===
 Subprogram <NullSubpDecl ["P"] c.adb:3:4-3:24> is skipped
 Subprogram <NullSubpDecl ["Q"] c.adb:4:4-4:24> is skipped
 
-=== Analysing unit:  <AnalysisUnit 'd-p2.adb'> """
+=== Analysing unit:  <AnalysisUnit 'd-p2.adb'> ===
 Subprogram <SubpBody ["P2"] d-p2.adb:2:1-5:5> is skipped
 
-=== Analysing unit:  <AnalysisUnit 'd.adb'> """
+=== Analysing unit:  <AnalysisUnit 'd.adb'> ===
 Subprogram <NullSubpDecl ["P1"] d.adb:2:4-2:25> is skipped
 Subprogram <NullSubpDecl ["P3"] d.adb:4:4-4:25> is skipped
 
-=== Analysing unit:  <AnalysisUnit 'e-p2.adb'> """
+=== Analysing unit:  <AnalysisUnit 'e-p2.adb'> ===
 Subprogram <SubpBody ["P2"] e-p2.adb:2:1-5:5> is analyzed
 
-=== Analysing unit:  <AnalysisUnit 'e.adb'> """
+=== Analysing unit:  <AnalysisUnit 'e.adb'> ===
 Subprogram <SubpBody ["P1"] e.adb:2:4-5:11> is analyzed
 Subprogram <SubpBody ["P3"] e.adb:8:4-12:11> is skipped
 
-=== Analysing unit:  <AnalysisUnit 'f.adb'> """
+=== Analysing unit:  <AnalysisUnit 'f.adb'> ===
 Subprogram <SubpBody ["P"] f.adb:3:4-19:10> is analyzed
 Subprogram <SubpBody ["Q"] f.adb:6:7-10:13> is skipped
 Subprogram <NullSubpDecl ["R"] f.adb:15:7-15:27> is analyzed
 
-=== Analysing unit:  <AnalysisUnit 'g.adb'> """
+=== Analysing unit:  <AnalysisUnit 'g.adb'> ===
 Subprogram <NullSubpDecl ["P"] g.adb:3:7-3:27> is skipped
 Subprogram <SubpBody ["F"] g.adb:11:7-14:13> is skipped
 Subprogram <NullSubpDecl ["Q"] g.adb:16:7-16:27> is skipped
diff --git a/testsuite/tests/properties/is_spark/mixed_pragma_and_aspect/test.py b/testsuite/tests/properties/is_spark/mixed_pragma_and_aspect/test.py
index b12ee3de2..b2c577b35 100644
--- a/testsuite/tests/properties/is_spark/mixed_pragma_and_aspect/test.py
+++ b/testsuite/tests/properties/is_spark/mixed_pragma_and_aspect/test.py
@@ -13,10 +13,10 @@
     unit = context.get_from_file(filename)
     subprograms = unit.root.findall(lal.BaseSubpBody)
     if subprograms:
-        print('=== Analysing unit: ', unit, '"""')
+        print('=== Analysing unit: ', unit, '===')
         for subprogram in subprograms:
             print("Subprogram {} is {}".format(
                 subprogram,
-                "analyzed" if subprogram.p_is_spark else "skipped"
+                "analyzed" if subprogram.p_is_spark() else "skipped"
             ))
         print('')
diff --git a/testsuite/tests/properties/is_spark/pkg_private_and_body/test.out b/testsuite/tests/properties/is_spark/pkg_private_and_body/test.out
index 91c808834..dab2fd66f 100644
--- a/testsuite/tests/properties/is_spark/pkg_private_and_body/test.out
+++ b/testsuite/tests/properties/is_spark/pkg_private_and_body/test.out
@@ -1,24 +1,24 @@
-=== Analysing unit:  <AnalysisUnit 'test.ads'> """
+=== Analysing unit:  <AnalysisUnit 'test.ads'> ===
 Subprogram <ExprFunction ["F1"] test.ads:6:4-6:64> is skipped
 Subprogram <ExprFunction ["F2"] test.ads:8:4-8:63> is analyzed
 Subprogram <ExprFunction ["F3"] test.ads:10:4-10:41> is skipped
 
-=== Analysing unit:  <AnalysisUnit 'test2.adb'> """
+=== Analysing unit:  <AnalysisUnit 'test2.adb'> ===
 Subprogram <ExprFunction ["F10"] test2.adb:5:4-5:42> is analyzed
 
-=== Analysing unit:  <AnalysisUnit 'test2.ads'> """
+=== Analysing unit:  <AnalysisUnit 'test2.ads'> ===
 Subprogram <ExprFunction ["F1"] test2.ads:6:4-6:41> is analyzed
 Subprogram <ExprFunction ["F2"] test2.ads:8:4-8:64> is skipped
 Subprogram <ExprFunction ["F3"] test2.ads:10:4-10:41> is skipped
 Subprogram <ExprFunction ["F4"] test2.ads:13:4-13:41> is skipped
 
-=== Analysing unit:  <AnalysisUnit 'test3.ads'> """
+=== Analysing unit:  <AnalysisUnit 'test3.ads'> ===
 Subprogram <ExprFunction ["F1"] test3.ads:4:4-4:41> is analyzed
 Subprogram <ExprFunction ["F2"] test3.ads:6:4-6:64> is skipped
 Subprogram <ExprFunction ["F3"] test3.ads:8:4-8:41> is skipped
 Subprogram <ExprFunction ["F4"] test3.ads:11:4-11:41> is skipped
 
-=== Analysing unit:  <AnalysisUnit 'test4.adb'> """
+=== Analysing unit:  <AnalysisUnit 'test4.adb'> ===
 Subprogram <NullSubpDecl ["P"] test4.adb:4:4-4:24> is analyzed
 Subprogram <SubpBody ["Q"] test4.adb:6:4-31:10> is analyzed
 Subprogram <SubpBody ["K"] test4.adb:12:7-16:13> is skipped
@@ -28,6 +28,6 @@ Subprogram <SubpBody ["P"] test4.adb:34:7-44:13> is analyzed
 Subprogram <NullSubpDecl ["K"] test4.adb:40:13-40:33> is analyzed
 Subprogram <NullSubpDecl ["P"] test4.adb:52:7-52:27> is analyzed
 
-=== Analysing unit:  <AnalysisUnit 'test5.adb'> """
+=== Analysing unit:  <AnalysisUnit 'test5.adb'> ===
 Subprogram <ExprFunction ["F"] test5.adb:4:7-4:43> is analyzed
 
diff --git a/testsuite/tests/properties/is_spark/pkg_private_and_body/test.py b/testsuite/tests/properties/is_spark/pkg_private_and_body/test.py
index e8af6933b..6a8f9bdfa 100644
--- a/testsuite/tests/properties/is_spark/pkg_private_and_body/test.py
+++ b/testsuite/tests/properties/is_spark/pkg_private_and_body/test.py
@@ -12,10 +12,10 @@
     unit = context.get_from_file(filename)
     subprograms = unit.root.findall(lal.BaseSubpBody)
     if subprograms:
-        print('=== Analysing unit: ', unit, '"""')
+        print('=== Analysing unit: ', unit, '===')
         for subprogram in subprograms:
             print("Subprogram {} is {}".format(
                 subprogram,
-                "analyzed" if subprogram.p_is_spark else "skipped"
+                "analyzed" if subprogram.p_is_spark() else "skipped"
             ))
         print('')
diff --git a/testsuite/tests/properties/is_spark/pragma/test.out b/testsuite/tests/properties/is_spark/pragma/test.out
index 61a16f501..d1ec1d7b4 100644
--- a/testsuite/tests/properties/is_spark/pragma/test.out
+++ b/testsuite/tests/properties/is_spark/pragma/test.out
@@ -1,36 +1,36 @@
-=== Analysing unit:  <AnalysisUnit 'a.adb'> """
+=== Analysing unit:  <AnalysisUnit 'a.adb'> ===
 Subprogram <NullSubpDecl ["P"] a.adb:3:4-3:24> is skipped
 Subprogram <NullSubpDecl ["Q"] a.adb:4:4-4:24> is skipped
 
-=== Analysing unit:  <AnalysisUnit 'b.adb'> """
+=== Analysing unit:  <AnalysisUnit 'b.adb'> ===
 Subprogram <NullSubpDecl ["P"] b.adb:2:4-2:24> is skipped
 Subprogram <NullSubpDecl ["Q"] b.adb:3:4-3:24> is skipped
 
-=== Analysing unit:  <AnalysisUnit 'c.adb'> """
+=== Analysing unit:  <AnalysisUnit 'c.adb'> ===
 Subprogram <NullSubpDecl ["P"] c.adb:3:4-3:24> is skipped
 Subprogram <NullSubpDecl ["Q"] c.adb:4:4-4:24> is skipped
 
-=== Analysing unit:  <AnalysisUnit 'd-p2.adb'> """
+=== Analysing unit:  <AnalysisUnit 'd-p2.adb'> ===
 Subprogram <SubpBody ["P2"] d-p2.adb:2:1-5:5> is skipped
 
-=== Analysing unit:  <AnalysisUnit 'd.adb'> """
+=== Analysing unit:  <AnalysisUnit 'd.adb'> ===
 Subprogram <NullSubpDecl ["P1"] d.adb:2:4-2:25> is skipped
 Subprogram <NullSubpDecl ["P3"] d.adb:4:4-4:25> is skipped
 
-=== Analysing unit:  <AnalysisUnit 'e-p2.adb'> """
+=== Analysing unit:  <AnalysisUnit 'e-p2.adb'> ===
 Subprogram <SubpBody ["P2"] e-p2.adb:2:1-6:5> is analyzed
 
-=== Analysing unit:  <AnalysisUnit 'e.adb'> """
+=== Analysing unit:  <AnalysisUnit 'e.adb'> ===
 Subprogram <SubpBody ["P1"] e.adb:2:4-6:11> is analyzed
 Subprogram <SubpBody ["P3"] e.adb:9:4-13:11> is skipped
 Subprogram <SubpBody ["P4"] e.adb:15:4-18:11> is skipped
 
-=== Analysing unit:  <AnalysisUnit 'f.adb'> """
+=== Analysing unit:  <AnalysisUnit 'f.adb'> ===
 Subprogram <SubpBody ["P"] f.adb:4:4-23:10> is analyzed
 Subprogram <SubpBody ["Q"] f.adb:10:7-14:13> is skipped
 Subprogram <NullSubpDecl ["R"] f.adb:19:7-19:27> is analyzed
 
-=== Analysing unit:  <AnalysisUnit 'g.adb'> """
+=== Analysing unit:  <AnalysisUnit 'g.adb'> ===
 Subprogram <NullSubpDecl ["P"] g.adb:5:7-5:27> is skipped
 Subprogram <SubpBody ["F"] g.adb:12:7-15:13> is skipped
 Subprogram <NullSubpDecl ["Q"] g.adb:17:7-17:27> is skipped
diff --git a/testsuite/tests/properties/is_spark/pragma/test.py b/testsuite/tests/properties/is_spark/pragma/test.py
index b12ee3de2..b2c577b35 100644
--- a/testsuite/tests/properties/is_spark/pragma/test.py
+++ b/testsuite/tests/properties/is_spark/pragma/test.py
@@ -13,10 +13,10 @@
     unit = context.get_from_file(filename)
     subprograms = unit.root.findall(lal.BaseSubpBody)
     if subprograms:
-        print('=== Analysing unit: ', unit, '"""')
+        print('=== Analysing unit: ', unit, '===')
         for subprogram in subprograms:
             print("Subprogram {} is {}".format(
                 subprogram,
-                "analyzed" if subprogram.p_is_spark else "skipped"
+                "analyzed" if subprogram.p_is_spark() else "skipped"
             ))
         print('')
diff --git a/testsuite/tests/properties/is_spark/skip_flow_and_proof/test.out b/testsuite/tests/properties/is_spark/skip_flow_and_proof/test.out
index 11cce2462..f687e2628 100644
--- a/testsuite/tests/properties/is_spark/skip_flow_and_proof/test.out
+++ b/testsuite/tests/properties/is_spark/skip_flow_and_proof/test.out
@@ -1,4 +1,4 @@
-=== Analysing unit:  <AnalysisUnit 'a.adb'> """
+=== Analysing unit:  <AnalysisUnit 'a.adb'> ===
 Subprogram <SubpBody ["P"] a.adb:4:4-7:10> is skipped
 Subprogram <SubpBody ["Q"] a.adb:10:4-19:10> is skipped
 Subprogram <SubpBody ["QQ"] a.adb:11:7-15:14> is skipped
diff --git a/testsuite/tests/properties/is_spark/skip_flow_and_proof/test.py b/testsuite/tests/properties/is_spark/skip_flow_and_proof/test.py
index b12ee3de2..b2c577b35 100644
--- a/testsuite/tests/properties/is_spark/skip_flow_and_proof/test.py
+++ b/testsuite/tests/properties/is_spark/skip_flow_and_proof/test.py
@@ -13,10 +13,10 @@
     unit = context.get_from_file(filename)
     subprograms = unit.root.findall(lal.BaseSubpBody)
     if subprograms:
-        print('=== Analysing unit: ', unit, '"""')
+        print('=== Analysing unit: ', unit, '===')
         for subprogram in subprograms:
             print("Subprogram {} is {}".format(
                 subprogram,
-                "analyzed" if subprogram.p_is_spark else "skipped"
+                "analyzed" if subprogram.p_is_spark() else "skipped"
             ))
         print('')
diff --git a/testsuite/tests/properties/is_spark/skip_proof/test.out b/testsuite/tests/properties/is_spark/skip_proof/test.out
index 3593112a1..95af721f9 100644
--- a/testsuite/tests/properties/is_spark/skip_proof/test.out
+++ b/testsuite/tests/properties/is_spark/skip_proof/test.out
@@ -1,4 +1,4 @@
-=== Analysing unit:  <AnalysisUnit 'a.adb'> """
+=== Analysing unit:  <AnalysisUnit 'a.adb'> ===
 Subprogram <SubpBody ["P"] a.adb:4:4-7:10> is skipped
 Subprogram <SubpBody ["Q"] a.adb:10:4-19:10> is skipped
 Subprogram <SubpBody ["QQ"] a.adb:11:7-15:14> is skipped
@@ -21,9 +21,9 @@ Subprogram <NullSubpDecl ["V"] a.adb:82:4-82:24> is skipped
 Subprogram <SubpBody ["W"] a.adb:85:4-88:10> is skipped
 Subprogram <SubpBody ["X"] a.adb:91:4-94:10> is skipped
 
-=== Analysing unit:  <AnalysisUnit 'b-p.adb'> """
+=== Analysing unit:  <AnalysisUnit 'b-p.adb'> ===
 Subprogram <SubpBody ["P"] b-p.adb:2:1-5:7> is skipped
 
-=== Analysing unit:  <AnalysisUnit 'b-q.adb'> """
+=== Analysing unit:  <AnalysisUnit 'b-q.adb'> ===
 Subprogram <SubpBody ["Q"] b-q.adb:2:1-5:7> is analyzed
 
diff --git a/testsuite/tests/properties/is_spark/skip_proof/test.py b/testsuite/tests/properties/is_spark/skip_proof/test.py
index b12ee3de2..b2c577b35 100644
--- a/testsuite/tests/properties/is_spark/skip_proof/test.py
+++ b/testsuite/tests/properties/is_spark/skip_proof/test.py
@@ -13,10 +13,10 @@
     unit = context.get_from_file(filename)
     subprograms = unit.root.findall(lal.BaseSubpBody)
     if subprograms:
-        print('=== Analysing unit: ', unit, '"""')
+        print('=== Analysing unit: ', unit, '===')
         for subprogram in subprograms:
             print("Subprogram {} is {}".format(
                 subprogram,
-                "analyzed" if subprogram.p_is_spark else "skipped"
+                "analyzed" if subprogram.p_is_spark() else "skipped"
             ))
         print('')
diff --git a/user_manual/changes/libadalang/1074.yaml b/user_manual/changes/libadalang/1074.yaml
new file mode 100644
index 000000000..aa44a1a35
--- /dev/null
+++ b/user_manual/changes/libadalang/1074.yaml
@@ -0,0 +1,9 @@
+type: api-change
+short_title: Skip annotations in `p_is_spark`
+title: Allow to skip `Skip_Proof` annotations in `p_is_spark`
+description: |
+  The property `p_is_spark` can now take a boolean parameter
+  (`include_skip_proof_annotations`, defaults to `True`) to specify whether the
+  `GNATprove` `Skip_Proof` and `Skip_Flow_And_Proof` annotations should be
+  ignored to determine if a subprogram is in SPARK or not.
+date: 2023-09-12