diff mbox

[Ada] Checks on aliasing and initialization of scalars for parameters

Message ID 20121001083741.GA3100@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Oct. 1, 2012, 8:37 a.m. UTC
This patch reimplements the checks related to aliasing and initialization of
scalars for subprogram parameters and ties them to compilation flags -gnateA
and -gnateV respectively.

Tested on x86_64-pc-linux-gnu, committed on trunk

2012-10-01  Hristian Kirtchev  <kirtchev@adacore.com>

	* checks.adb (Apply_Parameter_Aliasing_Checks): Removed.
	(Apply_Parameter_Aliasing_And_Validity_Checks): New routine.
	(Apply_Parameter_Validity_Checks): Removed.
	* checks.ads (Apply_Parameter_Aliasing_Checks): Removed.
	(Apply_Parameter_Aliasing_And_Validity_Checks): New routine.
	(Apply_Parameter_Validity_Checks): Removed.
	* exp_ch6.adb (Expand_Call): Remove the generation of parameter
	aliasing checks.
	* freeze.adb: Remove with and use clauses for Validsw.
	(Freeze_Entity): Update the guard and generation of aliasing
	and scalar initialization checks for subprogram parameters.
	* opt.ads: Add new flags Check_Aliasing_Of_Parameters and
	Check_Validity_Of_Parameters along with comments on usage.
	* sem_attr.adb (Analyze_Attribute): Pragma Overlaps_Storage is
	no longer an Ada 2012 feature.
	* sem_ch4.adb: Remove with and use clauses for Checks and Validsw.
	(Analyze_Call): Remove the generation of aliasing checks for
	subprogram parameters.
	* sem_ch13.adb: Remove with and use clauses for Validsw.
	(Analyze_Aspect_Specifications): Remove the generation of scalar
	initialization checks.
	* switch-c.adb (Scan_Front_End_Switches): Add processing for
	-gnateA and -gnateV.
	* usage.adb (Usage): Add information on switches -gnateA and
	-gnateV. Remove information on validity switches 'l', 'L',
	'v' and 'V'.
	* validsw.adb (Reset_Validity_Check_Options): Remove the
	reset of flags Validity_Check_Non_Overlapping_Params
	and Validity_Check_Valid_Scalars_On_Params.
	(Save_Validity_Check_Options): Remove the processing
	for flags Validity_Check_Non_Overlapping_Params
	and Validity_Check_Valid_Scalars_On_Params.
	(Set_Validity_Check_Options): Remove the processing
	for flags Validity_Check_Non_Overlapping_Params and
	Validity_Check_Valid_Scalars_On_Params.
	* validsw.ads: Remove flags Validity_Check_Non_Overlapping_Params
	and Validity_Check_Valid_Scalars_On_Params along with their
	comments on usage.
diff mbox

Patch

Index: switch-c.adb
===================================================================
--- switch-c.adb	(revision 191895)
+++ switch-c.adb	(working copy)
@@ -380,6 +380,12 @@ 
                      Enable_Switch_Storing;
                      Ptr := Ptr + 1;
 
+                  --  -gnateA (aliasing checks on parameters)
+
+                  when 'A' =>
+                     Ptr := Ptr + 1;
+                     Check_Aliasing_Of_Parameters := True;
+
                   --  -gnatec (configuration pragmas)
 
                   when 'c' =>
@@ -566,6 +572,22 @@ 
                   when 'P' =>
                      Treat_Categorization_Errors_As_Warnings := True;
 
+                  --  -gnateS (generate SCO information)
+
+                  --  Include Source Coverage Obligation information in ALI
+                  --  files for the benefit of source coverage analysis tools
+                  --  (xcov).
+
+                  when 'S' =>
+                     Generate_SCO := True;
+                     Ptr := Ptr + 1;
+
+                  --  -gnateV (validity checks on parameters)
+
+                  when 'V' =>
+                     Ptr := Ptr + 1;
+                     Check_Validity_Of_Parameters := True;
+
                   --  -gnatez (final delimiter of explicit switches)
 
                   --  All switches that come after -gnatez have been added by
@@ -577,16 +599,6 @@ 
                      Disable_Switch_Storing;
                      Ptr := Ptr + 1;
 
-                  --  -gnateS (generate SCO information)
-
-                  --  Include Source Coverage Obligation information in ALI
-                  --  files for the benefit of source coverage analysis tools
-                  --  (xcov).
-
-                  when 'S' =>
-                     Generate_SCO := True;
-                     Ptr := Ptr + 1;
-
                   --  All other -gnate? switches are unassigned
 
                   when others =>
Index: usage.adb
===================================================================
--- usage.adb	(revision 191890)
+++ usage.adb	(working copy)
@@ -167,6 +167,11 @@ 
    Write_Switch_Char ("Dnn");
    Write_Line ("Debug expanded generated code (max line length = nn)");
 
+   --  Line for -gnateA switch
+
+   Write_Switch_Char ("eA");
+   Write_Line ("Aliasing checks on subprogram parameters");
+
    --  Line for -gnatec switch
 
    Write_Switch_Char ("ec=?");
