Skip to content

R
riscv-gcc-1
Commit 520c0201 by Arnaud Charlet
Options

[multiple changes] 

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.

From-SVN: r235138
parent 274c2cda
Showing with 126 additions and 29 deletions
gcc/ada/ChangeLog
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):
......
gcc/ada/checks.adb
......@@ -2749,19 +2749,22 @@ package body Checks is
-- 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
......@@ -2968,18 +2971,17 @@ package body Checks is
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;
......
gcc/ada/debug.adb
......@@ -158,7 +158,7 @@ package body Debug is
-- 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
......@@ -762,6 +762,9 @@ package body Debug is
-- 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.
......
gcc/ada/gnat1drv.adb
......@@ -46,6 +46,7 @@ with Namet; use Namet;
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;
......@@ -1078,6 +1079,13 @@ begin
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);
......
gcc/ada/osint-c.adb
......@@ -292,6 +292,28 @@ package body Osint.C is
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 --
---------------------------------
......
gcc/ada/osint-c.ads
......@@ -159,7 +159,7 @@ package Osint.C is
--------------------------
-- 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.
......@@ -175,6 +175,11 @@ package Osint.C is
-- 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 --
----------------------
......
gcc/ada/sem_eval.adb
......@@ -1885,9 +1885,14 @@ package body Sem_Eval is
-- 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 @@ package body Sem_Eval is
-- 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 @@ package body Sem_Eval is
-- 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
......
gcc/ada/sem_res.adb
......@@ -5440,7 +5440,9 @@ package body Sem_Res is
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 @@ package body Sem_Res is
("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 @@ 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
......
gcc/ada/sem_util.adb
......@@ -4574,9 +4574,16 @@ package body Sem_Util is
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 @@ package body Sem_Util is
-- 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
......
gcc/ada/sem_util.ads
......@@ -135,7 +135,9 @@ package Sem_Util is
-- 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
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment