diff options
| author | Yannick Moy <moy@adacore.com> | 2021-09-29 15:26:54 +0200 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2021-12-01 10:24:39 +0000 |
| commit | aeaabe7b3cb0ca9b9426468afb838f3d84126349 (patch) | |
| tree | bddc1a3adf94843aac74de2d5196959d59ca7a6a /gcc/modulo-sched.c | |
| parent | 7b4069fb7c00564523f822c7fd94210862eeeae4 (diff) | |
| download | gcc-aeaabe7b3cb0ca9b9426468afb838f3d84126349.zip gcc-aeaabe7b3cb0ca9b9426468afb838f3d84126349.tar.gz gcc-aeaabe7b3cb0ca9b9426468afb838f3d84126349.tar.bz2 | |
[Ada] Improve messages on incorrect state refinement in SPARK
gcc/ada/
* sem_ch10.adb (Is_Private_Library_Unit): Move query to
Sem_Util for sharing.
* sem_ch7.adb (Analyze_Package_Body_Helper): Add continuation
message.
* sem_prag.adb (Analyze_Part_Of): Call new function
Is_Private_Library_Unit.
(Check_Valid_Library_Unit_Pragma): Specialize error messages on
misplaced pragmas.
(Analyze_Refined_State_In_Decl_Part): Recognize missing Part_Of
on object in private part.
* sem_util.adb (Check_State_Refinements): Add continuation
message.
(Find_Placement_In_State_Space): Fix detection of placement,
which relied wrongly on queries In_Package_Body/In_Private_Part
which do not provide the right information here for all cases.
(Is_Private_Library_Unit): Move query here for sharing.
* sem_util.ads (Is_Private_Library_Unit): Move query here for
sharing.
Diffstat (limited to 'gcc/modulo-sched.c')
0 files changed, 0 insertions, 0 deletions