From 91952132ebb4f0adadf617af5dce4ecb03509591 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Thu, 10 Oct 2013 15:04:53 +0200 Subject: [PATCH] [multiple changes] 2013-10-10 Yannick Moy * errout.adb (Compilation_Errors): In formal verification mode, always return False. 2013-10-10 Hristian Kirtchev * sem_prag.adb (Collect_Hidden_States_In_Decls): Only consider source non-constant objects. From-SVN: r203372 --- gcc/ada/ChangeLog | 10 ++++++++++ gcc/ada/errout.adb | 9 +++++++++ gcc/ada/errout.ads | 8 +++++--- gcc/ada/sem_prag.adb | 7 ++++++- 4 files changed, 30 insertions(+), 4 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 5da6a9ea305..0f2ae317a26 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,13 @@ +2013-10-10 Yannick Moy + + * errout.adb (Compilation_Errors): In formal verification mode, + always return False. + +2013-10-10 Hristian Kirtchev + + * sem_prag.adb (Collect_Hidden_States_In_Decls): Only consider source + non-constant objects. + 2013-10-10 Hristian Kirtchev * aspects.adb: Add an entry in table Canonical_Aspect for diff --git a/gcc/ada/errout.adb b/gcc/ada/errout.adb index e6ef3a715d3..aa07a6989dd 100644 --- 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 0c363222c37..0973b6801cc 100644 --- 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 c0475343e83..dc809040436 100644 --- 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); -- 2.30.2