From cb7fa356f01ab948150d228fac70a3e55575650d Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Tue, 2 Aug 2011 11:55:51 +0200 Subject: [PATCH] [multiple changes] 2011-08-02 Arnaud Charlet * s-osinte-linux.ads: Minor comment update and reformatting. * i-cexten.ads: Make this unit pure, as for its parent. Will allow its usage in more contexts if needed. 2011-08-02 Robert Dewar * s-utf_32.ads: Minor comment fix. 2011-08-02 Ed Schonberg * sem_res.adb (Resolve_Actuals): if the subprogram is a primitive operation of a tagged synchronized type, handle the case where the controlling argument is overloaded. 2011-08-02 Yannick Moy * gnat_rm.texi, opt.ads, sem_prag.adb, snames.ads-tmpl: Replace pragma SPARK_95 with pragma Restrictions (SPARK) * par-prag.adb (Process_Restrictions_Or_Restriction_Warnings): set SPARK mode and formal verification mode on processing SPARK restriction * s-rident.ads (Restriction_Id): add SPARK restriction in those not requiring consistency checking. From-SVN: r177117 --- gcc/ada/ChangeLog | 25 ++++++++++ gcc/ada/gnat_rm.texi | 58 ++++++++++------------- gcc/ada/i-cexten.ads | 3 ++ gcc/ada/opt.ads | 16 ------- gcc/ada/par-prag.adb | 36 ++++++--------- gcc/ada/s-osinte-linux.ads | 2 +- gcc/ada/s-rident.ads | 5 +- gcc/ada/s-utf_32.ads | 2 +- gcc/ada/sem_prag.adb | 19 -------- gcc/ada/sem_res.adb | 94 ++++++++++++++++++++++++++------------ gcc/ada/snames.ads-tmpl | 2 - 11 files changed, 136 insertions(+), 126 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 24556944b31..c10bc0abb12 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,28 @@ +2011-08-02 Arnaud Charlet + + * s-osinte-linux.ads: Minor comment update and reformatting. + * i-cexten.ads: Make this unit pure, as for its parent. + Will allow its usage in more contexts if needed. + +2011-08-02 Robert Dewar + + * s-utf_32.ads: Minor comment fix. + +2011-08-02 Ed Schonberg + + * sem_res.adb (Resolve_Actuals): if the subprogram is a primitive + operation of a tagged synchronized type, handle the case where the + controlling argument is overloaded. + +2011-08-02 Yannick Moy + + * gnat_rm.texi, opt.ads, sem_prag.adb, snames.ads-tmpl: + Replace pragma SPARK_95 with pragma Restrictions (SPARK) + * par-prag.adb (Process_Restrictions_Or_Restriction_Warnings): set + SPARK mode and formal verification mode on processing SPARK restriction + * s-rident.ads (Restriction_Id): add SPARK restriction in those not + requiring consistency checking. + 2011-08-02 Robert Dewar * sem_res.adb: Minor reformatting. diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi index e89468baf12..4ead06e0d30 100644 --- a/gcc/ada/gnat_rm.texi +++ b/gcc/ada/gnat_rm.texi @@ -192,7 +192,6 @@ Implementation Defined Pragmas * Pragma Source_File_Name:: * Pragma Source_File_Name_Project:: * Pragma Source_Reference:: -* Pragma SPARK_95:: * Pragma Static_Elaboration_Desired:: * Pragma Stream_Convert:: * Pragma Style_Checks:: @@ -825,7 +824,6 @@ consideration, the use of these pragmas should be minimized. * Pragma Source_File_Name:: * Pragma Source_File_Name_Project:: * Pragma Source_Reference:: -* Pragma SPARK_95:: * Pragma Static_Elaboration_Desired:: * Pragma Stream_Convert:: * Pragma Style_Checks:: @@ -4609,38 +4607,6 @@ The second argument must be a string literal, it cannot be a static string expression other than a string literal. This is because its value is needed for error messages issued by all phases of the compiler. -@node Pragma SPARK_95 -@unnumberedsec Pragma SPARK_95 -@findex SPARK_95 -@noindent -Syntax: -@smallexample @c ada -pragma SPARK_95; -@end smallexample - -@noindent -This is a configuration pragma that establishes SPARK 95 mode -for the unit to which -it applies, regardless of the mode set by the command line switches. -In this mode, the compiler rejects constructs not permitted by SPARK 95. -Error messages related to SPARK restrictions have the form: - -@code{(spark) error message}. - -This is not a replacement for the semantic checks performed by the -SPARK Examiner tool, as the compiler only deals currently with code, -not at all with SPARK annotations and does not guarantee catching all -cases of constructs forbidden by SPARK 95. - -Thus it may well be the case that code which -passes the compiler in SPARK 95 mode is rejected by the SPARK Examiner, -e.g. due to the different visibility rules of the Examiner based on -SPARK @code{inherit} annotations. - -SPARK 95 mode can be useful in providing an initial filter for -code developed using SPARK 95, or in examining legacy code to see how far -it is from meeting SPARK 95 restrictions. - @node Pragma Static_Elaboration_Desired @unnumberedsec Pragma Static_Elaboration_Desired @findex Static_Elaboration_Desired @@ -9085,6 +9051,30 @@ appear, and that no wide or wide wide string or character literals appear in the program (that is literals representing characters not in type @code{Character}. +@item SPARK +@findex SPARK +This restriction checks at compile time that some constructs forbidden in +SPARK are not present. The SPARK version used as a reference is the same as +the Ada mode for the unit, so a unit compiled in Ada 95 mode with SPARK +restrictions will be checked for constructs forbidden in SPARK 95. +Error messages related to SPARK restriction have the form: + +@code{(spark) error message}. + +This is not a replacement for the semantic checks performed by the +SPARK Examiner tool, as the compiler only deals currently with code, +not at all with SPARK annotations and does not guarantee catching all +cases of constructs forbidden by SPARK. + +Thus it may well be the case that code which +passes the compiler in SPARK mode is rejected by the SPARK Examiner, +e.g. due to the different visibility rules of the Examiner based on +SPARK @code{inherit} annotations. + +SPARK restriction can be useful in providing an initial filter for +code developed using SPARK, or in examining legacy code to see how far +it is from meeting SPARK restrictions. + @end table @sp 1 diff --git a/gcc/ada/i-cexten.ads b/gcc/ada/i-cexten.ads index 235aca4b472..95fb4559cef 100644 --- a/gcc/ada/i-cexten.ads +++ b/gcc/ada/i-cexten.ads @@ -35,6 +35,7 @@ with System; package Interfaces.C.Extensions is + pragma Pure; -- Definitions for C "void" and "void *" types @@ -45,11 +46,13 @@ package Interfaces.C.Extensions is subtype opaque_structure_def is System.Address; type opaque_structure_def_ptr is access opaque_structure_def; + for opaque_structure_def_ptr'Storage_Size use 0; -- Definitions for C++ incomplete/unknown classes subtype incomplete_class_def is System.Address; type incomplete_class_def_ptr is access incomplete_class_def; + for incomplete_class_def_ptr'Storage_Size use 0; -- C bool diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads index 32326ecd3c7..61fc1f1e3f3 100644 --- a/gcc/ada/opt.ads +++ b/gcc/ada/opt.ads @@ -1167,22 +1167,6 @@ package Opt is -- GNAT -- Set True if a pragma Short_Descriptors applies to the current unit. - type SPARK_Version_Type is (SPARK_None, SPARK_95); - pragma Ordered (SPARK_Version_Type); - -- Versions of SPARK for SPARK_Version below. Note that these are ordered, - -- so that tests like SPARK_Version >= SPARK_95 are legitimate and useful. - -- Think twice before using "="; SPARK_Version >= SPARK_95 is more likely - -- what you want, because it will apply to future versions of the language. - - SPARK_Version_Default : constant SPARK_Version_Type := SPARK_None; - -- GNAT - -- Default SPARK version if no switch given - - SPARK_Version : SPARK_Version_Type := SPARK_Version_Default; - -- GNAT - -- Current SPARK version for compiler, as set by configuration pragmas or - -- compiler switches. - Sprint_Line_Limit : Nat := 72; -- GNAT -- Limit values for chopping long lines in Sprint output, can be reset diff --git a/gcc/ada/par-prag.adb b/gcc/ada/par-prag.adb index f52857bab4f..d3959b74d0b 100644 --- a/gcc/ada/par-prag.adb +++ b/gcc/ada/par-prag.adb @@ -89,9 +89,9 @@ function Prag (Pragma_Node : Node_Id; Semi : Source_Ptr) return Node_Id is procedure Process_Restrictions_Or_Restriction_Warnings; -- Common processing for Restrictions and Restriction_Warnings pragmas. - -- This routine only processes the case of No_Obsolescent_Features, - -- which is the only restriction that has syntactic effects. No general - -- error checking is done, since this will be done in Sem_Prag. The + -- This routine only processes the cases of No_Obsolescent_Features and + -- SPARK, which are the only restrictions that have syntactic effects. No + -- general error checking is done, since this will be done in Sem_Prag. The -- other case processed is pragma Restrictions No_Dependence, since -- otherwise this is done too late. @@ -224,11 +224,19 @@ function Prag (Pragma_Node : Node_Id; Semi : Source_Ptr) return Node_Id is if Id = No_Name and then Nkind (Expr) = N_Identifier - and then Get_Restriction_Id (Chars (Expr)) = No_Obsolescent_Features then - Set_Restriction (No_Obsolescent_Features, Pragma_Node); - Restriction_Warnings (No_Obsolescent_Features) := - Prag_Id = Pragma_Restriction_Warnings; + case Get_Restriction_Id (Chars (Expr)) is + when No_Obsolescent_Features => + Set_Restriction (No_Obsolescent_Features, Pragma_Node); + Restriction_Warnings (No_Obsolescent_Features) := + Prag_Id = Pragma_Restriction_Warnings; + when SPARK => + SPARK_Mode := True; + Set_Error_Msg_Lang ("spark"); + Formal_Verification_Mode := True; + when others => + null; + end case; elsif Id = Name_No_Dependence then Set_Restriction_No_Dependence @@ -889,20 +897,6 @@ begin end if; end Source_Reference; - -------------- - -- SPARK_95 -- - -------------- - - -- This pragma must be processed at parse time, since we want to set the - -- SPARK version properly at parse time to recognize the appropriate - -- SPARK version syntax. - - when Pragma_SPARK_95 => - SPARK_Version := SPARK_95; - SPARK_Mode := True; - Set_Error_Msg_Lang ("spark"); - Formal_Verification_Mode := True; - ------------------------- -- Style_Checks (GNAT) -- ------------------------- diff --git a/gcc/ada/s-osinte-linux.ads b/gcc/ada/s-osinte-linux.ads index e2b891d60f8..02213086b12 100644 --- a/gcc/ada/s-osinte-linux.ads +++ b/gcc/ada/s-osinte-linux.ads @@ -553,7 +553,7 @@ private type pthread_mutex_t is new System.Linux.pthread_mutex_t; type unsigned_long_long_t is mod 2 ** 64; - -- Interfaces.C.Extensions isn't preelaborated so cannot be with'ed + -- Local type only used to get it's 'Alignment below type pthread_cond_t is array (0 .. 47) of unsigned_char; pragma Convention (C, pthread_cond_t); diff --git a/gcc/ada/s-rident.ads b/gcc/ada/s-rident.ads index 9423694afad..2f0a2f30ff1 100644 --- a/gcc/ada/s-rident.ads +++ b/gcc/ada/s-rident.ads @@ -131,6 +131,7 @@ package System.Rident is No_Elaboration_Code, -- GNAT No_Obsolescent_Features, -- Ada 2005 AI-368 No_Wide_Characters, -- GNAT + SPARK, -- GNAT -- The following cases require a parameter value @@ -180,7 +181,7 @@ package System.Rident is -- All restrictions (excluding only Not_A_Restriction_Id) subtype All_Boolean_Restrictions is Restriction_Id range - Simple_Barriers .. No_Wide_Characters; + Simple_Barriers .. SPARK; -- All restrictions which do not take a parameter subtype Partition_Boolean_Restrictions is All_Boolean_Restrictions range @@ -191,7 +192,7 @@ package System.Rident is -- case of Boolean restrictions. subtype Cunit_Boolean_Restrictions is All_Boolean_Restrictions range - Immediate_Reclamation .. No_Wide_Characters; + Immediate_Reclamation .. SPARK; -- Boolean restrictions that are not checked for partition consistency -- and that thus apply only to the current unit. Note that for these -- restrictions, the compiler does not apply restrictions found in diff --git a/gcc/ada/s-utf_32.ads b/gcc/ada/s-utf_32.ads index c4c04e0aec7..4cdbf95279e 100755 --- a/gcc/ada/s-utf_32.ads +++ b/gcc/ada/s-utf_32.ads @@ -120,7 +120,7 @@ package System.UTF_32 is function Is_UTF_32_Line_Terminator (U : UTF_32) return Boolean; pragma Inline (Is_UTF_32_Line_Terminator); -- Returns true iff U is an allowed line terminator for source programs, - -- if U is in the category Zp (Separator, Paragraph), or Zs (Separator, + -- if U is in the category Zp (Separator, Paragraph), or Zl (Separator, -- Line), or if U is a conventional line terminator (CR, LF, VT, FF). -- There is no category version for this function, since the set of -- characters does not correspond to a set of Unicode categories. diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 33aa6ac59c5..d416bd93264 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -12387,24 +12387,6 @@ package body Sem_Prag is when Pragma_Source_Reference => GNAT_Pragma; - -------------- - -- SPARK_95 -- - -------------- - - -- pragma SPARK_95; - - -- Note: this pragma also has some specific processing in Par.Prag - -- because we want to set the SPARK 95 version mode during parsing. - - when Pragma_SPARK_95 => - GNAT_Pragma; - Check_Arg_Count (0); - Check_Valid_Configuration_Pragma; - SPARK_Version := SPARK_95; - SPARK_Mode := True; - Formal_Verification_Mode := True; - Set_Error_Msg_Lang ("spark"); - -------------------------------- -- Static_Elaboration_Desired -- -------------------------------- @@ -14154,7 +14136,6 @@ package body Sem_Prag is Pragma_Source_File_Name => -1, Pragma_Source_File_Name_Project => -1, Pragma_Source_Reference => -1, - Pragma_SPARK_95 => -1, Pragma_Storage_Size => -1, Pragma_Storage_Unit => -1, Pragma_Static_Elaboration_Desired => -1, diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index eb736a03662..a2dc2061376 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -3503,48 +3503,82 @@ package body Sem_Res is -- or because it is a generic actual, so use base type to -- locate concurrent type. - A_Typ := Base_Type (Etype (A)); F_Typ := Base_Type (Etype (F)); - declare - Full_A_Typ : Entity_Id; + if Is_Tagged_Type (F_Typ) + and then (Is_Concurrent_Type (F_Typ) + or else Is_Concurrent_Record_Type (F_Typ)) + then + -- If the actual is overloaded, look for an interpretation + -- that has a synchronized type. + + if not Is_Overloaded (A) then + A_Typ := Base_Type (Etype (A)); - begin - if Present (Full_View (A_Typ)) then - Full_A_Typ := Base_Type (Full_View (A_Typ)); else - Full_A_Typ := A_Typ; + declare + Index : Interp_Index; + It : Interp; + begin + Get_First_Interp (A, Index, It); + while Present (It.Typ) loop + if Is_Concurrent_Type (It.Typ) + or else Is_Concurrent_Record_Type (It.Typ) + then + A_Typ := Base_Type (It.Typ); + exit; + end if; + + Get_Next_Interp (Index, It); + end loop; + end; end if; - -- Tagged synchronized type (case 1): the actual is a - -- concurrent type. + declare + Full_A_Typ : Entity_Id; - if Is_Concurrent_Type (A_Typ) - and then Corresponding_Record_Type (A_Typ) = F_Typ - then - Rewrite (A, - Unchecked_Convert_To - (Corresponding_Record_Type (A_Typ), A)); - Resolve (A, Etype (F)); + begin + if Present (Full_View (A_Typ)) then + Full_A_Typ := Base_Type (Full_View (A_Typ)); + else + Full_A_Typ := A_Typ; + end if; + + -- Tagged synchronized type (case 1): the actual is a + -- concurrent type. + + if Is_Concurrent_Type (A_Typ) + and then Corresponding_Record_Type (A_Typ) = F_Typ + then + Rewrite (A, + Unchecked_Convert_To + (Corresponding_Record_Type (A_Typ), A)); + Resolve (A, Etype (F)); - -- Tagged synchronized type (case 2): the formal is a - -- concurrent type. + -- Tagged synchronized type (case 2): the formal is a + -- concurrent type. - elsif Ekind (Full_A_Typ) = E_Record_Type - and then Present + elsif Ekind (Full_A_Typ) = E_Record_Type + and then Present (Corresponding_Concurrent_Type (Full_A_Typ)) - and then Is_Concurrent_Type (F_Typ) - and then Present (Corresponding_Record_Type (F_Typ)) - and then Full_A_Typ = Corresponding_Record_Type (F_Typ) - then - Resolve (A, Corresponding_Record_Type (F_Typ)); + and then Is_Concurrent_Type (F_Typ) + and then Present (Corresponding_Record_Type (F_Typ)) + and then Full_A_Typ = Corresponding_Record_Type (F_Typ) + then + Resolve (A, Corresponding_Record_Type (F_Typ)); - -- Common case + -- Common case - else - Resolve (A, Etype (F)); - end if; - end; + else + Resolve (A, Etype (F)); + end if; + end; + else + + -- not a synchronized operation. + + Resolve (A, Etype (F)); + end if; end if; A_Typ := Etype (A); diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl index ba346c49654..f10aefaddf9 100644 --- a/gcc/ada/snames.ads-tmpl +++ b/gcc/ada/snames.ads-tmpl @@ -404,7 +404,6 @@ package Snames is Name_Short_Descriptors : constant Name_Id := N + $; -- GNAT Name_Source_File_Name : constant Name_Id := N + $; -- GNAT Name_Source_File_Name_Project : constant Name_Id := N + $; -- GNAT - Name_SPARK_95 : constant Name_Id := N + $; -- GNAT Name_Style_Checks : constant Name_Id := N + $; -- GNAT Name_Suppress : constant Name_Id := N + $; Name_Suppress_Exception_Locations : constant Name_Id := N + $; -- GNAT @@ -1520,7 +1519,6 @@ package Snames is Pragma_Short_Descriptors, Pragma_Source_File_Name, Pragma_Source_File_Name_Project, - Pragma_SPARK_95, Pragma_Style_Checks, Pragma_Suppress, Pragma_Suppress_Exception_Locations, -- 2.30.2