diff options
| author | Arnaud Charlet <charlet@gcc.gnu.org> | 2017-09-07 11:40:16 +0200 |
|---|---|---|
| committer | Arnaud Charlet <charlet@gcc.gnu.org> | 2017-09-07 11:40:16 +0200 |
| commit | 1155ae01593b0b84cddf5031b7a85d684fe0dd0d (patch) | |
| tree | 317aae64851186240dd41fa497b899b1e385b800 /gcc/ada/ghost.adb | |
| parent | 0691ed6bd62582c22a33c42aa8f5303815a032af (diff) | |
| download | gcc-1155ae01593b0b84cddf5031b7a85d684fe0dd0d.zip gcc-1155ae01593b0b84cddf5031b7a85d684fe0dd0d.tar.gz gcc-1155ae01593b0b84cddf5031b7a85d684fe0dd0d.tar.bz2 | |
[multiple changes]
2017-09-07 Arnaud Charlet <charlet@adacore.com>
* sem_prag.adb (Find_Role): The Global_Seen flag
is now consulted not only for abstract states and variables,
but for all kinds of items.
(Collect_Subprogram_Inputs_Outputs): Do not process formal
generic parameters, because unlike ordinary formal parameters,
generic formals only act as input/ outputs if they are explicitly
mentioned in a Global contract.
2017-09-07 Yannick Moy <moy@adacore.com>
* ghost.adb (Check_Ghost_Context): Do not err on ghost code inside
predicate procedure. Check predicate pragma/aspect with Ghost entity.
* exp_ch6.adb, par-ch6.adb, sem_ch13.adb, sem_prag.adb; Minor
reformatting.
2017-09-07 Ed Schonberg <schonberg@adacore.com>
* sem_aggr.adb: Move New_Copy_Tree_And_Dimensions to sem_dim
(code cleanup);
* sem_ch3.adb (Build_Derived_Record_Type):i Call
Copy_Dimensions_Of_Components after creating the copy of the
record declaration.
* sem_dim.ads, sem_dim.adb (Copy_Dimensions_Of_Components): For a
derived recor type, copy the dikensions if any of each component
of the parent record to the corresponding component declarations
of the derived record. These expressions are used among other
things as default values in aggregates with box associations.
* a-dirval-mingw.adb, g-cgi.adb, gnatcmd.adb, lib-xref.adb,
repinfo.adb, sem_attr.adb, sem_ch10.adb, sem_ch6.adb, sem_prag.adb:
Minor reformatting.
2017-09-07 Arnaud Charlet <charlet@adacore.com>
* sem_util.adb: Remove extra space after THEN.
2017-09-07 Eric Botcazou <ebotcazou@adacore.com>
* sem_ch7.adb (Has_Referencer): For a subprogram renaming,
also mark the renamed subprogram as referenced.
From-SVN: r251836
Diffstat (limited to 'gcc/ada/ghost.adb')
| -rw-r--r-- | gcc/ada/ghost.adb | 28 |
1 files changed, 22 insertions, 6 deletions
diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb index beb05f4..78ba5f3 100644 --- a/gcc/ada/ghost.adb +++ b/gcc/ada/ghost.adb @@ -281,6 +281,13 @@ package body Ghost is if Chars (Subp_Id) = Name_uPostconditions then return True; + -- The context is the internally built predicate function, + -- which is OK because the real check was done before the + -- predicate function was generated. + + elsif Is_Predicate_Function (Subp_Id) then + return True; + else Subp_Decl := Original_Node (Unit_Declaration_Node (Subp_Id)); @@ -362,10 +369,12 @@ package body Ghost is return True; -- An assertion expression pragma is Ghost when it contains a - -- reference to a Ghost entity (SPARK RM 6.9(10)). - - elsif Assertion_Expression_Pragma (Prag_Id) then + -- reference to a Ghost entity (SPARK RM 6.9(10)), except for + -- predicate pragmas (SPARK RM 6.9(11)). + elsif Assertion_Expression_Pragma (Prag_Id) + and then Prag_Id /= Pragma_Predicate + then -- Ensure that the assertion policy and the Ghost policy are -- compatible (SPARK RM 6.9(18)). @@ -464,9 +473,16 @@ package body Ghost is return True; -- A reference to a Ghost entity can appear within an aspect - -- specification (SPARK RM 6.9(10)). - - elsif Nkind (Par) = N_Aspect_Specification then + -- specification (SPARK RM 6.9(10)). The precise checking will + -- occur when analyzing the corresponding pragma. We make an + -- exception for predicate aspects that only allow referencing + -- a Ghost entity when the corresponding type declaration is + -- Ghost (SPARK RM 6.9(11)). + + elsif Nkind (Par) = N_Aspect_Specification + and then not Same_Aspect + (Get_Aspect_Id (Par), Aspect_Predicate) + then return True; elsif Is_OK_Declaration (Par) then |