[multiple changes]

2012-12-05  Ed Schonberg  <schonberg@adacore.com>

	* sem_eval.adb: Remove spurious warnings.

2012-12-05  Ed Schonberg  <schonberg@adacore.com>

	* sem_util.adb (Build_Explicit_Dereference): Set properly
	the type of the prefix prior to rewriting, because subsequent
	legality checks examine the original node.

2012-12-05  Hristian Kirtchev  <kirtchev@adacore.com>

	* aspects.adb: Add Contract_Cases to the canonical aspects map.
	* aspects.ads: Add aspect Contract_Cases in the various aspect
	tables.
	* par-prag.adb: The parser does not need to perform special
	actions for pragma Contract_Cases.
	* sem_ch6.adb (Expand_Contract_Cases): New routine.
	(Process_Contract_Cases): Convert pragma Contract_Cases into pre-
	and post- condition checks that verify the runtime state of all
	case guards and their corresponding consequences.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Perform
	various legality checks on aspect Contract_Cases. The aspect is
	transformed into a pragma.
	* sem_prag.adb: Add an entry in table Sig_Flags for pragma
	Contract_Cases.
	(Analyze_Pragma): Perform various legality
	checks on pragma Contract_Cases.  The pragma is associated with
	the contract of the related subprogram.
	(Chain_CTC): Omit pragma
	Contract_Cases because it does not introduce a unique case name
	and does not follow the syntax of Contract_Case and Test_Case.
	* snames.ads-tmpl: Add new name Name_Contract_Cases. Add a
	Pragma_Id for Contract_Cases.

2012-12-05  Thomas Quinot  <quinot@adacore.com>

	* sem_ch5.adb: Minor reformatting.

2012-12-05  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_attr.ads: Add an entry for attribute Loop_Entry in the
	Attribute_Impl_Def table.

2012-12-05  Bob Duff  <duff@adacore.com>

	* gnatchop.adb (Read_File): Avoid storage leak, and in most cases avoid
	an extra copy of the string.

From-SVN: r194199

13 files changed, 815 insertions, 18 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 55c7118..0443c11 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,5 +1,54 @@
 2012-12-05  Ed Schonberg  <schonberg@adacore.com>
 
+	* sem_eval.adb: Remove spurious warnings.
+
+2012-12-05  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_util.adb (Build_Explicit_Dereference): Set properly
+	the type of the prefix prior to rewriting, because subsequent
+	legality checks examine the original node.
+
+2012-12-05  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* aspects.adb: Add Contract_Cases to the canonical aspects map.
+	* aspects.ads: Add aspect Contract_Cases in the various aspect
+	tables.
+	* par-prag.adb: The parser does not need to perform special
+	actions for pragma Contract_Cases.
+	* sem_ch6.adb (Expand_Contract_Cases): New routine.
+	(Process_Contract_Cases): Convert pragma Contract_Cases into pre-
+	and post- condition checks that verify the runtime state of all
+	case guards and their corresponding consequences.
+	* sem_ch13.adb (Analyze_Aspect_Specifications): Perform
+	various legality checks on aspect Contract_Cases. The aspect is
+	transformed into a pragma.
+	* sem_prag.adb: Add an entry in table Sig_Flags for pragma
+	Contract_Cases.
+	(Analyze_Pragma): Perform various legality
+	checks on pragma Contract_Cases.  The pragma is associated with
+	the contract of the related subprogram.
+	(Chain_CTC): Omit pragma
+	Contract_Cases because it does not introduce a unique case name
+	and does not follow the syntax of Contract_Case and Test_Case.
+	* snames.ads-tmpl: Add new name Name_Contract_Cases. Add a
+	Pragma_Id for Contract_Cases.
+
+2012-12-05  Thomas Quinot  <quinot@adacore.com>
+
+	* sem_ch5.adb: Minor reformatting.
+
+2012-12-05  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* sem_attr.ads: Add an entry for attribute Loop_Entry in the
+	Attribute_Impl_Def table.
+
+2012-12-05  Bob Duff  <duff@adacore.com>
+
+	* gnatchop.adb (Read_File): Avoid storage leak, and in most cases avoid
+	an extra copy of the string.
+
+2012-12-05  Ed Schonberg  <schonberg@adacore.com>
+
 	* sem_ch5.adb (Preanalyze_Range): If the expression, which
 	denotes some domain of iteration, has a type with implicit
 	dereference, and does not have any iterable aspects, insert
diff --git a/gcc/ada/aspects.adb b/gcc/ada/aspects.adb
index 880ee24..e3e7571 100644
--- a/gcc/ada/aspects.adb
+++ b/gcc/ada/aspects.adb
@@ -252,6 +252,7 @@ package body Aspects is
     Aspect_Component_Size               => Aspect_Component_Size,
     Aspect_Constant_Indexing            => Aspect_Constant_Indexing,
     Aspect_Contract_Case                => Aspect_Contract_Case,
+    Aspect_Contract_Cases               => Aspect_Contract_Cases,
     Aspect_Convention                   => Aspect_Convention,
     Aspect_CPU                          => Aspect_CPU,
     Aspect_Default_Component_Value      => Aspect_Default_Component_Value,