@@ -227,6 +232,11 @@ 
    Write_Switch_Char ("eS");
    Write_Line ("Generate SCO (Source Coverage Obligation) information");
 
+   --  Line for -gnateV switch
+
+   Write_Switch_Char ("eV");
+   Write_Line ("Validity checks on subprogram parameters");
+
    --  Line for -gnatE switch
 
    Write_Switch_Char ("E");
@@ -399,8 +409,6 @@ 
    Write_Line ("        F    turn off checking for floating-point");
    Write_Line ("        i    turn on checking for in params");
    Write_Line ("        I    turn off checking for in params");
-   Write_Line ("        l    turn on checking for non-overlapping params");
-   Write_Line ("        L    turn off checking for non-overlapping params");
    Write_Line ("        m    turn on checking for in out params");
    Write_Line ("        M    turn off checking for in out params");
    Write_Line ("        o    turn on checking for operators/attributes");
@@ -413,8 +421,6 @@ 
    Write_Line ("        S    turn off checking for subscripts");
    Write_Line ("        t    turn on checking for tests");
    Write_Line ("        T    turn off checking for tests");
-   Write_Line ("        v    turn on checking for 'Valid_Scalars on params");
-   Write_Line ("        V    turn off checking for 'Valid_Scalars on params");
    Write_Line ("        n    turn off all validity checks (including RM)");
 
    --  Lines for -gnatw switch
Index: checks.adb
===================================================================
--- checks.adb	(revision 191895)
+++ checks.adb	(working copy)
@@ -1774,263 +1774,60 @@ 
         (Ck_Node, Target_Typ, Source_Typ, Do_Static => False);
    end Apply_Length_Check;
 
-   -------------------------------------
-   -- Apply_Parameter_Aliasing_Checks --
-   -------------------------------------
+   --------------------------------------------------
+   -- Apply_Parameter_Aliasing_And_Validity_Checks --
+   --------------------------------------------------
 
-   procedure Apply_Parameter_Aliasing_Checks (Call : Node_Id) is
-      Loc        : constant Source_Ptr := Sloc (Call);
-      Actual     : Node_Id;
-      Actual_Typ : Entity_Id;
-      Check      : Node_Id;
-      Cond       : Node_Id := Empty;
-      Param      : Node_Id;
-      Param_Typ  : Entity_Id;
+   procedure Apply_Parameter_Aliasing_And_Validity_Checks (Subp : Entity_Id) is
+      Subp_Decl : Node_Id;
 
-   begin
-      --  Do not generate the checks in Ada 83, 95 or 05 mode because they
-      --  require an Ada 2012 construct.
+      procedure Add_Aliasing_Check
+        (Formal_1 : Entity_Id;
+         Formal_2 : Entity_Id);
+      --  Add a single 'Overlapping_Storage check to a post condition pragma
+      --  which verifies that Formal_1 is not aliasing Formal_2.
 
-      --  Why??? these pragmas and attributes are available in all ada modes
+      procedure Add_Validity_Check
+        (Context    : Entity_Id;
+         PPC_Nam    : Name_Id;
+         For_Result : Boolean := False);
+      --  Add a single 'Valid[_Scalar] check which verifies the initialization
+      --  of Context. PPC_Nam denotes the pre or post condition pragma name.
+      --  Set flag For_Result when to verify the result of a function.
 
-      if Ada_Version_Explicit < Ada_2012 then
-         return;
-      end if;
+      procedure Build_PPC_Pragma (PPC_Nam : Name_Id; Check : Node_Id);
+      --  Create a pre or post condition pragma with name PPC_Nam which
+      --  tests expression Check.
 
-      --  Inspect all pairs of parameters
+      ------------------------
+      -- Add_Aliasing_Check --
+      ------------------------
 
-      Actual := First_Actual (Call);
-      while Present (Actual) loop
-         Actual_Typ := Base_Type (Etype (Actual));
+      procedure Add_Aliasing_Check
+        (Formal_1 : Entity_Id;
+         Formal_2 : Entity_Id)
+      is
+         Loc : constant Source_Ptr := Sloc (Subp);
 
