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