diff options
Diffstat (limited to 'gcc')
-rw-r--r-- | gcc/ada/ChangeLog | 19 | ||||
-rw-r--r-- | gcc/ada/exp_ch7.adb | 61 | ||||
-rw-r--r-- | gcc/ada/lib-xref-spark_specific.adb | 7 | ||||
-rw-r--r-- | gcc/ada/sem_ch6.adb | 5 |
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; |