[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

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 5da6a9ea305bd01769a9df4a86ab1d4d25dccd82..0f2ae317a26e673e64a71efbc077c0c90d9d49ae 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,13 @@
+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

diff --git a/gcc/ada/errout.adb b/gcc/ada/errout.adb
index e6ef3a715d37ddf417e71b545b80ebf28b1fe5bf..aa07a6989dd98a6956ed686edde29a499968cecb 100644 (file)
--- a/gcc/ada/errout.adb
+++ b/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;

diff --git a/gcc/ada/errout.ads b/gcc/ada/errout.ads
index 0c363222c37d9d2df6b4f5861f704daaaa26c0c7..0973b6801cc83c9aa4721660c4eec2421a8537a5 100644 (file)
--- a/gcc/ada/errout.ads
+++ b/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

diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index c0475343e837e6e9dda94e51ad55212b968232f5..dc8090404366f09e34f551472bb04eb5da1a9e5c 100644 (file)
--- a/gcc/ada/sem_prag.adb
+++ b/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);