-         if Nkind (Actual) = N_Identifier
-           and then Is_Object_Reference (Actual)
-         then
-            Param := Next_Actual (Actual);
-            while Present (Param) loop
-               Param_Typ := Base_Type (Etype (Param));
-
-               if Nkind (Param) = N_Identifier
-                 and then Is_Object_Reference (Param)
-                 and then Actual_Typ = Param_Typ
-               then
-                  --  Generate:
-                  --    Actual'Overlaps_Storage (Param)
-
-                  Check :=
-                   Make_Attribute_Reference (Loc,
-                      Prefix         =>
-                        New_Reference_To (Entity (Actual), Loc),
-                      Attribute_Name => Name_Overlaps_Storage,
-                      Expressions    =>
-                        New_List (New_Reference_To (Entity (Param), Loc)));
-
-                  if No (Cond) then
-                     Cond := Check;
-                  else
-                     Cond :=
-                       Make_And_Then (Loc,
-                         Left_Opnd  => Cond,
-                         Right_Opnd => Check);
-                  end if;
-               end if;
-
-               Next_Actual (Param);
-            end loop;
-         end if;
-
-         Next_Actual (Actual);
-      end loop;
-
-      --  Raise Program_Error when the actuals overlap
-
-      if Present (Cond) then
-         Insert_Action (Call,
-           Make_Raise_Program_Error (Loc,
-             Condition => Cond,
-             Reason    => PE_Explicit_Raise));
-      end if;
-   end Apply_Parameter_Aliasing_Checks;
-
-   -------------------------------------
-   -- Apply_Parameter_Validity_Checks --
-   -------------------------------------
-
-   procedure Apply_Parameter_Validity_Checks (Subp : Entity_Id) is
-      Subp_Decl : Node_Id;
-      Subp_Spec : Node_Id;
-
-      procedure Create_PPC_Pragma (Prag : in out Node_Id; Nam : Name_Id);
-      --  Create a pre or post condition pragma with name Nam
-
-      -----------------------
-      -- Create_PPC_Pragma --
-      -----------------------
-
-      procedure Create_PPC_Pragma (Prag : in out Node_Id; Nam : Name_Id) is
-         Loc   : constant Source_Ptr := Sloc (Subp);
-         Assoc : Node_Id;
-
       begin
-         Prag :=
-           Make_Pragma (Loc,
-             Pragma_Identifier            => Make_Identifier (Loc, Nam),
-             Class_Present                =>
-               Is_Abstract_Subprogram (Subp)
-                 or else (Nkind (Subp_Spec) = N_Procedure_Specification
-                            and then Null_Present (Subp_Spec)),
-             Pragma_Argument_Associations => New_List (
-               Make_Pragma_Argument_Association (Loc,
-                 Chars      => Name_Check,
-                 Expression => Empty)));
+         Build_PPC_Pragma (Name_Postcondition,
+           Make_Attribute_Reference (Loc,
+             Prefix         => New_Reference_To (Formal_1, Loc),
+             Attribute_Name => Name_Overlaps_Storage,
+             Expressions    => New_List (New_Reference_To (Formal_2, Loc))));
+      end Add_Aliasing_Check;
 
-         --  Emulate the behavior of a from-aspect pragma
-
-         Set_From_Aspect_Specification (Prag);
-
-         --  Process all formals and a possible function result
-
-         Apply_Parameter_Validity_Checks (Subp, Prag);
-         Assoc := First (Pragma_Argument_Associations (Prag));
-
-         --  Insert the pragma in the tree only when the related subprogram
-         --  has eligible formals and function result that produced validity
-         --  checks.
-
-         if Present (Expression (Assoc)) then
-
-            --  Add a message unless exception messages are suppressed
-
-            if not Exception_Locations_Suppressed then
-               Append_To (Pragma_Argument_Associations (Prag),
-                 Make_Pragma_Argument_Association (Loc,
-                   Chars      => Name_Message,
-                   Expression =>
-                     Make_String_Literal (Loc,
-                       Strval => "failed " & Get_Name_String (Nam) &
-                                  " from " & Build_Location_String (Loc))));
-            end if;
-
-            --  Insert the pragma in the tree
-
-            if Nkind (Parent (Subp_Decl)) = N_Compilation_Unit then
-               Add_Global_Declaration (Prag);
-            else
-               Insert_After (Subp_Decl, Prag);
-            end if;
-
-            Analyze (Prag);
-         end if;
-      end Create_PPC_Pragma;
-
-      --  Local variables
-
-      Post : Node_Id := Empty;
-      Pre  : Node_Id := Empty;
-
-   --  Start of processing for Apply_Parameter_Validity_Checks
-
-   begin
-      --  Extract the subprogram specification and declaration nodes
-
-      Subp_Spec := Parent (Subp);
-
-      if Nkind (Subp_Spec) = N_Defining_Program_Unit_Name then
-         Subp_Spec := Parent (Subp_Spec);
-      end if;
-
-      Subp_Decl := Parent (Subp_Spec);
-
-      --  Do not generate checks in Ada 83 or 95 because the pragmas involved
-      --  are not allowed in those modes.
-
-      if Ada_Version_Explicit < Ada_2005 then
-         return;
-
-      --  Do not process subprograms where pre and post conditions do not make
-      --  sense.
-
-      elsif not Comes_From_Source (Subp)
-        or else Is_Imported (Subp)
-        or else Is_Intrinsic_Subprogram (Subp)
-        or else Is_Formal_Subprogram (Subp)
-        or else not Nkind_In (Subp_Decl, N_Abstract_Subprogram_Declaration,
-                                         N_Generic_Subprogram_Declaration,
-                                         N_Subprogram_Declaration)
-      then
-         return;
-      end if;
-
-      --  A subprogram may already have a pre or post condition pragma. Look
-      --  through the its contract and recover the pre and post conditions (if
-      --  available).
-
-      --  So what??? you can have multiple such pragmas, this is unnecessary
-      --  complexity being added for no purpose???
-
-      if Present (Contract (Subp)) then
-         declare
-            Nam  : Name_Id;
-            Prag : Node_Id;
-
-         begin
-            Prag := Spec_PPC_List (Contract (Subp));
-            while Present (Prag) loop
-               Nam := Pragma_Name (Prag);
-
-               if Nam = Name_Precondition then
-                  Pre := Prag;
-               elsif Nam = Name_Postcondition then
-                  Post := Prag;
-               end if;
-
-               Prag := Next_Pragma (Prag);
-            end loop;
-         end;
-      end if;
-
-      --  Generate the missing pre or post condition pragmas
-
-      if No (Pre) then
-         Create_PPC_Pragma (Pre, Name_Precondition);
-      end if;
-
-      if No (Post) then
-         Create_PPC_Pragma (Post, Name_Postcondition);
-      end if;
-   end Apply_Parameter_Validity_Checks;
-
-   -------------------------------------
-   -- Apply_Parameter_Validity_Checks --
-   -------------------------------------
-
-   procedure Apply_Parameter_Validity_Checks
-     (Subp : Entity_Id;
-      Prag : Node_Id)
-   is
-      Loc      : constant Source_Ptr := Sloc (Subp);
-      Prag_Nam : constant Name_Id    := Pragma_Name (Prag);
-      Formal   : Entity_Id;
-
-      procedure Add_Validity_Check
-        (Context    : Entity_Id;
-         For_Result : Boolean := False);
-      --  Add a single validity check to a pre or post condition which verifies
-      --  that Context has properly initialized scalars. Set flag For_Result to
-      --  verify the result of a function.
-
       ------------------------
       -- Add_Validity_Check --
       ------------------------
 
       procedure Add_Validity_Check
         (Context    : Entity_Id;
+         PPC_Nam    : Name_Id;
          For_Result : Boolean := False)
       is
