diff options
| -rw-r--r-- | gcc/ada/ChangeLog | 22 | ||||
| -rw-r--r-- | gcc/ada/checks.adb | 30 | ||||
| -rw-r--r-- | gcc/ada/debug.adb | 5 | ||||
| -rw-r--r-- | gcc/ada/gnat1drv.adb | 8 | ||||
| -rw-r--r-- | gcc/ada/osint-c.adb | 22 | ||||
| -rw-r--r-- | gcc/ada/osint-c.ads | 7 | ||||
| -rw-r--r-- | gcc/ada/sem_eval.adb | 22 | ||||
| -rw-r--r-- | gcc/ada/sem_res.adb | 22 | ||||
| -rw-r--r-- | gcc/ada/sem_util.adb | 13 | ||||
| -rw-r--r-- | gcc/ada/sem_util.ads | 4 |
10 files changed, 126 insertions, 29 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 11cbcb0..2b8e6ae 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,25 @@ +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): diff --git a/gcc/ada/checks.adb b/gcc/ada/checks.adb index a3ea477..e6eab0c 100644 --- a/gcc/ada/checks.adb +++ b/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; diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb index b38b82b..52de7a1 100644 --- a/gcc/ada/debug.adb +++ b/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. diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb index 220ad93..bc52f41 100644 --- a/gcc/ada/gnat1drv.adb +++ b/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); diff --git a/gcc/ada/osint-c.adb b/gcc/ada/osint-c.adb index a24a5a7..919f188 100644 --- a/gcc/ada/osint-c.adb +++ b/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 -- --------------------------------- diff --git a/gcc/ada/osint-c.ads b/gcc/ada/osint-c.ads index 6819ec0..54ffb01 100644 --- a/gcc/ada/osint-c.ads +++ b/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 -- ---------------------- diff --git a/gcc/ada/sem_eval.adb b/gcc/ada/sem_eval.adb index 67d464c..9703943 100644 --- a/gcc/ada/sem_eval.adb +++ b/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 diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index c12356c..6780772 100644 --- a/gcc/ada/sem_res.adb +++ b/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 diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 1146b9d..348da03 100644 --- a/gcc/ada/sem_util.adb +++ b/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 diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index d8a9b52..494a9e4 100644 --- a/gcc/ada/sem_util.ads +++ b/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 |