diff options
| author | Hristian Kirtchev <kirtchev@adacore.com> | 2014-02-24 17:07:48 +0000 |
|---|---|---|
| committer | Arnaud Charlet <charlet@gcc.gnu.org> | 2014-02-24 18:07:48 +0100 |
| commit | 2dade09735a63a5bd57e353bc02d99b2991aa441 (patch) | |
| tree | 9875799cdb5f5c19cd90b9c5af60bc4c90c5602e /gcc/ada/g-sercom-linux.adb | |
| parent | 158d55fa393867c794df5aa43b693f61e5916b83 (diff) | |
| download | gcc-2dade09735a63a5bd57e353bc02d99b2991aa441.zip gcc-2dade09735a63a5bd57e353bc02d99b2991aa441.tar.gz gcc-2dade09735a63a5bd57e353bc02d99b2991aa441.tar.bz2 | |
sem_ch6.adb (Analyze_Subprogram_Body_Contract): Do not enforce global and dependence refinement when SPARK_Mode is off.
2014-02-24 Hristian Kirtchev <kirtchev@adacore.com>
* sem_ch6.adb (Analyze_Subprogram_Body_Contract): Do not enforce
global and dependence refinement when SPARK_Mode is off.
* sem_ch7.adb (Analyze_Package_Body_Contract): Do not enforce
state refinement when SPARK_Mode is off.
* sem_ch13.adb (Analyze_Aspect_Specifications): Add local
variable Decl. Insert the generated pragma for Refined_State
after a potential pragma SPARK_Mode.
* sem_prag.adb (Analyze_Depends_In_Decl_Part): Add local
constant Deps. Remove local variable Expr. Check the syntax
of pragma Depends when SPARK_Mode is off. Factor out the
processing for extra parenthesis around individual clauses.
(Analyze_Global_In_Decl_List): Items is now a constant. Check
the syntax of pragma Global when SPARK_Mode is off.
(Analyze_Initializes_In_Decl_Part): Check the syntax of pragma
Initializes when SPARK_Mode is off.
(Analyze_Part_Of): Check
the syntax of the encapsulating state when SPARK_Mode is off.
(Analyze_Pragma): Check the syntax of pragma Abstract_State when
SPARK_Mode is off. Move the declaration order check with respect
to pragma Initializes to the end of the processing. Do not verify
the declaration order for pragma Initial_Condition when SPARK_Mode
is off. Do not complain about a useless package refinement when
SPARK_Mode is off.
(Analyze_Refined_Depends_In_Decl_Part): Refs
is now a constant. Check the syntax of pragma Refined_Depends
when SPARK_Mode is off.
(Analyze_Refined_Global_In_Decl_Part):
Check the syntax of pragma Refined_Global when SPARK_Mode is off.
(Analyze_Refined_State_In_Decl_Part): Check the syntax of pragma
Refined_State when SPARK_Mode is off.
(Check_Dependence_List_Syntax): New routine.
(Check_Global_List_Syntax): New routine.
(Check_Initialization_List_Syntax): New routine.
(Check_Item_Syntax): New routine.
(Check_State_Declaration_Syntax): New routine.
(Check_Refinement_List_Syntax): New routine.
(Has_Extra_Parentheses): Moved to the top level of Sem_Prag.
From-SVN: r208087
Diffstat (limited to 'gcc/ada/g-sercom-linux.adb')
0 files changed, 0 insertions, 0 deletions