-         Assoc : constant Node_Id   :=
-                   First (Pragma_Argument_Associations (Prag));
-         Expr  : constant Node_Id   := Expression (Assoc);
-         Typ   : constant Entity_Id := Etype (Context);
+         Loc   : constant Source_Ptr := Sloc (Subp);
+         Typ   : constant Entity_Id  := Etype (Context);
          Check : Node_Id;
          Nam   : Name_Id;
 
@@ -2069,67 +1866,146 @@ 
              Prefix         => Check,
              Attribute_Name => Nam);
 
-         --  Step 2: Associate the check with the related pragma
+         --  Step 2: Create a pre or post condition pragma
 
-         if No (Expr) then
-            Set_Expression (Assoc, Check);
+         Build_PPC_Pragma (PPC_Nam, Check);
+      end Add_Validity_Check;
+
+      ----------------------
+      -- Build_PPC_Pragma --
+      ----------------------
+
+      procedure Build_PPC_Pragma (PPC_Nam : Name_Id; Check : Node_Id) is
+         Loc  : constant Source_Ptr := Sloc (Subp);
+         Prag : Node_Id;
+
+      begin
+         Prag :=
+           Make_Pragma (Loc,
+             Pragma_Identifier            => Make_Identifier (Loc, PPC_Nam),
+             Pragma_Argument_Associations => New_List (
+               Make_Pragma_Argument_Association (Loc,
+                 Chars      => Name_Check,
+                 Expression => Check)));
+
+         --  Add a message unless exception messages are suppressed
+
+         if not Exception_Locations_Suppressed then
+            Append_To (Pragma_Argument_Associations (Prag),
+              Make_Pragma_Argument_Association (Loc,
+                Chars      => Name_Message,
+                Expression =>
+                  Make_String_Literal (Loc,
+                    Strval => "failed " & Get_Name_String (PPC_Nam) &
+                               " from " & Build_Location_String (Loc))));
+         end if;
+
+         --  Insert the pragma in the tree
+
+         if Nkind (Parent (Subp_Decl)) = N_Compilation_Unit then
+            Add_Global_Declaration (Prag);
          else
-            Set_Expression (Assoc,
-              Make_And_Then (Loc,
-                Left_Opnd  => Expr,
-                Right_Opnd => Check));
+            Insert_After (Subp_Decl, Prag);
          end if;
-      end Add_Validity_Check;
 
-   --  Start of processing for Apply_Parameter_Validity_Checks
+         Analyze (Prag);
+      end Build_PPC_Pragma;
 
+      --  Local variables
+
+      Formal    : Entity_Id;
+      Pair      : Entity_Id;
+      Subp_Spec : Node_Id;
+
+   --  Start of processing for Apply_Parameter_Aliasing_And_Validity_Checks
+
    begin
-      --  Do not process subprograms where pre and post conditions do not make
-      --  sense.
+      --  Extract the subprogram specification and declaration nodes
 