diff --git a/gcc/ada/aspects.ads b/gcc/ada/aspects.ads
index 3b4ebce..d79252b 100644
--- a/gcc/ada/aspects.ads
+++ b/gcc/ada/aspects.ads
@@ -81,6 +81,7 @@ package Aspects is
       Aspect_Component_Size,
       Aspect_Constant_Indexing,
       Aspect_Contract_Case,                 -- GNAT
+      Aspect_Contract_Cases,                -- GNAT
       Aspect_Convention,
       Aspect_CPU,
       Aspect_Default_Component_Value,
@@ -223,6 +224,7 @@ package Aspects is
                              Aspect_Ada_2012                 => True,
                              Aspect_Compiler_Unit            => True,
                              Aspect_Contract_Case            => True,
+                             Aspect_Contract_Cases           => True,
                              Aspect_Dimension                => True,
                              Aspect_Dimension_System         => True,
                              Aspect_Favor_Top_Level          => True,
@@ -254,9 +256,10 @@ package Aspects is
    --  the same aspect attached to the same declaration are allowed.
 
    No_Duplicates_Allowed : constant array (Aspect_Id) of Boolean :=
-                             (Aspect_Contract_Case => False,
-                              Aspect_Test_Case     => False,
-                              others               => True);
+                             (Aspect_Contract_Case  => False,
+                              Aspect_Contract_Cases => False,
+                              Aspect_Test_Case      => False,
+                              others                => True);
 
    --  The following array indicates type aspects that are inherited and apply
    --  to the class-wide type as well.
@@ -309,6 +312,7 @@ package Aspects is
                         Aspect_Component_Size          => Expression,
                         Aspect_Constant_Indexing       => Name,
                         Aspect_Contract_Case           => Expression,
+                        Aspect_Contract_Cases          => Expression,
                         Aspect_Convention              => Name,
                         Aspect_CPU                     => Expression,
                         Aspect_Default_Component_Value => Expression,
@@ -379,6 +383,7 @@ package Aspects is
      Aspect_Component_Size               => Name_Component_Size,
      Aspect_Constant_Indexing            => Name_Constant_Indexing,
      Aspect_Contract_Case                => Name_Contract_Case,
+     Aspect_Contract_Cases               => Name_Contract_Cases,
      Aspect_Convention                   => Name_Convention,
      Aspect_CPU                          => Name_CPU,
      Aspect_Default_Iterator             => Name_Default_Iterator,
diff --git a/gcc/ada/gnatchop.adb b/gcc/ada/gnatchop.adb
index 4cec050..0969c53 100644
--- a/gcc/ada/gnatchop.adb
+++ b/gcc/ada/gnatchop.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1998-2011, Free Software Foundation, Inc.         --
+--          Copyright (C) 1998-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- --
@@ -1004,7 +1004,7 @@ procedure Gnatchop is
    is
       Length      : constant File_Offset := File_Offset (File_Length (FD));
       --  Include room for EOF char
-      Buffer      : constant String_Access := new String (1 .. Length + 1);
+      Buffer      : String_Access := new String (1 .. Length + 1);
 
       This_Read   : Integer;
       Read_Ptr    : File_Offset := 1;
@@ -1020,8 +1020,15 @@ procedure Gnatchop is
       end loop;
 
       Buffer (Read_Ptr) := EOF;
-      Contents := new String (1 .. Read_Ptr);
-      Contents.all := Buffer (1 .. Read_Ptr);
+
+      if Read_Ptr = Length then
+         Contents := Buffer;
+
+      else
+         Contents := new String (1 .. Read_Ptr);
+         Contents.all := Buffer (1 .. Read_Ptr);
+         Free (Buffer);
+      end if;
 
       --  Things aren't simple on VMS due to the plethora of file types and
       --  organizations. It seems clear that there shouldn't be more bytes
diff --git a/gcc/ada/par-prag.adb b/gcc/ada/par-prag.adb
index 2468395..73a2fe4 100644
--- a/gcc/ada/par-prag.adb
+++ b/gcc/ada/par-prag.adb
@@ -1112,6 +1112,7 @@ begin
            Pragma_Compile_Time_Warning           |
            Pragma_Compiler_Unit                  |
            Pragma_Contract_Case                  |
+           Pragma_Contract_Cases                 |
            Pragma_Convention_Identifier          |
            Pragma_CPP_Class                      |
            Pragma_CPP_Constructor                |
diff --git a/gcc/ada/sem_attr.ads b/gcc/ada/sem_attr.ads
index 7258593..b993b9b 100644
--- a/gcc/ada/sem_attr.ads
+++ b/gcc/ada/sem_attr.ads
@@ -312,6 +312,11 @@ package Sem_Attr is
       --  the coding standards in use), but logically no initialization is
       --  needed, and the value should never be accessed.
 
