diff options
| -rw-r--r-- | gcc/ada/contracts.adb | 32 | ||||
| -rw-r--r-- | gcc/ada/sem_prag.adb | 49 | ||||
| -rw-r--r-- | gcc/ada/sem_util.adb | 37 | ||||
| -rw-r--r-- | gcc/ada/sem_util.ads | 11 |
4 files changed, 84 insertions, 45 deletions
diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb index 6f474eb..59121ca 100644 --- a/gcc/ada/contracts.adb +++ b/gcc/ada/contracts.adb @@ -316,6 +316,7 @@ package body Contracts is | Name_Async_Writers | Name_Effective_Reads | Name_Effective_Writes + | Name_No_Caching or else (Ekind (Id) = E_Task_Type and Prag_Nam in Name_Part_Of | Name_Depends @@ -859,6 +860,7 @@ package body Contracts is AW_Val : Boolean := False; ER_Val : Boolean := False; EW_Val : Boolean := False; + NC_Val : Boolean; Seen : Boolean := False; Prag : Node_Id; Obj_Typ : Entity_Id; @@ -956,18 +958,25 @@ package body Contracts is end if; -- Verify the mutual interaction of the various external properties. - -- For variables for which No_Caching is enabled, it has been checked - -- already that only False values for other external properties are - -- allowed. + -- For types and variables for which No_Caching is enabled, it has been + -- checked already that only False values for other external properties + -- are allowed. if Seen - and then (Ekind (Type_Or_Obj_Id) /= E_Variable - or else not No_Caching_Enabled (Type_Or_Obj_Id)) + and then not No_Caching_Enabled (Type_Or_Obj_Id) then Check_External_Properties (Type_Or_Obj_Id, AR_Val, AW_Val, ER_Val, EW_Val); end if; + -- Analyze the non-external volatility property No_Caching + + Prag := Get_Pragma (Type_Or_Obj_Id, Pragma_No_Caching); + + if Present (Prag) then + Analyze_External_Property_In_Decl_Part (Prag, NC_Val); + end if; + -- The following checks are relevant only when SPARK_Mode is on, as -- they are not standard Ada legality rules. Internally generated -- temporaries are ignored, as well as return objects. @@ -1047,10 +1056,10 @@ package body Contracts is if Is_Type_Id and then not Is_Effectively_Volatile (Type_Or_Obj_Id) - and then Has_Volatile_Component (Type_Or_Obj_Id) + and then Has_Effectively_Volatile_Component (Type_Or_Obj_Id) then Error_Msg_N - ("non-volatile type & cannot have volatile" + ("non-volatile type & cannot have effectively volatile" & " components", Type_Or_Obj_Id); end if; @@ -1076,7 +1085,6 @@ package body Contracts is Saved_SMP : constant Node_Id := SPARK_Mode_Pragma; -- Save the SPARK_Mode-related data to restore on exit - NC_Val : Boolean; Items : Node_Id; Prag : Node_Id; Ref_Elmt : Elmt_Id; @@ -1118,14 +1126,6 @@ package body Contracts is Check_Type_Or_Object_External_Properties (Type_Or_Obj_Id => Obj_Id); - -- Analyze the non-external volatility property No_Caching - - Prag := Get_Pragma (Obj_Id, Pragma_No_Caching); - - if Present (Prag) then - Analyze_External_Property_In_Decl_Part (Prag, NC_Val); - end if; - -- Constant-related checks if Ekind (Obj_Id) = E_Constant then diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 27bd879..f3c23ca 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -2116,9 +2116,16 @@ package body Sem_Prag is First (Pragma_Argument_Associations (N)); Obj_Decl : constant Node_Id := Find_Related_Context (N); Obj_Id : constant Entity_Id := Defining_Entity (Obj_Decl); + Obj_Typ : Entity_Id; Expr : Node_Id; begin + if Is_Type (Obj_Id) then + Obj_Typ := Obj_Id; + else + Obj_Typ := Etype (Obj_Id); + end if; + -- Ensure that the Boolean expression (if present) is static. A missing -- argument defaults the value to True (SPARK RM 7.1.2(5)). @@ -2153,9 +2160,7 @@ package body Sem_Prag is if Prag_Id /= Pragma_No_Caching and then not Is_Effectively_Volatile (Obj_Id) then - if Ekind (Obj_Id) = E_Variable - and then No_Caching_Enabled (Obj_Id) - then + if No_Caching_Enabled (Obj_Id) then if Expr_Val then -- Confirming value of False is allowed SPARK_Msg_N ("illegal combination of external property % and property " @@ -2167,15 +2172,16 @@ package body Sem_Prag is N); end if; - -- Pragma No_Caching should only apply to volatile variables of + -- Pragma No_Caching should only apply to volatile types or variables of -- a non-effectively volatile type (SPARK RM 7.1.2). elsif Prag_Id = Pragma_No_Caching then - if Is_Effectively_Volatile (Etype (Obj_Id)) then - SPARK_Msg_N ("property % must not apply to an object of " + if Is_Effectively_Volatile (Obj_Typ) then + SPARK_Msg_N ("property % must not apply to a type or object of " & "an effectively volatile type", N); elsif not Is_Volatile (Obj_Id) then - SPARK_Msg_N ("property % must apply to a volatile object", N); + SPARK_Msg_N + ("property % must apply to a volatile type or object", N); end if; end if; @@ -13484,22 +13490,19 @@ package body Sem_Prag is Obj_Or_Type_Decl := Find_Related_Context (N, Do_Checks => True); -- Pragma must apply to a object declaration or to a type - -- declaration (only the former in the No_Caching case). - -- Original_Node is necessary to account for untagged derived - -- types that are rewritten as subtypes of their - -- respective root types. - - if Nkind (Obj_Or_Type_Decl) /= N_Object_Declaration then - if Prag_Id = Pragma_No_Caching - or else Nkind (Original_Node (Obj_Or_Type_Decl)) not in - N_Full_Type_Declaration | - N_Private_Type_Declaration | - N_Formal_Type_Declaration | - N_Task_Type_Declaration | - N_Protected_Type_Declaration - then - Pragma_Misplaced; - end if; + -- declaration. Original_Node is necessary to account for + -- untagged derived types that are rewritten as subtypes of + -- their respective root types. + + if Nkind (Obj_Or_Type_Decl) /= N_Object_Declaration + and then Nkind (Original_Node (Obj_Or_Type_Decl)) not in + N_Full_Type_Declaration | + N_Private_Type_Declaration | + N_Formal_Type_Declaration | + N_Task_Type_Declaration | + N_Protected_Type_Declaration + then + Pragma_Misplaced; end if; Obj_Or_Type_Id := Defining_Entity (Obj_Or_Type_Decl); diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 1fef847..a1cebb0 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -13530,6 +13530,36 @@ package body Sem_Util is return Has_Undef_Ref; end Has_Undefined_Reference; + ---------------------------------------- + -- Has_Effectively_Volatile_Component -- + ---------------------------------------- + + function Has_Effectively_Volatile_Component + (Typ : Entity_Id) return Boolean + is + Comp : Entity_Id; + + begin + if Has_Volatile_Components (Typ) then + return True; + + elsif Is_Array_Type (Typ) then + return Is_Effectively_Volatile (Component_Type (Typ)); + + elsif Is_Record_Type (Typ) then + Comp := First_Component (Typ); + while Present (Comp) loop + if Is_Effectively_Volatile (Etype (Comp)) then + return True; + end if; + + Next_Component (Comp); + end loop; + end if; + + return False; + end Has_Effectively_Volatile_Component; + ---------------------------- -- Has_Volatile_Component -- ---------------------------- @@ -16663,9 +16693,11 @@ package body Sem_Util is if Is_Type (Id) then -- An arbitrary type is effectively volatile when it is subject to - -- pragma Atomic or Volatile. + -- pragma Atomic or Volatile, unless No_Caching is enabled. - if Is_Volatile (Id) then + if Is_Volatile (Id) + and then not No_Caching_Enabled (Id) + then return True; -- An array type is effectively volatile when it is subject to pragma @@ -24579,7 +24611,6 @@ package body Sem_Util is ------------------------ function No_Caching_Enabled (Id : Entity_Id) return Boolean is - pragma Assert (Ekind (Id) = E_Variable); Prag : constant Node_Id := Get_Pragma (Id, Pragma_No_Caching); Arg1 : Node_Id; diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 34aaa9a..b647e68 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -1564,6 +1564,11 @@ package Sem_Util is -- Given arbitrary expression Expr, determine whether it contains at -- least one name whose entity is Any_Id. + function Has_Effectively_Volatile_Component + (Typ : Entity_Id) return Boolean; + -- Given arbitrary type Typ, determine whether it contains at least one + -- effectively volatile component. + function Has_Volatile_Component (Typ : Entity_Id) return Boolean; -- Given arbitrary type Typ, determine whether it contains at least one -- volatile component. @@ -2758,9 +2763,9 @@ package Sem_Util is -- inline this procedural form, but not the functional form above. function No_Caching_Enabled (Id : Entity_Id) return Boolean; - -- Given the entity of a variable, determine whether Id is subject to - -- volatility property No_Caching and if it is, the related expression - -- evaluates to True. + -- Given any entity Id, determine whether Id is subject to volatility + -- property No_Caching and if it is, the related expression evaluates + -- to True. function No_Heap_Finalization (Typ : Entity_Id) return Boolean; -- Determine whether type Typ is subject to pragma No_Heap_Finalization |