From daec8eebdb7a3cfd3e59771455d24fac9adb151e Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Mon, 1 Aug 2011 15:34:50 +0000 Subject: [PATCH] par-endh.adb (Check_End): issue a syntax error in SPARK mode for missing label at end of declaration... 2011-08-01 Yannick Moy * par-endh.adb (Check_End): issue a syntax error in SPARK mode for missing label at end of declaration (subprogram or package) * par-ch4.adb (P_Name): issue a syntax error in SPARK mode for mixing of positional and named parameter association * par.adb, par-util.adb (Formal_Error_Msg_SP): new wrapper on Error_Msg_SP which adds a prefix to the error message giving the name of the formal language analyzed * sem_ch6.adb (Analyze_Return_Type): issue an error in formal mode for access result type in subprogram, unconstrained array as result type,. (Analyze_Subprogram_Declaration): issue an error in formal mode for null procedure * sem_ch8.adb: Code clean up. From-SVN: r177048 --- gcc/ada/ChangeLog | 15 +++++++++++++++ gcc/ada/par-ch4.adb | 4 ++++ gcc/ada/par-endh.adb | 11 +++++++++++ gcc/ada/par-util.adb | 10 ++++++++++ gcc/ada/par.adb | 4 ++++ gcc/ada/sem_ch6.adb | 27 +++++++++++++++++++++++++++ gcc/ada/sem_ch8.adb | 1 + 7 files changed, 72 insertions(+) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 0c0b22f7e1f..868af9bb1df 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,18 @@ +2011-08-01 Yannick Moy + + * par-endh.adb (Check_End): issue a syntax error in SPARK mode for + missing label at end of declaration (subprogram or package) + * par-ch4.adb (P_Name): issue a syntax error in SPARK mode for mixing + of positional and named parameter association + * par.adb, par-util.adb (Formal_Error_Msg_SP): new wrapper on + Error_Msg_SP which adds a prefix to the error message giving the name + of the formal language analyzed + * sem_ch6.adb (Analyze_Return_Type): issue an error in formal mode for + access result type in subprogram, unconstrained array as result type,. + (Analyze_Subprogram_Declaration): issue an error in formal mode for null + procedure + * sem_ch8.adb: Code clean up. + 2011-08-01 Javier Miranda * sem_ch7.adb (Uninstall_Declarations): Remove useless code. diff --git a/gcc/ada/par-ch4.adb b/gcc/ada/par-ch4.adb index 4c25c3ca649..a351446841f 100644 --- a/gcc/ada/par-ch4.adb +++ b/gcc/ada/par-ch4.adb @@ -669,6 +669,10 @@ package body Ch4 is -- Test for => (allow := as error substitute) if Token = Tok_Arrow or else Token = Tok_Colon_Equal then + if SPARK_Mode then + Formal_Error_Msg_SP ("no mixing of positional and named " + & "parameter association"); + end if; Restore_Scan_State (Scan_State); -- to Id goto LP_State_Call; diff --git a/gcc/ada/par-endh.adb b/gcc/ada/par-endh.adb index ca3506dd94d..ae18703e8ed 100644 --- a/gcc/ada/par-endh.adb +++ b/gcc/ada/par-endh.adb @@ -371,6 +371,17 @@ package body Endh is Set_Comes_From_Source (End_Labl, False); End_Labl_Present := False; + -- In SPARK mode, no missing label is allowed + + if SPARK_Mode + and then End_Type = E_Name + and then Explicit_Start_Label (Scope.Last) + then + Error_Msg_Node_1 := Scope.Table (Scope.Last).Labl; + Formal_Error_Msg_SP -- CODEFIX + ("`END &` required"); + end if; + -- Do style check for missing label if Style_Check diff --git a/gcc/ada/par-util.adb b/gcc/ada/par-util.adb index 6a0e8efc6cb..eeb93af639a 100644 --- a/gcc/ada/par-util.adb +++ b/gcc/ada/par-util.adb @@ -377,6 +377,16 @@ package body Util is null; end Discard_Junk_Node; + ------------------------- + -- Formal_Error_Msg_SP -- + ------------------------- + + procedure Formal_Error_Msg_SP (Msg : String) is + begin + pragma Assert (Formal_Verification_Mode); + Error_Msg_SP ("(" & Formal_Language & ") " & Msg); + end Formal_Error_Msg_SP; + ------------ -- Ignore -- ------------ diff --git a/gcc/ada/par.adb b/gcc/ada/par.adb index 99f6806057d..da84343b53a 100644 --- a/gcc/ada/par.adb +++ b/gcc/ada/par.adb @@ -1158,6 +1158,10 @@ function Par (Configuration_Pragmas : Boolean) return List_Id is -- the argument. A typical use is to skip by some junk that is not -- expected in the current context. + procedure Formal_Error_Msg_SP (Msg : String); + -- Wrapper on Errout.Error_Msg_SP which adds a prefix to Msg giving + -- the name of the formal language analyzed (spark or alfa) + procedure Ignore (T : Token_Type); -- If current token matches T, then give an error message and skip -- past it, otherwise the call has no effect at all. T may be any diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 338eae56149..8e2e2793ffc 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -1398,6 +1398,13 @@ package body Sem_Ch6 is if Result_Definition (N) /= Error then if Nkind (Result_Definition (N)) = N_Access_Definition then + -- Access result is not allowed in SPARK or ALFA + + if Formal_Verification_Mode then + Formal_Error_Msg_N + ("access result is not allowed", Result_Definition (N)); + end if; + -- Ada 2005 (AI-254): Handle anonymous access to subprograms declare @@ -1426,6 +1433,17 @@ package body Sem_Ch6 is Typ := Entity (Result_Definition (N)); Set_Etype (Designator, Typ); + -- Unconstrained array as result is not allowed in SPARK or ALFA + + if Formal_Verification_Mode + and then Is_Array_Type (Typ) + and then not Is_Constrained (Typ) + then + Formal_Error_Msg_N + ("returning an unconstrained array is not allowed", + Result_Definition (N)); + end if; + -- Ada 2005 (AI-231): Ensure proper usage of null exclusion Null_Exclusion_Static_Checks (N); @@ -2806,6 +2824,15 @@ package body Sem_Ch6 is -- Start of processing for Analyze_Subprogram_Declaration begin + -- Null procedures are not allowed in SPARK or ALFA + + if Formal_Verification_Mode + and then Nkind (Specification (N)) = N_Procedure_Specification + and then Null_Present (Specification (N)) + then + Formal_Error_Msg_N ("null procedure not allowed", N); + end if; + -- For a null procedure, capture the profile before analysis, for -- expansion at the freeze point and at each point of call. The body -- will only be used if the procedure has preconditions. In that case diff --git a/gcc/ada/sem_ch8.adb b/gcc/ada/sem_ch8.adb index 53804019392..56f57d177a5 100644 --- a/gcc/ada/sem_ch8.adb +++ b/gcc/ada/sem_ch8.adb @@ -6300,6 +6300,7 @@ package body Sem_Ch8 is end loop; pragma Assert (False); -- unreachable + raise Program_Error; end Has_Loop_In_Inner_Open_Scopes; -------------------- -- 2.30.2