+      Attribute_Loop_Entry => True,
+      --  For every object of a non-limited type, S'Loop_Entry { (Loop_Name) }
+      --  denotes the constant value of prefix S at the point of entry into the
+      --  related loop. The type of the attribute is the type of the prefix.
+
       ------------------
       -- Machine_Size --
       ------------------
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index cdddfa8..b5acf08 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -1629,14 +1629,89 @@ package body Sem_Ch13 is
 
                      Aitem :=
                        Make_Pragma (Loc,
-                                    Pragma_Identifier            =>
-                                      Make_Identifier (Sloc (Id), Nam),
-                                    Pragma_Argument_Associations =>
-                                      Args);
+                         Pragma_Identifier            =>
+                           Make_Identifier (Sloc (Id), Nam),
+                         Pragma_Argument_Associations => Args);
 
                      Delay_Required := False;
                   end;
 
+               when Aspect_Contract_Cases => Contract_Cases : declare
+                  Case_Guard  : Node_Id;
+                  Extra       : Node_Id;
+                  Others_Seen : Boolean := False;
+                  Post_Case   : Node_Id;
+
+               begin
+                  if Nkind (Parent (N)) = N_Compilation_Unit then
+                     Error_Msg_Name_1 := Nam;
+                     Error_Msg_N ("incorrect placement of aspect `%`", E);
+                     goto Continue;
+                  end if;
+
+                  if Nkind (Expr) /= N_Aggregate then
+                     Error_Msg_Name_1 := Nam;
+                     Error_Msg_NE
+                       ("wrong syntax for aspect `%` for &", Id, E);
+                     goto Continue;
+                  end if;
+
+                  --  Verify the legality of individual post cases
+
+                  Post_Case := First (Component_Associations (Expr));
+                  while Present (Post_Case) loop
+                     if Nkind (Post_Case) /= N_Component_Association then
+                        Error_Msg_N ("wrong syntax in post case", Post_Case);
+                        goto Continue;
+                     end if;
+
+                     --  Each post case must have exactly one case guard
+
+                     Case_Guard := First (Choices (Post_Case));
+                     Extra      := Next (Case_Guard);
+
+                     if Present (Extra) then
+                        Error_Msg_N
+                          ("post case may have only one case guard", Extra);
+                        goto Continue;
+                     end if;
+
+                     --  Check the placement of "others" (if available)
+
+                     if Nkind (Case_Guard) = N_Others_Choice then
+                        if Others_Seen then
+                           Error_Msg_Name_1 := Nam;
+                           Error_Msg_N
+                             ("only one others choice allowed in aspect %",
+                              Case_Guard);
+                           goto Continue;
+                        else
+                           Others_Seen := True;
+                        end if;
+
+                     elsif Others_Seen then
+                        Error_Msg_Name_1 := Nam;
+                        Error_Msg_N
+                          ("others must be the last choice in aspect %", N);
+                        goto Continue;
+                     end if;
+
+                     Next (Post_Case);
+                  end loop;
+
+                  --  Transform the aspect into a pragma
+
+                  Aitem :=
+                    Make_Pragma (Loc,
+                      Pragma_Identifier            =>
+                        Make_Identifier (Loc, Nam),
+                      Pragma_Argument_Associations => New_List (
+                        Make_Pragma_Argument_Association (Loc,
+                          Expression => Relocate_Node (Expr))));
+
+                  Delay_Required := False;
+               end Contract_Cases;
+
                --  Case 5: Special handling for aspects with an optional
                --  boolean argument.
 
@@ -6764,6 +6839,7 @@ package body Sem_Ch13 is
          --  Here is the list of aspects that don't require delay analysis.
 
          when Aspect_Contract_Case        |
+              Aspect_Contract_Cases       |
               Aspect_Dimension            |
               Aspect_Dimension_System     |
               Aspect_Implicit_Dereference |
diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb
index d17e689..a16e01e 100644
--- a/gcc/ada/sem_ch5.adb
+++ b/gcc/ada/sem_ch5.adb
@@ -3049,7 +3049,7 @@ package body Sem_Ch5 is
          if Is_Discrete_Type (Typ) then
             null;
 
-         --  Check that the resulting object is an iterable container.
+         --  Check that the resulting object is an iterable container
 
          elsif Present (Find_Aspect (Typ, Aspect_Iterator_Element))
            or else Present (Find_Aspect (Typ, Aspect_Constant_Indexing))
@@ -3057,7 +3057,7 @@ package body Sem_Ch5 is
          then
             null;
 
-         --  The expression may yield an implcit reference to an iterable
+         --  The expression may yield an implicit reference to an iterable
          --  container. Insert explicit dereference so that proper type is
          --  visible in the loop.
 
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 37dc5be..22feaebe 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -11139,6 +11139,11 @@ package body Sem_Ch6 is
       --  under the same visibility conditions as for other invariant checks,
       --  the type invariant must be applied to the returned value.
 
+      procedure Expand_Contract_Cases (CCs : Node_Id; Subp_Id : Entity_Id);
+      --  Given pragma Contract_Cases CCs, create the circuitry needed to
+      --  evaluate case guards and trigger consequence expressions. Subp_Id
+      --  denotes the related subprogram.
+
       function Grab_CC return Node_Id;
       --  Prag contains an analyzed contract case pragma. This function copies
       --  relevant components of the pragma, creates the corresponding Check
@@ -11206,6 +11211,459 @@ package body Sem_Ch6 is
          end if;
       end Check_Access_Invariants;
 
