diff options
| author | Yannick Moy <moy@adacore.com> | 2021-05-18 12:35:08 +0200 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2021-07-07 16:23:14 +0000 |
| commit | a7f66404a62179ed8d759e8d454635f775cef016 (patch) | |
| tree | bfe1382073a1efaa435101079664e290cfa2efed | |
| parent | f78c17d267271cf339e4a0efc3bfe7eb0c00b502 (diff) | |
| download | gcc-a7f66404a62179ed8d759e8d454635f775cef016.zip gcc-a7f66404a62179ed8d759e8d454635f775cef016.tar.gz gcc-a7f66404a62179ed8d759e8d454635f775cef016.tar.bz2 | |
[Ada] Simplify handling of sure errors in GNATprove mode
gcc/ada/
* checks.adb (Apply_Scalar_Range_Check): Remove special case for
GNATprove mode.
* sem_res.adb (Resolve_Arithmetic_Op): Same.
* sem_util.adb (Apply_Compile_Time_Constraint_Error): Same.
| -rw-r--r-- | gcc/ada/checks.adb | 7 | ||||
| -rw-r--r-- | gcc/ada/sem_res.adb | 7 | ||||
| -rw-r--r-- | gcc/ada/sem_util.adb | 11 |
3 files changed, 0 insertions, 25 deletions
diff --git a/gcc/ada/checks.adb b/gcc/ada/checks.adb index 76fd9b0..61ce9c2 100644 --- a/gcc/ada/checks.adb +++ b/gcc/ada/checks.adb @@ -3323,13 +3323,6 @@ package body Checks is Bad_Value (Warn => SPARK_Mode = On); - -- In GNATprove mode, we enable the range check so that - -- GNATprove will issue a message if it cannot be proved. - - if GNATprove_Mode then - Enable_Range_Check (Expr); - end if; - return; end if; diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index 54d476e..5791d3d 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -6151,13 +6151,6 @@ package body Sem_Res is raise Program_Error; end case; - -- In GNATprove mode, we enable the division check so that - -- GNATprove will issue a message if it cannot be proved. - - if GNATprove_Mode then - Activate_Division_Check (N); - end if; - -- Otherwise just set the flag to check at run time else diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 9d54309..799f720 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -1533,17 +1533,6 @@ package body Sem_Util is Discard_Node (Compile_Time_Constraint_Error (N, Msg, Ent, Loc, Warn => Warn)); - -- In GNATprove mode, do not replace the node with an exception raised. - -- In such a case, either the call to Compile_Time_Constraint_Error - -- issues an error which stops analysis, or it issues a warning in - -- a few cases where a suitable check flag is set for GNATprove to - -- generate a check message. - - if GNATprove_Mode then - Set_Raises_Constraint_Error (N); - return; - end if; - -- Now we replace the node by an N_Raise_Constraint_Error node -- This does not need reanalyzing, so set it as analyzed now. |