diff mbox series

[Ada] SCOs: generate 'P' decisions for [Type_]Invariant pragmas

Message ID 20210921152631.GA3094928@adacore.com
State Committed
Commit 57fb9d3820cd955ba0af1baadb27cd9a756a87c8
Headers
Series [Ada] SCOs: generate 'P' decisions for [Type_]Invariant pragmas |

Commit Message

Pierre-Marie de Rodat Sept. 21, 2021, 3:26 p.m. UTC 
  Those pragmas should be dealt with in the same way as their equivalent
aspects.

Tested on x86_64-pc-linux-gnu, committed on trunk

gcc/ada/

	* par_sco.adb (Traverse_One): Add support for pragma Invariant /
	Type_Invariant.
diff mbox series

Patch

diff --git a/gcc/ada/par_sco.adb b/gcc/ada/par_sco.adb
--- a/gcc/ada/par_sco.adb
+++ b/gcc/ada/par_sco.adb
@@ -2248,6 +2248,8 @@  package body Par_SCO is
                         | Name_Loop_Invariant
                         | Name_Postcondition
                         | Name_Precondition
+                        | Name_Type_Invariant
+                        | Name_Invariant
                      =>
                         --  For Assert/Check/Precondition/Postcondition, we
                         --  must generate a P entry for the decision. Note
@@ -2256,7 +2258,10 @@  package body Par_SCO is
                         --  on when we output the decision line in Put_SCOs,
                         --  depending on setting by Set_SCO_Pragma_Enabled.
 
-                        if Nam = Name_Check then
+                        if Nam = Name_Check
+                           or else Nam = Name_Type_Invariant
+                           or else Nam = Name_Invariant
+                        then
                            Next (Arg);
                         end if;
 
@@ -2285,8 +2290,7 @@  package body Par_SCO is
                      --  never disabled.
 
                      --  Should generate P decisions (not X) for assertion
-                     --  related pragmas: [Type_]Invariant,
-                     --  [{Static,Dynamic}_]Predicate???
+                     --  related pragmas: [{Static,Dynamic}_]Predicate???
 
                      when others =>
                         Process_Decisions_Defer (N, 'X');