+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.
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.
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) :=
-- --
-- GNAT RUN-TIME LIBRARY (GNARL) COMPONENTS --
-- --
--- SYSTEM.INTERRUPT_MANAGEMENT.OPERATIONS --
+-- SYSTEM.INTERRUPT_MANAGEMENT.OPERATIONS --
-- --
-- B o d y --
-- --
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
-- 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:
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
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
-- 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
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
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.
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);
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);
-- 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
-- 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
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
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;
------------------------
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
-- 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
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;
-- 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;
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
-- 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));
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
projects / gcc.git / commitdiff