From: Arnaud Charlet Date: Mon, 10 Feb 2020 20:18:47 +0000 (-0500) Subject: [Ada] Remove processing of SPARK_05 restriction X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7907619e7737b6cb38ee334996a7d7a33bb7a1d6;p=gcc.git [Ada] Remove processing of SPARK_05 restriction 2020-06-08 Arnaud Charlet gcc/ada/ * exp_aggr.adb, exp_ch6.adb, par-ch11.adb, par-ch6.adb, par-ch7.adb, par-prag.adb, restrict.adb, restrict.ads, scans.ads, scng.adb, sem_aggr.adb, sem_attr.adb, sem_ch11.adb, sem_ch12.adb, sem_ch3.adb, sem_ch3.ads, sem_ch4.adb, sem_ch5.adb, sem_ch6.adb, sem_ch7.adb, sem_ch8.adb, sem_ch9.adb, sem_res.adb, sem_util.adb, sem_util.ads, snames.ads-tmpl, gnatbind.adb, libgnat/s-rident.ads, doc/gnat_rm/standard_and_implementation_defined_restrictions.rst: Remove processing of SPARK_05 restriction. * gnat_rm.texi: Regenerate. * opt.ads: Remove processing of old checksum which is now handled by gprbuild directly. --- diff --git a/gcc/ada/doc/gnat_rm/standard_and_implementation_defined_restrictions.rst b/gcc/ada/doc/gnat_rm/standard_and_implementation_defined_restrictions.rst index 56dd6a7ab75..b0f59cfb5e0 100644 --- a/gcc/ada/doc/gnat_rm/standard_and_implementation_defined_restrictions.rst +++ b/gcc/ada/doc/gnat_rm/standard_and_implementation_defined_restrictions.rst @@ -1000,8 +1000,7 @@ SPARK_05 -------- .. index:: SPARK_05 -[GNAT] This restriction checks at compile time that some constructs forbidden -in SPARK 2005 are not present. Note that SPARK 2005 has been superseded by +[GNAT] This restriction no longer has any effect and is superseded by SPARK 2014, whose restrictions are checked by the tool GNATprove. To check that a codebase respects SPARK 2014 restrictions, mark the code with pragma or aspect ``SPARK_Mode``, and run the tool GNATprove at Stone assurance level, as @@ -1013,145 +1012,3 @@ or equivalently:: gnatprove -P project.gpr --mode=check_all -With restriction ``SPARK_05``, error messages related to SPARK 2005 restriction -have the form: - -:: - - violation of restriction "SPARK_05" at - - -.. index:: SPARK - -The restriction ``SPARK`` is recognized as a synonym for ``SPARK_05``. This is -retained for historical compatibility purposes (and an unconditional warning -will be generated for its use, advising replacement by ``SPARK_05``). - -This is not a replacement for the semantic checks performed by the -SPARK Examiner tool, as the compiler currently only deals with code, -not SPARK 2005 annotations, and does not guarantee catching all -cases of constructs forbidden by SPARK 2005. - -Thus it may well be the case that code which passes the compiler with -the SPARK 2005 restriction is rejected by the SPARK Examiner, e.g. due to -the different visibility rules of the Examiner based on SPARK 2005 -``inherit`` annotations. - -This restriction can be useful in providing an initial filter for code -developed using SPARK 2005, or in examining legacy code to see how far -it is from meeting SPARK 2005 restrictions. - -The list below summarizes the checks that are performed when this -restriction is in force: - -* No block statements -* No case statements with only an others clause -* Exit statements in loops must respect the SPARK 2005 language restrictions -* No goto statements -* Return can only appear as last statement in function -* Function must have return statement -* Loop parameter specification must include subtype mark -* Prefix of expanded name cannot be a loop statement -* Abstract subprogram not allowed -* User-defined operators not allowed -* Access type parameters not allowed -* Default expressions for parameters not allowed -* Default expressions for record fields not allowed -* No tasking constructs allowed -* Label needed at end of subprograms and packages -* No mixing of positional and named parameter association -* No access types as result type -* No unconstrained arrays as result types -* No null procedures -* Initial and later declarations must be in correct order (declaration can't come after body) -* No attributes on private types if full declaration not visible -* No package declaration within package specification -* No controlled types -* No discriminant types -* No overloading -* Selector name cannot be operator symbol (i.e. operator symbol cannot be prefixed) -* Access attribute not allowed -* Allocator not allowed -* Result of catenation must be String -* Operands of catenation must be string literal, static char or another catenation -* No conditional expressions -* No explicit dereference -* Quantified expression not allowed -* Slicing not allowed -* No exception renaming -* No generic renaming -* No object renaming -* No use clause -* Aggregates must be qualified -* Nonstatic choice in array aggregates not allowed -* The only view conversions which are allowed as in-out parameters are conversions of a tagged type to an ancestor type -* No mixing of positional and named association in aggregate, no multi choice -* AND, OR and XOR for arrays only allowed when operands have same static bounds -* Fixed point operands to * or / must be qualified or converted -* Comparison operators not allowed for Booleans or arrays (except strings) -* Equality not allowed for arrays with non-matching static bounds (except strings) -* Conversion / qualification not allowed for arrays with non-matching static bounds -* Subprogram declaration only allowed in package spec (unless followed by import) -* Access types not allowed -* Incomplete type declaration not allowed -* Object and subtype declarations must respect SPARK 2005 restrictions -* Digits or delta constraint not allowed -* Decimal fixed point type not allowed -* Aliasing of objects not allowed -* Modular type modulus must be power of 2 -* Base not allowed on subtype mark -* Unary operators not allowed on modular types (except not) -* Untagged record cannot be null -* No class-wide operations -* Initialization expressions must respect SPARK 2005 restrictions -* Nonstatic ranges not allowed except in iteration schemes -* String subtypes must have lower bound of 1 -* Subtype of Boolean cannot have constraint -* At most one tagged type or extension per package -* Interface is not allowed -* Character literal cannot be prefixed (selector name cannot be character literal) -* Record aggregate cannot contain 'others' -* Component association in record aggregate must contain a single choice -* Ancestor part cannot be a type mark -* Attributes 'Image, 'Width and 'Value not allowed -* Functions may not update globals -* Subprograms may not contain direct calls to themselves (prevents recursion within unit) -* Call to subprogram not allowed in same unit before body has been seen (prevents recursion within unit) - -The following restrictions are enforced, but note that they are actually more -strict that the latest SPARK 2005 language definition: - -* No derived types other than tagged type extensions -* Subtype of unconstrained array must have constraint - -This list summarises the main SPARK 2005 language rules that are not -currently checked by the SPARK_05 restriction: - -* SPARK 2005 annotations are treated as comments so are not checked at all -* Based real literals not allowed -* Objects cannot be initialized at declaration by calls to user-defined functions -* Objects cannot be initialized at declaration by assignments from variables -* Objects cannot be initialized at declaration by assignments from indexed/selected components -* Ranges shall not be null -* A fixed point delta expression must be a simple expression -* Restrictions on where renaming declarations may be placed -* Externals of mode 'out' cannot be referenced -* Externals of mode 'in' cannot be updated -* Loop with no iteration scheme or exits only allowed as last statement in main program or task -* Subprogram cannot have parent unit name -* SPARK 2005 inherited subprogram must be prefixed with overriding -* External variables (or functions that reference them) may not be passed as actual parameters -* Globals must be explicitly mentioned in contract -* Deferred constants cannot be completed by pragma Import -* Package initialization cannot read/write variables from other packages -* Prefix not allowed for entities that are directly visible -* Identifier declaration can't override inherited package name -* Cannot use Standard or other predefined packages as identifiers -* After renaming, cannot use the original name -* Subprograms can only be renamed to remove package prefix -* Pragma import must be immediately after entity it names -* No mutual recursion between multiple units (this can be checked with gnatcheck) - -Note that if a unit is compiled in Ada 95 mode with the SPARK 2005 restriction, -violations will be reported for constructs forbidden in SPARK 95, -instead of SPARK 2005. diff --git a/gcc/ada/exp_aggr.adb b/gcc/ada/exp_aggr.adb index aad902269db..d945fdbcefc 100644 --- a/gcc/ada/exp_aggr.adb +++ b/gcc/ada/exp_aggr.adb @@ -6333,10 +6333,6 @@ package body Exp_Aggr is -- object. (Note: we don't use a block statement because this would -- cause generated freeze nodes to be elaborated in the wrong scope). - -- Do not perform in-place expansion for SPARK 05 because aggregates are - -- expected to appear in qualified form. In-place expansion eliminates - -- the qualification and eventually violates this SPARK 05 restiction. - -- Arrays of limited components must be built in place. The code -- previously excluded controlled components but this is an old -- oversight: the rules in 7.6 (17) are clear. @@ -6347,7 +6343,6 @@ package body Exp_Aggr is and then not Must_Slide (Etype (Defining_Identifier (Parent_Node)), Typ) and then not Is_Bit_Packed_Array (Typ) - and then not Restriction_Check_Required (SPARK_05) then In_Place_Assign_OK_For_Declaration := True; Tmp := Defining_Identifier (Parent_Node); diff --git a/gcc/ada/exp_ch6.adb b/gcc/ada/exp_ch6.adb index 11980a6684c..4f8b47170c6 100644 --- a/gcc/ada/exp_ch6.adb +++ b/gcc/ada/exp_ch6.adb @@ -6244,33 +6244,7 @@ package body Exp_Ch6 is Prot_Decl : Node_Id; Prot_Id : Entity_Id; - -- Start of processing for Expand_N_Subprogram_Declaration - begin - -- In SPARK, subprogram declarations are only allowed in package - -- specifications. - - if Nkind (Parent (N)) /= N_Package_Specification then - if Nkind (Parent (N)) = N_Compilation_Unit then - Check_SPARK_05_Restriction - ("subprogram declaration is not a library item", N); - - elsif Present (Next (N)) - and then Nkind (Next (N)) = N_Pragma - and then Get_Pragma_Id (Next (N)) = Pragma_Import - then - -- In SPARK, subprogram declarations are also permitted in - -- declarative parts when immediately followed by a corresponding - -- pragma Import. We only check here that there is some pragma - -- Import. - - null; - else - Check_SPARK_05_Restriction - ("subprogram declaration is not allowed here", N); - end if; - end if; - -- Deal with case of protected subprogram. Do not generate protected -- operation if operation is flagged as eliminated. diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi index afe59eff5ab..f012e754f1e 100644 --- a/gcc/ada/gnat_rm.texi +++ b/gcc/ada/gnat_rm.texi @@ -13307,8 +13307,7 @@ associated with dispatch tables can be placed in read-only memory. @geindex SPARK_05 -[GNAT] This restriction checks at compile time that some constructs forbidden -in SPARK 2005 are not present. Note that SPARK 2005 has been superseded by +[GNAT] This restriction no longer has any effect and is superseded by SPARK 2014, whose restrictions are checked by the tool GNATprove. To check that a codebase respects SPARK 2014 restrictions, mark the code with pragma or aspect @code{SPARK_Mode}, and run the tool GNATprove at Stone assurance level, as @@ -13324,356 +13323,6 @@ or equivalently: gnatprove -P project.gpr --mode=check_all @end example -With restriction @code{SPARK_05}, error messages related to SPARK 2005 restriction -have the form: - -@example -violation of restriction "SPARK_05" at - -@end example - -@geindex SPARK - -The restriction @code{SPARK} is recognized as a synonym for @code{SPARK_05}. This is -retained for historical compatibility purposes (and an unconditional warning -will be generated for its use, advising replacement by @code{SPARK_05}). - -This is not a replacement for the semantic checks performed by the -SPARK Examiner tool, as the compiler currently only deals with code, -not SPARK 2005 annotations, and does not guarantee catching all -cases of constructs forbidden by SPARK 2005. - -Thus it may well be the case that code which passes the compiler with -the SPARK 2005 restriction is rejected by the SPARK Examiner, e.g. due to -the different visibility rules of the Examiner based on SPARK 2005 -@code{inherit} annotations. - -This restriction can be useful in providing an initial filter for code -developed using SPARK 2005, or in examining legacy code to see how far -it is from meeting SPARK 2005 restrictions. - -The list below summarizes the checks that are performed when this -restriction is in force: - - -@itemize * - -@item -No block statements - -@item -No case statements with only an others clause - -@item -Exit statements in loops must respect the SPARK 2005 language restrictions - -@item -No goto statements - -@item -Return can only appear as last statement in function - -@item -Function must have return statement - -@item -Loop parameter specification must include subtype mark - -@item -Prefix of expanded name cannot be a loop statement - -@item -Abstract subprogram not allowed - -@item -User-defined operators not allowed - -@item -Access type parameters not allowed - -@item -Default expressions for parameters not allowed - -@item -Default expressions for record fields not allowed - -@item -No tasking constructs allowed - -@item -Label needed at end of subprograms and packages - -@item -No mixing of positional and named parameter association - -@item -No access types as result type - -@item -No unconstrained arrays as result types - -@item -No null procedures - -@item -Initial and later declarations must be in correct order (declaration can't come after body) - -@item -No attributes on private types if full declaration not visible - -@item -No package declaration within package specification - -@item -No controlled types - -@item -No discriminant types - -@item -No overloading - -@item -Selector name cannot be operator symbol (i.e. operator symbol cannot be prefixed) - -@item -Access attribute not allowed - -@item -Allocator not allowed - -@item -Result of catenation must be String - -@item -Operands of catenation must be string literal, static char or another catenation - -@item -No conditional expressions - -@item -No explicit dereference - -@item -Quantified expression not allowed - -@item -Slicing not allowed - -@item -No exception renaming - -@item -No generic renaming - -@item -No object renaming - -@item -No use clause - -@item -Aggregates must be qualified - -@item -Nonstatic choice in array aggregates not allowed - -@item -The only view conversions which are allowed as in-out parameters are conversions of a tagged type to an ancestor type - -@item -No mixing of positional and named association in aggregate, no multi choice - -@item -AND, OR and XOR for arrays only allowed when operands have same static bounds - -@item -Fixed point operands to * or / must be qualified or converted - -@item -Comparison operators not allowed for Booleans or arrays (except strings) - -@item -Equality not allowed for arrays with non-matching static bounds (except strings) - -@item -Conversion / qualification not allowed for arrays with non-matching static bounds - -@item -Subprogram declaration only allowed in package spec (unless followed by import) - -@item -Access types not allowed - -@item -Incomplete type declaration not allowed - -@item -Object and subtype declarations must respect SPARK 2005 restrictions - -@item -Digits or delta constraint not allowed - -@item -Decimal fixed point type not allowed - -@item -Aliasing of objects not allowed - -@item -Modular type modulus must be power of 2 - -@item -Base not allowed on subtype mark - -@item -Unary operators not allowed on modular types (except not) - -@item -Untagged record cannot be null - -@item -No class-wide operations - -@item -Initialization expressions must respect SPARK 2005 restrictions - -@item -Nonstatic ranges not allowed except in iteration schemes - -@item -String subtypes must have lower bound of 1 - -@item -Subtype of Boolean cannot have constraint - -@item -At most one tagged type or extension per package - -@item -Interface is not allowed - -@item -Character literal cannot be prefixed (selector name cannot be character literal) - -@item -Record aggregate cannot contain 'others' - -@item -Component association in record aggregate must contain a single choice - -@item -Ancestor part cannot be a type mark - -@item -Attributes 'Image, 'Width and 'Value not allowed - -@item -Functions may not update globals - -@item -Subprograms may not contain direct calls to themselves (prevents recursion within unit) - -@item -Call to subprogram not allowed in same unit before body has been seen (prevents recursion within unit) -@end itemize - -The following restrictions are enforced, but note that they are actually more -strict that the latest SPARK 2005 language definition: - - -@itemize * - -@item -No derived types other than tagged type extensions - -@item -Subtype of unconstrained array must have constraint -@end itemize - -This list summarises the main SPARK 2005 language rules that are not -currently checked by the SPARK_05 restriction: - - -@itemize * - -@item -SPARK 2005 annotations are treated as comments so are not checked at all - -@item -Based real literals not allowed - -@item -Objects cannot be initialized at declaration by calls to user-defined functions - -@item -Objects cannot be initialized at declaration by assignments from variables - -@item -Objects cannot be initialized at declaration by assignments from indexed/selected components - -@item -Ranges shall not be null - -@item -A fixed point delta expression must be a simple expression - -@item -Restrictions on where renaming declarations may be placed - -@item -Externals of mode 'out' cannot be referenced - -@item -Externals of mode 'in' cannot be updated - -@item -Loop with no iteration scheme or exits only allowed as last statement in main program or task - -@item -Subprogram cannot have parent unit name - -@item -SPARK 2005 inherited subprogram must be prefixed with overriding - -@item -External variables (or functions that reference them) may not be passed as actual parameters - -@item -Globals must be explicitly mentioned in contract - -@item -Deferred constants cannot be completed by pragma Import - -@item -Package initialization cannot read/write variables from other packages - -@item -Prefix not allowed for entities that are directly visible - -@item -Identifier declaration can't override inherited package name - -@item -Cannot use Standard or other predefined packages as identifiers - -@item -After renaming, cannot use the original name - -@item -Subprograms can only be renamed to remove package prefix - -@item -Pragma import must be immediately after entity it names - -@item -No mutual recursion between multiple units (this can be checked with gnatcheck) -@end itemize - -Note that if a unit is compiled in Ada 95 mode with the SPARK 2005 restriction, -violations will be reported for constructs forbidden in SPARK 95, -instead of SPARK 2005. - @node Implementation Advice,Implementation Defined Characteristics,Standard and Implementation Defined Restrictions,Top @anchor{gnat_rm/implementation_advice doc}@anchor{210}@anchor{gnat_rm/implementation_advice implementation-advice}@anchor{a}@anchor{gnat_rm/implementation_advice id1}@anchor{211} @chapter Implementation Advice diff --git a/gcc/ada/gnatbind.adb b/gcc/ada/gnatbind.adb index b4a00ce6c28..4907082a42c 100644 --- a/gcc/ada/gnatbind.adb +++ b/gcc/ada/gnatbind.adb @@ -221,6 +221,9 @@ procedure Gnatbind is No_Use_Of_Pragma => False, -- Requires a parameter value, not a count + SPARK_05 => False, + -- Obsolete restriction + others => True); Additional_Restrictions_Listed : Boolean := False; diff --git a/gcc/ada/libgnat/s-rident.ads b/gcc/ada/libgnat/s-rident.ads index 2f46d5b4203..73a0450b458 100644 --- a/gcc/ada/libgnat/s-rident.ads +++ b/gcc/ada/libgnat/s-rident.ads @@ -232,7 +232,6 @@ package System.Rident is No_Dynamic_Interrupts : Restriction_Id renames No_Dynamic_Attachment; No_Requeue : Restriction_Id renames No_Requeue_Statements; No_Task_Attributes : Restriction_Id renames No_Task_Attributes_Package; - SPARK : Restriction_Id renames SPARK_05; subtype All_Restrictions is Restriction_Id range Simple_Barriers .. Max_Storage_At_Blocking; diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads index 2bf95e80275..8987f839572 100644 --- a/gcc/ada/opt.ads +++ b/gcc/ada/opt.ads @@ -57,50 +57,6 @@ package Opt is -- from a compilation point of view (e.g. spelling of identifiers and -- white space layout do not count in this computation). - -- The way the checksum is computed has evolved across the various versions - -- of GNAT. When gprbuild is called with -m, the checksums must be computed - -- the same way in gprbuild as it was in the GNAT version of the compiler. - -- The different ways are - - -- Version 6.4 and later: - - -- The Accumulate_Token_Checksum procedure is called after each numeric - -- literal and each identifier/keyword. For keywords, Tok_Identifier is - -- used in the call to Accumulate_Token_Checksum. - - -- Versions 5.04 to 6.3: - - -- For keywords, the token value were used in the call to procedure - -- Accumulate_Token_Checksum. Type Token_Type did not include Tok_Some. - - -- Versions 5.03: - - -- For keywords, the token value were used in the call to - -- Accumulate_Token_Checksum. Type Token_Type did not include - -- Tok_Interface, Tok_Overriding, Tok_Synchronized and Tok_Some. - - -- Versions 5.02 and before: - - -- No calls to procedure Accumulate_Token_Checksum (the checksum - -- mechanism was introduced in version 5.03). - - -- To signal to the scanner whether Accumulate_Token_Checksum needs to be - -- called and what versions to call, the following Boolean flags are used: - - Checksum_Accumulate_Token_Checksum : Boolean := True; - -- GPRBUILD - -- Set to False by gprbuild when the version of GNAT is 5.02 or before. If - -- this switch is False, then we do not call Accumulate_Token_Checksum, so - -- the setting of the following two flags is irrelevant. - - Checksum_GNAT_6_3 : Boolean := False; - -- GPRBUILD - -- Set to True by gprbuild when the version of GNAT is 6.3 or before. - - Checksum_GNAT_5_03 : Boolean := False; - -- GPRBUILD - -- Set to True by gprbuild when the version of GNAT is 5.03 or before. - Checksum_Accumulate_Limited_Checksum : Boolean := False; -- Used to control the computation of the limited view of a package. -- (Not currently used, possible optimization for ALI files of units diff --git a/gcc/ada/par-ch11.adb b/gcc/ada/par-ch11.adb index cd1344f23d5..468ba03a939 100644 --- a/gcc/ada/par-ch11.adb +++ b/gcc/ada/par-ch11.adb @@ -57,27 +57,9 @@ package body Ch11 is function P_Handled_Sequence_Of_Statements return Node_Id is Handled_Stmt_Seq_Node : Node_Id; - Seq_Is_Hidden_In_SPARK : Boolean; - Hidden_Region_Start : Source_Ptr; - begin Handled_Stmt_Seq_Node := New_Node (N_Handled_Sequence_Of_Statements, Token_Ptr); - - -- In SPARK, a HIDE directive can be placed at the beginning of a - -- package initialization, thus hiding the sequence of statements (and - -- possible exception handlers) from SPARK tool-set. No violation of the - -- SPARK restriction should be issued on nodes in a hidden part, which - -- is obtained by marking such hidden parts. - - if Token = Tok_SPARK_Hide then - Seq_Is_Hidden_In_SPARK := True; - Hidden_Region_Start := Token_Ptr; - Scan; -- past HIDE directive - else - Seq_Is_Hidden_In_SPARK := False; - end if; - Set_Statements (Handled_Stmt_Seq_Node, P_Sequence_Of_Statements (SS_Extm_Sreq)); @@ -87,10 +69,6 @@ package body Ch11 is (Handled_Stmt_Seq_Node, Parse_Exception_Handlers); end if; - if Seq_Is_Hidden_In_SPARK then - Set_Hidden_Part_In_SPARK (Hidden_Region_Start, Token_Ptr); - end if; - return Handled_Stmt_Seq_Node; end P_Handled_Sequence_Of_Statements; @@ -282,24 +260,8 @@ package body Ch11 is function Parse_Exception_Handlers return List_Id is Handler : Node_Id; Handlers_List : List_Id; - Handler_Is_Hidden_In_SPARK : Boolean; - Hidden_Region_Start : Source_Ptr; begin - -- In SPARK, a HIDE directive can be placed at the beginning of a - -- sequence of exception handlers for a subprogram implementation, thus - -- hiding the exception handlers from SPARK tool-set. No violation of - -- the SPARK restriction should be issued on nodes in a hidden part, - -- which is obtained by marking such hidden parts. - - if Token = Tok_SPARK_Hide then - Handler_Is_Hidden_In_SPARK := True; - Hidden_Region_Start := Token_Ptr; - Scan; -- past HIDE directive - else - Handler_Is_Hidden_In_SPARK := False; - end if; - Handlers_List := New_List; P_Pragmas_Opt (Handlers_List); @@ -320,10 +282,6 @@ package body Ch11 is end loop; end if; - if Handler_Is_Hidden_In_SPARK then - Set_Hidden_Part_In_SPARK (Hidden_Region_Start, Token_Ptr); - end if; - return Handlers_List; end Parse_Exception_Handlers; diff --git a/gcc/ada/par-ch6.adb b/gcc/ada/par-ch6.adb index 7140742d430..2cc3f08f94a 100644 --- a/gcc/ada/par-ch6.adb +++ b/gcc/ada/par-ch6.adb @@ -707,9 +707,6 @@ package body Ch6 is else Scan_Body_Or_Expression_Function : declare - Body_Is_Hidden_In_SPARK : Boolean; - Hidden_Region_Start : Source_Ptr; - function Likely_Expression_Function return Boolean; -- Returns True if we have a probable case of an expression -- function omitting the parentheses, if so, returns True @@ -942,25 +939,7 @@ package body Ch6 is Set_Aspect_Specifications (Body_Node, Aspects); end if; - -- In SPARK, a HIDE directive can be placed at the beginning - -- of a subprogram implementation, thus hiding the - -- subprogram body from SPARK tool-set. No violation of the - -- SPARK restriction should be issued on nodes in a hidden - -- part, which is obtained by marking such hidden parts. - - if Token = Tok_SPARK_Hide then - Body_Is_Hidden_In_SPARK := True; - Hidden_Region_Start := Token_Ptr; - Scan; -- past HIDE directive - else - Body_Is_Hidden_In_SPARK := False; - end if; - Parse_Decls_Begin_End (Body_Node); - - if Body_Is_Hidden_In_SPARK then - Set_Hidden_Part_In_SPARK (Hidden_Region_Start, Token_Ptr); - end if; end if; return Body_Node; diff --git a/gcc/ada/par-ch7.adb b/gcc/ada/par-ch7.adb index 6edb2ddeadb..e057daa52c5 100644 --- a/gcc/ada/par-ch7.adb +++ b/gcc/ada/par-ch7.adb @@ -115,10 +115,6 @@ package body Ch7 is -- Dummy node to attach aspect specifications to until we properly -- figure out where they eventually belong. - Body_Is_Hidden_In_SPARK : Boolean; - Private_Part_Is_Hidden_In_SPARK : Boolean; - Hidden_Region_Start : Source_Ptr; - begin Push_Scope_Stack; Scopes (Scope.Last).Etyp := E_Name; @@ -185,25 +181,7 @@ package body Ch7 is Move_Aspects (From => Dummy_Node, To => Package_Node); end if; - -- In SPARK, a HIDE directive can be placed at the beginning of a - -- package implementation, thus hiding the package body from SPARK - -- tool-set. No violation of the SPARK restriction should be - -- issued on nodes in a hidden part, which is obtained by marking - -- such hidden parts. - - if Token = Tok_SPARK_Hide then - Body_Is_Hidden_In_SPARK := True; - Hidden_Region_Start := Token_Ptr; - Scan; -- past HIDE directive - else - Body_Is_Hidden_In_SPARK := False; - end if; - Parse_Decls_Begin_End (Package_Node); - - if Body_Is_Hidden_In_SPARK then - Set_Hidden_Part_In_SPARK (Hidden_Region_Start, Token_Ptr); - end if; end if; -- Cases other than Package_Body @@ -303,27 +281,9 @@ package body Ch7 is Scan; -- past PRIVATE - if Token = Tok_SPARK_Hide then - Private_Part_Is_Hidden_In_SPARK := True; - Hidden_Region_Start := Token_Ptr; - Scan; -- past HIDE directive - else - Private_Part_Is_Hidden_In_SPARK := False; - end if; - Set_Private_Declarations (Specification_Node, P_Basic_Declarative_Items); - -- In SPARK, a HIDE directive can be placed at the beginning - -- of a private part, thus hiding all declarations in the - -- private part from SPARK tool-set. No violation of the - -- SPARK restriction should be issued on nodes in a hidden - -- part, which is obtained by marking such hidden parts. - - if Private_Part_Is_Hidden_In_SPARK then - Set_Hidden_Part_In_SPARK (Hidden_Region_Start, Token_Ptr); - end if; - -- Deal gracefully with multiple PRIVATE parts while Token = Tok_Private loop diff --git a/gcc/ada/par-prag.adb b/gcc/ada/par-prag.adb index 45830d97b3a..0a1905affee 100644 --- a/gcc/ada/par-prag.adb +++ b/gcc/ada/par-prag.adb @@ -102,10 +102,6 @@ function Prag (Pragma_Node : Node_Id; Semi : Source_Ptr) return Node_Id is -- are some obsolescent features (e.g. character replacements) which are -- handled at parse time. -- - -- SPARK must be processed at parse time, since this restriction controls - -- whether the scanner recognizes a spark HIDE directive formatted as an - -- Ada comment (and generates a Tok_SPARK_Hide token for the directive). - -- -- No_Dependence must be processed at parse time, since otherwise it gets -- handled too late. -- @@ -257,12 +253,11 @@ function Prag (Pragma_Node : Node_Id; Semi : Source_Ptr) return Node_Id is Restriction_Warnings (No_Obsolescent_Features) := Prag_Id = Pragma_Restriction_Warnings; - when Name_SPARK - | Name_SPARK_05 - => - Set_Restriction (SPARK_05, Pragma_Node); - Restriction_Warnings (SPARK_05) := - Prag_Id = Pragma_Restriction_Warnings; + when Name_SPARK_05 => + Error_Msg_Name_1 := Chars (Expr); + Error_Msg_N + ("??% restriction is obsolete and ignored, consider " & + "using 'S'P'A'R'K_'Mode and gnatprove instead", Arg); when others => null; diff --git a/gcc/ada/restrict.adb b/gcc/ada/restrict.adb index 768fd995a08..2c812e81d14 100644 --- a/gcc/ada/restrict.adb +++ b/gcc/ada/restrict.adb @@ -39,34 +39,6 @@ with Uname; use Uname; package body Restrict is - ------------------------------- - -- SPARK Restriction Control -- - ------------------------------- - - -- SPARK HIDE directives allow the effect of the SPARK_05 restriction to be - -- turned off for a specified region of code, and the following tables are - -- the data structures used to keep track of these regions. - - -- The table contains pairs of source locations, the first being the start - -- location for hidden region, and the second being the end location. - - -- Note that the start location is included in the hidden region, while - -- the end location is excluded from it. (It typically corresponds to the - -- next token during scanning.) - - type SPARK_Hide_Entry is record - Start : Source_Ptr; - Stop : Source_Ptr; - end record; - - package SPARK_Hides is new Table.Table ( - Table_Component_Type => SPARK_Hide_Entry, - Table_Index_Type => Natural, - Table_Low_Bound => 1, - Table_Initial => 100, - Table_Increment => 200, - Table_Name => "SPARK Hides"); - -------------------------------- -- Package Local Declarations -- -------------------------------- @@ -511,13 +483,6 @@ package body Restrict is return; end if; - -- In SPARK 05 mode, issue an error for any use of class-wide, even if - -- the No_Dispatch restriction is not set. - - if R = No_Dispatch then - Check_SPARK_05_Restriction ("class-wide is not allowed", N); - end if; - if UI_Is_In_Int_Range (V) then VV := Integer (UI_To_Int (V)); else @@ -846,94 +811,6 @@ package body Restrict is end if; end Check_Restriction_No_Use_Of_Pragma; - -------------------------------- - -- Check_SPARK_05_Restriction -- - -------------------------------- - - procedure Check_SPARK_05_Restriction - (Msg : String; - N : Node_Id; - Force : Boolean := False) - is - Msg_Issued : Boolean; - Save_Error_Msg_Sloc : Source_Ptr; - Onode : constant Node_Id := Original_Node (N); - - begin - -- Output message if Force set - - if Force - - -- Or if this node comes from source - - or else Comes_From_Source (N) - - -- Or if this is a range node which rewrites a range attribute and - -- the range attribute comes from source. - - or else (Nkind (N) = N_Range - and then Nkind (Onode) = N_Attribute_Reference - and then Attribute_Name (Onode) = Name_Range - and then Comes_From_Source (Onode)) - - -- Or this is an expression that does not come from source, which is - -- a rewriting of an expression that does come from source. - - or else (Nkind (N) in N_Subexpr and then Comes_From_Source (Onode)) - then - if Restriction_Check_Required (SPARK_05) - and then Is_In_Hidden_Part_In_SPARK (Sloc (N)) - then - return; - end if; - - -- Since the call to Restriction_Msg from Check_Restriction may set - -- Error_Msg_Sloc to the location of the pragma restriction, save and - -- restore the previous value of the global variable around the call. - - Save_Error_Msg_Sloc := Error_Msg_Sloc; - Check_Restriction (Msg_Issued, SPARK_05, First_Node (N)); - Error_Msg_Sloc := Save_Error_Msg_Sloc; - - if Msg_Issued then - Error_Msg_F ("\\| " & Msg, N); - end if; - end if; - end Check_SPARK_05_Restriction; - - procedure Check_SPARK_05_Restriction - (Msg1 : String; - Msg2 : String; - N : Node_Id) - is - Msg_Issued : Boolean; - Save_Error_Msg_Sloc : Source_Ptr; - - begin - pragma Assert (Msg2'Length /= 0 and then Msg2 (Msg2'First) = '\'); - - if Comes_From_Source (Original_Node (N)) then - if Restriction_Check_Required (SPARK_05) - and then Is_In_Hidden_Part_In_SPARK (Sloc (N)) - then - return; - end if; - - -- Since the call to Restriction_Msg from Check_Restriction may set - -- Error_Msg_Sloc to the location of the pragma restriction, save and - -- restore the previous value of the global variable around the call. - - Save_Error_Msg_Sloc := Error_Msg_Sloc; - Check_Restriction (Msg_Issued, SPARK_05, First_Node (N)); - Error_Msg_Sloc := Save_Error_Msg_Sloc; - - if Msg_Issued then - Error_Msg_F ("\\| " & Msg1, N); - Error_Msg_F (Msg2, N); - end if; - end if; - end Check_SPARK_05_Restriction; - -------------------------------------- -- Check_Wide_Character_Restriction -- -------------------------------------- @@ -1021,25 +898,6 @@ package body Restrict is return Not_A_Restriction_Id; end Get_Restriction_Id; - -------------------------------- - -- Is_In_Hidden_Part_In_SPARK -- - -------------------------------- - - function Is_In_Hidden_Part_In_SPARK (Loc : Source_Ptr) return Boolean is - begin - -- Loop through table of hidden ranges - - for J in SPARK_Hides.First .. SPARK_Hides.Last loop - if SPARK_Hides.Table (J).Start <= Loc - and then Loc < SPARK_Hides.Table (J).Stop - then - return True; - end if; - end loop; - - return False; - end Is_In_Hidden_Part_In_SPARK; - ------------------------------- -- No_Exception_Handlers_Set -- ------------------------------- @@ -1134,21 +992,11 @@ package body Restrict is when Name_No_Task_Attributes => New_Name := Name_No_Task_Attributes_Package; - -- SPARK is special in that we unconditionally warn - - when Name_SPARK => - Error_Msg_Name_1 := Name_SPARK; - Error_Msg_N ("restriction identifier % is obsolescent??", N); - Error_Msg_Name_1 := Name_SPARK_05; - Error_Msg_N ("|use restriction identifier % instead??", N); - return Name_SPARK_05; - when others => return Old_Name; end case; - -- Output warning if we are warning on obsolescent features for all - -- cases other than SPARK. + -- Output warning if we are warning on obsolescent features. if Warn_On_Obsolescent_Feature then Error_Msg_Name_1 := Old_Name; @@ -1250,8 +1098,7 @@ package body Restrict is -- Append given string to Msg, bumping Len appropriately procedure Id_Case (S : String; Quotes : Boolean := True); - -- Given a string S, case it according to current identifier casing, - -- except for SPARK_05 (an acronym) which is set all upper case, and + -- Given a string S, case it according to current identifier casing, and -- store in Error_Msg_String. Then append `~` to the message buffer -- to output the string unchanged surrounded in quotes. The quotes -- are suppressed if Quotes = False. @@ -1284,13 +1131,7 @@ package body Restrict is begin Name_Buffer (1 .. S'Last) := S; Name_Len := S'Length; - - if R = SPARK_05 then - Set_All_Upper_Case; - else - Set_Casing (Identifier_Casing (Get_Source_File_Index (Sloc (N)))); - end if; - + Set_Casing (Identifier_Casing (Get_Source_File_Index (Sloc (N)))); Error_Msg_Strlen := Name_Len; Error_Msg_String (1 .. Name_Len) := Name_Buffer (1 .. Name_Len); @@ -1443,17 +1284,6 @@ package body Restrict is Config_Cunit_Boolean_Restrictions := Cunit_Boolean_Restrictions_Save; end Save_Config_Cunit_Boolean_Restrictions; - ------------------------------ - -- Set_Hidden_Part_In_SPARK -- - ------------------------------ - - procedure Set_Hidden_Part_In_SPARK (Loc1, Loc2 : Source_Ptr) is - begin - SPARK_Hides.Increment_Last; - SPARK_Hides.Table (SPARK_Hides.Last).Start := Loc1; - SPARK_Hides.Table (SPARK_Hides.Last).Stop := Loc2; - end Set_Hidden_Part_In_SPARK; - ------------------------------ -- Set_Profile_Restrictions -- ------------------------------ diff --git a/gcc/ada/restrict.ads b/gcc/ada/restrict.ads index 5926892c06e..e0c6bbacf10 100644 --- a/gcc/ada/restrict.ads +++ b/gcc/ada/restrict.ads @@ -310,22 +310,6 @@ package Restrict is -- WARNING: There is a matching C declaration of this subprogram in fe.h - procedure Check_SPARK_05_Restriction - (Msg : String; - N : Node_Id; - Force : Boolean := False); - -- Node N represents a construct not allowed in SPARK_05 mode. If this is - -- a source node, or if the restriction is forced (Force = True), and - -- the SPARK_05 restriction is set, then an error is issued on N. Msg - -- is appended to the restriction failure message. - - procedure Check_SPARK_05_Restriction - (Msg1 : String; - Msg2 : String; - N : Node_Id); - -- Same as Check_SPARK_05_Restriction except there is a continuation - -- message Msg2 following the initial message Msg1. - procedure Check_No_Implicit_Aliasing (Obj : Node_Id); -- Obj is a node for which Is_Aliased_View is True, which is being used in -- a context (e.g. 'Access) where no implicit aliasing is allowed if the @@ -392,10 +376,6 @@ package Restrict is -- pragma Restrictions_Warning, or attribute Restriction_Set. Returns -- True if N has the proper form for an entity name, False otherwise. - function Is_In_Hidden_Part_In_SPARK (Loc : Source_Ptr) return Boolean; - -- Determine if given location is covered by a hidden region range in the - -- SPARK hides table. - function No_Exception_Handlers_Set return Boolean; -- Test to see if current restrictions settings specify that no exception -- handlers are present. This function is called by Gigi when it needs to @@ -442,11 +422,6 @@ package Restrict is -- of individual Restrictions pragmas). Returns True only if all the -- required restrictions are set. - procedure Set_Hidden_Part_In_SPARK (Loc1, Loc2 : Source_Ptr); - -- Insert a new hidden region range in the SPARK hides table. The effect - -- is to hide any SPARK violation messages which are in the range Loc1 to - -- Loc2-1 (i.e. Loc2 is the first location for reenabling checks). - procedure Set_Profile_Restrictions (P : Profile_Name; N : Node_Id; diff --git a/gcc/ada/scans.ads b/gcc/ada/scans.ads index 7a341081d90..746d337f576 100644 --- a/gcc/ada/scans.ads +++ b/gcc/ada/scans.ads @@ -226,9 +226,6 @@ package Scans is -- the characters '#', '$', '?', '@', '`', '\', '^', '~', or '_'. The -- character value itself is stored in Scans.Special_Character. - Tok_SPARK_Hide, - -- HIDE directive in SPARK - No_Token); -- No_Token is used for initializing Token values to indicate that -- no value has been set yet. diff --git a/gcc/ada/scng.adb b/gcc/ada/scng.adb index db326943911..46d1f8ef5a7 100644 --- a/gcc/ada/scng.adb +++ b/gcc/ada/scng.adb @@ -28,8 +28,6 @@ with Csets; use Csets; with Hostparm; use Hostparm; with Namet; use Namet; with Opt; use Opt; -with Restrict; use Restrict; -with Rident; use Rident; with Scans; use Scans; with Sinput; use Sinput; with Snames; use Snames; @@ -70,19 +68,6 @@ package body Scng is -- the token used is Tok_Identifier. This allows detection of additional -- spaces added in sources when using the builder switch -m. - procedure Accumulate_Token_Checksum_GNAT_6_3; - -- Used in place of Accumulate_Token_Checksum for GNAT versions 5.04 to - -- 6.3, when Tok_Some was not included in Token_Type and the actual - -- Token_Type was used for keywords. This procedure is never used in the - -- compiler or gnatmake, only in gprbuild. - - procedure Accumulate_Token_Checksum_GNAT_5_03; - -- Used in place of Accumulate_Token_Checksum for GNAT version 5.03, when - -- Tok_Interface, Tok_Some, Tok_Synchronized and Tok_Overriding were not - -- included in Token_Type and the actual Token_Type was used for keywords. - -- This procedure is never used in the compiler or gnatmake, only in - -- gprbuild. - procedure Accumulate_Checksum (C : Character); pragma Inline (Accumulate_Checksum); -- This routine accumulates the checksum given character C. During the @@ -138,307 +123,6 @@ package body Scng is Character'Val (Token_Type'Pos (Token))); end Accumulate_Token_Checksum; - ---------------------------------------- - -- Accumulate_Token_Checksum_GNAT_6_3 -- - ---------------------------------------- - - procedure Accumulate_Token_Checksum_GNAT_6_3 is - begin - -- Individual values of Token_Type are used, instead of subranges, so - -- that additions or suppressions of enumerated values in type - -- Token_Type are detected by the compiler. - - case Token is - when Tok_Abs - | Tok_Abstract - | Tok_Access - | Tok_Aliased - | Tok_All - | Tok_Ampersand - | Tok_And - | Tok_Apostrophe - | Tok_Array - | Tok_Asterisk - | Tok_At - | Tok_At_Sign - | Tok_Body - | Tok_Box - | Tok_Char_Literal - | Tok_Colon - | Tok_Colon_Equal - | Tok_Comma - | Tok_Constant - | Tok_Delta - | Tok_Digits - | Tok_Do - | Tok_Dot - | Tok_Double_Asterisk - | Tok_Equal - | Tok_Greater - | Tok_Greater_Equal - | Tok_Greater_Greater - | Tok_Identifier - | Tok_In - | Tok_Integer_Literal - | Tok_Interface - | Tok_Is - | Tok_Left_Bracket - | Tok_Left_Paren - | Tok_Less - | Tok_Less_Equal - | Tok_Limited - | Tok_Minus - | Tok_Mod - | Tok_New - | Tok_Not - | Tok_Not_Equal - | Tok_Null - | Tok_Of - | Tok_Operator_Symbol - | Tok_Or - | Tok_Others - | Tok_Out - | Tok_Plus - | Tok_Range - | Tok_Real_Literal - | Tok_Record - | Tok_Rem - | Tok_Renames - | Tok_Reverse - | Tok_Right_Bracket - | Tok_Right_Paren - | Tok_Slash - | Tok_String_Literal - | Tok_Xor - => - System.CRC32.Update - (System.CRC32.CRC32 (Checksum), - Character'Val (Token_Type'Pos (Token))); - - when Tok_Some => - System.CRC32.Update - (System.CRC32.CRC32 (Checksum), - Character'Val (Token_Type'Pos (Tok_Identifier))); - - when No_Token - | Tok_Abort - | Tok_Accept - | Tok_Arrow - | Tok_Begin - | Tok_Case - | Tok_Comment - | Tok_Declare - | Tok_Delay - | Tok_Dot_Dot - | Tok_Else - | Tok_Elsif - | Tok_End - | Tok_End_Of_Line - | Tok_Entry - | Tok_EOF - | Tok_Exception - | Tok_Exit - | Tok_Extends - | Tok_External - | Tok_External_As_List - | Tok_For - | Tok_Function - | Tok_Generic - | Tok_Goto - | Tok_If - | Tok_Less_Less - | Tok_Loop - | Tok_Overriding - | Tok_Package - | Tok_Pragma - | Tok_Private - | Tok_Procedure - | Tok_Project - | Tok_Protected - | Tok_Raise - | Tok_Requeue - | Tok_Return - | Tok_Select - | Tok_Semicolon - | Tok_Separate - | Tok_SPARK_Hide - | Tok_Special - | Tok_Subtype - | Tok_Synchronized - | Tok_Tagged - | Tok_Task - | Tok_Terminate - | Tok_Then - | Tok_Type - | Tok_Until - | Tok_Use - | Tok_Vertical_Bar - | Tok_When - | Tok_While - | Tok_With - => - System.CRC32.Update - (System.CRC32.CRC32 (Checksum), - Character'Val (Token_Type'Pos (Token_Type'Pred (Token)))); - end case; - end Accumulate_Token_Checksum_GNAT_6_3; - - ----------------------------------------- - -- Accumulate_Token_Checksum_GNAT_5_03 -- - ----------------------------------------- - - procedure Accumulate_Token_Checksum_GNAT_5_03 is - begin - -- Individual values of Token_Type are used, instead of subranges, so - -- that additions or suppressions of enumerated values in type - -- Token_Type are detected by the compiler. - - case Token is - when Tok_Abs - | Tok_Abstract - | Tok_Access - | Tok_Aliased - | Tok_All - | Tok_Ampersand - | Tok_And - | Tok_Apostrophe - | Tok_Array - | Tok_Asterisk - | Tok_At - | Tok_At_Sign - | Tok_Body - | Tok_Box - | Tok_Char_Literal - | Tok_Colon - | Tok_Colon_Equal - | Tok_Comma - | Tok_Constant - | Tok_Delta - | Tok_Digits - | Tok_Do - | Tok_Dot - | Tok_Double_Asterisk - | Tok_Equal - | Tok_Greater - | Tok_Greater_Equal - | Tok_Greater_Greater - | Tok_Identifier - | Tok_In - | Tok_Integer_Literal - | Tok_Is - | Tok_Left_Bracket - | Tok_Left_Paren - | Tok_Less - | Tok_Less_Equal - | Tok_Minus - | Tok_Mod - | Tok_New - | Tok_Not - | Tok_Not_Equal - | Tok_Null - | Tok_Operator_Symbol - | Tok_Or - | Tok_Others - | Tok_Plus - | Tok_Range - | Tok_Real_Literal - | Tok_Rem - | Tok_Right_Bracket - | Tok_Right_Paren - | Tok_Slash - | Tok_String_Literal - | Tok_Xor - => - System.CRC32.Update - (System.CRC32.CRC32 (Checksum), - Character'Val (Token_Type'Pos (Token))); - - when Tok_Interface - | Tok_Overriding - | Tok_Some - | Tok_Synchronized - => - System.CRC32.Update - (System.CRC32.CRC32 (Checksum), - Character'Val (Token_Type'Pos (Tok_Identifier))); - - when Tok_Limited - | Tok_Of - | Tok_Out - | Tok_Record - | Tok_Renames - | Tok_Reverse - => - System.CRC32.Update - (System.CRC32.CRC32 (Checksum), - Character'Val (Token_Type'Pos (Token) - 1)); - - when Tok_Abort - | Tok_Accept - | Tok_Begin - | Tok_Case - | Tok_Declare - | Tok_Delay - | Tok_Else - | Tok_Elsif - | Tok_End - | Tok_Entry - | Tok_Exception - | Tok_Exit - | Tok_For - | Tok_Goto - | Tok_If - | Tok_Less_Less - | Tok_Loop - | Tok_Pragma - | Tok_Protected - | Tok_Raise - | Tok_Requeue - | Tok_Return - | Tok_Select - | Tok_Subtype - | Tok_Tagged - | Tok_Task - | Tok_Terminate - | Tok_Then - | Tok_Type - | Tok_Until - | Tok_When - | Tok_While - => - System.CRC32.Update - (System.CRC32.CRC32 (Checksum), - Character'Val (Token_Type'Pos (Token) - 2)); - - when No_Token - | Tok_Arrow - | Tok_Comment - | Tok_Dot_Dot - | Tok_End_Of_Line - | Tok_EOF - | Tok_Extends - | Tok_External - | Tok_External_As_List - | Tok_Function - | Tok_Generic - | Tok_Package - | Tok_Private - | Tok_Procedure - | Tok_Project - | Tok_Semicolon - | Tok_Separate - | Tok_SPARK_Hide - | Tok_Special - | Tok_Use - | Tok_Vertical_Bar - | Tok_With - => - System.CRC32.Update - (System.CRC32.CRC32 (Checksum), - Character'Val (Token_Type'Pos (Token) - 4)); - end case; - end Accumulate_Token_Checksum_GNAT_5_03; - ----------------------- -- Check_End_Of_Line -- ----------------------- @@ -1058,11 +742,7 @@ package body Scng is end if; end if; - if Checksum_Accumulate_Token_Checksum then - Accumulate_Token_Checksum; - end if; - - return; + Accumulate_Token_Checksum; end Nlit; ---------- @@ -1980,47 +1660,6 @@ package body Scng is Token := Tok_Comment; return; end if; - - -- If the SPARK restriction is set for this unit, then generate - -- a token Tok_SPARK_Hide for a SPARK HIDE directive. - - if Restriction_Check_Required (SPARK_05) - and then Source (Start_Of_Comment) = '#' - then - declare - Scan_SPARK_Ptr : Source_Ptr; - - begin - Scan_SPARK_Ptr := Start_Of_Comment + 1; - - -- Scan out blanks - - while Source (Scan_SPARK_Ptr) = ' ' - or else Source (Scan_SPARK_Ptr) = HT - loop - Scan_SPARK_Ptr := Scan_SPARK_Ptr + 1; - end loop; - - -- Recognize HIDE directive. SPARK input cannot be - -- encoded as wide characters, so only deal with - -- lower/upper case. - - if (Source (Scan_SPARK_Ptr) = 'h' - or else Source (Scan_SPARK_Ptr) = 'H') - and then (Source (Scan_SPARK_Ptr + 1) = 'i' - or else Source (Scan_SPARK_Ptr + 1) = 'I') - and then (Source (Scan_SPARK_Ptr + 2) = 'd' - or else Source (Scan_SPARK_Ptr + 2) = 'D') - and then (Source (Scan_SPARK_Ptr + 3) = 'e' - or else Source (Scan_SPARK_Ptr + 3) = 'E') - and then (Source (Scan_SPARK_Ptr + 4) = ' ' - or else Source (Scan_SPARK_Ptr + 4) = HT) - then - Token := Tok_SPARK_Hide; - return; - end if; - end; - end if; end if; end Minus_Case; @@ -2926,21 +2565,8 @@ package body Scng is -- Here is where we check if it was a keyword if Is_Keyword_Name (Token_Name) then - if Opt.Checksum_GNAT_6_3 then - Token := Token_Type'Val (Get_Name_Table_Byte (Token_Name)); - - if Checksum_Accumulate_Token_Checksum then - if Checksum_GNAT_5_03 then - Accumulate_Token_Checksum_GNAT_5_03; - else - Accumulate_Token_Checksum_GNAT_6_3; - end if; - end if; - - else - Accumulate_Token_Checksum; - Token := Token_Type'Val (Get_Name_Table_Byte (Token_Name)); - end if; + Accumulate_Token_Checksum; + Token := Token_Type'Val (Get_Name_Table_Byte (Token_Name)); -- Keyword style checks @@ -2997,12 +2623,8 @@ package body Scng is -- It is an identifier after all else - if Checksum_Accumulate_Token_Checksum then - Accumulate_Token_Checksum; - end if; - + Accumulate_Token_Checksum; Post_Scan; - return; end if; end Scan; diff --git a/gcc/ada/sem_aggr.adb b/gcc/ada/sem_aggr.adb index 88df5355570..a3ac7caf6f7 100644 --- a/gcc/ada/sem_aggr.adb +++ b/gcc/ada/sem_aggr.adb @@ -117,15 +117,6 @@ package body Sem_Aggr is -- Expression is also OK in an instance or inlining context, because we -- have already preanalyzed and it is known to be type correct. - procedure Check_Qualified_Aggregate (Level : Nat; Expr : Node_Id); - -- Given aggregate Expr, check that sub-aggregates of Expr that are nested - -- at Level are qualified. If Level = 0, this applies to Expr directly. - -- Only issue errors in formal verification mode. - - function Is_Top_Level_Aggregate (Expr : Node_Id) return Boolean; - -- Return True of Expr is an aggregate not contained directly in another - -- aggregate. - ------------------------------------------------------ -- Subprograms used for RECORD AGGREGATE Processing -- ------------------------------------------------------ @@ -731,43 +722,6 @@ package body Sem_Aggr is end if; end Check_Expr_OK_In_Limited_Aggregate; - ------------------------------- - -- Check_Qualified_Aggregate -- - ------------------------------- - - procedure Check_Qualified_Aggregate (Level : Nat; Expr : Node_Id) is - Comp_Expr : Node_Id; - Comp_Assn : Node_Id; - - begin - if Level = 0 then - if Nkind (Parent (Expr)) /= N_Qualified_Expression then - Check_SPARK_05_Restriction ("aggregate should be qualified", Expr); - end if; - - else - Comp_Expr := First (Expressions (Expr)); - while Present (Comp_Expr) loop - if Nkind (Comp_Expr) = N_Aggregate then - Check_Qualified_Aggregate (Level - 1, Comp_Expr); - end if; - - Comp_Expr := Next (Comp_Expr); - end loop; - - Comp_Assn := First (Component_Associations (Expr)); - while Present (Comp_Assn) loop - Comp_Expr := Expression (Comp_Assn); - - if Nkind (Comp_Expr) = N_Aggregate then - Check_Qualified_Aggregate (Level - 1, Comp_Expr); - end if; - - Comp_Assn := Next (Comp_Assn); - end loop; - end if; - end Check_Qualified_Aggregate; - ---------------------------------------- -- Check_Static_Discriminated_Subtype -- ---------------------------------------- @@ -853,17 +807,6 @@ package body Sem_Aggr is and then No (Next (First (Choice_List (First (Assoc))))); end Is_Single_Aggregate; - ---------------------------- - -- Is_Top_Level_Aggregate -- - ---------------------------- - - function Is_Top_Level_Aggregate (Expr : Node_Id) return Boolean is - begin - return Nkind (Parent (Expr)) /= N_Aggregate - and then (Nkind (Parent (Expr)) /= N_Component_Association - or else Nkind (Parent (Parent (Expr))) /= N_Aggregate); - end Is_Top_Level_Aggregate; - -------------------------------- -- Make_String_Into_Aggregate -- -------------------------------- @@ -948,41 +891,6 @@ package body Sem_Aggr is end; end if; - -- An unqualified aggregate is restricted in SPARK to: - - -- An aggregate item inside an aggregate for a multi-dimensional array - - -- An expression being assigned to an unconstrained array, but only if - -- the aggregate specifies a value for OTHERS only. - - if Nkind (Parent (N)) = N_Qualified_Expression then - if Is_Array_Type (Typ) then - Check_Qualified_Aggregate (Number_Dimensions (Typ), N); - else - Check_Qualified_Aggregate (1, N); - end if; - else - if Is_Array_Type (Typ) - and then Nkind (Parent (N)) = N_Assignment_Statement - and then not Is_Constrained (Etype (Name (Parent (N)))) - then - if not Is_Others_Aggregate (N) then - Check_SPARK_05_Restriction - ("array aggregate should have only OTHERS", N); - end if; - - elsif Is_Top_Level_Aggregate (N) then - Check_SPARK_05_Restriction ("aggregate should be qualified", N); - - -- The legality of this unqualified aggregate is checked by calling - -- Check_Qualified_Aggregate from one of its enclosing aggregate, - -- unless one of these already causes an error to be issued. - - else - null; - end if; - end if; - -- Check for aggregates not allowed in configurable run-time mode. -- We allow all cases of aggregates that do not come from source, since -- these are all assumed to be small (e.g. bounds of a string literal). @@ -2069,16 +1977,6 @@ package body Sem_Aggr is -- bounds of the array aggregate are within range. Set_Do_Range_Check (Choice, False); - - -- In SPARK, the choice must be static - - if not (Is_OK_Static_Expression (Choice) - or else (Nkind (Choice) = N_Range - and then Is_OK_Static_Range (Choice))) - then - Check_SPARK_05_Restriction - ("choice should be static", Choice); - end if; end if; -- If we could not resolve the discrete choice stop here @@ -3257,7 +3155,6 @@ package body Sem_Aggr is -- In SPARK, the ancestor part cannot be a type mark if Is_Entity_Name (A) and then Is_Type (Entity (A)) then - Check_SPARK_05_Restriction ("ancestor part cannot be a type mark", A); -- AI05-0115: if the ancestor part is a subtype mark, the ancestor -- must not have unknown discriminants. @@ -4332,12 +4229,6 @@ package body Sem_Aggr is if Present (Component_Associations (N)) and then Present (First (Component_Associations (N))) then - if Present (Expressions (N)) then - Check_SPARK_05_Restriction - ("named association cannot follow positional one", - First (Choices (First (Component_Associations (N))))); - end if; - declare Assoc : Node_Id; @@ -4349,18 +4240,6 @@ package body Sem_Aggr is ("iterated component association can only appear in an " & "array aggregate", N); raise Unrecoverable_Error; - - else - if List_Length (Choices (Assoc)) > 1 then - Check_SPARK_05_Restriction - ("component association in record aggregate must " - & "contain a single choice", Assoc); - end if; - - if Nkind (First (Choices (Assoc))) = N_Others_Choice then - Check_SPARK_05_Restriction - ("record aggregate cannot contain OTHERS", Assoc); - end if; end if; Assoc := Next (Assoc); diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb index 5fef9c27fcf..c59c0595547 100644 --- a/gcc/ada/sem_attr.adb +++ b/gcc/ada/sem_attr.adb @@ -359,9 +359,6 @@ package body Sem_Attr is -- Verify that prefix of attribute N is a float type and that -- two attribute expressions are present - procedure Check_SPARK_05_Restriction_On_Attribute; - -- Issue an error in formal mode because attribute N is allowed - procedure Check_Integer_Type; -- Verify that prefix of attribute N is an integer type @@ -813,7 +810,6 @@ package body Sem_Attr is -- Start of processing for Analyze_Access_Attribute begin - Check_SPARK_05_Restriction_On_Attribute; Check_E0; if Nkind (P) = N_Character_Literal then @@ -1428,8 +1424,6 @@ package body Sem_Attr is procedure Analyze_Image_Attribute (Str_Typ : Entity_Id) is begin - Check_SPARK_05_Restriction_On_Attribute; - -- AI12-0124: The ARG has adopted the GNAT semantics of 'Img for -- scalar types, so that the prefix can be an object, a named value, -- or a type. If the prefix is an object, there is no argument. @@ -2312,16 +2306,6 @@ package body Sem_Attr is end if; end Check_Scalar_Type; - ------------------------------------------ - -- Check_SPARK_05_Restriction_On_Attribute -- - ------------------------------------------ - - procedure Check_SPARK_05_Restriction_On_Attribute is - begin - Error_Msg_Name_1 := Aname; - Check_SPARK_05_Restriction ("attribute % is not allowed", P); - end Check_SPARK_05_Restriction_On_Attribute; - --------------------------- -- Check_Standard_Prefix -- --------------------------- @@ -3056,21 +3040,6 @@ package body Sem_Attr is end if; end if; - -- In SPARK, attributes of private types are only allowed if the full - -- type declaration is visible. - - -- Note: the check for Present (Entity (P)) defends against some error - -- conditions where the Entity field is not set. - - if Is_Entity_Name (P) and then Present (Entity (P)) - and then Is_Type (Entity (P)) - and then Is_Private_Type (P_Type) - and then not In_Open_Scopes (Scope (P_Type)) - and then not In_Spec_Expression - then - Check_SPARK_05_Restriction ("invisible attribute of type", N); - end if; - -- Remaining processing depends on attribute case Attr_Id is @@ -3239,12 +3208,6 @@ package body Sem_Attr is ("?r?redundant attribute, & is its own base type", N, Typ); end if; - if Nkind (Parent (N)) /= N_Attribute_Reference then - Error_Msg_Name_1 := Aname; - Check_SPARK_05_Restriction - ("attribute% is only allowed as prefix of another attribute", P); - end if; - Set_Etype (N, Base_Type (Entity (P))); Set_Entity (N, Base_Type (Entity (P))); Rewrite (N, New_Occurrence_Of (Entity (N), Loc)); @@ -5230,14 +5193,6 @@ package body Sem_Attr is when Attribute_Pos => Check_Discrete_Type; Check_E1; - - if Is_Boolean_Type (P_Type) then - Error_Msg_Name_1 := Aname; - Error_Msg_Name_2 := Chars (P_Type); - Check_SPARK_05_Restriction - ("attribute% is not allowed for type%", P); - end if; - Resolve (E1, P_Base_Type); Set_Etype (N, Universal_Integer); @@ -5256,14 +5211,6 @@ package body Sem_Attr is when Attribute_Pred => Check_Scalar_Type; Check_E1; - - if Is_Real_Type (P_Type) or else Is_Boolean_Type (P_Type) then - Error_Msg_Name_1 := Aname; - Error_Msg_Name_2 := Chars (P_Type); - Check_SPARK_05_Restriction - ("attribute% is not allowed for type%", P); - end if; - Resolve (E1, P_Base_Type); Set_Etype (N, P_Base_Type); @@ -6175,14 +6122,6 @@ package body Sem_Attr is when Attribute_Succ => Check_Scalar_Type; Check_E1; - - if Is_Real_Type (P_Type) or else Is_Boolean_Type (P_Type) then - Error_Msg_Name_1 := Aname; - Error_Msg_Name_2 := Chars (P_Type); - Check_SPARK_05_Restriction - ("attribute% is not allowed for type%", P); - end if; - Resolve (E1, P_Base_Type); Set_Etype (N, P_Base_Type); @@ -6982,13 +6921,6 @@ package body Sem_Attr is Check_E1; Check_Discrete_Type; - if Is_Boolean_Type (P_Type) then - Error_Msg_Name_1 := Aname; - Error_Msg_Name_2 := Chars (P_Type); - Check_SPARK_05_Restriction - ("attribute% is not allowed for type%", P); - end if; - -- Note, we need a range check in general, but we wait for the -- Resolve call to do this, since we want to let Eval_Attribute -- have a chance to find an static illegality first. @@ -7090,7 +7022,6 @@ package body Sem_Attr is ----------- when Attribute_Value => - Check_SPARK_05_Restriction_On_Attribute; Check_E1; Check_Scalar_Type; @@ -7181,7 +7112,6 @@ package body Sem_Attr is ---------------- when Attribute_Wide_Value => - Check_SPARK_05_Restriction_On_Attribute; Check_E1; Check_Scalar_Type; @@ -7235,7 +7165,6 @@ package body Sem_Attr is ---------------- when Attribute_Wide_Width => - Check_SPARK_05_Restriction_On_Attribute; Check_E0; Check_Scalar_Type; Set_Etype (N, Universal_Integer); @@ -7245,7 +7174,6 @@ package body Sem_Attr is ----------- when Attribute_Width => - Check_SPARK_05_Restriction_On_Attribute; Check_E0; Check_Scalar_Type; Set_Etype (N, Universal_Integer); @@ -11316,6 +11244,7 @@ package body Sem_Attr is -- will be reported when resolving the call. if Attr_Id /= Attribute_Unrestricted_Access then + Error_Msg_Name_1 := Aname; Error_Msg_N ("prefix of % attribute must be aliased", P); -- Check for unrestricted access where expected type is a thin diff --git a/gcc/ada/sem_ch11.adb b/gcc/ada/sem_ch11.adb index 8ff7420b138..ea7f3641ada 100644 --- a/gcc/ada/sem_ch11.adb +++ b/gcc/ada/sem_ch11.adb @@ -460,8 +460,6 @@ package body Sem_Ch11 is Check_Compiler_Unit ("raise expression", N); end if; - Check_SPARK_05_Restriction ("raise expression is not allowed", N); - -- Check exception restrictions on the original source if Comes_From_Source (N) then @@ -517,10 +515,6 @@ package body Sem_Ch11 is Par : Node_Id; begin - if Comes_From_Source (N) then - Check_SPARK_05_Restriction ("raise statement is not allowed", N); - end if; - Check_Unreachable_Code (N); -- Check exception restrictions on the original source @@ -722,10 +716,6 @@ package body Sem_Ch11 is -- Start of processing for Analyze_Raise_xxx_Error begin - if Nkind (Original_Node (N)) = N_Raise_Statement then - Check_SPARK_05_Restriction ("raise statement is not allowed", N); - end if; - if No (Etype (N)) then Set_Etype (N, Standard_Void_Type); end if; diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index 2b38f924133..91c86feade6 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -3576,8 +3576,6 @@ package body Sem_Ch12 is Save_Parent : Node_Id; begin - Check_SPARK_05_Restriction ("generic is not allowed", N); - -- A generic may grant access to its private enclosing context depending -- on the placement of its corresponding body. From elaboration point of -- view, the flow of execution may enter this private context, and then @@ -3782,8 +3780,6 @@ package body Sem_Ch12 is Typ : Entity_Id; begin - Check_SPARK_05_Restriction ("generic is not allowed", N); - -- A generic may grant access to its private enclosing context depending -- on the placement of its corresponding body. From elaboration point of -- view, the flow of execution may enter this private context, and then @@ -4115,8 +4111,6 @@ package body Sem_Ch12 is Modes => True, Warnings => True); - Check_SPARK_05_Restriction ("generic is not allowed", N); - -- Very first thing: check for Text_IO special unit in case we are -- instantiating one of the children of [[Wide_]Wide_]Text_IO. @@ -5562,8 +5556,6 @@ package body Sem_Ch12 is Modes => True, Warnings => True); - Check_SPARK_05_Restriction ("generic is not allowed", N); - -- Very first thing: check for special Text_IO unit in case we are -- instantiating one of the children of [[Wide_]Wide_]Text_IO. Of course -- such an instantiation is bogus (these are packages, not subprograms), diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 4d6382e59d4..9cd1b35d5b4 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -725,8 +725,6 @@ package body Sem_Ch3 is Enclosing_Prot_Type : Entity_Id := Empty; begin - Check_SPARK_05_Restriction ("access type is not allowed", N); - if Is_Entry (Current_Scope) and then Is_Task_Type (Etype (Scope (Current_Scope))) then @@ -1059,8 +1057,6 @@ package body Sem_Ch3 is -- Start of processing for Access_Subprogram_Declaration begin - Check_SPARK_05_Restriction ("access type is not allowed", T_Def); - -- Associate the Itype node with the inner full-type declaration or -- subprogram spec or entry body. This is required to handle nested -- anonymous declarations. For example: @@ -1320,8 +1316,6 @@ package body Sem_Ch3 is Full_Desig : Entity_Id; begin - Check_SPARK_05_Restriction ("access type is not allowed", Def); - -- Check for permissible use of incomplete type if Nkind (S) /= N_Subtype_Indication then @@ -1932,10 +1926,6 @@ package body Sem_Ch3 is T := Find_Type_Of_Object (Subtype_Indication (Component_Definition (N)), N); - if not Nkind_In (Typ, N_Identifier, N_Expanded_Name) then - Check_SPARK_05_Restriction ("subtype mark required", Typ); - end if; - -- Ada 2005 (AI-230): Access Definition case else @@ -1986,7 +1976,6 @@ package body Sem_Ch3 is -- package Sem). if Present (E) then - Check_SPARK_05_Restriction ("default expression is not allowed", E); Preanalyze_Default_Expression (E, T); Check_Initialization (T, E); @@ -2611,23 +2600,9 @@ package body Sem_Ch3 is -- Start of processing for Analyze_Declarations begin - if Restriction_Check_Required (SPARK_05) then - Check_Later_Vs_Basic_Declarations (L, During_Parsing => False); - end if; - Decl := First (L); while Present (Decl) loop - -- Package spec cannot contain a package declaration in SPARK - - if Nkind (Decl) = N_Package_Declaration - and then Nkind (Parent (L)) = N_Package_Specification - then - Check_SPARK_05_Restriction - ("package specification cannot contain a package declaration", - Decl); - end if; - -- Complete analysis of declaration Analyze (Decl); @@ -3091,16 +3066,10 @@ package body Sem_Ch3 is when N_Derived_Type_Definition => null; - -- For record types, discriminants are allowed, unless we are in - -- SPARK. + -- For record types, discriminants are allowed. when N_Record_Definition => - if Present (Discriminant_Specifications (N)) then - Check_SPARK_05_Restriction - ("discriminant type is not allowed", - Defining_Identifier - (First (Discriminant_Specifications (N)))); - end if; + null; when others => if Present (Discriminant_Specifications (N)) then @@ -3211,12 +3180,6 @@ package body Sem_Ch3 is return; end if; - -- Controlled type is not allowed in SPARK - - if Is_Visibly_Controlled (T) then - Check_SPARK_05_Restriction ("controlled type is not allowed", N); - end if; - -- Some common processing for all types Set_Depends_On_Private (T, Has_Private_Component (T)); @@ -3358,8 +3321,6 @@ package body Sem_Ch3 is T : Entity_Id; begin - Check_SPARK_05_Restriction ("incomplete type is not allowed", N); - Generate_Definition (Defining_Identifier (N)); -- Process an incomplete declaration. The identifier must not have been @@ -4170,38 +4131,10 @@ package body Sem_Ch3 is Act_T := T; - -- These checks should be performed before the initialization expression - -- is considered, so that the Object_Definition node is still the same - -- as in source code. - - -- In SPARK, the nominal subtype is always given by a subtype mark - -- and must not be unconstrained. (The only exception to this is the - -- acceptance of declarations of constants of type String.) - - if not Nkind_In (Object_Definition (N), N_Expanded_Name, N_Identifier) - then - Check_SPARK_05_Restriction - ("subtype mark required", Object_Definition (N)); - - elsif Is_Array_Type (T) - and then not Is_Constrained (T) - and then T /= Standard_String - then - Check_SPARK_05_Restriction - ("subtype mark of constrained type expected", - Object_Definition (N)); - end if; - if Is_Library_Level_Entity (Id) then Check_Dynamic_Object (T); end if; - -- There are no aliased objects in SPARK - - if Aliased_Present (N) then - Check_SPARK_05_Restriction ("aliased object is not allowed", N); - end if; - -- Process initialization expression if present and not in error if Present (E) and then E /= Error then @@ -4396,18 +4329,6 @@ package body Sem_Ch3 is Apply_Scalar_Range_Check (E, T); Apply_Static_Length_Check (E, T); - if Nkind (Original_Node (N)) = N_Object_Declaration - and then Comes_From_Source (Original_Node (N)) - - -- Only call test if needed - - and then Restriction_Check_Required (SPARK_05) - and then not Is_SPARK_05_Initialization_Expr (Original_Node (E)) - then - Check_SPARK_05_Restriction - ("initialization expression is not appropriate", E); - end if; - -- A formal parameter of a specific tagged type whose related -- subprogram is subject to pragma Extensions_Visible with value -- "False" cannot be implicitly converted to a class-wide type by @@ -4505,14 +4426,6 @@ package body Sem_Ch3 is if not Is_Definite_Subtype (T) then - -- In SPARK, a declaration of unconstrained type is allowed - -- only for constants of type string. - - if Is_String_Type (T) and then not Constant_Present (N) then - Check_SPARK_05_Restriction - ("declaration of object of unconstrained type not allowed", N); - end if; - -- Nothing to do in deferred constant case if Constant_Present (N) and then No (E) then @@ -5410,58 +5323,6 @@ package body Sem_Ch3 is end if; end if; - -- Subtype of Boolean cannot have a constraint in SPARK - - if Is_Boolean_Type (T) - and then Nkind (Subtype_Indication (N)) = N_Subtype_Indication - then - Check_SPARK_05_Restriction - ("subtype of Boolean cannot have constraint", N); - end if; - - if Nkind (Subtype_Indication (N)) = N_Subtype_Indication then - declare - Cstr : constant Node_Id := Constraint (Subtype_Indication (N)); - One_Cstr : Node_Id; - Low : Node_Id; - High : Node_Id; - - begin - if Nkind (Cstr) = N_Index_Or_Discriminant_Constraint then - One_Cstr := First (Constraints (Cstr)); - while Present (One_Cstr) loop - - -- Index or discriminant constraint in SPARK must be a - -- subtype mark. - - if not - Nkind_In (One_Cstr, N_Identifier, N_Expanded_Name) - then - Check_SPARK_05_Restriction - ("subtype mark required", One_Cstr); - - -- String subtype must have a lower bound of 1 in SPARK. - -- Note that we do not need to test for the nonstatic case - -- here, since that was already taken care of in - -- Process_Range_Expr_In_Decl. - - elsif Base_Type (T) = Standard_String then - Get_Index_Bounds (One_Cstr, Low, High); - - if Is_OK_Static_Expression (Low) - and then Expr_Value (Low) /= 1 - then - Check_SPARK_05_Restriction - ("String subtype must have lower bound of 1", N); - end if; - end if; - - Next (One_Cstr); - end loop; - end if; - end; - end if; - -- In the case where there is no constraint given in the subtype -- indication, Process_Subtype just returns the Subtype_Mark, so its -- semantic attributes must be established here. @@ -5469,14 +5330,6 @@ package body Sem_Ch3 is if Nkind (Subtype_Indication (N)) /= N_Subtype_Indication then Set_Etype (Id, Base_Type (T)); - -- Subtype of unconstrained array without constraint is not allowed - -- in SPARK. - - if Is_Array_Type (T) and then not Is_Constrained (T) then - Check_SPARK_05_Restriction - ("subtype of unconstrained array must have constraint", N); - end if; - case Ekind (T) is when Array_Kind => Set_Ekind (Id, E_Array_Subtype); @@ -6140,12 +5993,6 @@ package body Sem_Ch3 is Set_Etype (Index, Standard_Boolean); end if; - -- Check SPARK restriction requiring a subtype mark - - if not Nkind_In (Index, N_Identifier, N_Expanded_Name) then - Check_SPARK_05_Restriction ("subtype mark required", Index); - end if; - -- Add a subtype declaration for each index of private array type -- declaration whose type is also private. For example: @@ -6221,14 +6068,8 @@ package body Sem_Ch3 is if Present (Component_Typ) then Element_Type := Process_Subtype (Component_Typ, P, Related_Id, 'C'); - Set_Etype (Component_Typ, Element_Type); - if not Nkind_In (Component_Typ, N_Identifier, N_Expanded_Name) then - Check_SPARK_05_Restriction - ("subtype mark required", Component_Typ); - end if; - -- Ada 2005 (AI-230): Access Definition case else pragma Assert (Present (Access_Definition (Component_Def))); @@ -6339,8 +6180,6 @@ package body Sem_Ch3 is Set_Packed_Array_Impl_Type (T, Empty); if Aliased_Present (Component_Definition (Def)) then - Check_SPARK_05_Restriction - ("aliased is not allowed", Component_Definition (Def)); Set_Has_Aliased_Components (Etype (T)); -- AI12-001: All aliased objects are considered to be specified as @@ -13855,8 +13694,6 @@ package body Sem_Ch3 is else pragma Assert (Nkind (C) = N_Digits_Constraint); - Check_SPARK_05_Restriction ("digits constraint is not allowed", S); - Digits_Expr := Digits_Expression (C); Analyze_And_Resolve (Digits_Expr, Any_Integer); @@ -14098,8 +13935,6 @@ package body Sem_Ch3 is -- Digits constraint present if Nkind (C) = N_Digits_Constraint then - - Check_SPARK_05_Restriction ("digits constraint is not allowed", S); Check_Restriction (No_Obsolescent_Features, C); if Warn_On_Obsolescent_Feature then @@ -14332,8 +14167,6 @@ package body Sem_Ch3 is -- Delta constraint present if Nkind (C) = N_Delta_Constraint then - - Check_SPARK_05_Restriction ("delta constraint is not allowed", S); Check_Restriction (No_Obsolescent_Features, C); if Warn_On_Obsolescent_Feature then @@ -14979,8 +14812,6 @@ package body Sem_Ch3 is Bound_Val : Ureal; begin - Check_SPARK_05_Restriction - ("decimal fixed point type is not allowed", Def); Check_Restriction (No_Fixed_Point, Def); -- Create implicit base type @@ -16622,8 +16453,6 @@ package body Sem_Ch3 is -- parent is also an interface. if Interface_Present (Def) then - Check_SPARK_05_Restriction ("interface is not allowed", Def); - if not Is_Interface (Parent_Type) then Diagnose_Interface (Indic, Parent_Type); @@ -16869,11 +16698,6 @@ package body Sem_Ch3 is if Is_Type (T) then Set_Has_Discriminants (T, False); end if; - - -- The type is allowed to have discriminants - - else - Check_SPARK_05_Restriction ("discriminant type is not allowed", N); end if; end if; @@ -17060,14 +16884,6 @@ package body Sem_Ch3 is end if; end if; end if; - - -- In SPARK, there are no derived type definitions other than type - -- extensions of tagged record types. - - if No (Extension) then - Check_SPARK_05_Restriction - ("derived type is not allowed", Original_Node (N)); - end if; end Derived_Type_Declaration; ------------------------ @@ -19184,8 +19000,7 @@ package body Sem_Ch3 is (N : Node_Id; Related_Nod : Node_Id; Related_Id : Entity_Id := Empty; - Suffix_Index : Nat := 1; - In_Iter_Schm : Boolean := False) + Suffix_Index : Nat := 1) is R : Node_Id; T : Entity_Id; @@ -19297,7 +19112,7 @@ package body Sem_Ch3 is end if; R := N; - Process_Range_Expr_In_Decl (R, T, In_Iter_Schm => In_Iter_Schm); + Process_Range_Expr_In_Decl (R, T); elsif Nkind (N) = N_Subtype_Indication then @@ -19314,8 +19129,7 @@ package body Sem_Ch3 is R := Range_Expression (Constraint (N)); Resolve (R, T); - Process_Range_Expr_In_Decl - (R, Entity (Subtype_Mark (N)), In_Iter_Schm => In_Iter_Schm); + Process_Range_Expr_In_Decl (R, Entity (Subtype_Mark (N))); elsif Nkind (N) = N_Attribute_Reference then @@ -19576,7 +19390,6 @@ package body Sem_Ch3 is -- Nonbinary case elsif M_Val < 2 ** Bits then - Check_SPARK_05_Restriction ("modulus should be a power of 2", T); Set_Non_Binary_Modulus (T); if Bits > System_Max_Nonbinary_Modulus_Power then @@ -20584,15 +20397,6 @@ package body Sem_Ch3 is -- ELSE. else - -- In formal mode, when completing a private extension the type - -- named in the private part must be exactly the same as that - -- named in the visible part. - - if Priv_Parent /= Full_Parent then - Error_Msg_Name_1 := Chars (Priv_Parent); - Check_SPARK_05_Restriction ("% expected", Full_Indic); - end if; - -- Check the rules of 7.3(10): if the private extension inherits -- known discriminants, then the full type must also inherit those -- discriminants from the same (ancestor) type, and the parent @@ -21225,8 +21029,7 @@ package body Sem_Ch3 is T : Entity_Id; Subtyp : Entity_Id := Empty; Check_List : List_Id := No_List; - R_Check_Off : Boolean := False; - In_Iter_Schm : Boolean := False) + R_Check_Off : Boolean := False) is Lo, Hi : Node_Id; R_Checks : Check_Result; @@ -21237,16 +21040,6 @@ package body Sem_Ch3 is Analyze_And_Resolve (R, Base_Type (T)); if Nkind (R) = N_Range then - - -- In SPARK, all ranges should be static, with the exception of the - -- discrete type definition of a loop parameter specification. - - if not In_Iter_Schm - and then not Is_OK_Static_Range (R) - then - Check_SPARK_05_Restriction ("range should be static", R); - end if; - Lo := Low_Bound (R); Hi := High_Bound (R); @@ -21967,14 +21760,6 @@ package body Sem_Ch3 is -- Normal case if Ada_Version < Ada_2005 or else not Interface_Present (Def) then - if Limited_Present (Def) then - Check_SPARK_05_Restriction ("limited is not allowed", N); - end if; - - if Abstract_Present (Def) then - Check_SPARK_05_Restriction ("abstract is not allowed", N); - end if; - -- The flag Is_Tagged_Type might have already been set by -- Find_Type_Name if it detected an error for declaration T. This -- arises in the case of private tagged types where the full view @@ -21998,8 +21783,6 @@ package body Sem_Ch3 is or else Abstract_Present (Def)); else - Check_SPARK_05_Restriction ("interface is not allowed", N); - Is_Tagged := True; Analyze_Interface_Declaration (T, Def); @@ -22141,40 +21924,6 @@ package body Sem_Ch3 is T := Prev_T; end if; - -- In SPARK, tagged types and type extensions may only be declared in - -- the specification of library unit packages. - - if Present (Def) and then Is_Tagged_Type (T) then - declare - Typ : Node_Id; - Ctxt : Node_Id; - - begin - if Nkind (Parent (Def)) = N_Full_Type_Declaration then - Typ := Parent (Def); - else - pragma Assert - (Nkind (Parent (Def)) = N_Derived_Type_Definition); - Typ := Parent (Parent (Def)); - end if; - - Ctxt := Parent (Typ); - - if Nkind (Ctxt) = N_Package_Body - and then Nkind (Parent (Ctxt)) = N_Compilation_Unit - then - Check_SPARK_05_Restriction - ("type should be defined in package specification", Typ); - - elsif Nkind (Ctxt) /= N_Package_Specification - or else Nkind (Parent (Parent (Ctxt))) /= N_Compilation_Unit - then - Check_SPARK_05_Restriction - ("type should be defined in library unit package", Typ); - end if; - end; - end if; - Final_Storage_Only := not Is_Controlled (T); -- Ada 2005: Check whether an explicit Limited is present in a derived @@ -22193,19 +21942,13 @@ package body Sem_Ch3 is -- record extension, in which case the current scope may have inherited -- components. - if No (Def) - or else No (Component_List (Def)) - or else Null_Present (Component_List (Def)) + if Present (Def) + and then Present (Component_List (Def)) + and then not Null_Present (Component_List (Def)) then - if not Is_Tagged_Type (T) then - Check_SPARK_05_Restriction ("untagged record cannot be null", Def); - end if; - - else Analyze_Declarations (Component_Items (Component_List (Def))); if Present (Variant_Part (Component_List (Def))) then - Check_SPARK_05_Restriction ("variant part is not allowed", Def); Analyze (Variant_Part (Component_List (Def))); end if; end if; diff --git a/gcc/ada/sem_ch3.ads b/gcc/ada/sem_ch3.ads index 1d1d983b6e2..02fe39ba76c 100644 --- a/gcc/ada/sem_ch3.ads +++ b/gcc/ada/sem_ch3.ads @@ -195,8 +195,7 @@ package Sem_Ch3 is (N : Node_Id; Related_Nod : Node_Id; Related_Id : Entity_Id := Empty; - Suffix_Index : Nat := 1; - In_Iter_Schm : Boolean := False); + Suffix_Index : Nat := 1); -- Process an index that is given in an array declaration, an entry -- family declaration or a loop iteration. The index is given by an index -- declaration (a 'box'), or by a discrete range. The later can be the name @@ -204,8 +203,7 @@ package Sem_Ch3 is -- -- Related_Nod is the node where the potential generated implicit types -- will be inserted. The next last parameters are used for creating the - -- name. In_Iter_Schm is True if Make_Index is called on the discrete - -- subtype definition in an iteration scheme. + -- name. procedure Make_Class_Wide_Type (T : Entity_Id); -- A Class_Wide_Type is created for each tagged type definition. The @@ -265,8 +263,7 @@ package Sem_Ch3 is T : Entity_Id; Subtyp : Entity_Id := Empty; Check_List : List_Id := No_List; - R_Check_Off : Boolean := False; - In_Iter_Schm : Boolean := False); + R_Check_Off : Boolean := False); -- Process a range expression that appears in a declaration context. The -- range is analyzed and resolved with the base type of the given type, and -- an appropriate check for expressions in non-static contexts made on the @@ -277,8 +274,7 @@ package Sem_Ch3 is -- when the subprogram is called from Build_Record_Init_Proc and is used to -- return a set of constraint checking statements generated by the Checks -- package. R_Check_Off is set to True when the call to Range_Check is to - -- be skipped. In_Iter_Schm is True if Process_Range_Expr_In_Decl is called - -- on the discrete subtype definition in an iteration scheme. + -- be skipped. -- -- If Subtyp is given, then the range is for the named subtype Subtyp, and -- in this case the bounds are captured if necessary using this name. diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb index 0b04c42aacc..4a80ff085be 100644 --- a/gcc/ada/sem_ch4.adb +++ b/gcc/ada/sem_ch4.adb @@ -469,8 +469,6 @@ package body Sem_Ch4 is Onode : Node_Id; begin - Check_SPARK_05_Restriction ("allocator is not allowed", N); - -- Deal with allocator restrictions -- In accordance with H.4(7), the No_Allocators restriction only applies @@ -997,10 +995,6 @@ package body Sem_Ch4 is -- Flag indicates whether an interpretation of the prefix is a -- parameterless call that returns an access_to_subprogram. - procedure Check_Mixed_Parameter_And_Named_Associations; - -- Check that parameter and named associations are not mixed. This is - -- a restriction in SPARK mode. - procedure Check_Writable_Actuals (N : Node_Id); -- If the call has out or in-out parameters then mark its outermost -- enclosing construct as a node on which the writable actuals check @@ -1016,36 +1010,6 @@ package body Sem_Ch4 is procedure No_Interpretation; -- Output error message when no valid interpretation exists - -------------------------------------------------- - -- Check_Mixed_Parameter_And_Named_Associations -- - -------------------------------------------------- - - procedure Check_Mixed_Parameter_And_Named_Associations is - Actual : Node_Id; - Named_Seen : Boolean; - - begin - Named_Seen := False; - - Actual := First (Actuals); - while Present (Actual) loop - case Nkind (Actual) is - when N_Parameter_Association => - if Named_Seen then - Check_SPARK_05_Restriction - ("named association cannot follow positional one", - Actual); - exit; - end if; - - when others => - Named_Seen := True; - end case; - - Next (Actual); - end loop; - end Check_Mixed_Parameter_And_Named_Associations; - ---------------------------- -- Check_Writable_Actuals -- ---------------------------- @@ -1187,10 +1151,6 @@ package body Sem_Ch4 is -- Start of processing for Analyze_Call begin - if Restriction_Check_Required (SPARK_05) then - Check_Mixed_Parameter_And_Named_Associations; - end if; - -- Initialize the type of the result of the call to the error type, -- which will be reset if the type is successfully resolved. @@ -2092,13 +2052,6 @@ package body Sem_Ch4 is -- Start of processing for Analyze_Explicit_Dereference begin - -- If source node, check SPARK restriction. We guard this with the - -- source node check, because ??? - - if Comes_From_Source (N) then - Check_SPARK_05_Restriction ("explicit dereference is not allowed", N); - end if; - -- In formal verification mode, keep track of all reads and writes -- through explicit dereferences. @@ -2317,10 +2270,6 @@ package body Sem_Ch4 is Else_Expr := Next (Then_Expr); - if Comes_From_Source (N) then - Check_SPARK_05_Restriction ("if expression is not allowed", N); - end if; - if Comes_From_Source (N) then Check_Compiler_Unit ("if expression", N); end if; @@ -3182,8 +3131,6 @@ package body Sem_Ch4 is procedure Analyze_Null (N : Node_Id) is begin - Check_SPARK_05_Restriction ("null is not allowed", N); - Set_Etype (N, Any_Access); end Analyze_Null; @@ -4131,8 +4078,6 @@ package body Sem_Ch4 is -- Start of processing for Analyze_Quantified_Expression begin - Check_SPARK_05_Restriction ("quantified expression is not allowed", N); - -- Create a scope to emulate the loop-like behavior of the quantified -- expression. The scope is needed to provide proper visibility of the -- loop variable. @@ -5499,10 +5444,6 @@ package body Sem_Ch4 is -- Start of processing for Analyze_Slice begin - if Comes_From_Source (N) then - Check_SPARK_05_Restriction ("slice is not allowed", N); - end if; - Analyze (P); Analyze (D); diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb index 269e9ffd686..e6766c75685 100644 --- a/gcc/ada/sem_ch5.adb +++ b/gcc/ada/sem_ch5.adb @@ -39,8 +39,6 @@ with Namet; use Namet; with Nlists; use Nlists; with Nmake; use Nmake; with Opt; use Opt; -with Restrict; use Restrict; -with Rident; use Rident; with Sem; use Sem; with Sem_Aux; use Sem_Aux; with Sem_Case; use Sem_Case; @@ -1263,13 +1261,6 @@ package body Sem_Ch5 is -- Start of processing for Analyze_Block_Statement begin - -- In SPARK mode, we reject block statements. Note that the case of - -- block statements generated by the expander is fine. - - if Nkind (Original_Node (N)) = N_Block_Statement then - Check_SPARK_05_Restriction ("block statement is not allowed", N); - end if; - -- If no handled statement sequence is present, things are really messed -- up, and we just return immediately (defence against previous errors). @@ -1583,13 +1574,6 @@ package body Sem_Ch5 is Analyze_Choices (Alternatives (N), Exp_Type); Check_Choices (N, Alternatives (N), Exp_Type, Others_Present); - -- Case statement with single OTHERS alternative not allowed in SPARK - - if Others_Present and then List_Length (Alternatives (N)) = 1 then - Check_SPARK_05_Restriction - ("OTHERS as unique case alternative is not allowed", N); - end if; - if Exp_Type = Universal_Integer and then not Others_Present then Error_Msg_N ("case on universal integer requires OTHERS choice", Exp); end if; @@ -1672,11 +1656,6 @@ package body Sem_Ch5 is return; else - if Has_Loop_In_Inner_Open_Scopes (U_Name) then - Check_SPARK_05_Restriction - ("exit label must name the closest enclosing loop", N); - end if; - Set_Has_Exit (U_Name); end if; @@ -1712,42 +1691,6 @@ package body Sem_Ch5 is Check_Unset_Reference (Cond); end if; - -- In SPARK mode, verify that the exit statement respects the SPARK - -- restrictions. - - if Present (Cond) then - if Nkind (Parent (N)) /= N_Loop_Statement then - Check_SPARK_05_Restriction - ("exit with when clause must be directly in loop", N); - end if; - - else - if Nkind (Parent (N)) /= N_If_Statement then - if Nkind (Parent (N)) = N_Elsif_Part then - Check_SPARK_05_Restriction - ("exit must be in IF without ELSIF", N); - else - Check_SPARK_05_Restriction ("exit must be directly in IF", N); - end if; - - elsif Nkind (Parent (Parent (N))) /= N_Loop_Statement then - Check_SPARK_05_Restriction - ("exit must be in IF directly in loop", N); - - -- First test the presence of ELSE, so that an exit in an ELSE leads - -- to an error mentioning the ELSE. - - elsif Present (Else_Statements (Parent (N))) then - Check_SPARK_05_Restriction ("exit must be in IF without ELSE", N); - - -- An exit in an ELSIF does not reach here, as it would have been - -- detected in the case (Nkind (Parent (N)) /= N_If_Statement). - - elsif Present (Elsif_Parts (Parent (N))) then - Check_SPARK_05_Restriction ("exit must be in IF without ELSIF", N); - end if; - end if; - -- Chain exit statement to associated loop entity Set_Next_Exit_Statement (N, First_Exit_Statement (Scope_Id)); @@ -1772,8 +1715,6 @@ package body Sem_Ch5 is Label_Ent : Entity_Id; begin - Check_SPARK_05_Restriction ("goto statement is not allowed", N); - -- Actual semantic checks Check_Unreachable_Code (N); @@ -3015,13 +2956,6 @@ package body Sem_Ch5 is end if; end; - -- Loop parameter specification must include subtype mark in SPARK - - if Nkind (DS) = N_Range then - Check_SPARK_05_Restriction - ("loop parameter specification must include subtype mark", N); - end if; - -- Analyze the subtype definition and create temporaries for the bounds. -- Do not evaluate the range when preanalyzing a quantified expression -- because bounds expressed as function calls with side effects will be @@ -3160,7 +3094,7 @@ package body Sem_Ch5 is Check_Predicate_Use (Entity (Subtype_Mark (DS))); end if; - Make_Index (DS, N, In_Iter_Schm => True); + Make_Index (DS, N); Set_Ekind (Id, E_Loop_Parameter); -- A quantified expression which appears in a pre- or post-condition may @@ -4139,12 +4073,9 @@ package body Sem_Ch5 is end loop; -- If a label follows us, then we never have dead code, since - -- someone could branch to the label, so we just ignore it, unless - -- we are in formal mode where goto statements are not allowed. + -- someone could branch to the label, so we just ignore it. - if Nkind (Nxt) = N_Label - and then not Restriction_Check_Required (SPARK_05) - then + if Nkind (Nxt) = N_Label then return; -- Otherwise see if we have a real statement following us @@ -4203,15 +4134,8 @@ package body Sem_Ch5 is end loop; end if; - -- Now issue the warning (or error in formal mode) - - if Restriction_Check_Required (SPARK_05) then - Check_SPARK_05_Restriction - ("unreachable code is not allowed", Error_Node); - else - Error_Msg - ("??unreachable code!", Sloc (Error_Node), Error_Node); - end if; + Error_Msg + ("??unreachable code!", Sloc (Error_Node), Error_Node); end if; -- If the unconditional transfer of control instruction is the diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 03211c111f0..860db03f78e 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -225,8 +225,6 @@ package body Sem_Ch6 is Analyze_Subprogram_Specification (Specification (N)); begin - Check_SPARK_05_Restriction ("abstract subprogram is not allowed", N); - Generate_Definition (Subp_Id); -- Set the SPARK mode from the current context (may be overwritten later @@ -1122,20 +1120,7 @@ package body Sem_Ch6 is Check_Return_Construct_Accessibility (N); end if; - - -- RETURN only allowed in SPARK as the last statement in function - - if Nkind (Parent (N)) /= N_Handled_Sequence_Of_Statements - and then - (Nkind (Parent (Parent (N))) /= N_Subprogram_Body - or else Present (Next (N))) - then - Check_SPARK_05_Restriction - ("RETURN should be the last statement in function", N); - end if; - else - Check_SPARK_05_Restriction ("extended RETURN is not allowed", N); Obj_Decl := Last (Return_Object_Declarations (N)); -- Analyze parts specific to extended_return_statement: @@ -2223,8 +2208,6 @@ package body Sem_Ch6 is if Result_Definition (N) /= Error then if Nkind (Result_Definition (N)) = N_Access_Definition then - Check_SPARK_05_Restriction - ("access result is not allowed", Result_Definition (N)); -- Ada 2005 (AI-254): Handle anonymous access to subprograms @@ -2254,14 +2237,6 @@ package body Sem_Ch6 is Typ := Entity (Result_Definition (N)); Set_Etype (Designator, Typ); - -- Unconstrained array as result is not allowed in SPARK - - if Is_Array_Type (Typ) and then not Is_Constrained (Typ) then - Check_SPARK_05_Restriction - ("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); @@ -3073,42 +3048,6 @@ package body Sem_Ch6 is Check_Returns (HSS, 'P', Missing_Ret, Id); end if; end if; - - -- Special checks in SPARK mode - - if Nkind (Body_Spec) = N_Function_Specification then - - -- In SPARK mode, last statement of a function should be a return - - declare - Stat : constant Node_Id := Last_Source_Statement (HSS); - begin - if Present (Stat) - and then not Nkind_In (Stat, N_Simple_Return_Statement, - N_Extended_Return_Statement) - then - Check_SPARK_05_Restriction - ("last statement in function should be RETURN", Stat); - end if; - end; - - -- In SPARK mode, verify that a procedure has no return - - elsif Nkind (Body_Spec) = N_Procedure_Specification then - if Present (Spec_Id) then - Id := Spec_Id; - else - Id := Body_Id; - end if; - - -- Would be nice to point to return statement here, can we - -- borrow the Check_Returns procedure here ??? - - if Return_Present (Id) then - Check_SPARK_05_Restriction - ("procedure should not have RETURN", N); - end if; - end if; end Check_Missing_Return; ----------------------- @@ -4930,8 +4869,6 @@ package body Sem_Ch6 is if Nkind (Specification (N)) = N_Procedure_Specification and then Null_Present (Specification (N)) then - Check_SPARK_05_Restriction ("null procedure is not allowed", N); - -- Null procedures are allowed in protected types, following the -- recent AI12-0147. @@ -5195,15 +5132,6 @@ package body Sem_Ch6 is -- Start of processing for Analyze_Subprogram_Specification begin - -- User-defined operator is not allowed in SPARK, except as a renaming - - if Nkind (Defining_Unit_Name (N)) = N_Defining_Operator_Symbol - and then Nkind (Parent (N)) /= N_Subprogram_Renaming_Declaration - then - Check_SPARK_05_Restriction - ("user-defined operator is not allowed", N); - end if; - -- Proceed with analysis. Do not emit a cross-reference entry if the -- specification comes from an expression function, because it may be -- the completion of a previous declaration. If it is not, the cross- @@ -11563,14 +11491,6 @@ package body Sem_Ch6 is Check_Ghost_Overriding (S, Overridden_Subp); - -- Overloading is not allowed in SPARK, except for operators - - if Nkind (S) /= N_Defining_Operator_Symbol then - Error_Msg_Sloc := Sloc (Homonym (S)); - Check_SPARK_05_Restriction - ("overloading not allowed with entity#", S); - end if; - -- If S is a derived operation for an untagged type then by -- definition it's not a dispatching operation (even if the parent -- operation was dispatching), so Check_Dispatching_Operation is not @@ -11902,9 +11822,6 @@ package body Sem_Ch6 is Default := Expression (Param_Spec); if Present (Default) then - Check_SPARK_05_Restriction - ("default expression is not allowed", Default); - if Out_Present (Param_Spec) then Error_Msg_N ("default initialization only allowed for IN parameters", diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb index e5bb8880816..fa17c8b5cbf 100644 --- a/gcc/ada/sem_ch7.adb +++ b/gcc/ada/sem_ch7.adb @@ -47,7 +47,6 @@ with Nmake; use Nmake; with Nlists; use Nlists; with Opt; use Opt; with Output; use Output; -with Restrict; use Restrict; with Rtsfind; use Rtsfind; with Sem; use Sem; with Sem_Aux; use Sem_Aux; @@ -1271,10 +1270,6 @@ package body Sem_Ch7 is -- private_with_clauses, and remove them at the end of the nested -- package. - procedure Check_One_Tagged_Type_Or_Extension_At_Most; - -- Issue an error in SPARK mode if a package specification contains - -- more than one tagged type or type extension. - procedure Clear_Constants (Id : Entity_Id; FE : Entity_Id); -- Clears constant indications (Never_Set_In_Source, Constant_Value, and -- Is_True_Constant) on all variables that are entities of Id, and on @@ -1301,58 +1296,6 @@ package body Sem_Ch7 is -- private part rather than being done in Sem_Ch12.Install_Parent -- (which is where the parents' visible declarations are installed). - ------------------------------------------------ - -- Check_One_Tagged_Type_Or_Extension_At_Most -- - ------------------------------------------------ - - procedure Check_One_Tagged_Type_Or_Extension_At_Most is - Previous : Node_Id; - - procedure Check_Decls (Decls : List_Id); - -- Check that either Previous is Empty and Decls does not contain - -- more than one tagged type or type extension, or Previous is - -- already set and Decls contains no tagged type or type extension. - - ----------------- - -- Check_Decls -- - ----------------- - - procedure Check_Decls (Decls : List_Id) is - Decl : Node_Id; - - begin - Decl := First (Decls); - while Present (Decl) loop - if Nkind (Decl) = N_Full_Type_Declaration - and then Is_Tagged_Type (Defining_Identifier (Decl)) - then - if No (Previous) then - Previous := Decl; - - else - Error_Msg_Sloc := Sloc (Previous); - Check_SPARK_05_Restriction - ("at most one tagged type or type extension allowed", - "\\ previous declaration#", - Decl); - end if; - end if; - - Next (Decl); - end loop; - end Check_Decls; - - -- Start of processing for Check_One_Tagged_Type_Or_Extension_At_Most - - begin - Previous := Empty; - Check_Decls (Vis_Decls); - - if Present (Priv_Decls) then - Check_Decls (Priv_Decls); - end if; - end Check_One_Tagged_Type_Or_Extension_At_Most; - --------------------- -- Clear_Constants -- --------------------- @@ -1889,11 +1832,6 @@ package body Sem_Ch7 is Clear_Constants (Id, First_Private_Entity (Id)); end if; - -- Issue an error in SPARK mode if a package specification contains - -- more than one tagged type or type extension. - - Check_One_Tagged_Type_Or_Extension_At_Most; - -- Output relevant information as to why the package requires a body. -- Do not consider generated packages as this exposes internal symbols -- and leads to confusing messages. diff --git a/gcc/ada/sem_ch8.adb b/gcc/ada/sem_ch8.adb index c65ab5cd95f..709a8393985 100644 --- a/gcc/ada/sem_ch8.adb +++ b/gcc/ada/sem_ch8.adb @@ -568,8 +568,6 @@ package body Sem_Ch8 is Nam : constant Node_Id := Name (N); begin - Check_SPARK_05_Restriction ("exception renaming is not allowed", N); - Enter_Name (Id); Analyze (Nam); @@ -682,8 +680,6 @@ package body Sem_Ch8 is return; end if; - Check_SPARK_05_Restriction ("generic renaming is not allowed", N); - Generate_Definition (New_P); if Current_Scope /= Standard_Standard then @@ -872,8 +868,6 @@ package body Sem_Ch8 is return; end if; - Check_SPARK_05_Restriction ("object renaming is not allowed", N); - Set_Is_Pure (Id, Is_Pure (Current_Scope)); Enter_Name (Id); @@ -3898,8 +3892,6 @@ package body Sem_Ch8 is -- Start of processing for Analyze_Use_Package begin - Check_SPARK_05_Restriction ("use clause is not allowed", N); - Set_Hidden_By_Use_Clause (N, No_Elist); -- Use clause not allowed in a spec of a predefined package declaration @@ -7240,21 +7232,6 @@ package body Sem_Ch8 is return; end if; - -- Selector name cannot be a character literal or an operator symbol in - -- SPARK, except for the operator symbol in a renaming. - - if Restriction_Check_Required (SPARK_05) then - if Nkind (Selector_Name (N)) = N_Character_Literal then - Check_SPARK_05_Restriction - ("character literal cannot be prefixed", N); - elsif Nkind (Selector_Name (N)) = N_Operator_Symbol - and then Nkind (Parent (N)) /= N_Subprogram_Renaming_Declaration - then - Check_SPARK_05_Restriction - ("operator symbol cannot be prefixed", N); - end if; - end if; - -- If the selector already has an entity, the node has been constructed -- in the course of expansion, and is known to be valid. Do not verify -- that it is defined for the type (it may be a private component used @@ -7709,21 +7686,6 @@ package body Sem_Ch8 is Error_Msg_N ("invalid prefix in selected component", P); end if; end if; - - -- Selector name is restricted in SPARK - - if Nkind (N) = N_Expanded_Name - and then Restriction_Check_Required (SPARK_05) - then - if Is_Subprogram (P_Name) then - Check_SPARK_05_Restriction - ("prefix of expanded name cannot be a subprogram", P); - elsif Ekind (P_Name) = E_Loop then - Check_SPARK_05_Restriction - ("prefix of expanded name cannot be a loop statement", P); - end if; - end if; - else -- If prefix is not the name of an entity, it must be an expression, -- whose type is appropriate for a record. This is determined by @@ -7881,10 +7843,6 @@ package body Sem_Ch8 is -- Base attribute, not allowed in Ada 83 elsif Attribute_Name (N) = Name_Base then - Error_Msg_Name_1 := Name_Base; - Check_SPARK_05_Restriction - ("attribute% is only allowed as prefix of another attribute", N); - if Ada_Version = Ada_83 and then Comes_From_Source (N) then Error_Msg_N ("(Ada 83) Base attribute not allowed in subtype mark", N); diff --git a/gcc/ada/sem_ch9.adb b/gcc/ada/sem_ch9.adb index 05a6d9aa1b5..5a7e3841804 100644 --- a/gcc/ada/sem_ch9.adb +++ b/gcc/ada/sem_ch9.adb @@ -706,7 +706,6 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Check_SPARK_05_Restriction ("abort statement is not allowed", N); T_Name := First (Names (N)); while Present (T_Name) loop @@ -777,7 +776,6 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Check_SPARK_05_Restriction ("accept statement is not allowed", N); -- Entry name is initialized to Any_Id. It should get reset to the -- matching entry entity. An error is signalled if it is not reset. @@ -1019,7 +1017,6 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Check_SPARK_05_Restriction ("select statement is not allowed", N); Check_Restriction (Max_Asynchronous_Select_Nesting, N); Check_Restriction (No_Select_Statements, N); @@ -1065,7 +1062,6 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Check_SPARK_05_Restriction ("select statement is not allowed", N); Check_Restriction (No_Select_Statements, N); -- Ada 2005 (AI-345): The trigger may be a dispatching call @@ -1163,7 +1159,6 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Check_SPARK_05_Restriction ("delay statement is not allowed", N); Check_Restriction (No_Relative_Delay, N); Check_Restriction (No_Delay, N); Check_Potentially_Blocking_Operation (N); @@ -1189,7 +1184,6 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Check_SPARK_05_Restriction ("delay statement is not allowed", N); Check_Restriction (No_Delay, N); Check_Potentially_Blocking_Operation (N); Analyze_And_Resolve (E); @@ -1505,7 +1499,6 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Check_SPARK_05_Restriction ("entry call is not allowed", N); if Present (Pragmas_Before (N)) then Analyze_List (Pragmas_Before (N)); @@ -1956,7 +1949,6 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Check_SPARK_05_Restriction ("protected definition is not allowed", N); Analyze_Declarations (Visible_Declarations (N)); if Present (Private_Declarations (N)) @@ -2312,7 +2304,6 @@ package body Sem_Ch9 is Warnings => True); Tasking_Used := True; - Check_SPARK_05_Restriction ("requeue statement is not allowed", N); Check_Restriction (No_Requeue_Statements, N); Check_Unreachable_Code (N); @@ -2606,7 +2597,6 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Check_SPARK_05_Restriction ("select statement is not allowed", N); Check_Restriction (No_Select_Statements, N); -- Loop to analyze alternatives @@ -3068,7 +3058,6 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Check_SPARK_05_Restriction ("task definition is not allowed", N); if Present (Visible_Declarations (N)) then Analyze_Declarations (Visible_Declarations (N)); @@ -3310,7 +3299,6 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Check_SPARK_05_Restriction ("select statement is not allowed", N); Check_Restriction (No_Select_Statements, N); -- Ada 2005 (AI-345): The trigger may be a dispatching call diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index 303f4dbad4a..83cd20d7d9a 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -4276,71 +4276,6 @@ package body Sem_Res is ("invalid use of untagged formal incomplete type", A); end if; - if Comes_From_Source (Original_Node (N)) - and then Nkind_In (Original_Node (N), N_Function_Call, - N_Procedure_Call_Statement) - then - -- In formal mode, check that actual parameters matching - -- formals of tagged types are objects (or ancestor type - -- conversions of objects), not general expressions. - - if Is_Actual_Tagged_Parameter (A) then - if Is_SPARK_05_Object_Reference (A) then - null; - - elsif Nkind (A) = N_Type_Conversion then - declare - Operand : constant Node_Id := Expression (A); - Operand_Typ : constant Entity_Id := Etype (Operand); - Target_Typ : constant Entity_Id := A_Typ; - - begin - if not Is_SPARK_05_Object_Reference (Operand) then - Check_SPARK_05_Restriction - ("object required", Operand); - - -- In formal mode, the only view conversions are those - -- involving ancestor conversion of an extended type. - - elsif not - (Is_Tagged_Type (Target_Typ) - and then not Is_Class_Wide_Type (Target_Typ) - and then Is_Tagged_Type (Operand_Typ) - and then not Is_Class_Wide_Type (Operand_Typ) - and then Is_Ancestor (Target_Typ, Operand_Typ)) - then - if Ekind_In - (F, E_Out_Parameter, E_In_Out_Parameter) - then - Check_SPARK_05_Restriction - ("ancestor conversion is the only permitted " - & "view conversion", A); - else - Check_SPARK_05_Restriction - ("ancestor conversion required", A); - end if; - - else - null; - end if; - end; - - else - Check_SPARK_05_Restriction ("object required", A); - end if; - - -- In formal mode, the only view conversions are those - -- involving ancestor conversion of an extended type. - - elsif Nkind (A) = N_Type_Conversion - and then Ekind_In (F, E_Out_Parameter, E_In_Out_Parameter) - then - Check_SPARK_05_Restriction - ("ancestor conversion is the only permitted view " - & "conversion", A); - end if; - end if; - -- has warnings suppressed, then we reset Never_Set_In_Source for -- the calling entity. The reason for this is to catch cases like -- GNAT.Spitbol.Patterns.Vstring_Var where the called subprogram @@ -5916,20 +5851,6 @@ package body Sem_Res is Analyze_Dimension (N); Eval_Arithmetic_Op (N); - -- In SPARK, a multiplication or division with operands of fixed point - -- types must be qualified or explicitly converted to identify the - -- result type. - - if (Is_Fixed_Point_Type (Etype (L)) - or else Is_Fixed_Point_Type (Etype (R))) - and then Nkind_In (N, N_Op_Multiply, N_Op_Divide) - and then - not Nkind_In (Parent (N), N_Qualified_Expression, N_Type_Conversion) - then - Check_SPARK_05_Restriction - ("operation should be qualified or explicitly converted", N); - end if; - -- Set overflow and division checking bit if Nkind (N) in N_Op then @@ -6308,30 +6229,6 @@ package body Sem_Res is end if; end if; - -- If the SPARK_05 restriction is active, we are not allowed - -- to have a call to a subprogram before we see its completion. - - if not Has_Completion (Nam) - and then Restriction_Check_Required (SPARK_05) - - -- Don't flag strange internal calls - - and then Comes_From_Source (N) - and then Comes_From_Source (Nam) - - -- Only flag calls in extended main source - - and then In_Extended_Main_Source_Unit (Nam) - and then In_Extended_Main_Source_Unit (N) - - -- Exclude enumeration literals from this processing - - and then Ekind (Nam) /= E_Enumeration_Literal - then - Check_SPARK_05_Restriction - ("call to subprogram cannot appear before its body", N); - end if; - -- Check that this is not a call to a protected procedure or entry from -- within a protected function. @@ -6566,16 +6463,6 @@ package body Sem_Res is if Comes_From_Source (N) then Scop := Current_Scope; - -- Check violation of SPARK_05 restriction which does not permit - -- a subprogram body to contain a call to the subprogram directly. - - if Restriction_Check_Required (SPARK_05) - and then Same_Or_Aliased_Subprograms (Nam, Scop) - then - Check_SPARK_05_Restriction - ("subprogram may not contain direct call to itself", N); - end if; - -- Issue warning for possible infinite recursion in the absence -- of the No_Recursion restriction. @@ -6933,17 +6820,6 @@ package body Sem_Res is Check_For_Eliminated_Subprogram (Subp, Nam); - -- In formal mode, the primitive operations of a tagged type or type - -- extension do not include functions that return the tagged type. - - if Nkind (N) = N_Function_Call - and then Is_Tagged_Type (Etype (N)) - and then Is_Entity_Name (Name (N)) - and then Is_Inherited_Operation_For_Type (Entity (Name (N)), Etype (N)) - then - Check_SPARK_05_Restriction ("function not inherited", N); - end if; - -- Implement rule in 12.5.1 (23.3/2): In an instance, if the actual is -- class-wide and the call dispatches on result in a context that does -- not provide a tag, the call raises Program_Error. @@ -7376,20 +7252,6 @@ package body Sem_Res is Generate_Operator_Reference (N, T); Check_Low_Bound_Tested (N); - -- In SPARK, ordering operators <, <=, >, >= are not defined for Boolean - -- types or array types except String. - - if Is_Boolean_Type (T) then - Check_SPARK_05_Restriction - ("comparison is not defined on Boolean type", N); - - elsif Is_Array_Type (T) - and then Base_Type (T) /= Standard_String - then - Check_SPARK_05_Restriction - ("comparison is not defined on array types other than String", N); - end if; - -- Check comparison on unordered enumeration if Bad_Unordered_Enumeration_Reference (N, Etype (L)) then @@ -8462,27 +8324,6 @@ package body Sem_Res is Resolve (L, T); Resolve (R, T); - -- In SPARK, equality operators = and /= for array types other than - -- String are only defined when, for each index position, the - -- operands have equal static bounds. - - if Is_Array_Type (T) then - - -- Protect call to Matching_Static_Array_Bounds to avoid costly - -- operation if not needed. - - if Restriction_Check_Required (SPARK_05) - and then Base_Type (T) /= Standard_String - and then Base_Type (Etype (L)) = Base_Type (Etype (R)) - and then Etype (L) /= Any_Composite -- or else L in error - and then Etype (R) /= Any_Composite -- or else R in error - and then not Matching_Static_Array_Bounds (Etype (L), Etype (R)) - then - Check_SPARK_05_Restriction - ("array types should have matching static bounds", N); - end if; - end if; - -- If the unique type is a class-wide type then it will be expanded -- into a dispatching call to the predefined primitive. Therefore we -- check here for potential violation of such restriction. @@ -9322,34 +9163,6 @@ package body Sem_Res is Set_Etype (N, B_Typ); Generate_Operator_Reference (N, B_Typ); Eval_Logical_Op (N); - - -- In SPARK, logical operations AND, OR and XOR for arrays are defined - -- only when both operands have same static lower and higher bounds. Of - -- course the types have to match, so only check if operands are - -- compatible and the node itself has no errors. - - if Is_Array_Type (B_Typ) - and then Nkind (N) in N_Binary_Op - then - declare - Left_Typ : constant Node_Id := Etype (Left_Opnd (N)); - Right_Typ : constant Node_Id := Etype (Right_Opnd (N)); - - begin - -- Protect call to Matching_Static_Array_Bounds to avoid costly - -- operation if not needed. - - if Restriction_Check_Required (SPARK_05) - and then Base_Type (Left_Typ) = Base_Type (Right_Typ) - and then Left_Typ /= Any_Composite -- or Left_Opnd in error - and then Right_Typ /= Any_Composite -- or Right_Opnd in error - and then not Matching_Static_Array_Bounds (Left_Typ, Right_Typ) - then - Check_SPARK_05_Restriction - ("array types should have matching static bounds", N); - end if; - end; - end if; end Resolve_Logical_Op; --------------------------- @@ -9707,11 +9520,6 @@ package body Sem_Res is exit when NN = N; NN := Parent (NN); end loop; - - if Base_Type (Etype (N)) /= Standard_String then - Check_SPARK_05_Restriction - ("result of concatenation should have type String", N); - end if; end Resolve_Op_Concat; --------------------------- @@ -9836,34 +9644,6 @@ package body Sem_Res is Resolve (Arg, Btyp); end if; - -- Concatenation is restricted in SPARK: each operand must be either a - -- string literal, the name of a string constant, a static character or - -- string expression, or another concatenation. Arg cannot be a - -- concatenation here as callers of Resolve_Op_Concat_Arg call it - -- separately on each final operand, past concatenation operations. - - if Is_Character_Type (Etype (Arg)) then - if not Is_OK_Static_Expression (Arg) then - Check_SPARK_05_Restriction - ("character operand for concatenation should be static", Arg); - end if; - - elsif Is_String_Type (Etype (Arg)) then - if not (Nkind_In (Arg, N_Identifier, N_Expanded_Name) - and then Is_Constant_Object (Entity (Arg))) - and then not Is_OK_Static_Expression (Arg) - then - Check_SPARK_05_Restriction - ("string operand for concatenation should be static", Arg); - end if; - - -- Do not issue error on an operand that is neither a character nor a - -- string, as the error is issued in Resolve_Op_Concat. - - else - null; - end if; - Check_Unset_Reference (Arg); end Resolve_Op_Concat_Arg; @@ -10189,19 +9969,6 @@ package body Sem_Res is begin Resolve (Expr, Target_Typ); - -- Protect call to Matching_Static_Array_Bounds to avoid costly - -- operation if not needed. - - if Restriction_Check_Required (SPARK_05) - and then Is_Array_Type (Target_Typ) - and then Is_Array_Type (Etype (Expr)) - and then Etype (Expr) /= Any_Composite -- or else Expr in error - and then not Matching_Static_Array_Bounds (Target_Typ, Etype (Expr)) - then - Check_SPARK_05_Restriction - ("array types should have matching static bounds", N); - end if; - -- A qualified expression requires an exact match of the type, class- -- wide matching is not allowed. However, if the qualifying type is -- specific and the expression has a class-wide type, it may still be @@ -11524,35 +11291,6 @@ package body Sem_Res is Resolve (Operand); - -- In SPARK, a type conversion between array types should be restricted - -- to types which have matching static bounds. - - -- Protect call to Matching_Static_Array_Bounds to avoid costly - -- operation if not needed. - - if Restriction_Check_Required (SPARK_05) - and then Is_Array_Type (Target_Typ) - and then Is_Array_Type (Operand_Typ) - and then Operand_Typ /= Any_Composite -- or else Operand in error - and then not Matching_Static_Array_Bounds (Target_Typ, Operand_Typ) - then - Check_SPARK_05_Restriction - ("array types should have matching static bounds", N); - end if; - - -- In formal mode, the operand of an ancestor type conversion must be an - -- object (not an expression). - - if Is_Tagged_Type (Target_Typ) - and then not Is_Class_Wide_Type (Target_Typ) - and then Is_Tagged_Type (Operand_Typ) - and then not Is_Class_Wide_Type (Operand_Typ) - and then Is_Ancestor (Target_Typ, Operand_Typ) - and then not Is_SPARK_05_Object_Reference (Operand) - then - Check_SPARK_05_Restriction ("object required", Operand); - end if; - Analyze_Dimension (N); -- Note: we do the Eval_Type_Conversion call before applying the @@ -11871,12 +11609,6 @@ package body Sem_Res is Hi : Uint; begin - if Is_Modular_Integer_Type (Typ) and then Nkind (N) /= N_Op_Not then - Error_Msg_Name_1 := Chars (Typ); - Check_SPARK_05_Restriction - ("unary operator not defined for modular type%", N); - end if; - -- Deal with intrinsic unary operators if Comes_From_Source (N) diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index b32d4fd6d14..4f7d2d0594b 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -3342,10 +3342,6 @@ package body Sem_Util is Error_Msg_N ("(Ada 83) decl cannot appear after body#", Decl); end if; - else - Error_Msg_Sloc := Body_Sloc; - Check_SPARK_05_Restriction - ("decl cannot appear after body#", Decl); end if; end if; @@ -7537,52 +7533,6 @@ package body Sem_Util is Append_Entity (Def_Id, S); Set_Public_Status (Def_Id); - -- Declaring a homonym is not allowed in SPARK ... - - if Present (C) and then Restriction_Check_Required (SPARK_05) then - declare - Enclosing_Subp : constant Node_Id := Enclosing_Subprogram (Def_Id); - Enclosing_Pack : constant Node_Id := Enclosing_Package (Def_Id); - Other_Scope : constant Node_Id := Enclosing_Dynamic_Scope (C); - - begin - -- ... unless the new declaration is in a subprogram, and the - -- visible declaration is a variable declaration or a parameter - -- specification outside that subprogram. - - if Present (Enclosing_Subp) - and then Nkind_In (Parent (C), N_Object_Declaration, - N_Parameter_Specification) - and then not Scope_Within_Or_Same (Other_Scope, Enclosing_Subp) - then - null; - - -- ... or the new declaration is in a package, and the visible - -- declaration occurs outside that package. - - elsif Present (Enclosing_Pack) - and then not Scope_Within_Or_Same (Other_Scope, Enclosing_Pack) - then - null; - - -- ... or the new declaration is a component declaration in a - -- record type definition. - - elsif Nkind (Parent (Def_Id)) = N_Component_Declaration then - null; - - -- Don't issue error for non-source entities - - elsif Comes_From_Source (Def_Id) - and then Comes_From_Source (C) - then - Error_Msg_Sloc := Sloc (C); - Check_SPARK_05_Restriction - ("redeclaration of identifier &#", Def_Id); - end if; - end; - end if; - -- Warn if new entity hides an old one if Warn_On_Hiding and then Present (C) @@ -17800,158 +17750,6 @@ package body Sem_Util is and then Is_Single_Concurrent_Type (Etype (Id)); end Is_Single_Task_Object; - ------------------------------------- - -- Is_SPARK_05_Initialization_Expr -- - ------------------------------------- - - function Is_SPARK_05_Initialization_Expr (N : Node_Id) return Boolean is - Is_Ok : Boolean; - Expr : Node_Id; - Comp_Assn : Node_Id; - Orig_N : constant Node_Id := Original_Node (N); - - begin - Is_Ok := True; - - if not Comes_From_Source (Orig_N) then - goto Done; - end if; - - pragma Assert (Nkind (Orig_N) in N_Subexpr); - - case Nkind (Orig_N) is - when N_Character_Literal - | N_Integer_Literal - | N_Real_Literal - | N_String_Literal - => - null; - - when N_Expanded_Name - | N_Identifier - => - if Is_Entity_Name (Orig_N) - and then Present (Entity (Orig_N)) -- needed in some cases - then - case Ekind (Entity (Orig_N)) is - when E_Constant - | E_Enumeration_Literal - | E_Named_Integer - | E_Named_Real - => - null; - - when others => - if Is_Type (Entity (Orig_N)) then - null; - else - Is_Ok := False; - end if; - end case; - end if; - - when N_Qualified_Expression - | N_Type_Conversion - => - Is_Ok := Is_SPARK_05_Initialization_Expr (Expression (Orig_N)); - - when N_Unary_Op => - Is_Ok := Is_SPARK_05_Initialization_Expr (Right_Opnd (Orig_N)); - - when N_Binary_Op - | N_Membership_Test - | N_Short_Circuit - => - Is_Ok := Is_SPARK_05_Initialization_Expr (Left_Opnd (Orig_N)) - and then - Is_SPARK_05_Initialization_Expr (Right_Opnd (Orig_N)); - - when N_Aggregate - | N_Extension_Aggregate - => - if Nkind (Orig_N) = N_Extension_Aggregate then - Is_Ok := - Is_SPARK_05_Initialization_Expr (Ancestor_Part (Orig_N)); - end if; - - Expr := First (Expressions (Orig_N)); - while Present (Expr) loop - if not Is_SPARK_05_Initialization_Expr (Expr) then - Is_Ok := False; - goto Done; - end if; - - Next (Expr); - end loop; - - Comp_Assn := First (Component_Associations (Orig_N)); - while Present (Comp_Assn) loop - Expr := Expression (Comp_Assn); - - -- Note: test for Present here needed for box assocation - - if Present (Expr) - and then not Is_SPARK_05_Initialization_Expr (Expr) - then - Is_Ok := False; - goto Done; - end if; - - Next (Comp_Assn); - end loop; - - when N_Attribute_Reference => - if Nkind (Prefix (Orig_N)) in N_Subexpr then - Is_Ok := Is_SPARK_05_Initialization_Expr (Prefix (Orig_N)); - end if; - - Expr := First (Expressions (Orig_N)); - while Present (Expr) loop - if not Is_SPARK_05_Initialization_Expr (Expr) then - Is_Ok := False; - goto Done; - end if; - - Next (Expr); - end loop; - - -- Selected components might be expanded named not yet resolved, so - -- default on the safe side. (Eg on sparklex.ads) - - when N_Selected_Component => - null; - - when others => - Is_Ok := False; - end case; - - <> - return Is_Ok; - end Is_SPARK_05_Initialization_Expr; - - ---------------------------------- - -- Is_SPARK_05_Object_Reference -- - ---------------------------------- - - function Is_SPARK_05_Object_Reference (N : Node_Id) return Boolean is - begin - if Is_Entity_Name (N) then - return Present (Entity (N)) - and then - (Ekind_In (Entity (N), E_Constant, E_Variable) - or else Ekind (Entity (N)) in Formal_Kind); - - else - case Nkind (N) is - when N_Selected_Component => - return Is_SPARK_05_Object_Reference (Prefix (N)); - - when others => - return False; - end case; - end if; - end Is_SPARK_05_Object_Reference; - -------------------------------------- -- Is_Special_Aliased_Formal_Access -- -------------------------------------- @@ -24050,19 +23848,6 @@ package body Sem_Util is Get_Decoded_Name_String (Chars (Endl)); Set_Sloc (Endl, Sloc (Endl) + Source_Ptr (Name_Len)); - - else - -- In SPARK mode, no missing label is allowed for packages and - -- subprogram bodies. Detect those cases by testing whether - -- Process_End_Label was called for a body (Typ = 't') or a package. - - if Restriction_Check_Required (SPARK_05) - and then (Typ = 't' or else Ekind (Ent) = E_Package) - then - Error_Msg_Node_1 := Endl; - Check_SPARK_05_Restriction - ("`END &` required", Endl, Force => True); - end if; end if; -- Now generate the e/t reference diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 0ac89f7532e..ba4c2898476 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -1977,17 +1977,6 @@ package Sem_Util is -- Determine whether arbitrary entity Id denotes the anonymous object -- created for a single task type. - function Is_SPARK_05_Initialization_Expr (N : Node_Id) return Boolean; - -- Determines if the tree referenced by N represents an initialization - -- expression in SPARK 2005, suitable for initializing an object in an - -- object declaration. - - function Is_SPARK_05_Object_Reference (N : Node_Id) return Boolean; - -- Determines if the tree referenced by N represents an object in SPARK - -- 2005. This differs from Is_Object_Reference in that only variables, - -- constants, formal parameters, and selected_components of those are - -- valid objects in SPARK 2005. - function Is_Special_Aliased_Formal_Access (Exp : Node_Id; Scop : Entity_Id) return Boolean; diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl index e5494ae73ab..094f7221c83 100644 --- a/gcc/ada/snames.ads-tmpl +++ b/gcc/ada/snames.ads-tmpl @@ -835,7 +835,6 @@ package Snames is Name_Section : constant Name_Id := N + $; Name_Semaphore : constant Name_Id := N + $; Name_Simple_Barriers : constant Name_Id := N + $; - Name_SPARK : constant Name_Id := N + $; Name_SPARK_05 : constant Name_Id := N + $; Name_Spec_File_Name : constant Name_Id := N + $; Name_State : constant Name_Id := N + $;