2017-01-13 Hristian Kirtchev <kirtchev@adacore.com>

	* exp_util.adb (Add_Inherited_Tagged_DIC):
	Pass the object parameters of both the parent and the derived
	type DIC procedure to the reference replacement circuitry.
	(Find_DIC_Type): Modify the circuitry to present the partial
	view of a private type in case the private type defines its own
	DIC pragma.
	(Replace_Object_And_Primitive_References): Add two
	optional formal parameters.  Update the comment on usage. Update
	the replacement of references to object parameters.

2017-01-13  Gary Dismukes  <dismukes@adacore.com>

	* einfo.adb, sem_ch6.adb, atree.adb: Minor reformatting and typo fix.

2017-01-13  Ed Schonberg  <schonberg@adacore.com>

	* sem_res.adb (Resolve_Actuals): Apply Scalar_Range_Check to
	an out parameter that is a type conversion, independently of th
	range check that may apply to the expression of the conversion,
	for use in GNATProve.

2017-01-13  Yannick Moy  <moy@adacore.com>

	* gnat1drv.adb (Gnat1drv): Move the implicit with for System in
	GNATprove_Mode here to Frontend.
	* frontend.adb (Frontend): Move the implicit with for System
	in GNATprove_Mode here as it ismore correct this way; the old
	place only worked by chance, since there were no overloaded names.
	* rtsfind.ads (RE_Id, RE_Unit_Table): Add RE_Tasking_State.
	* sem_attr.adb (Analyze_Attribute): In GNATprove_Mode, for the
	four attributes identified in SRM 9(18), add an implicit with
	to Ada.Task_Identification.
	* sem_ch8.adb (Analyze_Subprogram_Renaming.Build_Class_Wide_Wrapper):
	Deal specially with the wrapper introduced for AI05-0071 in GNATprove
	mode.
	* checks.adb (Apply_Discriminant_Check,
	Apply_Selected_Length_Checks, Apply_Selected_Range_Checks):
	In GNATprove mode, we do not apply the checks, but we still
	analyze the expression to possibly issue errors on SPARK
	code when a run-time error can be detected at compile time.
	(Selected_Length_Checks, Selected_Range_Checks): Perform analysis
	in GNATprove mode.



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@244398 138bc75d-0d04-0410-961f-82ee72b054a4

1 files changed, 53 insertions, 13 deletions

diff --git a/gcc/ada/checks.adb b/gcc/ada/checks.adb
index 10dbbaf75e9..6689cb56f07 100644
--- a/gcc/ada/checks.adb
+++ b/gcc/ada/checks.adb
@@ -1447,13 +1447,17 @@ package body Checks is
          T_Typ := Typ;
       end if;
 
-      --  Nothing to do if discriminant checks are suppressed or else no code
-      --  is to be generated
-
-      if not Expander_Active
-        or else Discriminant_Checks_Suppressed (T_Typ)
-      then
-         return;
+      --  Only apply checks when generating code and discriminant checks are
+      --  not suppressed. In GNATprove mode, we do not apply the checks, but we
+      --  still analyze the expression to possibly issue errors on SPARK code
+      --  when a run-time error can be detected at compile time.
+
+      if not GNATprove_Mode then
+         if not Expander_Active
+           or else Discriminant_Checks_Suppressed (T_Typ)
+         then
+            return;
+         end if;
       end if;
 
       --  No discriminant checks necessary for an access when expression is
@@ -1690,6 +1694,12 @@ package body Checks is
          end;
       end if;
 
+      --  In GNATprove mode, we do not apply the checks
+
+      if GNATprove_Mode then
+         return;
+      end if;
+
       --  Here we need a discriminant check. First build the expression
       --  for the comparisons of the discriminants:
 
@@ -3075,16 +3085,25 @@ package body Checks is
           or else (not Length_Checks_Suppressed (Target_Typ));
 
    begin
+      --  Only apply checks when generating code. In GNATprove mode, we do
+      --  not apply the checks, but we still call Selected_Length_Checks to
+      --  possibly issue errors on SPARK code when a run-time error can be
+      --  detected at compile time.
+
       --  Note: this means that we lose some useful warnings if the expander
-      --  is not active, and we also lose these warnings in SPARK mode ???
+      --  is not active.
 
-      if not Expander_Active then
+      if not Expander_Active and not GNATprove_Mode then
          return;
       end if;
 
       R_Result :=
         Selected_Length_Checks (Ck_Node, Target_Typ, Source_Typ, Empty);
 
+      if GNATprove_Mode then
+         return;
+      end if;
+
       for J in 1 .. 2 loop
          R_Cno := R_Result (J);
          exit when No (R_Cno);
@@ -3186,13 +3205,24 @@ package body Checks is
       R_Result : Check_Result;
 
    begin
-      if not Expander_Active or not Checks_On then
-         return;
+      --  Only apply checks when generating code. In GNATprove mode, we do not
+      --  apply the checks, but we still call Selected_Range_Checks to possibly
+      --  issue errors on SPARK code when a run-time error can be detected at
+      --  compile time.
+
+      if not GNATprove_Mode then
+         if not Expander_Active or not Checks_On then
+            return;
+         end if;
       end if;
 
       R_Result :=
         Selected_Range_Checks (Ck_Node, Target_Typ, Source_Typ, Empty);
 
+      if GNATprove_Mode then
+         return;
+      end if;
+
       for J in 1 .. 2 loop
          R_Cno := R_Result (J);
          exit when No (R_Cno);
@@ -9052,7 +9082,12 @@ package body Checks is
    --  Start of processing for Selected_Length_Checks
 
    begin
-      if not Expander_Active then
+      --  Checks will be applied only when generating code. In GNATprove mode,
+      --  we do not apply the checks, but we still call Selected_Length_Checks
+      --  to possibly issue errors on SPARK code when a run-time error can be
+      --  detected at compile time.
+
+      if not Expander_Active and not GNATprove_Mode then
          return Ret_Result;
       end if;
 
@@ -9602,7 +9637,12 @@ package body Checks is
    --  Start of processing for Selected_Range_Checks
 
    begin
-      if not Expander_Active then
+      --  Checks will be applied only when generating code. In GNATprove mode,
+      --  we do not apply the checks, but we still call Selected_Range_Checks
+      --  to possibly issue errors on SPARK code when a run-time error can be
+      --  detected at compile time.
+
+      if not Expander_Active and not GNATprove_Mode then
          return Ret_Result;
       end if;