Patchwork [Ada] Validity checks on subprogram parameters and results

login
register
mail settings
Submitter Arnaud Charlet
Date Oct. 1, 2012, 8:11 a.m.
Message ID <20121001081127.GA2464@adacore.com>
Download mbox | patch
Permalink /patch/188227/
State New
Headers show

Comments

Arnaud Charlet - Oct. 1, 2012, 8:11 a.m.
This patch introduces two new validity checks to the GNAT compiler:

1) -gnatVl   Check non-overlapping parameters
When this check is enabled, each subprogram call is preceded by a sequence of
checks that ensure no overlap between actual parameters.

2) -gnatVv   Check proper initialization of scalars on parameters and results
When this check is enabled, each IN, IN OUT and OUT formal parameter along with
a possible function result is checked on entry and exit of a subprogram for
properly initialized scalars.

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

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

	* checks.ads, checks.adb (Apply_Parameter_Aliasing_Checks): New routine.
	(Apply_Parameter_Validity_Checks): New routines.
	* exp_ch6.adb (Expand_Call): Add aliasing checks to detect
	overlapping objects.
	* freeze.adb: Add with and use clauses for Checks and Validsw.
	(Freeze_Entity): Add checks to detect proper initialization
	of scalars.
	* sem_ch4.adb: Add with and use clauses for Checks and Validsw.
	(Analyze_Call): Add aliasing checks to detect overlapping objects.
	* sem_ch13.adb: Add with and use clauses for Validsw.
	(Analyze_Aspect_Specifications): Add checks to detect proper
	initialization of scalars.
	* sem_prag.adb (Chain_PPC): Correct the extraction of the
	subprogram name.
	* sem_util.adb (Is_Object_Reference): Attribute 'Result now
	produces an object.
	* usage.adb (Usage): Add usage lines for validity switches 'l',
	'L', 'v' and 'V'.
	* validsw.adb (Reset_Validity_Check_Options): Include
	processing for flags Validity_Check_Non_Overlapping_Params and
	Validity_Check_Valid_Scalars_On_Params. Code reformatting.
	(Save_Validity_Check_Options): Include processing
	for flags Validity_Check_Non_Overlapping_Params
	and Validity_Check_Valid_Scalars_On_Params.
	(Set_Validity_Check_Options): Add processing for validity switches
	'a', 'l', 'L', 'n', 'v' and 'V'. Code reformatting.
	* validsw.ads: Add new flags Validity_Check_Non_Overlapping_Params
	and Validity_Check_Valid_Scalars_On_Params along with comments
	on usage.

Patch

Index: usage.adb
===================================================================
--- usage.adb	(revision 191888)
+++ usage.adb	(working copy)
@@ -399,6 +399,8 @@ 
    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");
@@ -411,6 +413,8 @@ 
    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 191888)
+++ checks.adb	(working copy)
@@ -1774,6 +1774,353 @@ 
         (Ck_Node, Target_Typ, Source_Typ, Do_Static => False);
    end Apply_Length_Check;
 
+   -------------------------------------
+   -- Apply_Parameter_Aliasing_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;
+
+   begin
+      --  Do not generate the checks in Ada 83, 95 or 05 mode because they
+      --  require an Ada 2012 construct.
+
+      if Ada_Version_Explicit < Ada_2012 then
+         return;
+      end if;
+
+      --  Inspect all pairs of parameters
+
+      Actual := First_Actual (Call);
+      while Present (Actual) loop
+         Actual_Typ := Base_Type (Etype (Actual));
+
+         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)));
+
+         --  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).
+
+      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;
+         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);
+         Check : Node_Id;
+         Nam   : Name_Id;
+
+      begin
+         --  Pick the proper version of 'Valid depending on the type of the
+         --  context. If the context is not eligible for such a check, return.
+
+         if Is_Scalar_Type (Typ) then
+            Nam := Name_Valid;
+         elsif not No_Scalar_Parts (Typ) then
+            Nam := Name_Valid_Scalars;
+         else
+            return;
+         end if;
+
+         --  Step 1: Create the expression to verify the validity of the
+         --  context.
+
+         Check := New_Reference_To (Context, Loc);
+
+         --  When processing a function result, use 'Result. Generate
+         --    Context'Result
+
+         if For_Result then
+            Check :=
+              Make_Attribute_Reference (Loc,
+                Prefix         => Check,
+                Attribute_Name => Name_Result);
+         end if;
+
+         --  Generate:
+         --    Context['Result]'Valid[_Scalars]
+
+         Check :=
+           Make_Attribute_Reference (Loc,
+             Prefix         => Check,
+             Attribute_Name => Nam);
+
+         --  Step 2: Associate the check with the related pragma
+
+         if No (Expr) then
+            Set_Expression (Assoc, Check);
+         else
+            Set_Expression (Assoc,
+              Make_And_Then (Loc,
+                Left_Opnd  => Expr,
+                Right_Opnd => Check));
+         end if;
+      end Add_Validity_Check;
+
+   --  Start of processing for Apply_Parameter_Validity_Checks
+
+   begin
+      --  Do not process subprograms where pre and post conditions do not make
+      --  sense.
+
+      if not Comes_From_Source (Subp)
+        or else Is_Imported (Subp)
+        or else Is_Intrinsic_Subprogram (Subp)
+      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]
+
+      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);
+         end if;
+
+         if Prag_Nam = Name_Postcondition
+           and then Ekind_In (Formal, E_In_Out_Parameter, E_Out_Parameter)
+         then
+            Add_Validity_Check (Formal);
+         end if;
+
+         Next_Formal (Formal);
+      end loop;
+
+      --  Generate the following validy check for a function result:
+      --
+      --    Post => Sub'Result'Valid[_Scalars]
+
+      if Prag_Nam = Name_Postcondition
+        and then Ekind_In (Subp, E_Function, E_Generic_Function)
+      then
+         Add_Validity_Check (Subp, For_Result => True);
+      end if;
+   end Apply_Parameter_Validity_Checks;
+
    ---------------------------
    -- Apply_Predicate_Check --
    ---------------------------