+      ---------------------------
+      -- Expand_Contract_Cases --
+      ---------------------------
+
+      --  Pragma Contract_Cases is expanded in the following manner:
+
+      --    subprogram S is
+      --       Flag_1   : Boolean := False;
+      --       . . .
+      --       Flag_N   : Boolean := False;
+      --       Flag_N+1 : Boolean := False;  --  when "others" present
+      --       Count    : Natural := 0;
+
+      --       <preconditions (if any)>
+
+      --       if Case_Guard_1 then
+      --          Flag_1 := True;
+      --          Count  := Count + 1;
+      --       end if;
+      --       . . .
+      --       if Case_Guard_N then
+      --          Flag_N := True;
+      --          Count  := Count + 1;
+      --       end if;
+
+      --       if Count = 0 then
+      --          raise Assertion_Error with "contract cases incomplete";
+      --            <or>
+      --          Flag_N+1 := True;  --  when "others" present
+
+      --       elsif Count > 1 then
+      --          declare
+      --             Str0 : constant String :=
+      --                      "contract cases overlap for subprogram ABC";
+      --             Str1 : constant String :=
+      --                      (if Flag_1 then
+      --                         Str0 & "case guard at xxx evaluates to True"
+      --                       else Str0);
+      --             StrN : constant String :=
+      --                      (if Flag_N then
+      --                         StrN-1 & "case guard at xxx evaluates to True"
+      --                       else StrN-1);
+      --          begin
+      --             raise Assertion_Error with StrN;
+      --          end;
+      --       end if;
+
+      --       procedure _Postconditions is
+      --       begin
+      --          <postconditions (if any)>
+
+      --          if Flag_1 and then not Consequence_1 then
+      --             raise Assertion_Error with "failed contract case at xxx";
+      --          end if;
+      --          . . .
+      --          if Flag_N[+1] and then not Consequence_N[+1] then
+      --             raise Assertion_Error with "failed contract case at xxx";
+      --          end if;
+      --       end _Postconditions;
+      --    begin
+      --       . . .
+      --    end S;
+
+      procedure Expand_Contract_Cases (CCs : Node_Id; Subp_Id : Entity_Id) is
+         Loc : constant Source_Ptr := Sloc (CCs);
+
+         procedure Case_Guard_Error
+           (Decls     : List_Id;
+            Flag      : Entity_Id;
+            Error_Loc : Source_Ptr;
+            Msg       : in out Entity_Id);
+         --  Given a declarative list Decls, status flag Flag, the location of
+         --  the error and a string Msg, construct the following check:
+         --    Msg : constant String :=
+         --            (if Flag then
+         --                Msg & "case guard at Error_Loc evaluates to True"
+         --             else Msg);
+         --  The resulting code is added to Decls
+
+         procedure Consequence_Error
+           (Checks : in out Node_Id;
+            Flag   : Entity_Id;
+            Conseq : Node_Id);
+         --  Given an if statement Checks, status flag Flag and a consequence
+         --  Conseq, construct the following check:
+         --    [els]if Flag and then not Conseq then
+         --       raise Assertion_Error
+         --         with "failed contract case at Sloc (Conseq)";
+         --    [end if;]
+         --  The resulting code is added to Checks
+
+         function Declaration_Of (Id : Entity_Id) return Node_Id;
+         --  Given the entity Id of a boolean flag, generate:
+         --    Id : Boolean := False;
+
+         function Increment (Id : Entity_Id) return Node_Id;
+         --  Given the entity Id of a numerical variable, generate:
+         --    Id := Id + 1;
+
+         function Set (Id : Entity_Id) return Node_Id;
+         --  Given the entity Id of a boolean variable, generate:
+         --    Id := True;
+
+         ----------------------
+         -- Case_Guard_Error --
+         ----------------------
+
+         procedure Case_Guard_Error
+           (Decls     : List_Id;
+            Flag      : Entity_Id;
+            Error_Loc : Source_Ptr;
+            Msg       : in out Entity_Id)
+         is
+            New_Line : constant Character := Character'Val (10);
+            New_Msg  : constant Entity_Id := Make_Temporary (Loc, 'S');
+
+         begin
+            Start_String;
+            Store_String_Char  (New_Line);
+            Store_String_Chars ("  case guard at ");
+            Store_String_Chars (Build_Location_String (Error_Loc));
+            Store_String_Chars (" evaluates to True");
+
+            --  Generate:
+            --    New_Msg : constant String :=
+            --      (if Flag then
+            --          Msg & "case guard at Error_Loc evaluates to True"
+            --       else Msg);
+
+            Append_To (Decls,
+              Make_Object_Declaration (Loc,
+                Defining_Identifier => New_Msg,
+                Constant_Present    => True,
+                Object_Definition   => New_Reference_To (Standard_String, Loc),
+                Expression          =>
+                  Make_If_Expression (Loc,
+                    Expressions => New_List (
+                      New_Reference_To (Flag, Loc),
+
+                      Make_Op_Concat (Loc,
+                        Left_Opnd  => New_Reference_To (Msg, Loc),
+                        Right_Opnd => Make_String_Literal (Loc, End_String)),
+
+                      New_Reference_To (Msg, Loc)))));
+
+            Msg := New_Msg;
+         end Case_Guard_Error;
+
+         -----------------------
+         -- Consequence_Error --
+         -----------------------
+
+         procedure Consequence_Error
+           (Checks : in out Node_Id;
+            Flag   : Entity_Id;
+            Conseq : Node_Id)
+         is
+            Cond  : Node_Id;
+            Error : Node_Id;
+
+         begin
+            --  Generate:
+            --    Flag and then not Conseq
+
+            Cond :=
+              Make_And_Then (Loc,
+                Left_Opnd  => New_Reference_To (Flag, Loc),
+                Right_Opnd =>
+                  Make_Op_Not (Loc,
+                    Right_Opnd => Relocate_Node (Conseq)));
+
+            --  Generate:
+            --    raise Assertion_Error
+            --      with "failed contract case at Sloc (Conseq)";
+
+            Start_String;
+            Store_String_Chars ("failed contract case at ");
+            Store_String_Chars (Build_Location_String (Sloc (Conseq)));
+
+            Error :=
+              Make_Procedure_Call_Statement (Loc,
+                Name                   =>
+                  New_Reference_To (RTE (RE_Raise_Assert_Failure), Loc),
+                Parameter_Associations => New_List (
+                  Make_String_Literal (Loc, End_String)));
+
+            if No (Checks) then
+               Checks :=
+                 Make_If_Statement (Loc,
+                   Condition       => Cond,
+                   Then_Statements => New_List (Error));
+
+            else
+               if No (Elsif_Parts (Checks)) then
+                  Set_Elsif_Parts (Checks, New_List);
+               end if;
+
+               Append_To (Elsif_Parts (Checks),
+                 Make_Elsif_Part (Loc,
+                   Condition       => Cond,
+                   Then_Statements => New_List (Error)));
+            end if;
+         end Consequence_Error;
+
+         --------------------
+         -- Declaration_Of --
+         --------------------
+
+         function Declaration_Of (Id : Entity_Id) return Node_Id is
+         begin
+            return
+              Make_Object_Declaration (Loc,
+                Defining_Identifier => Id,
+                Object_Definition   =>
+                  New_Reference_To (Standard_Boolean, Loc),
+                Expression          =>
+                  New_Reference_To (Standard_False, Loc));
+         end Declaration_Of;
+
+         ---------------
+         -- Increment --
+         ---------------
+
+         function Increment (Id : Entity_Id) return Node_Id is
+         begin
+            return
+              Make_Assignment_Statement (Loc,
+                Name       => New_Reference_To (Id, Loc),
+                Expression =>
+                  Make_Op_Add (Loc,
+                    Left_Opnd  => New_Reference_To (Id, Loc),
+                    Right_Opnd => Make_Integer_Literal (Loc, 1)));
+         end Increment;
+
+         ---------
+         -- Set --
+         ---------
+
+         function Set (Id : Entity_Id) return Node_Id is
+         begin
+            return
+              Make_Assignment_Statement (Loc,
+                Name       => New_Reference_To (Id, Loc),
+                Expression => New_Reference_To (Standard_True, Loc));
+         end Set;
+
+         --  Local variables
+
+         Aggr          : constant Node_Id :=
+                           Expression (First
+                             (Pragma_Argument_Associations (CCs)));
+         Decls         : constant List_Id := Declarations (N);
+         Multiple_PCs  : constant Boolean :=
+                           List_Length (Component_Associations (Aggr)) > 1;
+         Case_Guard    : Node_Id;
+         CG_Checks     : Node_Id;
+         CG_Stmts      : List_Id;
+         Conseq        : Node_Id;
+         Conseq_Checks : Node_Id := Empty;
+         Count         : Entity_Id;
+         Error_Decls   : List_Id;
+         Flag          : Entity_Id;
+         Msg_Str       : Entity_Id;
+         Others_Flag   : Entity_Id := Empty;
+         Post_Case     : Node_Id;
+
+      --  Start of processing for Expand_Contract_Cases
+
+      begin
+         --  Create the counter which tracks the number of case guards that
+         --  evaluate to True.
+
+         --    Count : Natural := 0;
+
+         Count := Make_Temporary (Loc, 'C');
+
+         Prepend_To (Decls,
+           Make_Object_Declaration (Loc,
+             Defining_Identifier => Count,
+             Object_Definition   => New_Reference_To (Standard_Natural, Loc),
+             Expression          => Make_Integer_Literal (Loc, 0)));
+
+         --  Create the base error message for multiple overlapping case
+         --  guards.
+
+         --    Msg_Str : constant String :=
+         --                "contract cases overlap for subprogram Subp_Id";
+
+         if Multiple_PCs then
+            Msg_Str := Make_Temporary (Loc, 'S');
+
+            Start_String;
+            Store_String_Chars ("contract cases overlap for subprogram ");
+            Store_String_Chars (Get_Name_String (Chars (Subp_Id)));
+
+            Error_Decls := New_List (
+              Make_Object_Declaration (Loc,
+                Defining_Identifier => Msg_Str,
+                Constant_Present    => True,
+                Object_Definition   => New_Reference_To (Standard_String, Loc),
+                Expression          => Make_String_Literal (Loc, End_String)));
+         end if;
+
+         --  Process individual post cases
+
+         Post_Case := First (Component_Associations (Aggr));
+         while Present (Post_Case) loop
+            Case_Guard := First (Choices (Post_Case));
+            Conseq     := Expression (Post_Case);
+
+            --  The "others" choice requires special processing
+
+            if Nkind (Case_Guard) = N_Others_Choice then
+               Others_Flag := Make_Temporary (Loc, 'F');
+               Prepend_To (Decls, Declaration_Of (Others_Flag));
+
+               --  Check possible overlap between a case guard and "others"
+
+               if Multiple_PCs then
+                  Case_Guard_Error
+                    (Decls     => Error_Decls,
+                     Flag      => Others_Flag,
+                     Error_Loc => Sloc (Case_Guard),
+                     Msg       => Msg_Str);
+               end if;
+
+               --  Check the corresponding consequence of "others"
+
+               Consequence_Error
+                 (Checks => Conseq_Checks,
+                  Flag   => Others_Flag,
+                  Conseq => Conseq);
+
+            --  Regular post case
+
+            else
+               --  Create the flag which tracks the state of its associated
+               --  case guard.
+
+               Flag := Make_Temporary (Loc, 'F');
+               Prepend_To (Decls, Declaration_Of (Flag));
+
+               --  The flag is set when the case guard is evaluated to True
+               --    if Case_Guard then
+               --       Flag  := True;
+               --       Count := Count + 1;
+               --    end if;
+
+               Append_To (Decls,
+                 Make_If_Statement (Loc,
+                   Condition       => Relocate_Node (Case_Guard),
+                   Then_Statements => New_List (
+                     Set (Flag),
+                     Increment (Count))));
+
+               --  Check whether this case guard overlaps with another case
+               --  guard.
+
+               if Multiple_PCs then
+                  Case_Guard_Error
+                    (Decls     => Error_Decls,
+                     Flag      => Flag,
+                     Error_Loc => Sloc (Case_Guard),
+                     Msg       => Msg_Str);
+               end if;
+
+               --  The corresponding consequence of the case guard which
+               --  evaluated to True must hold on exit from the subprogram.
+
+               Consequence_Error (Conseq_Checks, Flag, Conseq);
+            end if;
+
+            Next (Post_Case);
+         end loop;
+
+         --  Raise Assertion_Error when none of the case guards evaluate to
+         --  True. The only exception is when we have "others", in which case
+         --  there is no error because "others" acts as a default True.
+
+         --  Generate:
+         --    Flag := True;
+
+         if Present (Others_Flag) then
+            CG_Stmts := New_List (Set (Others_Flag));
+
+         --  Generate:
+         --    raise Assetion_Error with "contract cases incomplete";
+
+         else
+            Start_String;
+            Store_String_Chars ("contract cases incomplete");
+
+            CG_Stmts := New_List (
+              Make_Procedure_Call_Statement (Loc,
+                Name                   =>
+                  New_Reference_To (RTE (RE_Raise_Assert_Failure), Loc),
+                Parameter_Associations => New_List (
+                  Make_String_Literal (Loc, End_String))));
+         end if;
+
+         CG_Checks :=
+           Make_If_Statement (Loc,
+             Condition       =>
+               Make_Op_Eq (Loc,
+                 Left_Opnd  => New_Reference_To (Count, Loc),
+                 Right_Opnd => Make_Integer_Literal (Loc, 0)),
+             Then_Statements => CG_Stmts);
+
+         --  Detect a possible failure due to several case guards evaluating to
+         --  True.
+
+         --  Generate:
+         --    elsif Count > 0 then
+         --       declare
+         --          <Error_Decls>
+         --       begin
+         --          raise Assertion_Error with <Msg_Str>;
+         --    end if;
+
+         if Multiple_PCs then
+            Set_Elsif_Parts (CG_Checks, New_List (
+              Make_Elsif_Part (Loc,
+                Condition       =>
+                  Make_Op_Gt (Loc,
+                    Left_Opnd  => New_Reference_To (Count, Loc),
+                    Right_Opnd => Make_Integer_Literal (Loc, 1)),
+
+                Then_Statements => New_List (
+                  Make_Block_Statement (Loc,
+                    Declarations               => Error_Decls,
+                    Handled_Statement_Sequence =>
+                      Make_Handled_Sequence_Of_Statements (Loc,
+                        Statements => New_List (
+                          Make_Procedure_Call_Statement (Loc,
+                            Name                   =>
+                              New_Reference_To
+                                (RTE (RE_Raise_Assert_Failure), Loc),
+                            Parameter_Associations => New_List (
+                              New_Reference_To (Msg_Str, Loc))))))))));
+         end if;
+
+         Append_To (Decls, CG_Checks);
+
+         --  Raise Assertion_Error when the corresponding consequence of a case
+         --  guard that evaluated to True fails.
+
+         if No (Plist) then
+            Plist := New_List;
+         end if;
+
+         Append_To (Plist, Conseq_Checks);
+      end Expand_Contract_Cases;
+
       -------------
       -- Grab_CC --
       -------------
