--------
.. 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
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 <source-location>
- <error message>
-
-.. 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.
-- 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.
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);
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.
@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
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 <source-location>
- <error message>
-@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
No_Use_Of_Pragma => False,
-- Requires a parameter value, not a count
+ SPARK_05 => False,
+ -- Obsolete restriction
+
others => True);
Additional_Restrictions_Listed : Boolean := False;
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;
-- 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
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));
(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;
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);
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;
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
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;
-- 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;
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
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
-- 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.
--
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;
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 --
--------------------------------
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
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 --
--------------------------------------
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 --
-------------------------------
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;
-- 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.
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);
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 --
------------------------------
-- 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
-- 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
-- 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;
-- 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.
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;
-- 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
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 --
-----------------------
end if;
end if;
- if Checksum_Accumulate_Token_Checksum then
- Accumulate_Token_Checksum;
- end if;
-
- return;
+ Accumulate_Token_Checksum;
end Nlit;
----------
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;
-- 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
-- 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;
-- 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 --
------------------------------------------------------
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 --
----------------------------------------
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 --
--------------------------------
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).
-- 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
-- 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.
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;
("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);
-- 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
-- Start of processing for Analyze_Access_Attribute
begin
- Check_SPARK_05_Restriction_On_Attribute;
Check_E0;
if Nkind (P) = N_Character_Literal then
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.
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 --
---------------------------
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
("?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));
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);
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);
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);
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.
-----------
when Attribute_Value =>
- Check_SPARK_05_Restriction_On_Attribute;
Check_E1;
Check_Scalar_Type;
----------------
when Attribute_Wide_Value =>
- Check_SPARK_05_Restriction_On_Attribute;
Check_E1;
Check_Scalar_Type;
----------------
when Attribute_Wide_Width =>
- Check_SPARK_05_Restriction_On_Attribute;
Check_E0;
Check_Scalar_Type;
Set_Etype (N, Universal_Integer);
-----------
when Attribute_Width =>
- Check_SPARK_05_Restriction_On_Attribute;
Check_E0;
Check_Scalar_Type;
Set_Etype (N, Universal_Integer);
-- 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
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
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
-- 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;
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
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
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.
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),
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
-- 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:
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
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
-- 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);
-- 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);
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
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));
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
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
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
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
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.
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);
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:
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)));
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
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);
-- 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
-- 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
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
-- 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);
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;
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;
------------------------
(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;
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
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
-- 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
-- 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
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;
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);
-- 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
or else Abstract_Present (Def));
else
- Check_SPARK_05_Restriction ("interface is not allowed", N);
-
Is_Tagged := True;
Analyze_Interface_Declaration (T, Def);
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
-- 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;
(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
--
-- 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
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
-- 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.
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
-- 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
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 --
----------------------------
-- 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.
-- 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.
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;
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;
-- 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.
-- 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);
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;
-- 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).
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;
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;
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));
Label_Ent : Entity_Id;
begin
- Check_SPARK_05_Restriction ("goto statement is not allowed", N);
-
-- Actual semantic checks
Check_Unreachable_Code (N);
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
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
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
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
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
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:
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
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);
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;
-----------------------
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.
-- 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-
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
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",
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;
-- 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
-- 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 --
---------------------
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.
Nam : constant Node_Id := Name (N);
begin
- Check_SPARK_05_Restriction ("exception renaming is not allowed", N);
-
Enter_Name (Id);
Analyze (Nam);
return;
end if;
- Check_SPARK_05_Restriction ("generic renaming is not allowed", N);
-
Generate_Definition (New_P);
if Current_Scope /= Standard_Standard then
return;
end if;
- Check_SPARK_05_Restriction ("object renaming is not allowed", N);
-
Set_Is_Pure (Id, Is_Pure (Current_Scope));
Enter_Name (Id);
-- 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
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
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
-- 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);
begin
Tasking_Used := True;
- Check_SPARK_05_Restriction ("abort statement is not allowed", N);
T_Name := First (Names (N));
while Present (T_Name) loop
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.
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);
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
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);
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);
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));
begin
Tasking_Used := True;
- Check_SPARK_05_Restriction ("protected definition is not allowed", N);
Analyze_Declarations (Visible_Declarations (N));
if Present (Private_Declarations (N))
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);
begin
Tasking_Used := True;
- Check_SPARK_05_Restriction ("select statement is not allowed", N);
Check_Restriction (No_Select_Statements, N);
-- Loop to analyze alternatives
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));
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
("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
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
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.
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.
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.
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
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.
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;
---------------------------
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;
---------------------------
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;
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
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
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)
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;
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)
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;
-
- <<Done>>
- 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 --
--------------------------------------
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
-- 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;
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 + $;
projects / platform / upstream / gcc.git / commitdiff