-      --  More detail here of why these specific conditions are needed???
-      --  And remember to document them ???
+      Subp_Spec := Parent (Subp);
+      if Nkind (Subp_Spec) = N_Defining_Program_Unit_Name then
+         Subp_Spec := Parent (Subp_Spec);
+      end if;
+      Subp_Decl := Parent (Subp_Spec);
 
       if not Comes_From_Source (Subp)
+
+         --  Do not process formal subprograms because the corresponding actual
+         --  will receive the proper checks when the instance is analyzed.
+
+        or else Is_Formal_Subprogram (Subp)
+
+         --  Do not process imported subprograms since pre and post conditions
+         --  are never verified on routines coming from a different language.
+
         or else Is_Imported (Subp)
         or else Is_Intrinsic_Subprogram (Subp)
+
+         --  Do not consider subprogram bodies because pre and post conditions
+         --  cannot be associated with them.
+
+        or else Nkind (Subp_Decl) /= N_Subprogram_Declaration
+
+         --  Do not process null procedures because there is no benefit of
+         --  adding the checks to a no action routine.
+
+        or else (Nkind (Subp_Spec) = N_Procedure_Specification
+                   and then Null_Present (Subp_Spec))
       then
          return;
       end if;
 
-      --  Generate the following validity checks for each formal parameter:
-      --
-      --    mode IN     - Pre       => Formal'Valid[_Scalars]
-      --    mode IN OUT - Pre, Post => Formal'Valid[_Scalars]
-      --    mode    OUT -      Post => Formal'Valid[_Scalars]
+      --  Inspect all the formals applying aliasing and scalar initialization
+      --  checks where applicable.
 
       Formal := First_Formal (Subp);
       while Present (Formal) loop
-         if Prag_Nam = Name_Precondition
-           and then Ekind_In (Formal, E_In_Parameter, E_In_Out_Parameter)
-         then
-            Add_Validity_Check (Formal);
+
+         --  Generate the following scalar initialization checks for each
+         --  formal parameter:
+
+         --    mode IN     - Pre       => Formal'Valid[_Scalars]
+         --    mode IN OUT - Pre, Post => Formal'Valid[_Scalars]
+         --    mode    OUT -      Post => Formal'Valid[_Scalars]
+
+         if Check_Validity_Of_Parameters then
+            if Ekind_In (Formal, E_In_Parameter, E_In_Out_Parameter) then
+               Add_Validity_Check (Formal, Name_Precondition, False);
+            end if;
+
+            if Ekind_In (Formal, E_In_Out_Parameter, E_Out_Parameter) then
+               Add_Validity_Check (Formal, Name_Postcondition, False);
+            end if;
          end if;
 
-         if Prag_Nam = Name_Postcondition
-           and then Ekind_In (Formal, E_In_Out_Parameter, E_Out_Parameter)
-         then
-            Add_Validity_Check (Formal);
+         --  Generate the following aliasing checks for every pair of formal
+         --  parameters:
+
+         --    Formal'Overlapping_Storage (Pair)
+
+         if Check_Aliasing_Of_Parameters then
+            Pair := Next_Formal (Formal);
+            while Present (Pair) loop
+               Add_Aliasing_Check (Formal, Pair);
+
+               Next_Formal (Pair);
+            end loop;
          end if;
 
          Next_Formal (Formal);
       end loop;
 
-      --  Generate the following validy check for a function result:
-      --
-      --    Post => Sub'Result'Valid[_Scalars]
+      --  Generate the following scalar initialization check for a function
+      --  result:
 
-      if Prag_Nam = Name_Postcondition
-        and then Ekind_In (Subp, E_Function, E_Generic_Function)
+      --    Post => Subp'Result'Valid[_Scalars]
+
+      if Check_Validity_Of_Parameters
+        and then Ekind (Subp) = E_Function
       then
-         Add_Validity_Check (Subp, For_Result => True);
+         Add_Validity_Check (Subp, Name_Postcondition, True);
       end if;
-   end Apply_Parameter_Validity_Checks;
+   end Apply_Parameter_Aliasing_And_Validity_Checks;
 
    ---------------------------
    -- Apply_Predicate_Check --
Index: checks.ads
===================================================================
--- checks.ads	(revision 191897)
+++ checks.ads	(working copy)
@@ -154,21 +154,11 @@ 
    --  formals, the check is performed only if the corresponding actual is
    --  constrained, i.e., whether Lhs'Constrained is True.
 
-   procedure Apply_Parameter_Aliasing_Checks (Call : Node_Id);
-   --  Given a subprogram call Call, introduce a check to verify that none of
-   --  the actual parameters overlap.
-
-   procedure Apply_Parameter_Validity_Checks (Subp : Entity_Id);
+   procedure Apply_Parameter_Aliasing_And_Validity_Checks (Subp : Entity_Id);
    --  Given a subprogram Subp, add both a pre and post condition pragmas that
-   --  verify the validity of formal parameters and function results.
+   --  detect aliased objects and verify the proper initialization of scalars
+   --  in parameters and function results.
 
