+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.
* 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::
* 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::
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
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
with System;
package Interfaces.C.Extensions is
+ pragma Pure;
-- Definitions for C "void" and "void *" types
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
-- 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
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.
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
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) --
-------------------------
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);
No_Elaboration_Code, -- GNAT
No_Obsolescent_Features, -- Ada 2005 AI-368
No_Wide_Characters, -- GNAT
+ SPARK, -- GNAT
-- The following cases require a parameter value
-- 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
-- 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
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.
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 --
--------------------------------
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,
-- or because it is a generic actual, so use base type to
-- locate concurrent type.
- A_Typ := Base_Type (Etype (A));
F_Typ := Base_Type (Etype (F));
- declare
- Full_A_Typ : Entity_Id;
+ if Is_Tagged_Type (F_Typ)
+ and then (Is_Concurrent_Type (F_Typ)
+ or else Is_Concurrent_Record_Type (F_Typ))
+ then
+ -- If the actual is overloaded, look for an interpretation
+ -- that has a synchronized type.
+
+ if not Is_Overloaded (A) then
+ A_Typ := Base_Type (Etype (A));
- begin
- if Present (Full_View (A_Typ)) then
- Full_A_Typ := Base_Type (Full_View (A_Typ));
else
- Full_A_Typ := A_Typ;
+ declare
+ Index : Interp_Index;
+ It : Interp;
+ begin
+ Get_First_Interp (A, Index, It);
+ while Present (It.Typ) loop
+ if Is_Concurrent_Type (It.Typ)
+ or else Is_Concurrent_Record_Type (It.Typ)
+ then
+ A_Typ := Base_Type (It.Typ);
+ exit;
+ end if;
+
+ Get_Next_Interp (Index, It);
+ end loop;
+ end;
end if;
- -- Tagged synchronized type (case 1): the actual is a
- -- concurrent type.
+ declare
+ Full_A_Typ : Entity_Id;
- if Is_Concurrent_Type (A_Typ)
- and then Corresponding_Record_Type (A_Typ) = F_Typ
- then
- Rewrite (A,
- Unchecked_Convert_To
- (Corresponding_Record_Type (A_Typ), A));
- Resolve (A, Etype (F));
+ begin
+ if Present (Full_View (A_Typ)) then
+ Full_A_Typ := Base_Type (Full_View (A_Typ));
+ else
+ Full_A_Typ := A_Typ;
+ end if;
+
+ -- Tagged synchronized type (case 1): the actual is a
+ -- concurrent type.
+
+ if Is_Concurrent_Type (A_Typ)
+ and then Corresponding_Record_Type (A_Typ) = F_Typ
+ then
+ Rewrite (A,
+ Unchecked_Convert_To
+ (Corresponding_Record_Type (A_Typ), A));
+ Resolve (A, Etype (F));
- -- Tagged synchronized type (case 2): the formal is a
- -- concurrent type.
+ -- Tagged synchronized type (case 2): the formal is a
+ -- concurrent type.
- elsif Ekind (Full_A_Typ) = E_Record_Type
- and then Present
+ elsif Ekind (Full_A_Typ) = E_Record_Type
+ and then Present
(Corresponding_Concurrent_Type (Full_A_Typ))
- and then Is_Concurrent_Type (F_Typ)
- and then Present (Corresponding_Record_Type (F_Typ))
- and then Full_A_Typ = Corresponding_Record_Type (F_Typ)
- then
- Resolve (A, Corresponding_Record_Type (F_Typ));
+ and then Is_Concurrent_Type (F_Typ)
+ and then Present (Corresponding_Record_Type (F_Typ))
+ and then Full_A_Typ = Corresponding_Record_Type (F_Typ)
+ then
+ Resolve (A, Corresponding_Record_Type (F_Typ));
- -- Common case
+ -- Common case
- else
- Resolve (A, Etype (F));
- end if;
- end;
+ else
+ Resolve (A, Etype (F));
+ end if;
+ end;
+ else
+
+ -- not a synchronized operation.
+
+ Resolve (A, Etype (F));
+ end if;
end if;
A_Typ := Etype (A);
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
Pragma_Short_Descriptors,
Pragma_Source_File_Name,
Pragma_Source_File_Name_Project,
- Pragma_SPARK_95,
Pragma_Style_Checks,
Pragma_Suppress,
Pragma_Suppress_Exception_Locations,
OSDN Git Service
