+ -------------------------------------
+ -- Analyze_Aspects_On_Body_Or_Stub --
+ -------------------------------------
+
+ procedure Analyze_Aspects_On_Body_Or_Stub is
+ procedure Diagnose_Misplaced_Aspects;
+ -- Subprogram body [stub] N has aspects, but they are not properly
+ -- placed. Provide precise diagnostics depending on the aspects
+ -- involved.
+
+ --------------------------------
+ -- Diagnose_Misplaced_Aspects --
+ --------------------------------
+
+ procedure Diagnose_Misplaced_Aspects is
+ Asp : Node_Id;
+ Asp_Nam : Name_Id;
+ Asp_Id : Aspect_Id;
+ -- The current aspect along with its name and id
+
+ procedure SPARK_Aspect_Error (Ref_Nam : Name_Id);
+ -- Emit an error message concerning SPARK aspect Asp. Ref_Nam is
+ -- the name of the refined version of the aspect.
+
+ ------------------------
+ -- SPARK_Aspect_Error --
+ ------------------------
+
+ procedure SPARK_Aspect_Error (Ref_Nam : Name_Id) is
+ begin
+ -- The corresponding spec already contains the aspect in
+ -- question and the one appearing on the body must be the
+ -- refined form:
+
+ -- procedure P with Global ...;
+ -- procedure P with Global ... is ... end P;
+ -- ^
+ -- Refined_Global
+
+ if Has_Aspect (Spec_Id, Asp_Id) then
+ Error_Msg_Name_1 := Asp_Nam;
+
+ -- Subunits cannot carry aspects that apply to a subprogram
+ -- declaration.
+
+ if Nkind (Parent (N)) = N_Subunit then
+ Error_Msg_N ("aspect % cannot apply to a subunit", Asp);
+
+ else
+ Error_Msg_Name_2 := Ref_Nam;
+ Error_Msg_N ("aspect % should be %", Asp);
+ end if;
+
+ -- Otherwise the aspect must appear in the spec, not in the
+ -- body:
+
+ -- procedure P;
+ -- procedure P with Global ... is ... end P;
+
+ else
+ Error_Msg_N
+ ("aspect specification must appear in subprogram "
+ & "declaration", Asp);
+ end if;
+ end SPARK_Aspect_Error;
+
+ -- Start of processing for Diagnose_Misplaced_Aspects
+
+ begin
+ -- Iterate over the aspect specifications and emit specific errors
+ -- where applicable.
+
+ Asp := First (Aspect_Specifications (N));
+ while Present (Asp) loop
+ Asp_Nam := Chars (Identifier (Asp));
+ Asp_Id := Get_Aspect_Id (Asp_Nam);
+
+ -- Do not emit errors on aspects that can appear on a
+ -- subprogram body. This scenario occurs when the aspect
+ -- specification list contains both misplaced and properly
+ -- placed aspects.
+
+ if Aspect_On_Body_Or_Stub_OK (Asp_Id) then
+ null;
+
+ -- Special diagnostics for SPARK aspects
+
+ elsif Asp_Nam = Name_Depends then
+ SPARK_Aspect_Error (Name_Refined_Depends);
+
+ elsif Asp_Nam = Name_Global then
+ SPARK_Aspect_Error (Name_Refined_Global);
+
+ elsif Asp_Nam = Name_Post then
+ SPARK_Aspect_Error (Name_Refined_Post);
+
+ else
+ Error_Msg_N
+ ("aspect specification must appear in subprogram "
+ & "declaration", Asp);
+ end if;
+
+ Next (Asp);
+ end loop;
+ end Diagnose_Misplaced_Aspects;
+
+ -- Start of processing for Analyze_Aspects_On_Body_Or_Stub
+
+ begin
+ -- Language-defined aspects cannot be associated with a subprogram
+ -- body [stub] if the subprogram has a spec. Certain implementation
+ -- defined aspects are allowed to break this rule (for list, see
+ -- table Aspect_On_Body_Or_Stub_OK).
+
+ if Present (Spec_Id) and then not Aspects_On_Body_Or_Stub_OK (N) then
+ Diagnose_Misplaced_Aspects;
+ else
+ Analyze_Aspect_Specifications (N, Body_Id);
+ end if;
+ end Analyze_Aspects_On_Body_Or_Stub;
+