Commit 22da8770 by Arnaud Charlet

[multiple changes]

2016-06-22  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_ch7.adb (Add_Invariant): Replace the
	current type instance with the _object parameter even in ASIS mode.
	(Build_Invariant_Procedure_Body): Do not insert the
	invariant procedure body into the tree for ASIS and GNATprove.
	(Build_Invariant_Procedure_Declaration): Do not insert the
	invariant procedure declaration into the tree for ASIS and
	GNATprove.
	* lib-xref-spark_specific.adb (Add_SPARK_Scope): Update comment.

2016-06-22  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch6.adb (Set_Actual_Subtypes): If the type of the actual
	has predicates, the actual subtype must be frozen properly
	because of the generated tests that may follow.  The predicate
	may be specified by an explicit aspect, or may be inherited in
	a derivation.

From-SVN: r237684
parent 444656ce
2016-06-22 Hristian Kirtchev <kirtchev@adacore.com>
* exp_ch7.adb (Add_Invariant): Replace the
current type instance with the _object parameter even in ASIS mode.
(Build_Invariant_Procedure_Body): Do not insert the
invariant procedure body into the tree for ASIS and GNATprove.
(Build_Invariant_Procedure_Declaration): Do not insert the
invariant procedure declaration into the tree for ASIS and
GNATprove.
* lib-xref-spark_specific.adb (Add_SPARK_Scope): Update comment.
2016-06-22 Ed Schonberg <schonberg@adacore.com>
* sem_ch6.adb (Set_Actual_Subtypes): If the type of the actual
has predicates, the actual subtype must be frozen properly
because of the generated tests that may follow. The predicate
may be specified by an explicit aspect, or may be inherited in
a derivation.
2016-06-22 Ed Schonberg <schonberg@adacore.com>
* exp_ch4.adb (In_Range_Chec)): New predicate, subsidiary of
......
......@@ -4154,39 +4154,32 @@ package body Exp_Ch7 is
Set_Etype (Selector_Name (N), Rep_Typ);
end if;
-- Do not alter the tree for ASIS. As a result all references
-- to Ref_Typ remain as is, but they have sufficent semantic
-- information.
-- Perform the following substitution:
if not ASIS_Mode then
-- Ref_Typ --> _object
-- Perform the following substitution:
Ref := Make_Identifier (Nloc, Chars (Obj_Id));
Set_Entity (Ref, Obj_Id);
Set_Etype (Ref, Rep_Typ);
-- Ref_Typ --> _object
-- When the pragma denotes a class-wide invariant, perform the
-- following substitution:
Ref := Make_Identifier (Nloc, Chars (Obj_Id));
Set_Entity (Ref, Obj_Id);
Set_Etype (Ref, Rep_Typ);
-- Rep_Typ --> Rep_Typ'Class (_object)
-- When the pragma denotes a class-wide invariant, perform
-- the following substitution:
-- Rep_Typ --> Rep_Typ'Class (_object)
if Class_Present (Prag) then
Ref :=
Make_Type_Conversion (Nloc,
Subtype_Mark =>
Make_Attribute_Reference (Nloc,
Prefix =>
New_Occurrence_Of (Rep_Typ, Nloc),
Attribute_Name => Name_Class),
Expression => Ref);
end if;
Rewrite (N, Ref);
Set_Comes_From_Source (N, True);
if Class_Present (Prag) then
Ref :=
Make_Type_Conversion (Nloc,
Subtype_Mark =>
Make_Attribute_Reference (Nloc,
Prefix =>
New_Occurrence_Of (Rep_Typ, Nloc),
Attribute_Name => Name_Class),
Expression => Ref);
end if;
Rewrite (N, Ref);
Set_Comes_From_Source (N, True);
end Replace_Type_Ref;
procedure Replace_Type_Refs is
......@@ -4787,11 +4780,12 @@ package body Exp_Ch7 is
Set_Corresponding_Body (Proc_Decl, Proc_Body_Id);
Set_Corresponding_Spec (Proc_Body, Proc_Id);
-- The body should not be inserted into the tree when the context is a
-- generic unit because it is not part of the template. Note that the
-- body must still be generated in order to resolve the invariants.
-- The body should not be inserted into the tree when the context is
-- ASIS, GNATprove or a generic unit because it is not part of the
-- template. Note that the body must still be generated in order to
-- resolve the invariants.
if Inside_A_Generic then
if ASIS_Mode or GNATprove_Mode or Inside_A_Generic then
null;
-- Otherwise the body is part of the freezing actions of the type
......@@ -4988,9 +4982,10 @@ package body Exp_Ch7 is
New_Occurrence_Of (Work_Typ, Loc)))));
-- The declaration should not be inserted into the tree when the context
-- is a generic unit because it is not part of the template.
-- is ASIS, GNATprove or a generic unit because it is not part of the
-- template.
if Inside_A_Generic then
if ASIS_Mode or GNATprove_Mode or Inside_A_Generic then
null;
-- Otherwise insert the declaration
......
......@@ -934,10 +934,9 @@ package body SPARK_Specific is
D2 := D1;
end if;
-- Some files do not correspond to Ada units, and as such present no
-- interest for SPARK cross references. Skip these files, as printing
-- their name may require printing the full name with spaces, which
-- is not handled in the code doing I/O of SPARK cross references.
-- Skip dependencies with no entity node, e.g. configuration files
-- with pragmas (.adc) or target description (.atp), since they
-- present no interest for SPARK cross references.
if Present (Cunit_Entity (Sdep_Table (D1))) then
Add_SPARK_File
......
......@@ -11308,9 +11308,10 @@ package body Sem_Ch6 is
Freeze_Entity (Defining_Identifier (Decl), N));
-- Ditto if the type has a dynamic predicate, because the
-- generated function will mention the actual subtype.
-- generated function will mention the actual subtype. The
-- predicate may come from an explicit aspect of be inherited.
elsif Has_Dynamic_Predicate_Aspect (T) then
elsif Has_Predicates (T) then
Insert_List_Before_And_Analyze (Decl,
Freeze_Entity (Defining_Identifier (Decl), N));
end if;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment