+2016-04-18 Arnaud Charlet <charlet@adacore.com>
+
+ * osint-c.ads, osint-c.adb (Delete_C_File, Delete_H_File): New.
+ * gnat1drv.adb (Gnat1drv): Delete old C files before regenerating them.
+ * debug.adb: Reserve -gnatd.4 to force generation of C files.
+
+2016-04-18 Yannick Moy <moy@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.
+
+2016-04-18 Yannick Moy <moy@adacore.com>
+
+ * checks.adb (Apply_Scalar_Range_Check): Force
+ warning instead of error when SPARK_Mode is On, on index out of
+ bounds, and set check flag for GNATprove.
+
2016-04-18 Hristian Kirtchev <kirtchev@adacore.com>
* sem_prag.adb (Check_In_Out_States.Check_Constituent_Usage):
-- Set to True if Expr should be regarded as a real value even though
-- the type of Expr might be discrete.
- procedure Bad_Value;
- -- Procedure called if value is determined to be out of range
+ procedure Bad_Value (Warn : Boolean := False);
+ -- Procedure called if value is determined to be out of range. Warn is
+ -- True to force a warning instead of an error, even when SPARK_Mode is
+ -- On.
---------------
-- Bad_Value --
---------------
- procedure Bad_Value is
+ procedure Bad_Value (Warn : Boolean := False) is
begin
Apply_Compile_Time_Constraint_Error
(Expr, "value not in range of}??", CE_Range_Check_Failed,
- Ent => Target_Typ,
- Typ => Target_Typ);
+ Ent => Target_Typ,
+ Typ => Target_Typ,
+ Warn => Warn);
end Bad_Value;
-- Start of processing for Apply_Scalar_Range_Check
if Lov > Hiv then
- -- In GNATprove mode, do not issue a message in that case
- -- (which would be an error stopping analysis), as this
- -- likely corresponds to deactivated code based on a
- -- given configuration (say, dead code inside a loop over
- -- the empty range). Instead, we enable the range check
- -- so that GNATprove will issue a message if it cannot be
- -- proved.
+ -- When SPARK_Mode is On, force a warning instead of
+ -- an error in that case, as this likely corresponds
+ -- to deactivated code.
+
+ 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);
- else
- Bad_Value;
end if;
return;
-- d.1 Enable unnesting of nested procedures
-- d.2 Allow statements in declarative part
-- d.3 Output debugging information from Exp_Unst
- -- d.4
+ -- d.4 Do not delete generated C file in case of errors
-- d.5 Do not generate imported subprogram definitions in C code
-- d.6
-- d.7
-- d.3 Output debugging information from Exp_Unst, including the name of
-- any unreachable subprograms that get deleted.
+ -- d.4 By default in case of an error during C generation, the .c or .h
+ -- file is delete. This flag keeps the C file.
+
-- d.5 By default a subprogram imported generates a subprogram profile.
-- This debug flag disables this generation when generating C code,
-- assuming a proper #include will be used instead.
with Nlists;
with Opt; use Opt;
with Osint; use Osint;
+with Osint.C; use Osint.C;
with Output; use Output;
with Par_SCO;
with Prepcomp;
Comperr.Delete_SCIL_Files;
end if;
+ -- Ditto for old C files before regenerating new ones
+
+ if Generate_C_Code then
+ Delete_C_File;
+ Delete_H_File;
+ end if;
+
-- Exit if compilation errors detected
Errout.Finalize (Last_Call => False);
end if;
end Debug_File_Eol_Length;
+ -------------------
+ -- Delete_C_File --
+ -------------------
+
+ procedure Delete_C_File is
+ Dummy : Boolean;
+ begin
+ Set_File_Name ("c");
+ Delete_File (Name_Buffer (1 .. Name_Len), Dummy);
+ end Delete_C_File;
+
+ -------------------
+ -- Delete_H_File --
+ -------------------
+
+ procedure Delete_H_File is
+ Dummy : Boolean;
+ begin
+ Set_File_Name ("h");
+ Delete_File (Name_Buffer (1 .. Name_Len), Dummy);
+ end Delete_H_File;
+
---------------------------------
-- Get_Output_Object_File_Name --
---------------------------------
--------------------------
-- These routines are used by the compiler when the C translation option
- -- is activated to write *.c and *.h files to the current object directory.
+ -- is activated to write *.c or *.h files to the current object directory.
-- Each routine exists in a C and an H form for the two kinds of files.
-- Only one of these files can be written at a time. Note that the files
-- are written via the Output package routines, using Output_FD.
-- Closes the file created by Create_C_File or Create_H file, flushing any
-- buffers etc. from writes by Write_C_File and Write_H_File;
+ procedure Delete_C_File;
+ procedure Delete_H_File;
+ -- Deletes the .c or .h file corresponding to the source file which is
+ -- currently being compiled.
+
----------------------
-- List File Output --
----------------------
-- 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;
-- 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;
-- 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
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 =>
("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.
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
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
-- 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
-- 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
projects / gcc.git / commitdiff