Index: checks.ads
===================================================================
--- checks.ads	(revision 191888)
+++ checks.ads	(working copy)
@@ -6,7 +6,7 @@ 
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2011, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2012, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -154,6 +154,21 @@ 
    --  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);
+   --  Given a subprogram Subp, add both a pre and post condition pragmas that
+   --  verify the validity of formal 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: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 191888)
+++ sem_prag.adb	(working copy)
@@ -2057,6 +2057,10 @@ 
                S := Defining_Entity (PO);
             else
                S := Defining_Unit_Name (Specification (PO));
+
+               if Nkind (S) = N_Defining_Program_Unit_Name then
+                  S := Defining_Identifier (S);
+               end if;
             end if;
 
             --  Note: we do not analyze the pragma at this point. Instead we
Index: freeze.adb
===================================================================
--- freeze.adb	(revision 191888)
+++ freeze.adb	(working copy)
@@ -24,6 +24,7 @@ 
 ------------------------------------------------------------------------------
 
 with Atree;    use Atree;
+with Checks;   use Checks;
 with Debug;    use Debug;
 with Einfo;    use Einfo;
 with Elists;   use Elists;
@@ -64,6 +65,7 @@ 
 with Ttypes;   use Ttypes;
 with Uintp;    use Uintp;
 with Urealp;   use Urealp;
+with Validsw;  use Validsw;
 
 package body Freeze is
 
@@ -2655,6 +2657,14 @@ 
          end;
       end if;
 
+      --  Add checks to detect proper initialization of scalars
+
+      if Is_Subprogram (E)
+        and then Validity_Check_Valid_Scalars_On_Params
+      then
+         Apply_Parameter_Validity_Checks (E);
+      end if;
+
       --  Deal with delayed aspect specifications. The analysis of the
       --  aspect is required to be delayed to the freeze point, thus we
       --  analyze the pragma or attribute definition clause in the tree at
Index: sem_util.adb
===================================================================
--- sem_util.adb	(revision 191888)
+++ sem_util.adb	(working copy)
@@ -7719,10 +7719,12 @@ 
             when N_Function_Call =>
                return Etype (N) /= Standard_Void_Type;
 
-            --  A reference to the stream attribute Input is a function call
+            --  Attributes 'Input and 'Result produce objects
 
             when N_Attribute_Reference =>
-               return Attribute_Name (N) = Name_Input;
+               return Attribute_Name (N) = Name_Input
+                        or else
+                      Attribute_Name (N) = Name_Result;
 
             when N_Selected_Component =>
                return
Index: exp_ch6.adb
===================================================================
--- exp_ch6.adb	(revision 191888)
+++ exp_ch6.adb	(working copy)
@@ -3404,6 +3404,13 @@ 
 
       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 191888)
+++ sem_ch4.adb	(working copy)
@@ -25,6 +25,7 @@ 
 
 with Aspects;  use Aspects;
 with Atree;    use Atree;
+with Checks;   use Checks;
 with Debug;    use Debug;
 with Einfo;    use Einfo;
 with Elists;   use Elists;
@@ -62,6 +63,7 @@ 
 with Snames;   use Snames;
 with Tbuild;   use Tbuild;
 with Uintp;    use Uintp;
+with Validsw;  use Validsw;
 
 package body Sem_Ch4 is
 
@@ -1243,6 +1245,15 @@ 
 
          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 191888)
+++ validsw.adb	(working copy)
@@ -6,7 +6,7 @@ 
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 2001-2007, Free Software Foundation, Inc.         --
+--          Copyright (C) 2001-2012, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -33,16 +33,18 @@ 
 
    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_Operands       := False;
-      Validity_Check_Returns        := False;
-      Validity_Check_Subscripts     := False;
-      Validity_Check_Tests          := 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_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;
    end Reset_Validity_Check_Options;
 
    ---------------------------------
@@ -78,11 +80,13 @@ 
       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;
 
    ----------------------------------------
@@ -133,97 +137,113 @@ 
          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;
+
             when 'I' =>
-               Validity_Check_In_Params      := False;
+               Validity_Check_In_Params               := False;
 
-            when 'F' =>
-               Validity_Check_Floating_Point := 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;
+
             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_Non_Overlapping_Params  := True;
+               Validity_Check_Operands                := True;
+               Validity_Check_Parameters              := True;
+               Validity_Check_Returns                 := True;
+               Validity_Check_Subscripts              := True;
+               Validity_Check_Tests                   := True;
+               Validity_Check_Valid_Scalars_On_Params := 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_Operands       := False;
-               Validity_Check_Parameters     := False;
-               Validity_Check_Returns        := False;
-               Validity_Check_Subscripts     := False;
-               Validity_Check_Tests          := 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_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;
 
             when ' ' =>
                null;
Index: validsw.ads
===================================================================
--- validsw.ads	(revision 191888)
+++ validsw.ads	(working copy)
@@ -6,7 +6,7 @@ 
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 2001-2008, Free Software Foundation, Inc.         --
+--          Copyright (C) 2001-2012, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -82,6 +82,13 @@ 
    --  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
@@ -117,6 +124,13 @@ 
    --  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: sem_ch13.adb
===================================================================
--- sem_ch13.adb	(revision 191889)
+++ sem_ch13.adb	(working copy)
@@ -63,6 +63,7 @@ 
 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;
@@ -1522,6 +1523,12 @@ 
                           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