@@ -11736,6 +12194,9 @@ package body Sem_Ch6 is
                      else
                         Append (Grab_CC, Plist);
                      end if;
+
+                  elsif Pragma_Name (Prag) = Name_Contract_Cases then
+                     Expand_Contract_Cases (Prag, Spec_Id);
                   end if;
 
                   Prag := Next_Pragma (Prag);
@@ -11850,7 +12311,7 @@ package body Sem_Ch6 is
                     Make_Invariant_Call (New_Occurrence_Of (Rent, Loc)));
                end if;
 
-               --  Same if return value is an access to type with invariants.
+               --  Same if return value is an access to type with invariants
 
                Check_Access_Invariants (Rent);
             end;
diff --git a/gcc/ada/sem_eval.adb b/gcc/ada/sem_eval.adb
index cf2a922..4a8fa2c 100644
--- a/gcc/ada/sem_eval.adb
+++ b/gcc/ada/sem_eval.adb
@@ -1314,11 +1314,22 @@ package body Sem_Eval is
       --  is at optimizing and knowing that things are constant when they are
       --  nonstatic.
 
+      --  We make an exception for expressions that evaluate to True/False, to
+      --  suppress spurious checks in ZFP mode.
+
       if Configurable_Run_Time_Mode
         and then K /= N_Null
         and then not Is_Static_Expression (Op)
       then
