diff options
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/ChangeLog | 10 | ||||
| -rw-r--r-- | gcc/ada/errout.adb | 9 | ||||
| -rw-r--r-- | gcc/ada/errout.ads | 8 | ||||
| -rw-r--r-- | gcc/ada/sem_prag.adb | 7 |
4 files changed, 30 insertions, 4 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 5da6a9e..0f2ae31 100644 --- 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 e6ef3a7..aa07a69 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 0c36322..0973b68 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 c047534..dc80904 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); |