-   procedure Apply_Parameter_Validity_Checks
-     (Subp : Entity_Id;
-      Prag : Node_Id);
-   --  Given a subprogram Subp and a pre or post condition pragma Prag, augment
-   --  the expression of the pragma to verify the validity of qualifying formal
-   --  parameter and function results.
-
    procedure Apply_Predicate_Check (N : Node_Id; Typ : Entity_Id);
    --  N is an expression to which a predicate check may need to be applied
    --  for Typ, if Typ has a predicate function. The check is applied only
Index: freeze.adb
===================================================================
--- freeze.adb	(revision 191890)
+++ freeze.adb	(working copy)
@@ -65,7 +65,6 @@ 
 with Ttypes;   use Ttypes;
 with Uintp;    use Uintp;
 with Urealp;   use Urealp;
-with Validsw;  use Validsw;
 
 package body Freeze is
 
@@ -2657,12 +2656,14 @@ 
          end;
       end if;
 
-      --  Add checks to detect proper initialization of scalars
+      --  Add checks to detect proper initialization of scalars and overlapping
+      --  storage of subprogram parameters.
 
       if Is_Subprogram (E)
-        and then Validity_Check_Valid_Scalars_On_Params
+        and then (Check_Aliasing_Of_Parameters
+                    or else Check_Validity_Of_Parameters)
       then
-         Apply_Parameter_Validity_Checks (E);
+         Apply_Parameter_Aliasing_And_Validity_Checks (E);
       end if;
 
       --  Deal with delayed aspect specifications. The analysis of the
Index: sem_attr.adb
===================================================================
--- sem_attr.adb	(revision 191894)
+++ sem_attr.adb	(working copy)
@@ -4062,7 +4062,6 @@ 
       ----------------------
 
       when Attribute_Overlaps_Storage =>
-         Check_Ada_2012_Attribute;
          Check_E1;
 
          --  Both arguments must be objects of any type
Index: exp_ch6.adb
===================================================================
--- exp_ch6.adb	(revision 191890)
+++ exp_ch6.adb	(working copy)
@@ -3404,13 +3404,6 @@ 
 
       Expand_Actuals (Call_Node, Subp);
 
-      --  Now that we have all parameters, add aliasing checks to detect
-      --  overlapping objects.
-
-      if Validity_Check_Non_Overlapping_Params then
-         Apply_Parameter_Aliasing_Checks (N);
-      end if;
-
       --  If the subprogram is a renaming, or if it is inherited, replace it in
       --  the call with the name of the actual subprogram being called. If this
       --  is a dispatching call, the run-time decides what to call. The Alias
Index: sem_ch4.adb
===================================================================
--- sem_ch4.adb	(revision 191894)
+++ sem_ch4.adb	(working copy)
@@ -25,7 +25,6 @@ 
 
 with Aspects;  use Aspects;
 with Atree;    use Atree;
-with Checks;   use Checks;
 with Debug;    use Debug;
 with Einfo;    use Einfo;
 with Elists;   use Elists;
@@ -63,7 +62,6 @@ 
 with Snames;   use Snames;
 with Tbuild;   use Tbuild;
 with Uintp;    use Uintp;
-with Validsw;  use Validsw;
 
 package body Sem_Ch4 is
 
@@ -1245,15 +1243,6 @@ 
 
          End_Interp_List;
       end if;
-
-      --  Add aliasing checks to detect overlapping objects. Process the call
-      --  now in case expansion is disabled.
-
-      if not Expander_Active
-        and then Validity_Check_Non_Overlapping_Params
-      then
-         Apply_Parameter_Aliasing_Checks (N);
-      end if;
    end Analyze_Call;
 
    -----------------------------
Index: validsw.adb
===================================================================
--- validsw.adb	(revision 191894)
+++ validsw.adb	(working copy)
@@ -33,18 +33,16 @@ 
 
    procedure Reset_Validity_Check_Options is
    begin
-      Validity_Check_Components              := False;
-      Validity_Check_Copies                  := False;
-      Validity_Check_Default                 := True;
-      Validity_Check_Floating_Point          := False;
-      Validity_Check_In_Out_Params           := False;
-      Validity_Check_In_Params               := False;
-      Validity_Check_Non_Overlapping_Params  := False;
-      Validity_Check_Operands                := False;
-      Validity_Check_Returns                 := False;
-      Validity_Check_Subscripts              := False;
-      Validity_Check_Tests                   := False;
-      Validity_Check_Valid_Scalars_On_Params := False;
+      Validity_Check_Components     := False;
+      Validity_Check_Copies         := False;
+      Validity_Check_Default        := True;
+      Validity_Check_Floating_Point := False;
+      Validity_Check_In_Out_Params  := False;
+      Validity_Check_In_Params      := False;
+      Validity_Check_Operands       := False;
+      Validity_Check_Returns        := False;
+      Validity_Check_Subscripts     := False;
+      Validity_Check_Tests          := False;
    end Reset_Validity_Check_Options;
 
    ---------------------------------
