[multiple changes]

2011-08-02  Yannick Moy  <moy@adacore.com>

	* exp_ch6.adb (Expand_N_Subprogram_Declaration): issue error in formal
	mode on subprogram declaration outside of package specification, unless
	it is followed by a pragma Import
	* sem_ch3.adb (Access_Definition, Access_Subprogram_Declaration,
	Access_Type_Declaration): issue error in formal mode on access type
	(Analyze_Incomplete_Type_Decl): issue error in formal mode on
	incomplete type
	(Analyze_Object_Declaration): issue error in formal mode on object
	declaration which does not respect SPARK restrictions
	(Analyze_Subtype_Declaration): issue error in formal mode on subtype
	declaration which does not respect SPARK restrictions
	(Constrain_Decimal, Constrain_Float, Constrain_Ordinary_Fixed): issue
	error in formal mode on digits or delta constraint
	(Decimal_Fixed_Point_Type_Declaration): issue error in formal mode on
	decimal fixed point type
	(Derived_Type_Declaration): issue error in formal mode on derived type
	other than type extensions of tagged record types
	* sem_ch6.adb (Process_Formals): remove check in formal mode, redundant
	with check on access definition
	* sem_ch9.adb (Analyze_Protected_Definition): issue error in formal
	mode on protected definition.
	(Analyze_Task_Definition): issue error in formal mode on task definition

2011-08-02  Robert Dewar  <dewar@adacore.com>

	* make.adb, sem_ch8.adb, s-inmaop-vxworks.adb: Minor reformatting.

From-SVN: r177093

gcc/ada/ChangeLog

+2011-08-02  Yannick Moy  <moy@adacore.com>
+
+	* exp_ch6.adb (Expand_N_Subprogram_Declaration): issue error in formal
+	mode on subprogram declaration outside of package specification, unless
+	it is followed by a pragma Import
+	* sem_ch3.adb (Access_Definition, Access_Subprogram_Declaration,
+	Access_Type_Declaration): issue error in formal mode on access type
+	(Analyze_Incomplete_Type_Decl): issue error in formal mode on
+	incomplete type
+	(Analyze_Object_Declaration): issue error in formal mode on object
+	declaration which does not respect SPARK restrictions
+	(Analyze_Subtype_Declaration): issue error in formal mode on subtype
+	declaration which does not respect SPARK restrictions
+	(Constrain_Decimal, Constrain_Float, Constrain_Ordinary_Fixed): issue
+	error in formal mode on digits or delta constraint
+	(Decimal_Fixed_Point_Type_Declaration): issue error in formal mode on
+	decimal fixed point type
+	(Derived_Type_Declaration): issue error in formal mode on derived type
+	other than type extensions of tagged record types
+	* sem_ch6.adb (Process_Formals): remove check in formal mode, redundant
+	with check on access definition
+	* sem_ch9.adb (Analyze_Protected_Definition): issue error in formal
+	mode on protected definition.
+	(Analyze_Task_Definition): issue error in formal mode on task definition
+
+2011-08-02  Robert Dewar  <dewar@adacore.com>
+
+	* make.adb, sem_ch8.adb, s-inmaop-vxworks.adb: Minor reformatting.
+
 2011-08-02  Javier Miranda  <miranda@adacore.com>
 
 	* sem_ch6.adb (Can_Override_Operator): New function.

gcc/ada/exp_ch6.adb

@@ -5406,6 +5406,28 @@ package body Exp_Ch6 is
       Prot_Id   : Entity_Id;
 
    begin