-         return False;
+         if Is_Entity_Name (Op)
+           and then Ekind (Entity (Op)) = E_Enumeration_Literal
+           and then Etype (Entity (Op)) = Standard_Boolean
+         then
+            null;
+
+         else
+            return False;
+         end if;
       end if;
 
       --  If we have an entity name, then see if it is the name of a constant
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index fa3e066..e4ee1f6 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -1499,7 +1499,17 @@ package body Sem_Prag is
             begin
                CTC := Spec_CTC_List (Contract (S));
                while Present (CTC) loop
-                  if String_Equal (Name, Get_Name_From_CTC_Pragma (CTC)) then
+
+                  --  Omit pragma Contract_Cases because it does not introduce
+                  --  a unique case name and it does not follow the syntax of
+                  --  Contract_Case and Test_Case.
+
+                  if Pragma_Name (CTC) = Name_Contract_Cases then
+                     null;
+
+                  elsif String_Equal
+                          (Name, Get_Name_From_CTC_Pragma (CTC))
+                  then
                      Error_Msg_Sloc := Sloc (CTC);
                      Error_Pragma ("name for pragma% is already used#");
                   end if;
@@ -7705,6 +7715,166 @@ package body Sem_Prag is
          when Pragma_Contract_Case =>
             Check_Contract_Or_Test_Case;
 
