aboutsummaryrefslogtreecommitdiff
path: root/gcc
diff options
context:
space:
mode:
Diffstat (limited to 'gcc')
-rw-r--r--gcc/ada/ChangeLog19
-rw-r--r--gcc/ada/exp_ch7.adb61
-rw-r--r--gcc/ada/lib-xref-spark_specific.adb7
-rw-r--r--gcc/ada/sem_ch6.adb5
4 files changed, 53 insertions, 39 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 5703832..a8b4fcb 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,22 @@
+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
diff --git a/gcc/ada/exp_ch7.adb b/gcc/ada/exp_ch7.adb
index b962fcc..3152237 100644
--- a/gcc/ada/exp_ch7.adb
+++ b/gcc/ada/exp_ch7.adb
@@ -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
diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb
index 062e50c..8bc6603 100644
--- a/gcc/ada/lib-xref-spark_specific.adb
+++ b/gcc/ada/lib-xref-spark_specific.adb
@@ -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
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index ce5f556..0a60d04 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -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;