diff options
| author | Yannick Moy <moy@adacore.com> | 2023-05-10 16:10:54 +0200 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2023-06-20 09:30:50 +0200 |
| commit | f1c15fe3f054d453f94e1412ec5bcb2c1e7205e8 (patch) | |
| tree | 2b234f37f08ffc7a437963f0792a648e5f228eb1 /gcc/ada/contracts.adb | |
| parent | b367a66cfb620b88338111eebd549cc2fad1c16b (diff) | |
| download | gcc-f1c15fe3f054d453f94e1412ec5bcb2c1e7205e8.zip gcc-f1c15fe3f054d453f94e1412ec5bcb2c1e7205e8.tar.gz gcc-f1c15fe3f054d453f94e1412ec5bcb2c1e7205e8.tar.bz2 | |
ada: Add the ability to add error codes to error messages
Add a new character sequence [] for error codes in error messages
handled by Error_Msg procedures, to use for SPARK-related errors.
Display of additional information on the error or warning based on
the error code is delegated to GNATprove.
gcc/ada/
* err_vars.ads (Error_Msg_Code): New variable for error codes.
* errout.adb (Error_Msg_Internal): Display continuation message
when an error code was present.
(Set_Msg_Text): Handle character sequence [] for error codes.
* errout.ads: Document new insertion sequence [].
(Error_Msg_Code): New renaming.
* erroutc.adb (Prescan_Message): Detect presence of error code.
(Set_Msg_Insertion_Code): Handle new insertion sequence [].
* erroutc.ads (Has_Error_Code): New variable for prescan.
(Set_Msg_Insertion_Code): Handle new insertion sequence [].
* contracts.adb (Check_Type_Or_Object_External_Properties):
Replace reference to SPARK RM section by an error code.
* sem_elab.adb (SPARK_Processor): Same.
* sem_prag.adb (Check_Missing_Part_Of): Same.
* sem_res.adb (Resolve_Actuals, Resolve_Entity_Name): Same.
Diffstat (limited to 'gcc/ada/contracts.adb')
| -rw-r--r-- | gcc/ada/contracts.adb | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb index 26bc4b3..77578da 100644 --- a/gcc/ada/contracts.adb +++ b/gcc/ada/contracts.adb @@ -1040,11 +1040,12 @@ package body Contracts is -- appear at the library level (SPARK RM 7.1.3(3), C.6(6)). if not Is_Library_Level_Entity (Type_Or_Obj_Id) then + Error_Msg_Code := GEC_Volatile_At_Library_Level; Error_Msg_N ("effectively volatile " & Decl_Kind - & " & must be declared at library level " - & "(SPARK RM 7.1.3(3))", Type_Or_Obj_Id); + & " & must be declared at library level '[[]']", + Type_Or_Obj_Id); -- An object of a discriminated type cannot be effectively -- volatile except for protected objects (SPARK RM 7.1.3(5)). |