From: Yannick Moy Date: Tue, 25 Feb 2014 14:51:20 +0000 (+0000) Subject: sem_ch3.adb, [...]: Mark most references to SPARK RM in error messages for removal. X-Git-Tag: upstream/12.2.0~64509 X-Git-Url: http://review.tizen.org/git/?a=commitdiff_plain;h=3684d1fc71263d05352648115737a3cf35a1764b;p=platform%2Fupstream%2Fgcc.git sem_ch3.adb, [...]: Mark most references to SPARK RM in error messages for removal. 2014-02-25 Yannick Moy * sem_ch3.adb, sem_ch5.adb, sem_prag.adb, sem_attr.adb, errout.ads, sem_ch6.adb: Mark most references to SPARK RM in error messages for removal. From-SVN: r208125 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index b3690eb..ac263d9 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,9 @@ +2014-02-25 Yannick Moy + + * sem_ch3.adb, sem_ch5.adb, sem_prag.adb, sem_attr.adb, errout.ads, + sem_ch6.adb: Mark most references to SPARK RM in error messages + for removal. + 2014-02-24 Ed Schonberg * par-ch3.adb (P_Basic_Declarative_Items): If an improper body diff --git a/gcc/ada/errout.ads b/gcc/ada/errout.ads index 84d7490..6895a5b 100644 --- a/gcc/ada/errout.ads +++ b/gcc/ada/errout.ads @@ -316,6 +316,10 @@ package Errout is -- quotes are added unless manual quotation mode is currently set. -- RM and SPARK are special exceptions, they are never treated as -- keywords, and just appear verbatim, with no surrounding quotes. + -- As a special case, 'R'M is used instead of RM (which is not treated + -- as a keyword) to indicate when the reference to the RM is possibly + -- not useful anymore, and could possibly be replaced by a comment + -- in the source. -- Insertion character ` (Backquote: set manual quotation mode) -- The backquote character always appears in pairs. Each backquote of @@ -327,7 +331,7 @@ package Errout is -- Insertion character ' (Quote: literal character) -- Precedes a character which is placed literally into the message. -- Used to insert characters into messages that are one of the - -- insertion characters defined here. Also used when insertion + -- insertion characters defined here. Also used for insertion of -- upper case letter sequences not to be treated as keywords. -- Insertion character \ (Backslash: continuation message) diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb index f45fe2a..45210e4 100644 --- a/gcc/ada/sem_attr.adb +++ b/gcc/ada/sem_attr.adb @@ -4484,7 +4484,7 @@ package body Sem_Attr is else Error_Attr ("attribute % cannot appear in the condition of a contract " - & "case (SPARK RM 6.1.3(2))", P); + & "case (SPARK 'R'M 6.1.3(2))", P); end if; end Check_Use_In_Contract_Cases; diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 6289f1c..1c11473 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -2999,7 +2999,7 @@ package body Sem_Ch3 is and then No (Corresponding_Generic_Association (Parent (Obj_Id))) then Error_Msg_N - ("constant cannot be volatile (SPARK RM 7.1.3(6))", Obj_Id); + ("constant cannot be volatile (SPARK 'R'M 7.1.3(6))", Obj_Id); end if; else pragma Assert (Ekind (Obj_Id) = E_Variable); @@ -3016,7 +3016,7 @@ package body Sem_Ch3 is then Error_Msg_N ("non-volatile variable & cannot have volatile components " - & "(SPARK RM 7.1.3(7))", Obj_Id); + & "(SPARK 'R'M 7.1.3(7))", Obj_Id); -- The declaration of a volatile object must appear at the library -- level. @@ -18048,7 +18048,7 @@ package body Sem_Ch3 is and then Is_SPARK_Volatile_Object (Defining_Identifier (Discr)) then Error_Msg_N - ("discriminant cannot be volatile (SPARK RM 7.1.3(6))", Discr); + ("discriminant cannot be volatile (SPARK 'R'M 7.1.3(6))", Discr); end if; Next (Discr); diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb index a4eaa56..13f0a48 100644 --- a/gcc/ada/sem_ch5.adb +++ b/gcc/ada/sem_ch5.adb @@ -1972,7 +1972,7 @@ package body Sem_Ch5 is and then Is_SPARK_Volatile_Object (Ent) then Error_Msg_N - ("loop parameter cannot be volatile (SPARK RM 7.1.3(6))", Ent); + ("loop parameter cannot be volatile (SPARK 'R'M 7.1.3(6))", Ent); end if; end Analyze_Iterator_Specification; @@ -2618,7 +2618,7 @@ package body Sem_Ch5 is if SPARK_Mode = On and then Is_SPARK_Volatile_Object (Id) then Error_Msg_N - ("loop parameter cannot be volatile (SPARK RM 7.1.3(6))", Id); + ("loop parameter cannot be volatile (SPARK 'R'M 7.1.3(6))", Id); end if; end Analyze_Loop_Parameter_Specification; diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index f456131..2bfb8bb 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -11421,14 +11421,14 @@ package body Sem_Ch6 is if Ekind_In (Formal, E_In_Out_Parameter, E_Out_Parameter) then Error_Msg_N ("function cannot have parameter of mode `OUT` or `IN OUT` " - & "(SPARK RM 6.1)", Formal); + & "(SPARK 'R'M 6.1)", Formal); -- A function cannot have a volatile formal parameter elsif Is_SPARK_Volatile_Object (Formal) then Error_Msg_N ("function cannot have a volatile formal parameter " - & "(SPARK RM 7.1.3(10))", Formal); + & "(SPARK 'R'M 7.1.3(10))", Formal); end if; end if; diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index b7321e8..8047a4c 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -427,7 +427,7 @@ package body Sem_Prag is if Others_Seen then Error_Msg_N ("only one others choice allowed in contract cases " - & "(SPARK RM 6.1.3(1))", Case_Guard); + & "(SPARK 'R'M 6.1.3(1))", Case_Guard); else Others_Seen := True; end if; @@ -435,7 +435,7 @@ package body Sem_Prag is elsif Others_Seen then Error_Msg_N ("others must be the last choice in contract cases " - & "(SPARK RM 6.1.3(1))", N); + & "(SPARK 'R'M 6.1.3(1))", N); end if; -- Preanalyze the case guard and consequence @@ -783,15 +783,15 @@ package body Sem_Prag is Error_Msg_Name_1 := Name_Result; Error_Msg_N ("prefix of attribute % must denote the enclosing " - & "function (SPARK RM 6.1.5(11))", Item); + & "function (SPARK 'R'M 6.1.5(11))", Item); -- Function'Result is allowed to appear on the output side of a -- dependency clause. elsif Is_Input then Error_Msg_N - ("function result cannot act as input (SPARK RM 6.1.5(6))", - Item); + ("function result cannot act as input " + & "(SPARK 'R'M 6.1.5(6))", Item); elsif Null_Seen then Error_Msg_N @@ -821,7 +821,8 @@ package body Sem_Prag is if not Is_Last then Error_Msg_N ("null output list must be the last clause in a " - & "dependency relation (SPARK RM 6.1.5(12))", Item); + & "dependency relation (SPARK 'R'M 6.1.5(12))", + Item); -- Catch a useless dependence of the form: -- null =>+ ... @@ -885,7 +886,7 @@ package body Sem_Prag is then Error_Msg_N ("input of a null output list cannot appear in " - & "multiple input lists (SPARK RM 6.1.5(13))", + & "multiple input lists (SPARK 'R'M 6.1.5(13))", Item); end if; @@ -905,7 +906,7 @@ package body Sem_Prag is Item, Item_Id); Error_Msg_N ("\\use its constituents instead " - & "(SPARK RM 6.1.5(3))", Item); + & "(SPARK 'R'M 6.1.5(3))", Item); return; -- If the reference to the abstract state appears in @@ -947,7 +948,7 @@ package body Sem_Prag is else Error_Msg_N ("item must denote parameter, variable or state " - & "(SPARK RM 6.1.5(1))", Item); + & "(SPARK 'R'M 6.1.5(1))", Item); end if; -- All other input/output items are illegal @@ -955,7 +956,7 @@ package body Sem_Prag is else Error_Msg_N ("item must denote parameter, variable or state " - & "(SPARK RM 6.1.5(1))", Item); + & "(SPARK 'R'M 6.1.5(1))", Item); end if; end if; end Analyze_Input_Output; @@ -1013,7 +1014,7 @@ package body Sem_Prag is if Ekind (Spec_Id) = E_Function and then not Result_Seen then Error_Msg_NE ("result of & must appear in exactly one output list " - & "(SPARK RM 6.1.5(10))", N, Spec_Id); + & "(SPARK 'R'M 6.1.5(10))", N, Spec_Id); end if; end Check_Function_Return; @@ -1195,9 +1196,9 @@ package body Sem_Prag is -- and updating. if Item_Is_Input then - Add_Str_To_Name_Buffer ("(SPARK RM 6.1.5(5))"); + Add_Str_To_Name_Buffer ("(SPARK 'R'M 6.1.5(5))"); else - Add_Str_To_Name_Buffer ("(SPARK RM 6.1.5(6))"); + Add_Str_To_Name_Buffer ("(SPARK 'R'M 6.1.5(6))"); end if; Error_Msg := Name_Find; @@ -1270,7 +1271,7 @@ package body Sem_Prag is Add_Item_To_Name_Buffer (Item_Id); Add_Str_To_Name_Buffer (" & must appear in at least one input dependence list " - & "(SPARK RM 6.1.5(8))"); + & "(SPARK 'R'M 6.1.5(8))"); Error_Msg := Name_Find; Error_Msg_NE (Get_Name_String (Error_Msg), Item, Item_Id); @@ -1284,7 +1285,7 @@ package body Sem_Prag is Add_Item_To_Name_Buffer (Item_Id); Add_Str_To_Name_Buffer (" & must appear in exactly one output dependence list " - & "(SPARK RM 6.1.5(10))"); + & "(SPARK 'R'M 6.1.5(10))"); Error_Msg := Name_Find; Error_Msg_NE (Get_Name_String (Error_Msg), Item, Item_Id); @@ -1496,7 +1497,7 @@ package body Sem_Prag is elsif Is_Attribute_Result (Output) then Error_Msg_N ("function result cannot depend on itself " - & "(SPARK RM 6.1.5(10))", Output); + & "(SPARK 'R'M 6.1.5(10))", Output); return; end if; @@ -1867,7 +1868,7 @@ package body Sem_Prag is else Error_Msg_N ("external property % must apply to a volatile object " - & "(SPARK RM 7.1.3(2))", N); + & "(SPARK 'R'M 7.1.3(2))", N); end if; -- Ensure that the expression (if present) is static Boolean. A missing @@ -1883,7 +1884,7 @@ package body Sem_Prag is else Error_Msg_Name_1 := Pragma_Name (N); Error_Msg_N - ("expression of % must be static (SPARK RM 7.1.2(5))", Expr); + ("expression of % must be static (SPARK 'R'M 7.1.2(5))", Expr); end if; end if; end Analyze_External_Property_In_Decl_Part; @@ -2001,7 +2002,7 @@ package body Sem_Prag is if Scope (Item_Id) = Spec_Id then Error_Msg_NE ("global item cannot reference parameter of subprogram " - & "& (SPARK RM 6.1.4(6))", Item, Spec_Id); + & "& (SPARK 'R'M 6.1.4(6))", Item, Spec_Id); return; end if; @@ -2011,7 +2012,7 @@ package body Sem_Prag is elsif Ekind (Item_Id) = E_Constant then Error_Msg_N ("global item cannot denote a constant " - & "(SPARK RM 6.1.4(7))", Item); + & "(SPARK 'R'M 6.1.4(7))", Item); -- The only legal references are those to abstract states and -- variables. @@ -2019,7 +2020,7 @@ package body Sem_Prag is elsif not Ekind_In (Item_Id, E_Abstract_State, E_Variable) then Error_Msg_N ("global item must denote variable or state " - & "(SPARK RM 6.1.4(4))", Item); + & "(SPARK 'R'M 6.1.4(4))", Item); return; end if; @@ -2036,7 +2037,7 @@ package body Sem_Prag is ("cannot mention state & in global refinement", Item, Item_Id); Error_Msg_N - ("\\use its constituents instead (SPARK RM 6.1.4(8))", + ("\\use its constituents instead (SPARK 'R'M 6.1.4(8))", Item); return; @@ -2063,7 +2064,7 @@ package body Sem_Prag is if Ekind_In (Spec_Id, E_Function, E_Generic_Function) then Error_Msg_NE ("volatile object & cannot act as global item of a " - & "function (SPARK RM 7.1.3(9))", Item, Item_Id); + & "function (SPARK 'R'M 7.1.3(9))", Item, Item_Id); return; -- A volatile object with property Effective_Reads set to @@ -2093,7 +2094,7 @@ package body Sem_Prag is else Error_Msg_N ("global item must denote variable or state " - & "(SPARK RM 6.1.4(4))", Item); + & "(SPARK 'R'M 6.1.4(4))", Item); return; end if; @@ -2109,7 +2110,7 @@ package body Sem_Prag is if Contains (Seen, Item_Id) then Error_Msg_N - ("duplicate global item (SPARK RM 6.1.4(11))", Item); + ("duplicate global item (SPARK 'R'M 6.1.4(11))", Item); -- Add the entity of the current item to the list of processed -- items. @@ -2139,7 +2140,8 @@ package body Sem_Prag is is begin if Status then - Error_Msg_N ("duplicate global mode (SPARK RM 6.1.4(9))", Mode); + Error_Msg_N + ("duplicate global mode (SPARK 'R'M 6.1.4(9))", Mode); end if; Status := True; @@ -2184,7 +2186,7 @@ package body Sem_Prag is then Error_Msg_NE ("global item & cannot have mode In_Out or Output " - & "(SPARK RM 6.1.4(12))", Item, Item_Id); + & "(SPARK 'R'M 6.1.4(12))", Item, Item_Id); Error_Msg_NE ("\\item already appears as input of subprogram &", Item, Context); @@ -2208,7 +2210,7 @@ package body Sem_Prag is if Ekind (Spec_Id) = E_Function then Error_Msg_N ("global mode & is not applicable to functions " - & "(SPARK RM 6.1.4(10))", Mode); + & "(SPARK 'R'M 6.1.4(10))", Mode); end if; end Check_Mode_Restriction_In_Function; @@ -2501,14 +2503,14 @@ package body Sem_Prag is Error_Msg_Name_1 := Chars (Pack_Id); Error_Msg_NE ("initialization item & must appear in the visible " - & "declarations of package % (SPARK RM 7.1.5(7))", + & "declarations of package % (SPARK 'R'M 7.1.5(7))", Item, Item_Id); -- Detect a duplicate use of the same initialization item elsif Contains (Items_Seen, Item_Id) then Error_Msg_N - ("duplicate initialization item (SPARK RM 7.1.5(5))", + ("duplicate initialization item (SPARK 'R'M 7.1.5(5))", Item); -- The item is legal, add it to the list of processed states @@ -2532,7 +2534,7 @@ package body Sem_Prag is else Error_Msg_N ("initialization item must denote variable or state " - & "(SPARK RM 7.1.5(3))", Item); + & "(SPARK 'R'M 7.1.5(3))", Item); end if; -- Some form of illegal construct masquerading as a name @@ -2540,7 +2542,7 @@ package body Sem_Prag is else Error_Msg_N ("initialization item must denote variable or state " - & "(SPARK RM 7.1.5(3))", Item); + & "(SPARK 'R'M 7.1.5(3))", Item); end if; end if; end Analyze_Initialization_Item; @@ -2615,7 +2617,8 @@ package body Sem_Prag is elsif Contains (Inputs_Seen, Input_Id) then Error_Msg_N - ("duplicate input item (SPARK RM 7.1.5(5))", Input); + ("duplicate input item (SPARK 'R'M 7.1.5(5))", + Input); -- Input is legal, add it to the list of processed inputs @@ -10305,7 +10308,7 @@ package body Sem_Prag is else Error_Msg_N ("expression of external state property must be " - & "static (SPARK RM 7.1.2(5))", Expr); + & "static (SPARK 'R'M 7.1.2(5))", Expr); end if; -- The lack of expression defaults the property to True @@ -10398,7 +10401,7 @@ package body Sem_Prag is begin if Status then Error_Msg_N - ("duplicate state option (SPARK RM 7.1.4(1))", Opt); + ("duplicate state option (SPARK 'R'M 7.1.4(1))", Opt); end if; Status := True; @@ -10415,7 +10418,7 @@ package body Sem_Prag is begin if Status then Error_Msg_N - ("duplicate external property (SPARK RM 7.1.4(2))", + ("duplicate external property (SPARK 'R'M 7.1.4(2))", Prop); end if; @@ -10547,7 +10550,7 @@ package body Sem_Prag is elsif Chars (Opt) = Name_Part_Of then Error_Msg_N ("indicator Part_Of must denote an abstract state " - & "(SPARK RM 7.1.4(9))", Opt); + & "(SPARK 'R'M 7.1.4(9))", Opt); else Error_Msg_N @@ -11526,7 +11529,8 @@ package body Sem_Prag is -- construct, issue a generic error. Error_Pragma - ("pragma % must apply to a volatile object (SPARK RM 7.1.3(2))"); + ("pragma % must apply to a volatile object " + & "(SPARK 'R'M 7.1.3(2))"); end Async_Effective; ------------------ @@ -18925,7 +18929,7 @@ package body Sem_Prag is then Error_Msg_NE ("useless refinement, package & does not define abstract " - & "states (SPARK RM 7.2.2(3))", N, Spec_Id); + & "states (SPARK 'R'M 7.2.2(3))", N, Spec_Id); return; end if; @@ -22346,7 +22350,7 @@ package body Sem_Prag is if No (Depends) then Error_Msg_NE ("useless refinement, declaration of subprogram & lacks aspect or " - & "pragma Depends (SPARK RM 7.2.5(2))", N, Spec_Id); + & "pragma Depends (SPARK 'R'M 7.2.5(2))", N, Spec_Id); return; end if; @@ -22359,7 +22363,8 @@ package body Sem_Prag is if Nkind (Deps) = N_Null then Error_Msg_NE ("useless refinement, subprogram & does not depend on abstract " - & "state with visible refinement (SPARK RM 7.2.5(2))", N, Spec_Id); + & "state with visible refinement (SPARK 'R'M 7.2.5(2))", + N, Spec_Id); return; end if; @@ -22548,7 +22553,7 @@ package body Sem_Prag is Error_Msg_Name_1 := Chars (State_Id); Error_Msg_NE ("constituent & of state % must have mode Input, In_Out " - & "or Output in global refinement (SPARK RM 7.2.4(5))", + & "or Output in global refinement (SPARK 'R'M 7.2.4(5))", N, Constit_Id); else @@ -22578,7 +22583,7 @@ package body Sem_Prag is else Error_Msg_NE ("global refinement of state & redefines the mode of its " - & "constituents (SPARK RM 7.2.4(5))", N, State_Id); + & "constituents (SPARK 'R'M 7.2.4(5))", N, State_Id); end if; end Check_Constituent_Usage; @@ -22651,7 +22656,7 @@ package body Sem_Prag is Error_Msg_Name_1 := Chars (State_Id); Error_Msg_NE ("constituent & of state % must have mode Input in global " - & "refinement (SPARK RM 7.2.4(5))", N, Constit_Id); + & "refinement (SPARK 'R'M 7.2.4(5))", N, Constit_Id); end if; Next_Elmt (Constit_Elmt); @@ -22733,7 +22738,8 @@ package body Sem_Prag is Error_Msg_Name_1 := Chars (State_Id); Error_Msg_NE ("constituent & of state % must have mode Output in " - & "global refinement (SPARK RM 7.2.4(5))", N, Constit_Id); + & "global refinement (SPARK 'R'M 7.2.4(5))", + N, Constit_Id); -- The constituent is altogether missing @@ -22743,7 +22749,7 @@ package body Sem_Prag is Error_Msg_NE ("output state & must be replaced by all its " & "constituents in global refinement " - & "(SPARK RM 7.2.5(3))", N, State_Id); + & "(SPARK 'R'M 7.2.5(3))", N, State_Id); end if; Error_Msg_NE @@ -22824,7 +22830,8 @@ package body Sem_Prag is Error_Msg_Name_1 := Chars (State_Id); Error_Msg_NE ("constituent & of state % must have mode Proof_In in " - & "global refinement (SPARK RM 7.2.4(5))", N, Constit_Id); + & "global refinement (SPARK 'R'M 7.2.4(5))", + N, Constit_Id); end if; Next_Elmt (Constit_Elmt); @@ -22960,7 +22967,7 @@ package body Sem_Prag is else Error_Msg_NE - ("extra global item & (SPARK RM 7.2.4(3))", Item, Item_Id); + ("extra global item & (SPARK 'R'M 7.2.4(3))", Item, Item_Id); end if; end Check_Refined_Global_Item; @@ -23141,7 +23148,8 @@ package body Sem_Prag is then Error_Msg_NE ("useless refinement, subprogram & does not depends on abstract " - & "state with visible refinement (SPARK RM 7.2.4(2))", N, Spec_Id); + & "state with visible refinement (SPARK 'R'M 7.2.4(2))", + N, Spec_Id); return; end if; @@ -23438,7 +23446,7 @@ package body Sem_Prag is Error_Msg_Name_1 := Chars (Spec_Id); Error_Msg_NE ("cannot use & in refinement, constituent is not a hidden " - & "state of package % (SPARK RM 7.2.2(9))", + & "state of package % (SPARK 'R'M 7.2.2(9))", Constit, Constit_Id); end if; end Check_Matching_Constituent; @@ -23531,7 +23539,7 @@ package body Sem_Prag is if No (Constit) then Error_Msg_NE ("external state & requires at least one constituent with " - & "property % (SPARK RM 7.2.8(3))", State, State_Id); + & "property % (SPARK 'R'M 7.2.8(3))", State, State_Id); end if; -- The property is missing in the declaration of the state, but a @@ -23541,7 +23549,7 @@ package body Sem_Prag is Error_Msg_Name_2 := Chars (Constit); Error_Msg_NE ("external state & lacks property % set by constituent % " - & "(SPARK RM 7.2.8(3))", State, State_Id); + & "(SPARK 'R'M 7.2.8(3))", State, State_Id); end if; end Check_External_Property; @@ -23557,7 +23565,7 @@ package body Sem_Prag is if Contains (Refined_States_Seen, State_Id) then Error_Msg_NE - ("duplicate refinement of state & (SPARK RM 7.2.2(8))", + ("duplicate refinement of state & (SPARK 'R'M 7.2.2(8))", State, State_Id); return; end if; @@ -23690,7 +23698,7 @@ package body Sem_Prag is Body_Ref := Node (Body_Ref_Elmt); Error_Msg_N - ("reference to & not allowed (SPARK RM 6.1.4(8))", + ("reference to & not allowed (SPARK 'R'M 6.1.4(8))", Body_Ref); Error_Msg_Sloc := Sloc (State); Error_Msg_N ("\\refinement of & is visible#", Body_Ref); @@ -23788,7 +23796,7 @@ package body Sem_Prag is else Error_Msg_NE ("external state & requires at least one external " - & "constituent or null refinement (SPARK RM 7.2.8(2))", + & "constituent or null refinement (SPARK 'R'M 7.2.8(2))", State, State_Id); end if; @@ -23798,7 +23806,7 @@ package body Sem_Prag is elsif External_Constit_Seen then Error_Msg_NE ("non-external state & cannot contain external constituents in " - & "refinement (SPARK RM 7.2.8(1))", State, State_Id); + & "refinement (SPARK 'R'M 7.2.8(1))", State, State_Id); end if; -- Ensure that all Part_Of candidate constituents have been mentioned @@ -24733,7 +24741,7 @@ package body Sem_Prag is Error_Msg_Name_1 := Chars (Constit_Id); Error_Msg_NE ("cannot mention state & and its constituent % in the same " - & "context (SPARK RM 7.2.6(7))", Context, State_Id); + & "context (SPARK 'R'M 7.2.6(7))", Context, State_Id); exit; end if;