From: Ed Schonberg Date: Mon, 4 Jul 2016 10:03:34 +0000 (+0000) Subject: freeze.adb (Check_Inherited_Conditions): Perform two passes over the primitive operat... X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=002e3d16cbf86f160bc6467983ca515471c4156d;p=gcc.git freeze.adb (Check_Inherited_Conditions): Perform two passes over the primitive operations of the type... 2016-07-04 Ed Schonberg * freeze.adb (Check_Inherited_Conditions): Perform two passes over the primitive operations of the type: one over source overridings to build the primitives mapping, and one over inherited operations to check for the need to create wrappers, and to check legality of inherited condition in SPARK. * sem_prag.ads (Update_Primitive_Mapping): Make public, for use in freeze actions. * sem_prag.adb (Build_Pragma_Check_Equivalent): Refine error message in the case of an inherited condition in SPARK that includes a call to some other overriding primitive. From-SVN: r237960 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index bcd9e52fa34..6784eb24502 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,16 @@ +2016-07-04 Ed Schonberg + + * freeze.adb (Check_Inherited_Conditions): Perform two passes over + the primitive operations of the type: one over source overridings + to build the primitives mapping, and one over inherited operations + to check for the need to create wrappers, and to check legality + of inherited condition in SPARK. + * sem_prag.ads (Update_Primitive_Mapping): Make public, for use + in freeze actions. + * sem_prag.adb (Build_Pragma_Check_Equivalent): Refine error + message in the case of an inherited condition in SPARK that + includes a call to some other overriding primitive. + 2016-07-04 Hristian Kirtchev * exp_aggr.adb (Ctrl_Init_Expression): New routine. diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb index 31c77394949..b9d70c416c9 100644 --- a/gcc/ada/freeze.adb +++ b/gcc/ada/freeze.adb @@ -1403,24 +1403,39 @@ package body Freeze is while Present (Op_Node) loop Prim := Node (Op_Node); - -- In SPARK mode this is where we can collect the inherited - -- conditions, because we do not create the Check pragmas that - -- normally convey the modified classwide conditions on overriding - -- operations. - - if SPARK_Mode = On - and then Comes_From_Source (Prim) - and then Present (Overridden_Operation (Prim)) + -- Map the overridden primitive to the overriding one. This + -- takes care of all overridings and is done only once. + + if Present (Overridden_Operation (Prim)) + and then Comes_From_Source (Prim) then - Collect_Inherited_Class_Wide_Conditions (Prim); + Update_Primitives_Mapping (Overridden_Operation (Prim), Prim); + + -- In SPARK mode this is where we can collect the inherited + -- conditions, because we do not create the Check pragmas that + -- normally convey the the modified classwide conditions on + -- overriding operations. + + if SPARK_Mode = On then + Collect_Inherited_Class_Wide_Conditions (Prim); + end if; end if; - -- In normal mode, we examine inherited operations to check whether - -- they require a wrapper to handle inherited conditions that call - -- other primitives. - -- Wrapper construction TBD. + Next_Elmt (Op_Node); + end loop; + + -- In all cases, we examine inherited operations to check whether they + -- require a wrapper to handle inherited conditions that call other + -- primitives, so that LSP can be verified/enforced. + + -- Wrapper construction TBD. - if not Comes_From_Source (Prim) and then Present (Alias (Prim)) then + Op_Node := First_Elmt (Prim_Ops); + while Present (Op_Node) loop + Prim := Node (Op_Node); + if not Comes_From_Source (Prim) + and then Present (Alias (Prim)) + then Par_Prim := Alias (Prim); A_Pre := Find_Aspect (Par_Prim, Aspect_Pre); diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index a2392e68ee3..90d00fca9a1 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -322,13 +322,6 @@ package body Sem_Prag is -- pragma. Entity name for unit and its parents is taken from item in -- previous with_clause that mentions the unit. - procedure Update_Primitives_Mapping - (Inher_Id : Entity_Id; - Subp_Id : Entity_Id); - -- Map primitive operations of the parent type to the corresponding - -- operations of the descendant. Note that the descendant type may - -- not be frozen yet, so we cannot use the dispatch table directly. - Dummy : Integer := 0; pragma Volatile (Dummy); -- Dummy volatile integer used in bodies of ip/rv to prevent optimization @@ -26380,13 +26373,25 @@ package body Sem_Prag is ("cannot call abstract subprogram in inherited condition " & "for&#", N, Current_Scope); + -- In SPARK mode, reject an inherited condition for an + -- inherited operation if it contains a call to an overriding + -- operation, because this implies that the pre/postcondition + -- of the inherited operation have changed silently. + elsif SPARK_Mode = On and then Warn_On_Suspicious_Contract and then Present (Alias (Subp)) + and then Present (New_E) + and then Comes_From_Source (New_E) then + Error_Msg_N + ("cannot modify inherited condition (SPARK RM 6.1.1(1))", + Parent (Subp)); + Error_Msg_Sloc := Sloc (New_E); + Error_Msg_Node_2 := Subp; Error_Msg_NE - ("?inherited condition is modified, build a wrapper " - & "for&", Parent (Subp), Subp); + ("\overriding of&# forces overriding of&", + Parent (Subp), New_E); end if; end if; diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads index 064534f6ee3..8613bba1831 100644 --- a/gcc/ada/sem_prag.ads +++ b/gcc/ada/sem_prag.ads @@ -528,4 +528,15 @@ package Sem_Prag is -- -- Empty if there is no such argument + procedure Update_Primitives_Mapping + (Inher_Id : Entity_Id; + Subp_Id : Entity_Id); + + -- map primitive operations of the parent type to the corresponding + -- operations of the descendant. note that the descendant type may + -- not be frozen yet, so we cannot use the dispatch table directly. + -- This is called when elaborating a contract for a subprogram, and + -- when freezing a type extension to verify legality rules on inherited + -- conditions. + end Sem_Prag;