[multiple changes]

2013-10-10  Yannick Moy  <moy@adacore.com>

	* errout.adb (Compilation_Errors): In formal verification mode,
	always return False.

2013-10-10  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_prag.adb (Collect_Hidden_States_In_Decls): Only consider source
	non-constant objects.

From-SVN: r203372

gcc/ada/ChangeLog

+2013-10-10  Yannick Moy  <moy@adacore.com>
+
+	* errout.adb (Compilation_Errors): In formal verification mode,
+	always return False.
+
+2013-10-10  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* sem_prag.adb (Collect_Hidden_States_In_Decls): Only consider source
+	non-constant objects.
+
 2013-10-10  Hristian Kirtchev  <kirtchev@adacore.com>
 
 	* aspects.adb: Add an entry in table Canonical_Aspect for

gcc/ada/errout.adb

@@ -233,6 +233,15 @@ package body Errout is
    begin
       if not Finalize_Called then
          raise Program_Error;
+
+      --  In formal verification mode, errors issued when generating Why code
+      --  are not compilation errors, and should not result in exiting with
+      --  an error status. These errors are handled in the driver of the
+      --  verification process instead.
+
+      elsif SPARK_Mode and not Frame_Condition_Mode then
+         return False;
+
       else
          return Erroutc.Compilation_Errors;
       end if;

gcc/ada/errout.ads

@@ -813,9 +813,11 @@ package Errout is
    --  matching Warnings Off pragma preceding this one.
 
    function Compilation_Errors return Boolean;
-   --  Returns true if errors have been detected, or warnings in -gnatwe
-   --  (treat warnings as errors) mode. Note that it is mandatory to call
-   --  Finalize before calling this routine.
+   --  Returns True if errors have been detected, or warnings in -gnatwe (treat
+   --  warnings as errors) mode. Note that it is mandatory to call Finalize
+   --  before calling this routine. Always returns False in formal verification
+   --  mode, because errors issued when generating Why code are not compilation
+   --  errors, and should not result in exiting with an error status.
 
    procedure Error_Msg_CRT (Feature : String; N : Node_Id);
    --  Posts a non-fatal message on node N saying that the feature identified

gcc/ada/sem_prag.adb

@@ -18889,10 +18889,15 @@ package body Sem_Prag is
             Decl := First (Decls);
             while Present (Decl) loop
 
-               --  Objects (non-constants) are valid hidden states
+               --  Source objects (non-constants) are valid hidden states
+
+               --  This is a very odd test, it misses many cases, e.g.
+               --  renamings of objects, in-out parameters etc ???. Why
+               --  not test the Ekind ???
 
                if Nkind (Decl) = N_Object_Declaration
                  and then not Constant_Present (Decl)
+                 and then Comes_From_Source (Decl)
                then
                   Add_Item (Defining_Entity (Decl), Result);