2014-02-19 Robert Dewar <dewar@adacore.com>
authorcharlet <charlet@138bc75d-0d04-0410-961f-82ee72b054a4>
Wed, 19 Feb 2014 11:05:35 +0000 (11:05 +0000)
committercharlet <charlet@138bc75d-0d04-0410-961f-82ee72b054a4>
Wed, 19 Feb 2014 11:05:35 +0000 (11:05 +0000)
* exp_util.adb: Update comments.

2014-02-19  Doug Rupp  <rupp@adacore.com>

* bindgen.adb (Gen_Adainit) [VMS] New global Float_Format.
* init.c (__gl_float_format): [VMS] New global.
(__gnat_set_features): Call FP_CONTROL to set FPSR for the float
representation in effect.

2014-02-19  Hristian Kirtchev  <kirtchev@adacore.com>

* exp_ch6.adb Add with and use clause for Exp_Prag.
(Expand_Contract_Cases): Relocated to Exp_Prag.
* exp_ch6.ads (Expand_Contract_Cases): Relocated to Exp_Prag.
* exp_prag.adb Add with and use clauses for Checks and Validsw.
(Expand_Contract_Cases): Relocated from Exp_Ch6. Update the
structure of the expanded code to showcase the evaluation of
attribute 'Old prefixes. Add local variable Old_Evals. Expand
any attribute 'Old references found within a consequence. Add
circuitry to evaluate the prefixes of attribute 'Old that
belong to a selected consequence.
(Expand_Old_In_Consequence): New routine.
* exp_prag.ads (Expand_Contract_Cases): Relocated from Exp_Ch6.
* sem_attr.adb (Check_Use_In_Contract_Cases): Warn that a
potentially unevaluated prefix is always evaluated.

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

gcc/ada/ChangeLog
gcc/ada/bindgen.adb
gcc/ada/exp_ch6.adb
gcc/ada/exp_ch6.ads
gcc/ada/exp_prag.adb
gcc/ada/exp_prag.ads
gcc/ada/exp_util.adb
gcc/ada/init.c
gcc/ada/sem_attr.adb

index e8f0c63..dba833b 100644 (file)
@@ -1,5 +1,33 @@
 2014-02-19  Robert Dewar  <dewar@adacore.com>
 
+       * exp_util.adb: Update comments.
+
+2014-02-19  Doug Rupp  <rupp@adacore.com>
+
+       * bindgen.adb (Gen_Adainit) [VMS] New global Float_Format.
+       * init.c (__gl_float_format): [VMS] New global.
+       (__gnat_set_features): Call FP_CONTROL to set FPSR for the float
+       representation in effect.
+
+2014-02-19  Hristian Kirtchev  <kirtchev@adacore.com>
+
+       * exp_ch6.adb Add with and use clause for Exp_Prag.
+       (Expand_Contract_Cases): Relocated to Exp_Prag.
+       * exp_ch6.ads (Expand_Contract_Cases): Relocated to Exp_Prag.
+       * exp_prag.adb Add with and use clauses for Checks and Validsw.
+       (Expand_Contract_Cases): Relocated from Exp_Ch6. Update the
+       structure of the expanded code to showcase the evaluation of
+       attribute 'Old prefixes. Add local variable Old_Evals. Expand
+       any attribute 'Old references found within a consequence. Add
+       circuitry to evaluate the prefixes of attribute 'Old that
+       belong to a selected consequence.
+       (Expand_Old_In_Consequence): New routine.
+       * exp_prag.ads (Expand_Contract_Cases): Relocated from Exp_Ch6.
+       * sem_attr.adb (Check_Use_In_Contract_Cases): Warn that a
+       potentially unevaluated prefix is always evaluated.
+
+2014-02-19  Robert Dewar  <dewar@adacore.com>
+
        * exp_attr.adb (Expand_Min_Max_Attribute): Use Insert_Declaration
        (Expand_Min_Max_Attribute): Use Matching_Standard_Type.
        * exp_ch4.adb (Expand_N_Expression_With_Actions): Remove special
