diff options
Diffstat (limited to 'gcc/ada/contracts.adb')
| -rw-r--r-- | gcc/ada/contracts.adb | 125 |
1 files changed, 25 insertions, 100 deletions
diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb index 8b94a67..70e9487 100644 --- a/gcc/ada/contracts.adb +++ b/gcc/ada/contracts.adb @@ -110,8 +110,8 @@ package body Contracts is -- Expand the contracts of a subprogram body and its correspoding spec (if -- any). This routine processes all [refined] pre- and postconditions as -- well as Always_Terminates, Contract_Cases, Exceptional_Cases, - -- Subprogram_Variant, invariants and predicates. Body_Id denotes the - -- entity of the subprogram body. + -- Program_Exit, Subprogram_Variant, invariants and predicates. Body_Id + -- denotes the entity of the subprogram body. procedure Preanalyze_Condition (Subp : Entity_Id; @@ -235,6 +235,7 @@ package body Contracts is -- Interrupt_Handler -- Postcondition -- Precondition + -- Program_Exit -- Side_Effects -- Subprogram_Variant -- Test_Case @@ -267,6 +268,7 @@ package body Contracts is | Name_Contract_Cases | Name_Exceptional_Cases | Name_Exit_Cases + | Name_Program_Exit | Name_Subprogram_Variant | Name_Test_Case then @@ -647,9 +649,9 @@ package body Contracts is end if; -- Deal with preconditions, [refined] postconditions, Always_Terminates, - -- Contract_Cases, Exceptional_Cases, Subprogram_Variant, invariants and - -- predicates associated with body and its spec. Do not expand the - -- contract of subprogram body stubs. + -- Contract_Cases, Exceptional_Cases, Program_Exit, Subprogram_Variant, + -- invariants and predicates associated with body and its spec. Do not + -- expand the contract of subprogram body stubs. if Nkind (Body_Decl) = N_Subprogram_Body then Expand_Subprogram_Contract (Body_Id); @@ -797,6 +799,9 @@ package body Contracts is elsif Prag_Nam = Name_Exceptional_Cases then Analyze_Exceptional_Cases_In_Decl_Part (Prag); + elsif Prag_Nam = Name_Program_Exit then + Analyze_Program_Exit_In_Decl_Part (Prag); + elsif Prag_Nam = Name_Subprogram_Variant then Analyze_Subprogram_Variant_In_Decl_Part (Prag); @@ -1413,6 +1418,7 @@ package body Contracts is -- Global -- Postcondition -- Precondition + -- Program_Exit -- Subprogram_Variant -- Test_Case @@ -2422,6 +2428,7 @@ package body Contracts is -- verify the return value. Result := Make_Defining_Identifier (Loc, Name_uResult); + Mutate_Ekind (Result, E_Constant); Set_Etype (Result, Typ); -- Add an invariant check when the return type has invariants and @@ -2761,6 +2768,9 @@ package body Contracts is elsif Pragma_Name (Prag) = Name_Exit_Cases then Expand_Pragma_Exit_Cases (Prag); + elsif Pragma_Name (Prag) = Name_Program_Exit then + Expand_Pragma_Program_Exit (Prag); + elsif Pragma_Name (Prag) = Name_Subprogram_Variant then Expand_Pragma_Subprogram_Variant (Prag => Prag, @@ -4389,10 +4399,10 @@ package body Contracts is Seen : Subprogram_List (Subps'Range) := (others => Empty); function Inherit_Condition - (Par_Subp : Entity_Id; - Subp : Entity_Id) return Node_Id; - -- Inherit the class-wide condition from Par_Subp to Subp and adjust - -- all the references to formals in the inherited condition. + (Par_Subp : Entity_Id) return Node_Id; + -- Inherit the class-wide condition from Par_Subp. Simply makes + -- a copy of the condition in preparation for later mapping of + -- referenced formals and functions by Build_Class_Wide_Expression. procedure Merge_Conditions (From : Node_Id; Into : Node_Id); -- Merge two class-wide preconditions or postconditions (the former @@ -4407,92 +4417,11 @@ package body Contracts is ----------------------- function Inherit_Condition - (Par_Subp : Entity_Id; - Subp : Entity_Id) return Node_Id - is - function Check_Condition (Expr : Node_Id) return Boolean; - -- Used in assertion to check that Expr has no reference to the - -- formals of Par_Subp. - - --------------------- - -- Check_Condition -- - --------------------- - - function Check_Condition (Expr : Node_Id) return Boolean is - Par_Formal_Id : Entity_Id; - - function Check_Entity (N : Node_Id) return Traverse_Result; - -- Check occurrence of Par_Formal_Id - - ------------------ - -- Check_Entity -- - ------------------ - - function Check_Entity (N : Node_Id) return Traverse_Result is - begin - if Nkind (N) = N_Identifier - and then Present (Entity (N)) - and then Entity (N) = Par_Formal_Id - then - return Abandon; - end if; - - return OK; - end Check_Entity; - - function Check_Expression is new Traverse_Func (Check_Entity); - - -- Start of processing for Check_Condition - - begin - Par_Formal_Id := First_Formal (Par_Subp); - - while Present (Par_Formal_Id) loop - if Check_Expression (Expr) = Abandon then - return False; - end if; - - Next_Formal (Par_Formal_Id); - end loop; - - return True; - end Check_Condition; - - -- Local variables - - Assoc_List : constant Elist_Id := New_Elmt_List; - Par_Formal_Id : Entity_Id := First_Formal (Par_Subp); - Subp_Formal_Id : Entity_Id := First_Formal (Subp); - New_Condition : Node_Id; - + (Par_Subp : Entity_Id) return Node_Id is begin - while Present (Par_Formal_Id) loop - Append_Elmt (Par_Formal_Id, Assoc_List); - Append_Elmt (Subp_Formal_Id, Assoc_List); - - Next_Formal (Par_Formal_Id); - Next_Formal (Subp_Formal_Id); - end loop; - - -- Check that Parent field of all the nodes have their correct - -- decoration; required because otherwise mapped nodes with - -- wrong Parent field are left unmodified in the copied tree - -- and cause reporting wrong errors at later stages. - - pragma Assert - (Check_Parents (Class_Condition (Kind, Par_Subp), Assoc_List)); - - New_Condition := + return New_Copy_Tree - (Source => Class_Condition (Kind, Par_Subp), - Map => Assoc_List); - - -- Ensure that the inherited condition has no reference to the - -- formals of the parent subprogram. - - pragma Assert (Check_Condition (New_Condition)); - - return New_Condition; + (Source => Class_Condition (Kind, Par_Subp)); end Inherit_Condition; ---------------------- @@ -4606,9 +4535,7 @@ package body Contracts is Par_Prim := Subp_Id; Par_Iface_Prims := Covered_Interface_Primitives (Par_Prim); - Cond := Inherit_Condition - (Subp => Spec_Id, - Par_Subp => Subp_Id); + Cond := Inherit_Condition (Par_Subp => Subp_Id); if Present (Class_Cond) then Merge_Conditions (Cond, Class_Cond); @@ -4652,9 +4579,7 @@ package body Contracts is then Seen (Index) := Subp_Id; - Cond := Inherit_Condition - (Subp => Spec_Id, - Par_Subp => Subp_Id); + Cond := Inherit_Condition (Par_Subp => Subp_Id); Check_Class_Condition (Cond => Cond, @@ -4909,7 +4834,7 @@ package body Contracts is Install_Formals (Subp); Inside_Class_Condition_Preanalysis := True; - Preanalyze_Spec_Expression (Expr, Standard_Boolean); + Preanalyze_And_Resolve_Spec_Expression (Expr, Standard_Boolean); Inside_Class_Condition_Preanalysis := False; End_Scope; |