2014-08-04 Hristian Kirtchev <kirtchev@adacore.com>
+ * sem_ch7.adb (Analyze_Package_Body_Helper): When verifying the
+ compatibility of SPARK_Mode between a spec and a body, use the
+ SPARK_Mode of the public part.
+ * sem_ch12.adb (Analyze_Generic_Subprogram_Declaration): Use
+ the already available routine to exchange the aspects between
+ the template and its copy. Analyze the aspects of copy to
+ ensure that the corresponding pragmas perform their semantic
+ effects. The partial analysis of aspects is no longer needed.
+ (Analyze_Package_Instantiation): Save and restore the SPARK_Mode
+ of the context.
+ (Analyze_Subprogram_Instantiation): Save and restore the SPARK_Mode of
+ the context.
+ * sem_prag.adb (Analyze_Pragma): Do not bypass a subprogram
+ instantiation which does not come from source.
+
+2014-08-04 Hristian Kirtchev <kirtchev@adacore.com>
+
* a-cfhama.ads, a-cfhase.ads, a-cforma.ads, a-cforse.ads Add
SPARK_Mode pragmas to the public and private part of the unit.
* sem_ch3.adb (Derive_Type_Declaration): Ensure that a derived
Set_Parent_Spec (New_N, Save_Parent);
Rewrite (N, New_N);
- -- The aspect specifications are not attached to the tree, and must
- -- be copied and attached to the generic copy explicitly.
+ -- Once the contents of the generic copy and the template are swapped,
+ -- do the same for their respective aspect specifications.
- if Present (Aspect_Specifications (New_N)) then
- declare
- Aspects : constant List_Id := Aspect_Specifications (N);
- begin
- Set_Has_Aspects (N, False);
- Move_Aspects (New_N, To => N);
- Set_Has_Aspects (Original_Node (N), False);
- Set_Aspect_Specifications (Original_Node (N), Aspects);
- end;
- end if;
+ Exchange_Aspects (N, New_N);
Spec := Specification (N);
Id := Defining_Entity (Spec);
Start_Generic;
Enter_Name (Id);
-
Set_Scope_Depth_Value (Id, Scope_Depth (Current_Scope) + 1);
+
+ -- Analyze the aspects of the generic copy to ensure that all generated
+ -- pragmas (if any) perform their semantic effects.
+
+ if Has_Aspects (N) then
+ Analyze_Aspect_Specifications (N, Id);
+ end if;
+
Push_Scope (Id);
Enter_Generic_Scope (Id);
Set_Inner_Instances (Id, New_Elmt_List);
Make_Aspect_For_PPC_In_Gen_Sub_Decl (N);
end if;
- -- To capture global references, analyze the expressions of aspects,
- -- and propagate information to original tree. Note that in this case
- -- analysis of attributes is not delayed until the freeze point.
-
- -- It seems very hard to recreate the proper visibility of the generic
- -- subprogram at a later point because the analysis of an aspect may
- -- create pragmas after the generic copies have been made ???
-
- if Has_Aspects (N) then
- declare
- Aspect : Node_Id;
-
- begin
- Aspect := First (Aspect_Specifications (N));
- while Present (Aspect) loop
- if Get_Aspect_Id (Aspect) /= Aspect_Warnings
- and then Present (Expression (Aspect))
- then
- Analyze (Expression (Aspect));
- end if;
-
- Next (Aspect);
- end loop;
-
- Aspect := First (Aspect_Specifications (Original_Node (N)));
- while Present (Aspect) loop
- if Present (Expression (Aspect)) then
- Save_Global_References (Expression (Aspect));
- end if;
-
- Next (Aspect);
- end loop;
- end;
- end if;
-
End_Generic;
End_Scope;
Exit_Generic_Scope (Id);
Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
-- Save flag Ignore_Pragma_SPARK_Mode for restore on exit
+ Save_SM : constant SPARK_Mode_Type := SPARK_Mode;
+ Save_SMP : constant Node_Id := SPARK_Mode_Pragma;
+ -- Save the SPARK_Mode-related data for restore on exit
+
Save_Style_Check : constant Boolean := Style_Check;
-- Save style check mode for restore on exit
end if;
Ignore_Pragma_SPARK_Mode := Save_IPSM;
- Style_Check := Save_Style_Check;
+ SPARK_Mode := Save_SM;
+ SPARK_Mode_Pragma := Save_SMP;
+ Style_Check := Save_Style_Check;
-- Check that if N is an instantiation of System.Dim_Float_IO or
-- System.Dim_Integer_IO, the formal type has a dimension system.
end if;
Ignore_Pragma_SPARK_Mode := Save_IPSM;
- Style_Check := Save_Style_Check;
+ SPARK_Mode := Save_SM;
+ SPARK_Mode_Pragma := Save_SMP;
+ Style_Check := Save_Style_Check;
end Analyze_Package_Instantiation;
--------------------------
Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
-- Save flag Ignore_Pragma_SPARK_Mode for restore on exit
+ Save_SM : constant SPARK_Mode_Type := SPARK_Mode;
+ Save_SMP : constant Node_Id := SPARK_Mode_Pragma;
+ -- Save the SPARK_Mode-related data for restore on exit
+
Vis_Prims_List : Elist_Id := No_Elist;
-- List of primitives made temporarily visible in the instantiation
-- to match the visibility of the formal type
Generic_Renamings_HTable.Reset;
Ignore_Pragma_SPARK_Mode := Save_IPSM;
+ SPARK_Mode := Save_SM;
+ SPARK_Mode_Pragma := Save_SMP;
end if;
<<Leave>>
end if;
Ignore_Pragma_SPARK_Mode := Save_IPSM;
+ SPARK_Mode := Save_SM;
+ SPARK_Mode_Pragma := Save_SMP;
end Analyze_Subprogram_Instantiation;
-------------------------
raise Pragma_Exit;
end if;
+ -- Skip internally generated code, but consider subprogram
+ -- instantiations housed within their wrapper packages.
+
+ elsif not Comes_From_Source (Stmt)
+ and then
+ (Nkind (Stmt) /= N_Subprogram_Declaration
+ or else No (Generic_Parent (Specification (Stmt))))
+ then
+ null;
+
-- The pragma is associated with a package or subprogram
-- instantiation that does not act as a compilation unit.
Set_SPARK_Pragma_Inherited (Inst_Id, False);
return;
- -- The pragma applies to a subprogram declaration
+ -- The pragma applies to a [generic] subprogram declaration
+ -- [generic]
-- procedure Proc ...;
-- pragma SPARK_Mode ..;
- elsif Nkind (Stmt) = N_Subprogram_Declaration then
+ elsif Nkind_In (Stmt, N_Generic_Subprogram_Declaration,
+ N_Subprogram_Declaration)
+ then
Spec_Id := Defining_Entity (Stmt);
Check_Library_Level_Entity (Spec_Id);
Check_Pragma_Conformance
Entity_Pragma => Empty,
Entity => Empty);
- Set_SPARK_Pragma (Spec_Id, N);
- Set_SPARK_Pragma_Inherited (Spec_Id, False);
+ Set_SPARK_Pragma (Spec_Id, N);
+ Set_SPARK_Pragma_Inherited (Spec_Id, False);
return;
- -- Skip internally generated code
-
- elsif not Comes_From_Source (Stmt) then
- null;
-
-- Otherwise the pragma does not apply to a legal construct
-- or it does not appear at the top of a declarative or a
-- statement list. Issue an error and stop the analysis.
exit;
end if;
- Stmt := Prev (Stmt);
+ Prev (Stmt);
end loop;
-- The pragma appears within package declarations
projects / platform / upstream / gcc.git / commitdiff