+         --------------------
+         -- Contract_Cases --
+         --------------------
+
+         --  pragma Contract_Cases (POST_CASE_LIST);
+
+         --  POST_CASE_LIST ::= POST_CASE {, POST_CASE}
+
+         --  POST_CASE ::= CASE_GUARD => CONSEQUENCE
+
+         --  CASE_GUARD ::= boolean_EXPRESSION | others
+
+         --  CONSEQUENCE ::= boolean_EXPRESSION
+
+         when Pragma_Contract_Cases => Contract_Cases : declare
+            procedure Chain_Contract_Cases (Subp_Decl : Node_Id);
+            --  Chain pragma Contract_Cases to the contract of a subprogram.
+            --  Subp_Decl is the declaration of the subprogram.
+
+            --------------------------
+            -- Chain_Contract_Cases --
+            --------------------------
+
+            procedure Chain_Contract_Cases (Subp_Decl : Node_Id) is
+               Subp : constant Entity_Id :=
+                        Defining_Unit_Name (Specification (Subp_Decl));
+               CTC  : Node_Id;
+
+            begin
+               CTC := Spec_CTC_List (Contract (Subp));
+               while Present (CTC) loop
+                  if Chars (Pragma_Identifier (CTC)) = Pname then
+                     Error_Pragma ("pragma % already in use");
+                     return;
+                  end if;
+
+                  CTC := Next_Pragma (CTC);
+               end loop;
+
+               --  Prepend pragma Contract_Cases to the contract
+
+               Set_Next_Pragma (N, Spec_CTC_List (Contract (Subp)));
+               Set_Spec_CTC_List (Contract (Subp), N);
+            end Chain_Contract_Cases;
+
+            --  Local variables
+
+            Case_Guard  : Node_Id;
+            Decl        : Node_Id;
+            Extra       : Node_Id;
+            Others_Seen : Boolean := False;
+            Post_Case   : Node_Id;
+            Subp_Decl   : Node_Id;
+
+         --  Start of processing for Contract_Cases
+
+         begin
+            GNAT_Pragma;
+            S14_Pragma;
+            Check_Arg_Count (1);
+
+            --  Completely ignore if disabled
+
+            if Check_Disabled (Pname) then
+               Rewrite (N, Make_Null_Statement (Loc));
+               Analyze (N);
+               return;
+            end if;
+
+            --  Check the placement of the pragma
+
+            if not Is_List_Member (N) then
+               Pragma_Misplaced;
+            end if;
+
+            --  Pragma Contract_Cases must be associated with a subprogram
+
+            Decl := N;
+            while Present (Prev (Decl)) loop
+               Decl := Prev (Decl);
+
+               if Nkind (Decl) in N_Generic_Declaration then
+                  Subp_Decl := Decl;
+               else
+                  Subp_Decl := Original_Node (Decl);
+               end if;
+
+               --  Skip prior pragmas
+
+               if Nkind (Subp_Decl) = N_Pragma then
+                  null;
+
+               --  Skip internally generated code
+
+               elsif not Comes_From_Source (Subp_Decl) then
+                  null;
+
+               --  We have found the related subprogram
+
+               elsif Nkind_In (Subp_Decl, N_Generic_Subprogram_Declaration,
+                                          N_Subprogram_Declaration)
+               then
+                  exit;
+
+               else
+                  Pragma_Misplaced;
+               end if;
+            end loop;
+
+            --  All post cases must appear as an aggregate
+
+            if Nkind (Expression (Arg1)) /= N_Aggregate then
+               Error_Pragma ("wrong syntax for pragma %");
+               return;
+            end if;
+
+            --  Verify the legality of individual post cases
+
+            Post_Case := First (Component_Associations (Expression (Arg1)));
+            while Present (Post_Case) loop
+               if Nkind (Post_Case) /= N_Component_Association then
+                  Error_Pragma_Arg ("wrong syntax in post case", Post_Case);
+                  return;
+               end if;
+
+               Case_Guard := First (Choices (Post_Case));
+
+               --  Each post case must have exactly on case guard
+
+               Extra := Next (Case_Guard);
+               if Present (Extra) then
+                  Error_Pragma_Arg
+                    ("post case may have only one case guard", Extra);
+                  return;
+               end if;
+
+               --  Check the placement of "others" (if available)
+
+               if Nkind (Case_Guard) = N_Others_Choice then
+                  if Others_Seen then
+                     Error_Pragma_Arg
+                       ("only one others choice allowed in pragma %",
+                        Case_Guard);
+                     return;
+                  else
+                     Others_Seen := True;
+                  end if;
+
+               elsif Others_Seen then
+                  Error_Pragma_Arg
+                    ("others must be the last choice in pragma %", N);
+                  return;
+               end if;
+
+               Next (Post_Case);
+            end loop;
+
+            Chain_Contract_Cases (Subp_Decl);
+         end Contract_Cases;
+
          ----------------
          -- Controlled --
          ----------------
