diff options
| author | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2017-09-25 09:24:26 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2017-09-25 09:24:26 +0000 |
| commit | f71b4cd44483310677019f5d47cabbdeedfcfc75 (patch) | |
| tree | cab437b38002c96a86377eab7c6057ea7acb7267 /gcc/ada/sem_prag.ads | |
| parent | e98cd75fc3322a267173010e07bb11c6bdb674d1 (diff) | |
| download | gcc-f71b4cd44483310677019f5d47cabbdeedfcfc75.zip gcc-f71b4cd44483310677019f5d47cabbdeedfcfc75.tar.gz gcc-f71b4cd44483310677019f5d47cabbdeedfcfc75.tar.bz2 | |
[multiple changes]
2017-09-25 Hristian Kirtchev <kirtchev@adacore.com>
* sem_res.adb (Replace_Actual_Discriminants): Replace a discriminant
for GNATprove.
(Resolve_Entry): Clean up predicate
2017-09-25 Hristian Kirtchev <kirtchev@adacore.com>
* sem_prag.adb (Analyze_Constituent): Raise Unrecoverable_Error rather
than Program_Error because U_E is more in line with respect to the
intended behavior.
2017-09-25 Ed Schonberg <schonberg@adacore.com>
* sem_ch13.adb (Resolve_Aspect_Expressions): The expression for aspect
Storage_Size does not freeze, and thus can include references to
deferred constants.
2017-09-25 Hristian Kirtchev <kirtchev@adacore.com>
* exp_spark.adb (Expand_SPARK_Potential_Renaming): Do not process a
reference when it appears within a pragma of no significance to SPARK.
(In_Insignificant_Pragma): New routine.
* sem_prag.ads: Add new table Pragma_Significant_In_SPARK.
2017-09-25 Ed Schonberg <schonberg@adacore.com>
* sem_ch12.adb (Analyze_Associations, case N_Formal_Package): If the
actual is a renaming, indicate that it is the renamed package that must
be frozen before the instantiation.
2017-09-25 Yannick Moy <moy@adacore.com>
* doc/gnat_ugn/gnat_and_program_execution.rst: Fix typo in description
of dimensionality system in GNAT UG.
* gnat_ugn.texi: Regenerate.
2017-09-25 Yannick Moy <moy@adacore.com>
* gnat1drv.adb: Call Check_Safe_Pointers from the frontend in
GNATprove_Mode when switch -gnatdF used.
2017-09-25 Piotr Trojanek <trojanek@adacore.com>
* adabkend.adb (Call_Back_End): Reset Current_Error_Node when starting
the backend.
From-SVN: r253140
Diffstat (limited to 'gcc/ada/sem_prag.ads')
| -rw-r--r-- | gcc/ada/sem_prag.ads | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads index ff4a1cb..33dbe48 100644 --- a/gcc/ada/sem_prag.ads +++ b/gcc/ada/sem_prag.ads @@ -175,6 +175,25 @@ package Sem_Prag is Pragma_Warnings => True, others => False); + -- The following table lists all pragmas which are significant in SPARK and + -- as a result get translated into verification conditions. The table is an + -- amalgamation of the pragmas listed in SPARK RM 16.1 and internally added + -- entries. + + Pragma_Significant_In_SPARK : constant array (Pragma_Id) of Boolean := + (Pragma_All_Calls_Remote => False, + Pragma_Asynchronous => False, + Pragma_Default_Storage_Pool => False, + Pragma_Discard_Names => False, + Pragma_Dispatching_Domain => False, + Pragma_Priority_Specific_Dispatching => False, + Pragma_Remote_Call_Interface => False, + Pragma_Remote_Types => False, + Pragma_Shared_Passive => False, + Pragma_Task_Dispatching_Policy => False, + Pragma_Warnings => False, + others => True); + ----------------- -- Subprograms -- ----------------- |