@@ -80,13 +78,11 @@ 
       Add ('e', Validity_Check_Components);
       Add ('f', Validity_Check_Floating_Point);
       Add ('i', Validity_Check_In_Params);
-      Add ('l', Validity_Check_Non_Overlapping_Params);
       Add ('m', Validity_Check_In_Out_Params);
       Add ('o', Validity_Check_Operands);
       Add ('r', Validity_Check_Returns);
       Add ('s', Validity_Check_Subscripts);
       Add ('t', Validity_Check_Tests);
-      Add ('v', Validity_Check_Valid_Scalars_On_Params);
    end Save_Validity_Check_Options;
 
    ----------------------------------------
@@ -137,119 +133,97 @@ 
          case C is
 
             when 'c' =>
-               Validity_Check_Copies                  := True;
+               Validity_Check_Copies         := True;
 
             when 'd' =>
-               Validity_Check_Default                 := True;
+               Validity_Check_Default        := True;
 
             when 'e' =>
-               Validity_Check_Components              := True;
+               Validity_Check_Components     := True;
 
             when 'f' =>
-               Validity_Check_Floating_Point          := True;
+               Validity_Check_Floating_Point := True;
 
             when 'i' =>
-               Validity_Check_In_Params               := True;
+               Validity_Check_In_Params      := True;
 
-            when 'l' =>
-               Validity_Check_Non_Overlapping_Params  := True;
-
             when 'm' =>
-               Validity_Check_In_Out_Params           := True;
+               Validity_Check_In_Out_Params  := True;
 
             when 'o' =>
-               Validity_Check_Operands                := True;
+               Validity_Check_Operands       := True;
 
             when 'p' =>
-               Validity_Check_Parameters              := True;
+               Validity_Check_Parameters     := True;
 
             when 'r' =>
-               Validity_Check_Returns                 := True;
+               Validity_Check_Returns        := True;
 
             when 's' =>
-               Validity_Check_Subscripts              := True;
+               Validity_Check_Subscripts     := True;
 
             when 't' =>
-               Validity_Check_Tests                   := True;
+               Validity_Check_Tests          := True;
 
-            when 'v' =>
-               Validity_Check_Valid_Scalars_On_Params := True;
-
             when 'C' =>
-               Validity_Check_Copies                  := False;
+               Validity_Check_Copies         := False;
 
             when 'D' =>
-               Validity_Check_Default                 := False;
+               Validity_Check_Default        := False;
 
             when 'E' =>
-               Validity_Check_Components              := False;
+               Validity_Check_Components     := False;
 
             when 'F' =>
-               Validity_Check_Floating_Point          := False;
+               Validity_Check_Floating_Point := False;
 
             when 'I' =>
-               Validity_Check_In_Params               := False;
+               Validity_Check_In_Params      := False;
 
-            when 'L' =>
-               Validity_Check_Non_Overlapping_Params  := False;
-
             when 'M' =>
-               Validity_Check_In_Out_Params           := False;
+               Validity_Check_In_Out_Params  := False;
 
             when 'O' =>
-               Validity_Check_Operands                := False;
+               Validity_Check_Operands       := False;
 
             when 'P' =>
-               Validity_Check_Parameters              := False;
+               Validity_Check_Parameters     := False;
 
             when 'R' =>
-               Validity_Check_Returns                 := False;
+               Validity_Check_Returns        := False;
 
             when 'S' =>
-               Validity_Check_Subscripts              := False;
+               Validity_Check_Subscripts     := False;
 
             when 'T' =>
-               Validity_Check_Tests                   := False;
+               Validity_Check_Tests          := False;
 
-            when 'V' =>
-               Validity_Check_Valid_Scalars_On_Params := False;
-
-            --  Note: The following two flags are not set when "-gnatVa" is in
-            --  effect because the associated checks are deemed too aggressive.
-
-            --     Validity_Check_Non_Overlapping_Params
-            --     Validity_Check_Valid_Scalars_On_Params
-
-            --  and in any case these do not belong as validity checks ???
-
             when 'a' =>
-               Validity_Check_Components              := True;
-               Validity_Check_Copies                  := True;
-               Validity_Check_Default                 := True;
-               Validity_Check_Floating_Point          := True;
-               Validity_Check_In_Out_Params           := True;
-               Validity_Check_In_Params               := True;
-               Validity_Check_Operands                := True;
-               Validity_Check_Parameters              := True;
-               Validity_Check_Returns                 := True;
-               Validity_Check_Subscripts              := True;
-               Validity_Check_Tests                   := True;
+               Validity_Check_Components     := True;
+               Validity_Check_Copies         := True;
+               Validity_Check_Default        := True;
+               Validity_Check_Floating_Point := True;
+               Validity_Check_In_Out_Params  := True;
+               Validity_Check_In_Params      := True;
+               Validity_Check_Operands       := True;
+               Validity_Check_Parameters     := True;
+               Validity_Check_Returns        := True;
+               Validity_Check_Subscripts     := True;
+               Validity_Check_Tests          := True;
 
             when 'n' =>
