In some cases of generic instantiations, or code configuration, some code
may be deactivated and contain static divisions by zero. Instead of
issuing an error in SPARK code, generate a suitable check.
Tested on x86_64-pc-linux-gnu, committed on trunk
2016-04-18 Yannick Moy <m...@adacore.com>
* sem_eval.adb (Eval_Arithmetic_Op): Do not issue error on static
division by zero, instead possibly issue a warning.
* sem_res.adb (Resolve_Arithmetic_Op): Do not issue error on
static division by zero, instead add check flag on original
expression.
* sem_util.adb, sem_util.ads (Compile_Time_Constraint_Error):
Only issue error when both SPARK_Mode is On and Warn is False.
Index: sem_util.adb
===================================================================
--- sem_util.adb (revision 235122)
+++ sem_util.adb (working copy)
@@ -4574,9 +4574,16 @@
begin
-- If this is a warning, convert it into an error if we are in code
- -- subject to SPARK_Mode being set ON.
+ -- subject to SPARK_Mode being set On, unless Warn is True to force a
+ -- warning. The rationale is that a compile-time constraint error should
+ -- lead to an error instead of a warning when SPARK_Mode is On, but in
+ -- a few cases we prefer to issue a warning and generate both a suitable
+ -- run-time error in GNAT and a suitable check message in GNATprove.
+ -- Those cases are those that likely correspond to deactivated SPARK
+ -- code, so that this kind of code can be compiled and analyzed instead
+ -- of being rejected.
- Error_Msg_Warn := SPARK_Mode /= On;
+ Error_Msg_Warn := Warn or SPARK_Mode /= On;
-- A static constraint error in an instance body is not a fatal error.
-- we choose to inhibit the message altogether, because there is no
@@ -4648,8 +4655,6 @@
-- evaluated.
if not Is_Statically_Unevaluated (N) then
- Error_Msg_Warn := SPARK_Mode /= On;
-
if Present (Ent) then
Error_Msg_NEL (Msgc (1 .. Msgl), N, Ent, Eloc);
else
Index: sem_util.ads
===================================================================
--- sem_util.ads (revision 235122)
+++ sem_util.ads (working copy)
@@ -135,7 +135,9 @@
-- is present, this is used instead. Warn is normally False. If it is
-- True then the message is treated as a warning even though it does
-- not end with a ? (this is used when the caller wants to parameterize
- -- whether an error or warning is given).
+ -- whether an error or warning is given), or when the message should be
+ -- treated as a warning even when SPARK_Mode is On (which otherwise would
+ -- force an error).
function Async_Readers_Enabled (Id : Entity_Id) return Boolean;
-- Given the entity of an abstract state or a variable, determine whether
Index: sem_res.adb
===================================================================
--- sem_res.adb (revision 235116)
+++ sem_res.adb (working copy)
@@ -5440,7 +5440,9 @@
and then Expr_Value_R (Rop) = Ureal_0))
then
-- Specialize the warning message according to the operation.
- -- The following warnings are for the case
+ -- When SPARK_Mode is On, force a warning instead of an error
+ -- in that case, as this likely corresponds to deactivated
+ -- code. The following warnings are for the case
case Nkind (N) is
when N_Op_Divide =>
@@ -5459,23 +5461,26 @@
("float division by zero, may generate "
& "'+'/'- infinity??", Right_Opnd (N));
- -- For all other cases, we get a Constraint_Error
+ -- For all other cases, we get a Constraint_Error
else
Apply_Compile_Time_Constraint_Error
(N, "division by zero??", CE_Divide_By_Zero,
- Loc => Sloc (Right_Opnd (N)));
+ Loc => Sloc (Right_Opnd (N)),
+ Warn => SPARK_Mode = On);
end if;
when N_Op_Rem =>
Apply_Compile_Time_Constraint_Error
(N, "rem with zero divisor??", CE_Divide_By_Zero,
- Loc => Sloc (Right_Opnd (N)));
+ Loc => Sloc (Right_Opnd (N)),
+ Warn => SPARK_Mode = On);
when N_Op_Mod =>
Apply_Compile_Time_Constraint_Error
(N, "mod with zero divisor??", CE_Divide_By_Zero,
- Loc => Sloc (Right_Opnd (N)));
+ Loc => Sloc (Right_Opnd (N)),
+ Warn => SPARK_Mode = On);
-- Division by zero can only happen with division, rem,
-- and mod operations.
@@ -5484,6 +5489,13 @@
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
Index: sem_eval.adb
===================================================================
--- sem_eval.adb (revision 235124)
+++ sem_eval.adb (working copy)
@@ -1885,9 +1885,14 @@
-- division, rem and mod if the right operand is zero.
if Right_Int = 0 then
+
+ -- When SPARK_Mode is On, force a warning instead of
+ -- an error in that case, as this likely corresponds
+ -- to deactivated code.
+
Apply_Compile_Time_Constraint_Error
(N, "division by zero", CE_Divide_By_Zero,
- Warn => not Stat);
+ Warn => not Stat or SPARK_Mode = On);
Set_Raises_Constraint_Error (N);
return;
@@ -1903,10 +1908,16 @@
-- division, rem and mod if the right operand is zero.
if Right_Int = 0 then
+
+ -- When SPARK_Mode is On, force a warning instead of
+ -- an error in that case, as this likely corresponds
+ -- to deactivated code.
+
Apply_Compile_Time_Constraint_Error
(N, "mod with zero divisor", CE_Divide_By_Zero,
- Warn => not Stat);
+ Warn => not Stat or SPARK_Mode = On);
return;
+
else
Result := Left_Int mod Right_Int;
end if;
@@ -1917,9 +1928,14 @@
-- division, rem and mod if the right operand is zero.
if Right_Int = 0 then
+
+ -- When SPARK_Mode is On, force a warning instead of
+ -- an error in that case, as this likely corresponds
+ -- to deactivated code.
+
Apply_Compile_Time_Constraint_Error
(N, "rem with zero divisor", CE_Divide_By_Zero,
- Warn => not Stat);
+ Warn => not Stat or SPARK_Mode = On);
return;
else