@@ -15468,6 +15638,7 @@ package body Sem_Prag is
       Pragma_Complex_Representation         =>  0,
       Pragma_Component_Alignment            => -1,
       Pragma_Contract_Case                  => -1,
+      Pragma_Contract_Cases                 => -1,
       Pragma_Controlled                     =>  0,
       Pragma_Convention                     =>  0,
       Pragma_Convention_Identifier          =>  0,
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 8fa7c37..7d3215e 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -1100,13 +1100,17 @@ package body Sem_Util is
       Loc : constant Source_Ptr := Sloc (Expr);
    begin
 
-      --  An entity of a type with implicit dereference is overloaded with
+      --  An entity of a type with a reference aspect is overloaded with
       --  both interpretations: with and without the dereference. Now that
       --  the dereference is made explicit, set the type of the node properly,
-      --  to prevent anomalies in the backend.
+      --  to prevent anomalies in the backend. Same if the expression is an
+      --  overloaded function call whose return type has a reference aspect.
 
       if Is_Entity_Name (Expr) then
          Set_Etype (Expr, Etype (Entity (Expr)));
+
+      elsif Nkind (Expr) = N_Function_Call then
+         Set_Etype (Expr, Etype (Name (Expr)));
       end if;
 
       Set_Is_Overloaded (Expr, False);
@@ -9335,6 +9339,8 @@ package body Sem_Util is
                loop
                   --  If no matching formal, that's peculiar, some kind of
                   --  previous error, so return False to be conservative.
+                  --  Actually this also happens in legal code in the case
+                  --  where P is a parameter association for an Extra_Formal???
 
                   if No (Form) then
                      return False;
@@ -9640,6 +9646,8 @@ package body Sem_Util is
                loop
                   --  If no matching formal, that's peculiar, some kind of
                   --  previous error, so return True to be conservative.
+                  --  Actually happens with legal code for an unresolved call
+                  --  where we may get the wrong homonym???
 
                   if No (Form) then
                      return True;
diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl
index 296d431..3b3f8db 100644
--- a/gcc/ada/snames.ads-tmpl
+++ b/gcc/ada/snames.ads-tmpl
@@ -463,6 +463,7 @@ package Snames is
    Name_Complete_Representation        : constant Name_Id := N + $; -- GNAT
    Name_Complex_Representation         : constant Name_Id := N + $; -- GNAT
    Name_Contract_Case                  : constant Name_Id := N + $; -- GNAT
+   Name_Contract_Cases                 : constant Name_Id := N + $; -- GNAT
    Name_Controlled                     : constant Name_Id := N + $;
    Name_Convention                     : constant Name_Id := N + $;
    Name_CPP_Class                      : constant Name_Id := N + $; -- GNAT
@@ -1736,6 +1737,7 @@ package Snames is
       Pragma_Complete_Representation,
       Pragma_Complex_Representation,
       Pragma_Contract_Case,
+      Pragma_Contract_Cases,
       Pragma_Controlled,
       Pragma_Convention,
       Pragma_CPP_Class,