mirror of git://gcc.gnu.org/git/gcc.git
[multiple changes]
2014-06-13 Robert Dewar <dewar@adacore.com> * sem_cat.adb: Minor reformatting. 2014-06-13 Yannick Moy <moy@adacore.com> * sem_prag.adb (Analyze_Pragma/Post_Class): Fix typo. 2014-06-13 Arnaud Charlet <charlet@adacore.com> * gnat_rm.texi: Add detail on SPARK_05 restriction. 2014-06-13 Bob Duff <duff@adacore.com> * s-solita.adb (Get_Sec_Stack_Addr, Init_Tasking_Soft_Links): Add assertions requiring the secondary stack to be initialized. * s-solita.ads (Init_Tasking_Soft_Links): Comment. * s-taprob.adb, s-tarest.adb, s-tasini.adb (elab code): Make sure the secondary stack is initialized before calling Init_Tasking_Soft_Links, by adding pragmas Elaborate_Body. 2014-06-13 Thomas Quinot <quinot@adacore.com> * sem_ch13.adb (Analyze_Stream_TSS_Definition): Remove temporary kludge disabling new legality check. From-SVN: r211614
This commit is contained in:
Arnaud Charlet
parent
aa6113321a
commit
e3a325f2f0
|
|
@ -1,3 +1,29 @@
|
|||
2014-06-13 Robert Dewar <dewar@adacore.com>
|
||||
|
||||
* sem_cat.adb: Minor reformatting.
|
||||
|
||||
2014-06-13 Yannick Moy <moy@adacore.com>
|
||||
|
||||
* sem_prag.adb (Analyze_Pragma/Post_Class): Fix typo.
|
||||
|
||||
2014-06-13 Arnaud Charlet <charlet@adacore.com>
|
||||
|
||||
* gnat_rm.texi: Add detail on SPARK_05 restriction.
|
||||
|
||||
2014-06-13 Bob Duff <duff@adacore.com>
|
||||
|
||||
* s-solita.adb (Get_Sec_Stack_Addr, Init_Tasking_Soft_Links):
|
||||
Add assertions requiring the secondary stack to be initialized.
|
||||
* s-solita.ads (Init_Tasking_Soft_Links): Comment.
|
||||
* s-taprob.adb, s-tarest.adb, s-tasini.adb (elab code): Make sure the
|
||||
secondary stack is initialized before calling Init_Tasking_Soft_Links,
|
||||
by adding pragmas Elaborate_Body.
|
||||
|
||||
2014-06-13 Thomas Quinot <quinot@adacore.com>
|
||||
|
||||
* sem_ch13.adb (Analyze_Stream_TSS_Definition): Remove temporary
|
||||
kludge disabling new legality check.
|
||||
|
||||
2014-06-13 Hristian Kirtchev <kirtchev@adacore.com>
|
||||
|
||||
* freeze.adb (Freeze_Record_Type): Remove checks related to SPARK
|
||||
|
|
|
|||
|
|
@ -10463,8 +10463,8 @@ violation of restriction "SPARK" at <file>
|
|||
@end smallexample
|
||||
|
||||
This is not a replacement for the semantic checks performed by the
|
||||
SPARK Examiner tool, as the compiler only deals currently with code,
|
||||
not at all with SPARK 2005 annotations and does not guarantee catching all
|
||||
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
|
||||
|
|
@ -10476,7 +10476,120 @@ 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 restrictions.
|
||||
|
||||
Note that if a unit is compiled in Ada 95 mode with SPARK restriction,
|
||||
The list below summarises the checks that are performed when this
|
||||
restriction is in force:
|
||||
@itemize @bullet
|
||||
@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 Non-static 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 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 Non-tagged record cannot be null
|
||||
@item No class-wide operations
|
||||
@item Initialization expressions must respect SPARK restrictions
|
||||
@item Non-static 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
|
||||
@end itemize
|
||||
|
||||
The following restrictions are enforced, but note that they are actually more
|
||||
strict that the latest SPARK 2005 language definition:
|
||||
|
||||
@itemize @bullet
|
||||
@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 @bullet
|
||||
@item SPARK 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
|
||||
@end itemize
|
||||
|
||||
Note that if a unit is compiled in Ada 95 mode with the SPARK restriction,
|
||||
violations will be reported for constructs forbidden in SPARK 95,
|
||||
instead of SPARK 2005.
|
||||
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@
|
|||
-- --
|
||||
-- B o d y --
|
||||
-- --
|
||||
-- Copyright (C) 2004-2013, Free Software Foundation, Inc. --
|
||||
-- Copyright (C) 2004-2014, Free Software Foundation, Inc. --
|
||||
-- --
|
||||
-- GNAT is free software; you can redistribute it and/or modify it under --
|
||||
-- terms of the GNU General Public License as published by the Free Soft- --
|
||||
|
|
@ -95,7 +95,11 @@ package body System.Soft_Links.Tasking is
|
|||
|
||||
function Get_Sec_Stack_Addr return Address is
|
||||
begin
|
||||
return STPO.Self.Common.Compiler_Data.Sec_Stack_Addr;
|
||||
return Result : constant Address :=
|
||||
STPO.Self.Common.Compiler_Data.Sec_Stack_Addr
|
||||
do
|
||||
pragma Assert (Result /= Null_Address);
|
||||
end return;
|
||||
end Get_Sec_Stack_Addr;
|
||||
|
||||
function Get_Stack_Info return Stack_Checking.Stack_Access is
|
||||
|
|
@ -222,6 +226,8 @@ package body System.Soft_Links.Tasking is
|
|||
SSL.Set_Sec_Stack_Addr (SSL.Get_Sec_Stack_Addr_NT);
|
||||
SSL.Set_Jmpbuf_Address (SSL.Get_Jmpbuf_Address_NT);
|
||||
end if;
|
||||
|
||||
pragma Assert (Get_Sec_Stack_Addr /= Null_Address);
|
||||
end Init_Tasking_Soft_Links;
|
||||
|
||||
end System.Soft_Links.Tasking;
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@
|
|||
-- --
|
||||
-- S p e c --
|
||||
-- --
|
||||
-- Copyright (C) 2009, Free Software Foundation, Inc. --
|
||||
-- Copyright (C) 2009-2014, Free Software Foundation, Inc. --
|
||||
-- --
|
||||
-- GNAT is free software; you can redistribute it and/or modify it under --
|
||||
-- terms of the GNU General Public License as published by the Free Soft- --
|
||||
|
|
@ -38,6 +38,7 @@ package System.Soft_Links.Tasking is
|
|||
|
||||
procedure Init_Tasking_Soft_Links;
|
||||
-- Set the tasking soft links that are common to the full and the
|
||||
-- restricted run times.
|
||||
-- restricted run times. Clients need to make sure the body of
|
||||
-- System.Secondary_Stack is elaborated before calling this.
|
||||
|
||||
end System.Soft_Links.Tasking;
|
||||
|
|
|
|||
|
|
@ -7,7 +7,7 @@
|
|||
-- B o d y --
|
||||
-- --
|
||||
-- Copyright (C) 1991-1994, Florida State University --
|
||||
-- Copyright (C) 1995-2011, AdaCore --
|
||||
-- Copyright (C) 1995-2014, AdaCore --
|
||||
-- --
|
||||
-- GNAT is free software; you can redistribute it and/or modify it under --
|
||||
-- terms of the GNU General Public License as published by the Free Soft- --
|
||||
|
|
@ -38,6 +38,10 @@ with System.Task_Primitives.Operations;
|
|||
with System.Parameters;
|
||||
with System.Traces;
|
||||
with System.Soft_Links.Tasking;
|
||||
with System.Secondary_Stack; pragma Elaborate_All (System.Secondary_Stack);
|
||||
pragma Unreferenced (System.Secondary_Stack);
|
||||
-- Make sure the body of Secondary_Stack is elaborated before calling
|
||||
-- Init_Tasking_Soft_Links.
|
||||
|
||||
package body System.Tasking.Protected_Objects is
|
||||
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@
|
|||
-- --
|
||||
-- B o d y --
|
||||
-- --
|
||||
-- Copyright (C) 1999-2013, Free Software Foundation, Inc. --
|
||||
-- Copyright (C) 1999-2014, Free Software Foundation, Inc. --
|
||||
-- --
|
||||
-- GNARL is free software; you can redistribute it and/or modify it under --
|
||||
-- terms of the GNU General Public License as published by the Free Soft- --
|
||||
|
|
@ -47,9 +47,12 @@ with Ada.Exceptions;
|
|||
|
||||
with System.Task_Primitives.Operations;
|
||||
with System.Soft_Links.Tasking;
|
||||
with System.Secondary_Stack;
|
||||
with System.Storage_Elements;
|
||||
|
||||
with System.Secondary_Stack; pragma Elaborate_All (System.Secondary_Stack);
|
||||
-- Make sure the body of Secondary_Stack is elaborated before calling
|
||||
-- Init_Tasking_Soft_Links.
|
||||
|
||||
with System.Soft_Links;
|
||||
-- Used for the non-tasking routines (*_NT) that refer to global data. They
|
||||
-- are needed here before the tasking run time has been elaborated. used for
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@
|
|||
-- --
|
||||
-- B o d y --
|
||||
-- --
|
||||
-- Copyright (C) 1992-2013, Free Software Foundation, Inc. --
|
||||
-- Copyright (C) 1992-2014, Free Software Foundation, Inc. --
|
||||
-- --
|
||||
-- GNARL is free software; you can redistribute it and/or modify it under --
|
||||
-- terms of the GNU General Public License as published by the Free Soft- --
|
||||
|
|
@ -47,6 +47,11 @@ with System.Soft_Links.Tasking;
|
|||
with System.Tasking.Debug;
|
||||
with System.Parameters;
|
||||
|
||||
with System.Secondary_Stack; pragma Elaborate_All (System.Secondary_Stack);
|
||||
pragma Unreferenced (System.Secondary_Stack);
|
||||
-- Make sure the body of Secondary_Stack is elaborated before calling
|
||||
-- Init_Tasking_Soft_Links.
|
||||
|
||||
package body System.Tasking.Initialization is
|
||||
|
||||
package STPO renames System.Task_Primitives.Operations;
|
||||
|
|
|
|||
|
|
@ -2164,10 +2164,10 @@ package body Sem_Cat is
|
|||
and then Is_Entity_Name (Renamed_Object (E))
|
||||
and then
|
||||
(Is_Preelaborated
|
||||
(Scope (Renamed_Object (E)))
|
||||
or else
|
||||
Is_Pure (Scope
|
||||
(Renamed_Object (E))))))
|
||||
(Scope (Renamed_Object (E)))
|
||||
or else
|
||||
Is_Pure
|
||||
(Scope (Renamed_Object (E))))))
|
||||
then
|
||||
null;
|
||||
|
||||
|
|
@ -2182,7 +2182,7 @@ package body Sem_Cat is
|
|||
and then Is_Entity_Name (Val)
|
||||
and then Is_Array_Type (Etype (Val))
|
||||
and then not Comes_From_Source (Val)
|
||||
and then Nkind (Original_Node (Val)) = N_Aggregate
|
||||
and then Nkind (Original_Node (Val)) = N_Aggregate
|
||||
then
|
||||
null;
|
||||
|
||||
|
|
|
|||
|
|
@ -3236,10 +3236,6 @@ package body Sem_Ch13 is
|
|||
not Null_Present
|
||||
(Specification
|
||||
(Unit_Declaration_Node (Ultimate_Alias (Subp))))
|
||||
|
||||
-- Disable this test for now till Polyorb issue is fixed???
|
||||
|
||||
and then False
|
||||
then
|
||||
Error_Msg_N
|
||||
("stream subprogram for interface type "
|
||||
|
|
|
|||
|
|
@ -18032,10 +18032,10 @@ package body Sem_Prag is
|
|||
Check_No_Identifiers;
|
||||
Check_Pre_Post;
|
||||
|
||||
-- Rewrite Post[_Class] pragma as Precondition pragma setting the
|
||||
-- Rewrite Post[_Class] pragma as Postcondition pragma setting the
|
||||
-- flag Class_Present to True for the Post_Class case.
|
||||
|
||||
Set_Class_Present (N, Prag_Id = Pragma_Pre_Class);
|
||||
Set_Class_Present (N, Prag_Id = Pragma_Post_Class);
|
||||
PC_Pragma := New_Copy (N);
|
||||
Set_Pragma_Identifier
|
||||
(PC_Pragma, Make_Identifier (Loc, Name_Postcondition));
|
||||
|
|
|
|||
Loading…
Reference in New Issue