Merge branch 'topic/1074' into 'master'

Allow to skip `Skip_Proof` annotations in `p_is_spark` Closes #1074 See merge request eng/libadalang/libadalang!1406
AdaCore · Sep 12, 2023 · 4ec5f4f · 4ec5f4f
2 parents ec1825f + 4d4d76d
commit 4ec5f4f
Show file tree

Hide file tree

Showing 22 changed files with 88 additions and 63 deletions.
diff --git a/ada/ast.py b/ada/ast.py
@@ -20696,15 +20696,15 @@ 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.
         """
         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
@@ -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
@@ -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
@@ -1,8 +1,16 @@
-=== 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
 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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