* [Ada] Allow confirming volatile properties on No_Caching variables
@ 2022-06-01 8:45 Pierre-Marie de Rodat
0 siblings, 0 replies; only message in thread
From: Pierre-Marie de Rodat @ 2022-06-01 8:45 UTC (permalink / raw)
To: gcc-patches; +Cc: Yannick Moy
[-- Attachment #1: Type: text/plain, Size: 432 bytes --]
Volatile variables marked with the No_Caching aspect can now have
confirming aspects for other volatile properties, with a value of
False.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* contracts.adb (Check_Type_Or_Object_External_Properties): Check
the validity of combinations only when No_Caching is not used.
* sem_prag.adb (Analyze_External_Property_In_Decl_Part): Check
valid combinations with No_Caching.
[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 3101 bytes --]
diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb
--- a/gcc/ada/contracts.adb
+++ b/gcc/ada/contracts.adb
@@ -892,9 +892,15 @@ package body Contracts is
end;
end if;
- -- Verify the mutual interaction of the various external properties
-
- if Seen then
+ -- 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.
+
+ if Seen
+ and then (Ekind (Type_Or_Obj_Id) /= E_Variable
+ or else 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;
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -2139,11 +2139,24 @@ package body Sem_Prag is
Expr : Node_Id;
begin
- -- Do not analyze the pragma multiple times, but set the output
- -- parameter to the argument specified by the pragma.
+ -- Ensure that the Boolean expression (if present) is static. A missing
+ -- argument defaults the value to True (SPARK RM 7.1.2(5)).
+
+ Expr_Val := True;
+
+ if Present (Arg1) then
+ Expr := Get_Pragma_Arg (Arg1);
+
+ if Is_OK_Static_Expression (Expr) then
+ Expr_Val := Is_True (Expr_Value (Expr));
+ end if;
+ end if;
+
+ -- The output parameter was set to the argument specified by the pragma.
+ -- Do not analyze the pragma multiple times.
if Is_Analyzed_Pragma (N) then
- goto Leave;
+ return;
end if;
Error_Msg_Name_1 := Pragma_Name (N);
@@ -2163,9 +2176,11 @@ package body Sem_Prag is
if Ekind (Obj_Id) = E_Variable
and then No_Caching_Enabled (Obj_Id)
then
- SPARK_Msg_N
- ("illegal combination of external property % and property "
- & """No_Caching"" (SPARK RM 7.1.2(6))", N);
+ if Expr_Val then -- Confirming value of False is allowed
+ SPARK_Msg_N
+ ("illegal combination of external property % and property "
+ & """No_Caching"" (SPARK RM 7.1.2(6))", N);
+ end if;
else
SPARK_Msg_N
("external property % must apply to a volatile type or object",
@@ -2185,22 +2200,6 @@ package body Sem_Prag is
end if;
Set_Is_Analyzed_Pragma (N);
-
- <<Leave>>
-
- -- Ensure that the Boolean expression (if present) is static. A missing
- -- argument defaults the value to True (SPARK RM 7.1.2(5)).
-
- Expr_Val := True;
-
- if Present (Arg1) then
- Expr := Get_Pragma_Arg (Arg1);
-
- if Is_OK_Static_Expression (Expr) then
- Expr_Val := Is_True (Expr_Value (Expr));
- end if;
- end if;
-
end Analyze_External_Property_In_Decl_Part;
---------------------------------
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2022-06-01 8:45 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-06-01 8:45 [Ada] Allow confirming volatile properties on No_Caching variables Pierre-Marie de Rodat
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).