diff options
| author | Arnaud Charlet <charlet@gcc.gnu.org> | 2014-01-20 14:52:19 +0100 |
|---|---|---|
| committer | Arnaud Charlet <charlet@gcc.gnu.org> | 2014-01-20 14:52:19 +0100 |
| commit | aca90db9e258f2c5644ead687d604337839f0db0 (patch) | |
| tree | cf6bf18d53a5d2fe4198bf0c7c668af20741f2b4 /gcc/ada/spark_xrefs.ads | |
| parent | dc72675740ac7e955a2ae13855da45f7818686ae (diff) | |
| download | gcc-aca90db9e258f2c5644ead687d604337839f0db0.zip gcc-aca90db9e258f2c5644ead687d604337839f0db0.tar.gz gcc-aca90db9e258f2c5644ead687d604337839f0db0.tar.bz2 | |
[multiple changes]
2014-01-20 Hristian Kirtchev <kirtchev@adacore.com>
* einfo.ads: E_Abstract_State is now part of the entities that
can be overloaded. Update type Overloadable_Kind to reflect the
inclusion of abstract states.
* sem_ch6.adb (New_Overloaded_Entity): A function can now
overload an abstract state.
* sem_prag.adb (Analyze_Constituent): Handle the overloading
of states by functions. Use Entity_Of to obtain the entity of
a constituent. (Analyze_Global_Item): Handle the overloading of
states by functions.
(Analyze_Initialization_Item): Handle the
overloading of states by functions. Use Entity_Of to obtain the
entity of an item.
(Analyze_Input_Item): Handle the overloading
of states by functions. Use Entity_Of to obtain the entity of an item.
(Analyze_Input_Output): Handle the overloading of states by functions.
(Analyze_Refinement_Clause): Handle the overloading
of states by functions. Use Entity_Of to obtain the entity of an item.
(Appears_In): Use Entity_Of to obtain the entity of an element.
(Check_Usage): Use Entity_Of to obtain the entity of
an item. Add a guard to prevent a crash due to a previous error.
(Resolve_State): New routine.
2014-01-20 Yannick Moy <moy@adacore.com>
* spark_xrefs.ads, debug.adb, gnat1drv.adb, errout.adb, errout.ads,
opt.ads: Minor comments updates.
From-SVN: r206809
Diffstat (limited to 'gcc/ada/spark_xrefs.ads')
| -rw-r--r-- | gcc/ada/spark_xrefs.ads | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/gcc/ada/spark_xrefs.ads b/gcc/ada/spark_xrefs.ads index 2b0a708..e7df033 100644 --- a/gcc/ada/spark_xrefs.ads +++ b/gcc/ada/spark_xrefs.ads @@ -56,8 +56,7 @@ package SPARK_Xrefs is -- SPARK cross-reference information is generated on a unit-by-unit basis -- in the ALI file, using lines that start with the identifying character F - -- ("Formal"). These lines are generated if -gnatd.E or -gnatd.F (Why - -- generation mode) switches are set. + -- ("Formal"). These lines are generated if Frame_Condition_Mode is True. -- The SPARK cross-reference information comes after the shared -- cross-reference information, so it needs not be read by tools like |