-               Validity_Check_Components              := False;
-               Validity_Check_Copies                  := False;
-               Validity_Check_Default                 := False;
-               Validity_Check_Floating_Point          := False;
-               Validity_Check_In_Out_Params           := False;
-               Validity_Check_In_Params               := False;
-               Validity_Check_Non_Overlapping_Params  := False;
-               Validity_Check_Operands                := False;
-               Validity_Check_Parameters              := False;
-               Validity_Check_Returns                 := False;
-               Validity_Check_Subscripts              := False;
-               Validity_Check_Tests                   := False;
-               Validity_Check_Valid_Scalars_On_Params := False;
-               Validity_Checks_On                     := False;
+               Validity_Check_Components     := False;
+               Validity_Check_Copies         := False;
+               Validity_Check_Default        := False;
+               Validity_Check_Floating_Point := False;
+               Validity_Check_In_Out_Params  := False;
+               Validity_Check_In_Params      := False;
+               Validity_Check_Operands       := False;
+               Validity_Check_Parameters     := False;
+               Validity_Check_Returns        := False;
+               Validity_Check_Subscripts     := False;
+               Validity_Check_Tests          := False;
+               Validity_Checks_On            := False;
 
             when ' ' =>
                null;
Index: validsw.ads
===================================================================
--- validsw.ads	(revision 191890)
+++ validsw.ads	(working copy)
@@ -82,13 +82,6 @@ 
    --  Validity_Checks, then the initial value of all IN parameters
    --  will be checked at the point of call of a procedure or function.
 
-   Validity_Check_Non_Overlapping_Params : Boolean := False;
-   --  Controls the validity checking of IN, IN OUT and OUT parameters in terms
-   --  of overlapping storage. If this switch is set to True using -gnatVl or
-   --  an 'l' in the argument of a pragma Validity_Checks, each subprogram call
-   --  is preceded by a sequence of checks which ensure that actual parameters
-   --  do not alias the same object or space.
-
    Validity_Check_Operands : Boolean := False;
    --  Controls validity checking of operands. If this switch is set to
    --  True using -gnatVo or an 'o' in the argument of a Validity_Checks
@@ -124,13 +117,6 @@ 
    --  switch is set to True using -gnatVt, or a 't' in the argument of a
    --  Validity_Checks pragma, then all such conditions are validity checked.
 
-   Validity_Check_Valid_Scalars_On_Params : Boolean := False;
-   --  Controls validity checking of parameters with respect to properly
-   --  initialized scalars. If this switch is set to True using -gnatVv, or a
-   --  'v' in the argument of pragma Validity_Checks, each IN, IN OUT and OUT
-   --  parameter along with possible function result is checked on entry and
-   --  exit of a subprogram for properly initialized scalars.
-
    Force_Validity_Checks : Boolean := False;
    --  Normally, operands that do not come from source (i.e. cases of expander
    --  generated code) are not checked, if this flag is set True, then checking
Index: opt.ads
===================================================================
--- opt.ads	(revision 191895)
+++ opt.ads	(working copy)
@@ -270,6 +270,11 @@ 
    --  Set to True to build, bind and link all the sources of a project file
    --  (switch -B)
 
+   Check_Aliasing_Of_Parameters : Boolean := False;
+   --  GNAT
+   --  Set to True to detect whether subprogram parameters and function results
+   --  alias the same object(s).
+
    Check_Object_Consistency : Boolean := False;
    --  GNATBIND, GNATMAKE
    --  Set to True to check whether every object file is consistent with
@@ -315,9 +320,14 @@ 
 
    Check_Unreferenced_Formals : Boolean := False;
    --  GNAT
-   --  Set True to check for unreferenced formals. This is turned on by
+   --  Set to True to check for unreferenced formals. This is turned on by
    --  -gnatwa/wf/wu and turned off by -gnatwA/wF/wU.
 
+   Check_Validity_Of_Parameters : Boolean := False;
+   --  GNAT
+   --  Set to True to check for proper scalar initialization of subprogram
+   --  parameters on both entry and exit.
+
    Check_Withs : Boolean := False;
    --  GNAT
    --  Set to True to enable checking for unused withs, and also the case
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb	(revision 191898)
+++ sem_ch13.adb	(working copy)
@@ -63,7 +63,6 @@ 
 with Ttypes;   use Ttypes;
 with Tbuild;   use Tbuild;
 with Urealp;   use Urealp;
-with Validsw;  use Validsw;
 with Warnsw;   use Warnsw;
 
 with GNAT.Heap_Sort_G;
@@ -1523,12 +1522,6 @@ 
                           Chars      => Name_Check,
                           Expression => Relocate_Node (Expr))));
 
-                  --  Add checks to detect proper initialization of scalars
-
-                  if Validity_Check_Valid_Scalars_On_Params then
-                     Apply_Parameter_Validity_Checks (E, Aitem);
-                  end if;
-
                   --  Add message unless exception messages are suppressed
 
                   if not Opt.Exception_Locations_Suppressed then