+      --  In SPARK or ALFA, subprogram declarations are only allowed in
+      --  package specifications.
+
+      if Formal_Verification_Mode
+        and then Comes_From_Source (Original_Node (N))
+        and then Nkind (Parent (N)) /= N_Package_Specification
+      then
+         if Present (Next (N))
+           and then Nkind (Next (N)) = N_Pragma
+           and then Get_Pragma_Id (Pragma_Name (Next (N))) = Pragma_Import
+         then
+            --  In SPARK or ALFA, 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
+            Error_Msg_F ("|~~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.
 

gcc/ada/make.adb

@@ -6066,8 +6066,8 @@ package body Make is
                      end loop;
 
                      for Index in 1 .. Library_Projs.Last loop
-                        if
-                          Library_Projs.Table (Index).Library_Kind = Static
+                        if Library_Projs.Table
+                            (Index).Library_Kind = Static
                         then
                            Linker_Switches.Increment_Last;
                            Linker_Switches.Table (Linker_Switches.Last) :=

gcc/ada/s-inmaop-vxworks.adb

@@ -2,7 +2,7 @@
 --                                                                          --
 --                  GNAT RUN-TIME LIBRARY (GNARL) COMPONENTS                --
 --                                                                          --
---                  SYSTEM.INTERRUPT_MANAGEMENT.OPERATIONS                  --
+--                   SYSTEM.INTERRUPT_MANAGEMENT.OPERATIONS                 --
 --                                                                          --
 --                                  B o d y                                 --
 --                                                                          --

gcc/ada/sem_ch3.adb

@@ -716,6 +716,16 @@ package body Sem_Ch3 is
       Enclosing_Prot_Type : Entity_Id := Empty;
 
    begin
+      --  Access type is not allowed in SPARK or ALFA
+
+      if Formal_Verification_Mode
+        and then Comes_From_Source (N)
+      then
+         Error_Msg_F ("|~~access type is not allowed", N);
+      end if;
+
+      --  Proceed with analysis
+
       if Is_Entry (Current_Scope)
         and then Is_Task_Type (Etype (Scope (Current_Scope)))
       then
@@ -1028,6 +1038,14 @@ package body Sem_Ch3 is
    --  Start of processing for Access_Subprogram_Declaration
 
    begin
+      --  Access type is not allowed in SPARK or ALFA
+
+      if Formal_Verification_Mode
+        and then Comes_From_Source (T_Def)
+      then
+         Error_Msg_F ("|~~access type is not allowed", T_Def);
+      end if;
+
       --  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:
@@ -1280,6 +1298,14 @@ package body Sem_Ch3 is
       S : constant Node_Id := Subtype_Indication (Def);
       P : constant Node_Id := Parent (Def);
    begin
+      --  Access type is not allowed in SPARK or ALFA
+
+      if Formal_Verification_Mode
+        and then Comes_From_Source (Def)
+      then
+         Error_Msg_F ("|~~access type is not allowed", Def);
+      end if;
+
       --  Check for permissible use of incomplete type
 
       if Nkind (S) /= N_Subtype_Indication then
@@ -2477,6 +2503,16 @@ package body Sem_Ch3 is
       T : Entity_Id;
 
    begin
+      --  Incomplete type is not allowed in SPARK or ALFA
+
+      if Formal_Verification_Mode
+        and then Comes_From_Source (Original_Node (N))
+      then
+         Error_Msg_F ("|~~incomplete type is not allowed", N);
+      end if;
+
+      --  Proceed with analysis
+
       Generate_Definition (Defining_Identifier (N));
 
       --  Process an incomplete declaration. The identifier must not have been
@@ -2805,7 +2841,7 @@ package body Sem_Ch3 is
       --  There are three kinds of implicit types generated by an
       --  object declaration:
 
-      --   1. Those for generated by the original Object Definition
+      --   1. Those generated by the original Object Definition
 
       --   2. Those generated by the Expression
 
@@ -3010,6 +3046,39 @@ package body Sem_Ch3 is
 
       Act_T := T;
 
+      --  These checks should be performed before the initialization expression
+      --  is considered, so that the Object_Definition node is still the same
+      --  as in source code.
+
+      if Formal_Verification_Mode
+        and then Comes_From_Source (Original_Node (N))
+      then
+         --  In SPARK or ALFA, the nominal subtype shall be given by a subtype
+         --  mark and shall not be unconstrained. (The only exception to this
+         --  is the admission of declarations of constants of type String.)
+
+         if not Nkind_In (Object_Definition (N),
+                          N_Identifier,
+                          N_Expanded_Name)
+         then
+            Error_Msg_F ("|~~subtype mark expected", Object_Definition (N));
+         elsif Is_Array_Type (T)
+           and then not Is_Constrained (T)
+           and then T /= Standard_String
+         then
+            Error_Msg_F ("|~~subtype mark of constrained type expected",
+                         Object_Definition (N));
+         else
+            null;
+         end if;
+
+         --  There are no aliased objects in SPARK or ALFA
+
+         if Aliased_Present (N) then
+            Error_Msg_F ("|~~aliased object is not allowed", N);
+         end if;
+      end if;
+
       --  Process initialization expression if present and not in error
 
       if Present (E) and then E /= Error then
@@ -3949,6 +4018,17 @@ package body Sem_Ch3 is
          Set_Has_Delayed_Freeze (Id);
       end if;
 
+      --  Subtype of Boolean is not allowed to have a constraint in SPARK or
+      --  ALFA.
+
+      if Formal_Verification_Mode
+        and then Comes_From_Source (Original_Node (N))
+        and then Is_Boolean_Type (T)
+        and then Nkind (Subtype_Indication (N)) = N_Subtype_Indication
+      then
+         Error_Msg_F ("|~~subtype of Boolean cannot have constraint", N);
+      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.
@@ -3956,6 +4036,20 @@ package body Sem_Ch3 is
       if Nkind (Subtype_Indication (N)) /= N_Subtype_Indication then
          Set_Etype (Id, Base_Type (T));
 
+         --  Subtype of unconstrained array without constraint is not allowed
+         --  in SPARK or ALFA.
+
+         if Formal_Verification_Mode
+           and then Comes_From_Source (Original_Node (N))
+           and then Is_Array_Type (T)
+           and then not Is_Constrained (T)
+         then
+            Error_Msg_F
+              ("|~~subtype of unconstrained array must have constraint", N);
+         end if;
+
+         --  Proceed with analysis
+
          case Ekind (T) is
             when Array_Kind =>
                Set_Ekind                       (Id, E_Array_Subtype);
@@ -11149,6 +11243,17 @@ package body Sem_Ch3 is
 
       else
          pragma Assert (Nkind (C) = N_Digits_Constraint);
+
+         --  Digits constraint is not allowed in SPARK or ALFA
+
+         if Formal_Verification_Mode
+           and then Comes_From_Source (Original_Node (S))
+         then
+            Error_Msg_F ("|~~digits constraint is not allowed", S);
+         end if;
+
+         --  Proceed with analysis
+
          Digits_Expr := Digits_Expression (C);
          Analyze_And_Resolve (Digits_Expr, Any_Integer);
 
@@ -11375,6 +11480,17 @@ package body Sem_Ch3 is
       --  Digits constraint present
 
       if Nkind (C) = N_Digits_Constraint then
+
+         --  Digits constraint is not allowed in SPARK or ALFA
+
+         if Formal_Verification_Mode
+           and then Comes_From_Source (Original_Node (S))
+         then
+            Error_Msg_F ("|~~digits constraint is not allowed", S);
+         end if;
+
+         --  Proceed with analysis
+
          Check_Restriction (No_Obsolescent_Features, C);
 
          if Warn_On_Obsolescent_Feature then
@@ -11595,6 +11711,16 @@ package body Sem_Ch3 is
       --  Delta constraint present
 
       if Nkind (C) = N_Delta_Constraint then
+         --  Delta constraint is not allowed in SPARK or ALFA
+
+         if Formal_Verification_Mode
+           and then Comes_From_Source (Original_Node (S))
+         then
+            Error_Msg_F ("|~~delta constraint is not allowed", S);
+         end if;
+
+         --  Proceed with analysis
+
          Check_Restriction (No_Obsolescent_Features, C);
 
          if Warn_On_Obsolescent_Feature then
@@ -12251,6 +12377,17 @@ package body Sem_Ch3 is
       Bound_Val     : Ureal;
 
    begin
+      --  Decimal fixed point type is not allowed in SPARK or ALFA
+
+      if Formal_Verification_Mode
+        and then Comes_From_Source (Original_Node (Def))
+      then
+         Error_Msg_F
+           ("|~~decimal fixed point type is not allowed", Def);
+      end if;
+
+      --  Proceed with analysis
+
       Check_Restriction (No_Fixed_Point, Def);
 
       --  Create implicit base type
@@ -14198,6 +14335,15 @@ package body Sem_Ch3 is
             end if;
          end if;
       end if;
+
+      --  In SPARK or ALFA, there are no derived type definitions other than
+      --  type extensions of tagged record types.
+
+      if Formal_Verification_Mode
+        and then No (Extension)
+      then
+         Error_Msg_F ("|~~derived type is not allowed", N);
+      end if;
    end Derived_Type_Declaration;
 
    ------------------------

gcc/ada/sem_ch6.adb

@@ -8785,14 +8785,6 @@ package body Sem_Ch6 is
          Set_Etype (Formal, Formal_Type);
          Default := Expression (Param_Spec);
 
-         --  Access parameter is not allowed in SPARK or ALFA
-
-         if Formal_Verification_Mode
-           and then Ekind (Formal_Type) = E_Anonymous_Access_Type
-         then
-            Error_Msg_F ("|~~access parameter is not allowed", Param_Spec);
-         end if;
-
          if Present (Default) then
             --  Default expression is not allowed in SPARK or ALFA
 

gcc/ada/sem_ch8.adb

@@ -506,9 +506,12 @@ package body Sem_Ch8 is
    --  re-installing use clauses of parent units. N is the use_clause that
    --  names P (and possibly other packages).
 
-   procedure Use_One_Type (Id : Node_Id);
+   procedure Use_One_Type (Id : Node_Id; Installed : Boolean := False);
    --  Id is the subtype mark from a use type clause. This procedure makes
-   --  the primitive operators of the type potentially use-visible.
+   --  the primitive operators of the type potentially use-visible. The
+   --  boolean flag Installed indicates that the clause is being reinstalled
+   --  after previous analysis, and primitive operations are already chained
+   --  on the Used_Operations list of the clause.
 
    procedure Write_Info;
    --  Write debugging information on entities declared in current scope
@@ -2693,11 +2696,8 @@ package body Sem_Ch8 is
          begin
             Mark := First (Subtype_Marks (N));
             while Present (Mark) loop
-               if not In_Use (Entity (Mark))
-                 and then not Is_Potentially_Use_Visible (Entity (Mark))
-               then
-                  Set_In_Use (Base_Type (Entity (Mark)));
-               end if;
+               Use_One_Type (Mark, Installed => True);
+
                Next (Mark);
             end loop;
 
@@ -7565,7 +7565,7 @@ package body Sem_Ch8 is
    -- Use_One_Type --
    ------------------
 
-   procedure Use_One_Type (Id : Node_Id) is
+   procedure Use_One_Type (Id : Node_Id; Installed : Boolean := False) is
       Elmt          : Elmt_Id;
       Is_Known_Used : Boolean;
       Op_List       : Elist_Id;
@@ -7719,40 +7719,46 @@ package body Sem_Ch8 is
          end if;
 
          Set_Current_Use_Clause (T, Parent (Id));
-         Op_List := Collect_Primitive_Operations (T);
 
          --  Iterate over primitive operations of the type. If an operation is
          --  already use_visible, it is the result of a previous use_clause,
-         --  and already appears on the corresponding entity chain.
+         --  and already appears on the corresponding entity chain. If the
+         --  clause is being reinstalled, operations are already use-visible.
 
-         Elmt := First_Elmt (Op_List);
-         while Present (Elmt) loop
-            if (Nkind (Node (Elmt)) = N_Defining_Operator_Symbol
-                 or else Chars (Node (Elmt)) in Any_Operator_Name)
-              and then not Is_Hidden (Node (Elmt))
-              and then not Is_Potentially_Use_Visible (Node (Elmt))
-            then
-               Set_Is_Potentially_Use_Visible (Node (Elmt));
-               Append_Elmt (Node (Elmt), Used_Operations (Parent (Id)));
+         if Installed then
+            null;
 
-            elsif Ada_Version >= Ada_2012
-              and then All_Present (Parent (Id))
-              and then not Is_Hidden (Node (Elmt))
-              and then not Is_Potentially_Use_Visible (Node (Elmt))
-            then
-               Set_Is_Potentially_Use_Visible (Node (Elmt));
-               Append_Elmt (Node (Elmt), Used_Operations (Parent (Id)));
-            end if;
+         else
+            Op_List := Collect_Primitive_Operations (T);
+            Elmt := First_Elmt (Op_List);
+            while Present (Elmt) loop
+               if (Nkind (Node (Elmt)) = N_Defining_Operator_Symbol
+                    or else Chars (Node (Elmt)) in Any_Operator_Name)
+                 and then not Is_Hidden (Node (Elmt))
+                 and then not Is_Potentially_Use_Visible (Node (Elmt))
+               then
+                  Set_Is_Potentially_Use_Visible (Node (Elmt));
+                  Append_Elmt (Node (Elmt), Used_Operations (Parent (Id)));
 
-            Next_Elmt (Elmt);
-         end loop;
-      end if;
+               elsif Ada_Version >= Ada_2012
+                 and then All_Present (Parent (Id))
+                 and then not Is_Hidden (Node (Elmt))
+                 and then not Is_Potentially_Use_Visible (Node (Elmt))
+               then
+                  Set_Is_Potentially_Use_Visible (Node (Elmt));
+                  Append_Elmt (Node (Elmt), Used_Operations (Parent (Id)));
+               end if;
 
-      if Ada_Version >= Ada_2012
-        and then All_Present (Parent (Id))
-        and then Is_Tagged_Type (T)
-      then
-         Use_Class_Wide_Operations (T);
+               Next_Elmt (Elmt);
+            end loop;
+         end if;
+
+         if Ada_Version >= Ada_2012
+           and then All_Present (Parent (Id))
+           and then Is_Tagged_Type (T)
+         then
+            Use_Class_Wide_Operations (T);
+         end if;
       end if;
 
       --  If warning on redundant constructs, check for unnecessary WITH

gcc/ada/sem_ch9.adb

@@ -1158,6 +1158,14 @@ package body Sem_Ch9 is
    --  Start of processing for Analyze_Protected_Definition
 
    begin
+      --  Protected definition is not allowed in SPARK or ALFA
+
+      if Formal_Verification_Mode then
+         Error_Msg_F ("|~~protected definition is not allowed", N);
+      end if;
+
+      --  Proceed with analysis
+
       Tasking_Used := True;
       Analyze_Declarations (Visible_Declarations (N));
 
@@ -2009,6 +2017,14 @@ package body Sem_Ch9 is
       L : Entity_Id;
 
    begin
+      --  Task definition is not allowed in SPARK or ALFA
+
+      if Formal_Verification_Mode then
+         Error_Msg_F ("|~~task definition is not allowed", N);
+      end if;
+
+      --  Proceed with analysis
+
       Tasking_Used := True;
 
       if Present (Visible_Declarations (N)) then