+2014-11-07 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * freeze.adb (Freeze_Entity): Issue an error regardless of the
+ SPARK_Mode when a ghost type is effectively volatile.
+ * sem_ch3.adb (Analyze_Object_Contract): Decouple the checks
+ related to Ghost from SPARK_Mode.
+ * sem_res.adb (Check_Ghost_Policy): Issue an error regardless
+ of the SPARK_Mode when the Ghost policies do not match.
+ * sem_util.adb (Check_Ghost_Completion): Issue an error regardless
+ of the SPARK_Mode when the Ghost policies do not match.
+
+2014-11-07 Ed Schonberg <schonberg@adacore.com>
+
+ * sem_ch5.adb (Analyze_Iterator_Specification): return if name
+ in iterator does not have any usable aspect for iteration.
+
+2014-11-07 Ed Schonberg <schonberg@adacore.com>
+
+ * sem_ch6.adb (Analyze_Null_Procedure): Reject a null procedure
+ that there is a previous null procedure in scope with a matching
+ profile.
+
+2014-11-07 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * atree.adb (Copy_Separate_Tree): Copy the aspect specifications.
+ * inline.adb (Has_Some_Contract): Do the check only when the
+ related entity has been analyzed.
+
2014-11-07 Ed Schonberg <schonberg@adacore.com>
* exp_fixd.adb (Expand_Multiply_Fixed_By_Fixed_Giving_Integer):
Set_Field4 (New_Id, Possible_Copy (Field4 (New_Id)));
Set_Field5 (New_Id, Possible_Copy (Field5 (New_Id)));
+ -- Explicitly copy the aspect specifications as those do not reside
+ -- in a node field.
+
+ if Permits_Aspect_Specifications (Source)
+ and then Has_Aspects (Source)
+ then
+ Set_Aspect_Specifications
+ (New_Id, Copy_List (Aspect_Specifications (Source)));
+ end if;
+
-- Set Entity field to Empty to ensure that no entity references
-- are shared between the two, if the source is already analyzed.
Set_Has_Non_Standard_Rep (Base_Type (Arr), True);
Set_Is_Bit_Packed_Array (Base_Type (Arr), True);
Set_Is_Packed (Base_Type (Arr), True);
+
+ -- Make sure that we have the necessary routines to
+ -- implement the packing, and complain now if not.
+
+ declare
+ CS : constant Int := UI_To_Int (Csiz);
+ RE : constant RE_Id := Get_Id (CS);
+
+ begin
+ if RE /= RE_Null
+ and then not RTE_Available (RE)
+ then
+ Error_Msg_CRT
+ ("packing of " & UI_Image (Csiz)
+ & "-bit components",
+ First_Subtype (Etype (Arr)));
+ end if;
+ end;
end if;
end;
end if;
Create_Packed_Array_Impl_Type (Arr);
Freeze_And_Append (Packed_Array_Impl_Type (Arr), N, Result);
- -- Make sure that we have the necessary routines to implement the
- -- packing, and complain now if not. Note that we only test this
- -- for constrained array types.
-
- if Is_Constrained (Arr)
- and then Is_Bit_Packed_Array (Arr)
- and then Present (Packed_Array_Impl_Type (Arr))
- and then Is_Array_Type (Packed_Array_Impl_Type (Arr))
- then
- declare
- CS : constant Uint := Component_Size (Arr);
- RE : constant RE_Id := Get_Id (UI_To_Int (CS));
-
- begin
- if RE /= RE_Null
- and then not RTE_Available (RE)
- then
- Error_Msg_CRT
- ("packing of " & UI_Image (CS) & "-bit components",
- First_Subtype (Etype (Arr)));
-
- -- Cancel the packing
-
- Set_Is_Packed (Base_Type (Arr), False);
- Set_Is_Bit_Packed_Array (Base_Type (Arr), False);
- Set_Packed_Array_Impl_Type (Arr, Empty);
- goto Skip_Packed;
- end if;
- end;
- end if;
-
-- Size information of packed array type is copied to the array
-- type, since this is really the representation. But do not
-- override explicit existing size values. If the ancestor subtype
end if;
end if;
- <<Skip_Packed>>
-
-- For non-packed arrays set the alignment of the array to the
-- alignment of the component type if it is unknown. Skip this
-- in atomic case (atomic arrays may need larger alignments).
if Is_Ghost_Entity (E)
and then Is_Effectively_Volatile (E)
then
- SPARK_Msg_N ("ghost type & cannot be volatile", E);
+ Error_Msg_N ("ghost type & cannot be volatile", E);
end if;
-- Deal with special cases of freezing for subtype
-----------------------
function Has_Some_Contract (Id : Entity_Id) return Boolean is
- Items : constant Node_Id := Contract (Id);
+ Items : Node_Id;
+
begin
- return Present (Items)
- and then (Present (Pre_Post_Conditions (Items)) or else
- Present (Contract_Test_Cases (Items)) or else
- Present (Classifications (Items)));
+ -- A call to an expression function may precede the actual body which
+ -- is inserted at the end of the enclosing declarations. Ensure that
+ -- the related entity is analyzed before inspecting the contract.
+
+ if Analyzed (Id) then
+ Items := Contract (Id);
+
+ return Present (Items)
+ and then (Present (Pre_Post_Conditions (Items)) or else
+ Present (Contract_Test_Cases (Items)) or else
+ Present (Classifications (Items)));
+ end if;
+
+ return False;
end Has_Some_Contract;
-----------------------------
Obj_Id);
end if;
end if;
+ end if;
- if Is_Ghost_Entity (Obj_Id) then
+ if Is_Ghost_Entity (Obj_Id) then
- -- A Ghost object cannot be effectively volatile
- -- (SPARK RM 6.9(8)).
+ -- A Ghost object cannot be effectively volatile (SPARK RM 6.9(8))
- if Is_Effectively_Volatile (Obj_Id) then
- SPARK_Msg_N ("ghost variable & cannot be volatile", Obj_Id);
+ if Is_Effectively_Volatile (Obj_Id) then
+ Error_Msg_N ("ghost variable & cannot be volatile", Obj_Id);
- -- A Ghost object cannot be imported or exported
- -- (SPARK RM 6.9(8)).
+ -- A Ghost object cannot be imported or exported (SPARK RM 6.9(8))
- elsif Is_Imported (Obj_Id) then
- SPARK_Msg_N ("ghost object & cannot be imported", Obj_Id);
+ elsif Is_Imported (Obj_Id) then
+ Error_Msg_N ("ghost object & cannot be imported", Obj_Id);
- elsif Is_Exported (Obj_Id) then
- SPARK_Msg_N ("ghost object & cannot be exported", Obj_Id);
- end if;
+ elsif Is_Exported (Obj_Id) then
+ Error_Msg_N ("ghost object & cannot be exported", Obj_Id);
end if;
end if;
if Is_Ghost_Entity (Obj_Id) then
if Is_Exported (Obj_Id) then
- SPARK_Msg_N ("ghost object & cannot be exported", Obj_Id);
+ Error_Msg_N ("ghost object & cannot be exported", Obj_Id);
elsif Is_Imported (Obj_Id) then
- SPARK_Msg_N ("ghost object & cannot be imported", Obj_Id);
+ Error_Msg_N ("ghost object & cannot be imported", Obj_Id);
end if;
end if;
end Analyze_Object_Contract;
when Class_Wide_Kind =>
Set_Ekind (Id, E_Class_Wide_Subtype);
- Set_First_Entity (Id, First_Entity (T));
- Set_Last_Entity (Id, Last_Entity (T));
Set_Class_Wide_Type (Id, Class_Wide_Type (T));
Set_Cloned_Subtype (Id, T);
Set_Is_Tagged_Type (Id, True);
Error_Msg_NE
("\to iterate directly over the elements of a container, "
& "write `of &`", Name (N), Original_Node (Name (N)));
+
+ -- No point in continuing analysis of iterator spec.
+
+ return;
end if;
end if;
-- there are various error checks that are applied on this body
-- when it is analyzed (e.g. correct aspect placement).
+ if Has_Completion (Prev) then
+ Error_Msg_Sloc := Sloc (Prev);
+ Error_Msg_NE ("duplicate body for & declared#", N, Prev);
+ end if;
+
Is_Completion := True;
Rewrite (N, Null_Body);
Analyze (N);
if Is_Checked_Ghost_Entity (Id) and then Policy = Name_Ignore then
Error_Msg_Sloc := Sloc (Err_N);
- SPARK_Msg_N ("incompatible ghost policies in effect", Err_N);
- SPARK_Msg_NE ("\& declared with ghost policy Check", Err_N, Id);
- SPARK_Msg_NE ("\& used # with ghost policy Ignore", Err_N, Id);
+ Error_Msg_N ("incompatible ghost policies in effect", Err_N);
+ Error_Msg_NE ("\& declared with ghost policy Check", Err_N, Id);
+ Error_Msg_NE ("\& used # with ghost policy Ignore", Err_N, Id);
elsif Is_Ignored_Ghost_Entity (Id) and then Policy = Name_Check then
Error_Msg_Sloc := Sloc (Err_N);
- SPARK_Msg_N ("incompatible ghost policies in effect", Err_N);
- SPARK_Msg_NE ("\& declared with ghost policy Ignore", Err_N, Id);
- SPARK_Msg_NE ("\& used # with ghost policy Check", Err_N, Id);
+ Error_Msg_N ("incompatible ghost policies in effect", Err_N);
+ Error_Msg_NE ("\& declared with ghost policy Ignore", Err_N, Id);
+ Error_Msg_NE ("\& used # with ghost policy Check", Err_N, Id);
end if;
end Check_Ghost_Policy;
-- its behavior or value.
else
- SPARK_Msg_N
+ Error_Msg_N
("ghost entity cannot appear in this context (SPARK RM 6.9(12))",
Ghost_Ref);
end if;
("volatile object cannot appear in this context "
& "(SPARK RM 7.1.3(13))", N);
end if;
+ end if;
+ end if;
- -- A Ghost entity must appear in a specific context
+ -- A Ghost entity must appear in a specific context
- elsif Is_Ghost_Entity (E) and then Comes_From_Source (N) then
- Check_Ghost_Context (E, N);
- end if;
+ if Is_Ghost_Entity (E) and then Comes_From_Source (N) then
+ Check_Ghost_Context (E, N);
end if;
end Resolve_Entity_Name;
then
Error_Msg_Sloc := Sloc (Full_View);
- SPARK_Msg_N ("incompatible ghost policies in effect", Partial_View);
- SPARK_Msg_N ("\& declared with ghost policy Check", Partial_View);
- SPARK_Msg_N ("\& completed # with ghost policy Ignore", Partial_View);
+ Error_Msg_N ("incompatible ghost policies in effect", Partial_View);
+ Error_Msg_N ("\& declared with ghost policy Check", Partial_View);
+ Error_Msg_N ("\& completed # with ghost policy Ignore", Partial_View);
elsif Is_Ignored_Ghost_Entity (Partial_View)
and then Policy = Name_Check
then
Error_Msg_Sloc := Sloc (Full_View);
- SPARK_Msg_N ("incompatible ghost policies in effect", Partial_View);
- SPARK_Msg_N ("\& declared with ghost policy Ignore", Partial_View);
- SPARK_Msg_N ("\& completed # with ghost policy Check", Partial_View);
+ Error_Msg_N ("incompatible ghost policies in effect", Partial_View);
+ Error_Msg_N ("\& declared with ghost policy Ignore", Partial_View);
+ Error_Msg_N ("\& completed # with ghost policy Check", Partial_View);
end if;
end Check_Ghost_Completion;
-- The parent type of a Ghost type extension must be Ghost
elsif not Is_Ghost_Entity (Parent_Typ) then
- SPARK_Msg_N ("type extension & cannot be ghost", Typ);
- SPARK_Msg_NE ("\parent type & is not ghost", Typ, Parent_Typ);
+ Error_Msg_N ("type extension & cannot be ghost", Typ);
+ Error_Msg_NE ("\parent type & is not ghost", Typ, Parent_Typ);
return;
end if;
Iface := Node (Iface_Elmt);
if not Is_Ghost_Entity (Iface) then
- SPARK_Msg_N ("type extension & cannot be ghost", Typ);
- SPARK_Msg_NE ("\interface type & is not ghost", Typ, Iface);
+ Error_Msg_N ("type extension & cannot be ghost", Typ);
+ Error_Msg_NE ("\interface type & is not ghost", Typ, Iface);
return;
end if;
projects / gcc.git / commitdiff