index 7174144..270aa5e 100644 (file)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2012, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2013, 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- --
@@ -132,7 +132,7 @@ package body Bindgen is
    -- Run-Time Globals --
    ----------------------
 
-   --  This section documents the global variables that set from the
+   --  This section documents the global variables that are set from the
    --  generated binder file.
 
    --     Main_Priority                 : Integer;
@@ -167,6 +167,9 @@ package body Bindgen is
    --  -Hnn parameter for the binder or by the GNAT$NO_MALLOC_64 logical.
    --  Valid values are 32 and 64. This switch is only effective on VMS.
 
+   --  Float_Format is the float representation in use. Valid values are
+   --  'I' for IEEE and 'V' for VAX Float. This is only for VMS.
+
    --  WC_Encoding shows the wide character encoding method used for the main
    --  program. This is one of the encoding letters defined in
    --  System.WCh_Con.WC_Encoding_Letters.
@@ -677,6 +680,13 @@ package body Bindgen is
 
                Write_Statement_Buffer;
             end if;
+
+            WBI ("");
+            WBI ("      Float_Format : Character;");
+            WBI ("      pragma Import (C, Float_Format, " &
+                    """__gl_float_format"");");
+
+            Write_Statement_Buffer;
          end if;
 
          --  Initialize stack limit variable of the environment task if the
@@ -868,6 +878,25 @@ package body Bindgen is
          --  Generate call to Set_Features
 
          if OpenVMS_On_Target then
+
+            --  Set_Features will call IEEE$SET_FP_CONTROL appropriately
+            --  depending on the setting of Float_Format.
+
+            WBI ("");
+            Set_String ("      Float_Format := '");
+
+            if Float_Format_Specified = 'G'
+                 or else
+               Float_Format_Specified = 'D'
+            then
+               Set_Char ('V');
+            else
+               Set_Char ('I');
+            end if;
+
+            Set_String ("';");
+            Write_Statement_Buffer;
+
             WBI ("");
             WBI ("      if Features_Set = 0 then");
             WBI ("         Set_Features;");
index e1c4722..ccf8579 100644 (file)
@@ -41,6 +41,7 @@ with Exp_Disp; use Exp_Disp;
 with Exp_Dist; use Exp_Dist;
 with Exp_Intr; use Exp_Intr;
 with Exp_Pakd; use Exp_Pakd;
+with Exp_Prag; use Exp_Prag;
 with Exp_Tss;  use Exp_Tss;
 with Exp_Util; use Exp_Util;
 with Exp_VFpt; use Exp_VFpt;
@@ -4118,476 +4119,6 @@ package body Exp_Ch6 is
       end if;
    end Expand_Call;
 
-   ---------------------------
-   -- 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 "xxx 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;
-      Decls   : List_Id;
-      Stmts   : in out List_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_Implicit_If_Statement (CCs,
-                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)));
-      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;
-      Multiple_PCs  : Boolean;
-      Others_Flag   : Entity_Id := Empty;
-      Post_Case     : Node_Id;
-
-   --  Start of processing for Expand_Contract_Cases
-
-   begin
-      --  Do nothing if pragma is not enabled. If pragma is disabled, it has
-      --  already been rewritten as a Null statement.
-
-      if Is_Ignored (CCs) then
-         return;
-
-      --  Guard against malformed contract cases
-
-      elsif Nkind (Aggr) /= N_Aggregate then
-         return;
-      end if;
-
-      Multiple_PCs := List_Length (Component_Associations (Aggr)) > 1;
-
-      --  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 and Exception_Extra_Info 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_Implicit_If_Statement (CCs,
-                Condition       => Relocate_Node (Case_Guard),
-                Then_Statements => New_List (
-                  Set (Flag),
-                  Increment (Count))));
-
-            --  Check whether this case guard overlaps with another one
-
-            if Multiple_PCs and Exception_Extra_Info 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
-              (Checks => Conseq_Checks,
-               Flag   => Flag,
-               Conseq => 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 Assertion_Error with "xxx contract cases incomplete";
-
-      else
-         Start_String;
-         Store_String_Chars (Build_Location_String (Loc));
-         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_Implicit_If_Statement (CCs,
-          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 (Stmts) then
-         Stmts := New_List;
-      end if;
-
-      Append_To (Stmts, Conseq_Checks);
-   end Expand_Contract_Cases;
-
    -------------------------------
    -- Expand_Ctrl_Function_Call --
    -------------------------------
index 02cca24..8cdd6fa 100644 (file)
@@ -71,17 +71,6 @@ package Exp_Ch6 is
    --  This procedure contains common processing for Expand_N_Function_Call,
    --  Expand_N_Procedure_Statement, and Expand_N_Entry_Call.
 
-   procedure Expand_Contract_Cases
-     (CCs     : Node_Id;
-      Subp_Id : Entity_Id;
-      Decls   : List_Id;
-      Stmts   : in out List_Id);
-   --  Given pragma Contract_Cases CCs, create the circuitry needed to evaluate
-   --  case guards and trigger consequence expressions. Subp_Id is the related
-   --  subprogram for which the pragma applies. Decls are the declarations of
-   --  Subp_Id's body. All generated code is added to list Stmts. If Stmts is
-   --  empty, a new list is created.
-
    procedure Expand_Subprogram_Contract
      (N       : Node_Id;
       Spec_Id : Entity_Id;
index 976e0ea..f477b8e 100644 (file)
@@ -25,6 +25,7 @@
 
 with Atree;    use Atree;
 with Casing;   use Casing;
+with Checks;   use Checks;
 with Debug;    use Debug;
 with Einfo;    use Einfo;
 with Errout;   use Errout;
@@ -50,6 +51,7 @@ with Stand;    use Stand;
 with Targparm; use Targparm;
 with Tbuild;   use Tbuild;
 with Uintp;    use Uintp;
+with Validsw;  use Validsw;
 
 package body Exp_Prag is
 
@@ -148,6 +150,645 @@ package body Exp_Prag is
       end if;
    end Arg3;
 
+   ---------------------------
+   -- Expand_Contract_Cases --
+   ---------------------------
+
+   --  Pragma Contract_Cases is expanded in the following manner:
+
+   --    subprogram S is
+   --       Count    : Natural := 0;
+   --       Flag_1   : Boolean := False;
+   --       . . .
+   --       Flag_N   : Boolean := False;
+   --       Flag_N+1 : Boolean := False;  --  when "others" present
+   --       Pref_1   : ...;
+   --       . . .
+   --       Pref_M   : ...;
+
+   --       <preconditions (if any)>
+
+   --       --  Evaluate all case guards
+
+   --       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;
+
+   --       --  Emit errors depending on the number of case guards that
+   --       --  evaluated to True.
+
+   --       if Count = 0 then
+   --          raise Assertion_Error with "xxx 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;
+
+   --       --  Evaluate all attribute 'Old prefixes found in the selected
+   --       --  consequence.
+
+   --       if Flag_1 then
+   --          Pref_1 := <prefix of 'Old found in Consequence_1>
+   --       . . .
+   --       elsif Flag_N then
+   --          Pref_M := <prefix of 'Old found in Consequence_N>
+   --       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;
+      Decls   : List_Id;
+      Stmts   : in out List_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;
+
+      procedure Expand_Old_In_Consequence
+        (Decls  : List_Id;
+         Evals  : in out Node_Id;
+         Flag   : Entity_Id;
+         Conseq : Node_Id);
+      --  Perform specialized expansion of all attribute 'Old references found
+      --  in consequence Conseq such that at runtime only prefixes coming from
+      --  the selected consequence are evaluated. Any temporaries generated in
+      --  the process are added to declarative list Decls. Evals is a complex
+      --  if statement tasked with the evaluation of all prefixes coming from
+      --  a selected consequence. Flag is the corresponding case guard flag.
+      --  Conseq is the consequence expression.
+
+      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_Implicit_If_Statement (CCs,
+                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;
+
+      -------------------------------
+      -- Expand_Old_In_Consequence --
+      -------------------------------
+
+      procedure Expand_Old_In_Consequence
+        (Decls  : List_Id;
+         Evals  : in out Node_Id;
+         Flag   : Entity_Id;
+         Conseq : Node_Id)
+      is
+         Eval_Stmts : List_Id := No_List;
+         --  The evaluation sequence expressed as assignment statements of all
+         --  prefixes of attribute 'Old found in the current consequence.
+
+         function Expand_Old (N : Node_Id) return Traverse_Result;
+         --  Determine whether an arbitrary node denotes attribute 'Old and if
+         --  it does, perform all expansion-related actions.
+
+         ----------------
+         -- Expand_Old --
+         ----------------
+
+         function Expand_Old (N : Node_Id) return Traverse_Result is
+            Decl : Node_Id;
+            Pref : Node_Id;
+            Temp : Entity_Id;
+
+         begin
+            if Nkind (N) = N_Attribute_Reference
+              and then Attribute_Name (N) = Name_Old
+            then
+               Pref := Prefix (N);
+               Temp := Make_Temporary (Loc, 'T', Pref);
+
+               --  Generate a temporary to capture the value of the prefix:
+               --    Temp : <Pref type>;
+
+               Decl :=
+                 Make_Object_Declaration (Loc,
+                   Defining_Identifier => Temp,
+                   Object_Definition   =>
+                     New_Reference_To (Etype (Pref), Loc));
+               Set_No_Initialization (Decl);
+
+               Append_To (Decls, Decl);
+
+               --  Evaluate the prefix, generate:
+               --    Temp := <Pref>;
+
+               if No (Eval_Stmts) then
+                  Eval_Stmts := New_List;
+               end if;
+
+               Append_To (Eval_Stmts,
+                 Make_Assignment_Statement (Loc,
+                   Name       => New_Reference_To (Temp, Loc),
+                   Expression => Pref));
+
+               --  Ensure that the prefix is valid
+
+               if Validity_Checks_On and then Validity_Check_Operands then
+                  Ensure_Valid (Pref);
+               end if;
+
+               --  Replace the original attribute 'Old by a reference to the
+               --  generated temporary.
+
+               Rewrite (N, New_Reference_To (Temp, Loc));
+            end if;
+
+            return OK;
+         end Expand_Old;
+
+         procedure Expand_Olds is new Traverse_Proc (Expand_Old);
+
+      --  Start of processing for Expand_Old_In_Consequence
+
+      begin
+         --  Inspect the consequence and expand any attribute 'Old references
+         --  found within.
+
+         Expand_Olds (Conseq);
+
+         --  Augment the machinery to trigger the evaluation of all prefixes
+         --  found in the step above. If Eval is empty, then this is the first
+         --  consequence to yield expansion of 'Old. Generate:
+
+         --    if Flag then
+         --       <evaluation statements>
+         --    end if;
+
+         if No (Evals) then
+            Evals :=
+              Make_Implicit_If_Statement (CCs,
+                Condition       => New_Reference_To (Flag, Loc),
+                Then_Statements => Eval_Stmts);
+
+         --  Otherwise generate:
+         --    elsif Flag then
+         --       <evaluation statements>
+         --    end if;
+
+         else
+            if No (Elsif_Parts (Evals)) then
+               Set_Elsif_Parts (Evals, New_List);
+            end if;
+
+            Append_To (Elsif_Parts (Evals),
+              Make_Elsif_Part (Loc,
+                Condition       => New_Reference_To (Flag, Loc),
+                Then_Statements => Eval_Stmts));
+         end if;
+      end Expand_Old_In_Consequence;
+
+      ---------------
+      -- 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)));
+      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;
+      Multiple_PCs  : Boolean;
+      Old_Evals     : Node_Id   := Empty;
+      Others_Flag   : Entity_Id := Empty;
+      Post_Case     : Node_Id;
+
+   --  Start of processing for Expand_Contract_Cases
+
+   begin
+      --  Do nothing if pragma is not enabled. If pragma is disabled, it has
+      --  already been rewritten as a Null statement.
+
+      if Is_Ignored (CCs) then
+         return;
+
+      --  Guard against malformed contract cases
+
+      elsif Nkind (Aggr) /= N_Aggregate then
+         return;
+      end if;
+
+      Multiple_PCs := List_Length (Component_Associations (Aggr)) > 1;
+
+      --  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 and Exception_Extra_Info then
+               Case_Guard_Error
+                 (Decls     => Error_Decls,
+                  Flag      => Others_Flag,
+                  Error_Loc => Sloc (Case_Guard),
+                  Msg       => Msg_Str);
+            end if;
+
+            --  Inspect the consequence and perform special expansion of any
+            --  attribute 'Old references found within.
+
+            Expand_Old_In_Consequence
+              (Decls  => Decls,
+               Evals  => Old_Evals,
+               Flag   => Others_Flag,
+               Conseq => Conseq);
+
+            --  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_Implicit_If_Statement (CCs,
+                Condition       => Relocate_Node (Case_Guard),
+                Then_Statements => New_List (
+                  Set (Flag),
+                  Increment (Count))));
+
+            --  Check whether this case guard overlaps with another one
+
+            if Multiple_PCs and Exception_Extra_Info then
+               Case_Guard_Error
+                 (Decls     => Error_Decls,
+                  Flag      => Flag,
+                  Error_Loc => Sloc (Case_Guard),
+                  Msg       => Msg_Str);
+            end if;
+
+            --  Inspect the consequence and perform special expansion of any
+            --  attribute 'Old references found within.
+
+            Expand_Old_In_Consequence
+              (Decls  => Decls,
+               Evals  => Old_Evals,
+               Flag   => Flag,
+               Conseq => Conseq);
+
+            --  The corresponding consequence of the case guard which evaluated
+            --  to True must hold on exit from the subprogram.
+
+            Consequence_Error
+              (Checks => Conseq_Checks,
+               Flag   => Flag,
+               Conseq => 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 Assertion_Error with "xxx contract cases incomplete";
+
+      else
+         Start_String;
+         Store_String_Chars (Build_Location_String (Loc));
+         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_Implicit_If_Statement (CCs,
+          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);
+
+      --  Once all case guards are evaluated and checked, evaluate any prefixes
+      --  of attribute 'Old founds in the selected consequence.
+
+      Append_To (Decls, Old_Evals);
+
+      --  Raise Assertion_Error when the corresponding consequence of a case
+      --  guard that evaluated to True fails.
+
+      if No (Stmts) then
+         Stmts := New_List;
+      end if;
+
+      Append_To (Stmts, Conseq_Checks);
+   end Expand_Contract_Cases;
+
    ---------------------
    -- Expand_N_Pragma --
    ---------------------
index e995501..681f116 100644 (file)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2007, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2013, 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- --
@@ -31,4 +31,15 @@ package Exp_Prag is
 
    procedure Expand_N_Pragma (N : Node_Id);
 
+   procedure Expand_Contract_Cases
+     (CCs     : Node_Id;
+      Subp_Id : Entity_Id;
+      Decls   : List_Id;
+      Stmts   : in out List_Id);
+   --  Given pragma Contract_Cases CCs, create the circuitry needed to evaluate
+   --  case guards and trigger consequence expressions. Subp_Id is the related
+   --  subprogram for which the pragma applies. Decls are the declarations of
+   --  Subp_Id's body. All generated code is added to list Stmts. If Stmts is
+   --  No_List on entry, a new list is created.
+
 end Exp_Prag;
index 251e919..ff18d08 100644 (file)
@@ -7981,6 +7981,13 @@ package body Exp_Util is
                 Side_Effect_Free
                   (First (Parameter_Associations (N)), Name_Req, Variable_Ref);
 
+         --  An IF expression is side effect free if its components are all
+         --  side effect free (conditions and then actions and else actions).
+
+         --  when N_If_Expression =>
+         --  return Side_Effect_Free (Expressions (N), Name_Req, Variable_Ref);
+         --  commented out for now, caused some crashes ???
+
          --  An indexed component is side effect free if it is a side
          --  effect free prefixed reference and all the indexing
          --  expressions are side effect free.
index e943837..d61086e 100644 (file)
@@ -1508,6 +1508,14 @@ __gnat_set_stack_limit (void)
 #endif
 }
 
+#ifdef IN_RTS
+extern int SYS$IEEE_SET_FP_CONTROL (void *, void *, void *);
+#define K_TRUE 1
+#define __int64 long long
+#define __NEW_STARLET
+#include <vms/ieeedef.h>
+#endif
+
 /* Feature logical name and global variable address pair.
    If we ever add another feature logical to this list, the
    feature struct will need to be enhanced to take into account
@@ -1517,9 +1525,21 @@ struct feature {
   int *gl_addr;
 };
 
-/* Default values for GNAT features set by environment.  */
+/* Default values for GNAT features set by environment or binder.  */
 int __gl_heap_size = 64;
 
+/* Default float format is 'I' meaning IEEE.  If gnatbind detetcts that a
+   VAX Float format is specified, it will set this global variable to 'V'.
+   Subsequently __gnat_set_features will test the variable and if set for
+   VAX Float will call a Starlet function to enable trapping for invalid
+   operation, drivide by zero, and overflow. This will prevent the VMS runtime
+   (specifically OTS$CHECK_FP_MODE) from complaining about inconsistent
+   floating point settings in a mixed language program. Ideally the setting
+   would be determined at link time based on setttings in the object files,
+   however the VMS linker seems to take the setting from the first object
+   in the link, e.g. pcrt0.o which is float representation neutral.  */
+char __gl_float_format = 'I';
+
 /* Array feature logical names and global variable addresses.  */
 static const struct feature features[] =
 {
@@ -1532,6 +1552,12 @@ __gnat_set_features (void)
 {
   int i;
   char buff[16];
+#ifdef IN_RTS
+  IEEE clrmsk, setmsk, prvmsk;
+
+  clrmsk.ieee$q_flags = 0LL;
+  setmsk.ieee$q_flags = 0LL;
+#endif
 
   /* Loop through features array and test name for enable/disable.  */
   for (i = 0; features[i].name; i++)
@@ -1551,6 +1577,16 @@ __gnat_set_features (void)
   /* Features to artificially limit the stack size.  */
   __gnat_set_stack_limit ();
 
+#ifdef IN_RTS
+  if (__gl_float_format == 'V')
+    {
+      setmsk.ieee$v_trap_enable_inv = K_TRUE;
+      setmsk.ieee$v_trap_enable_dze = K_TRUE;
+      setmsk.ieee$v_trap_enable_ovf = K_TRUE;
+      SYS$IEEE_SET_FP_CONTROL (&clrmsk, &setmsk, &prvmsk);
+    }
+#endif
+
   __gnat_features_set = 1;
 }
 
index b25bf17..3e39d3a 100644 (file)
@@ -4466,7 +4466,22 @@ package body Sem_Attr is
             --  contract case as this is the only postcondition-like part of
             --  the pragma.
 
-            if Expr /= Expression (Parent (Expr)) then
+            if Expr = Expression (Parent (Expr)) then
+
+               --  Warn that a potentially unevaluated prefix is always
+               --  evaluated when the corresponding consequence is selected.
+
+               if Is_Potentially_Unevaluated (P) then
+                  Error_Msg_Name_1 := Aname;
+                  Error_Msg_N
+                    ("?prefix of attribute % is always evaluated when "
+                     & "related consequence is selected", P);
+               end if;
+
+            --  Attribute 'Old appears in the condition of a contract case.
+            --  Emit an error since this is not a postcondition-like context.
+
+            else
                Error_Attr
                  ("attribute % cannot appear in the condition of a contract "
                   & "case (SPARK RM 6.1.3(2))", P);