4127ebece7
2020-06-11 Steve Baird <baird@adacore.com> gcc/ada/ * contracts.adb (Add_Contract_Item): Support specifying volatility refinement aspects for types. (Analyze_Contracts): Add call to Analyze_Type_Contract in the case of a contract for a type. (Freeze_Contracts): Add call to Analyze_Type_Contract in the case of a contract for a type. (Check_Type_Or_Object_External_Properties): A new procedure which performs the work that needs to be done for both object declarations and types. (Analyze_Object_Contract): Add a call to Check_Type_Or_Object_External_Properties and remove the code in this procedure which did much of the work that is now performed by that call. (Analyze_Type_Contract): Implement this new routine as nothing more than a call to Check_Type_Or_Object_External_Properties. * contracts.ads: Update comment for Add_Contract_To_Item because types can have contracts. Follow (questionable) precedent and declare new routine Analyze_Type_Contract as visible (following example of Analyze_Object_Contract), despite the fact that it is never called from outside of the package where it is declared. * einfo.adb (Contract, Set_Contract): Id argument can be a type; support this case. (Write_Field34_Name): Field name is "contract" for a type. * einfo.ads: Update comment describing Contract attribute. * sem_ch3.adb (Build_Derived_Numeric_Type): Is_Volatile should return same answer for all subtypes of a given type. Thus, when building the base type for something like type Volatile_1_To_10 is range 1 .. 10 with Volatile; that basetype should be marked as being volatile. (Access_Type_Declaration): Add SPARK-specific legality check that the designated type of an access type shall be compatible with respect to volatility with the access type. * sem_ch12.adb (Check_Shared_Variable_Control_Aspects): Add SPARK-specific legality check that an actual type parameter in an instantiation shall be compatible with respect to volatility with the corresponding formal type. * sem_ch13.adb (Analyze_Aspect_Specifications): Perform checks for aspect specs for the 4 volatility refinement aspects that were already being performed for all language-defined aspects. * sem_prag.adb (Analyze_External_Property_In_Decl_Part, Analyze_Pragma): External properties (other than No_Caching) may be specified for a type, including a generic formal type. * sem_util.ads: Declare new subprograms - Async_Readers_Enabled, Async_Writers_Enabled, Effective_Reads, Effective_Writes, and Check_Volatility_Compatibility. * sem_util.adb (Async_Readers_Enabled, Async_Writers_Enabled, Effective_Reads, Effective_Writes): Initial implementation of new functions for querying aspect values. (Check_Volatility_Compatibility): New procedure intended for use in checking all SPARK legality rules of the form "<> shall be compatible with respect to volatility with <>". (Has_Enabled_Property): Update comment because Item_Id can be a type. Change name of nested Variable_Has_Enabled_Property function to Type_Or_Variable_Has_Enabled_Property; add a parameter to that function because recursion may be needed, e.g., in the case of a derived typ). Cope with the case where the argument to Has_Enabled_Property is a type. |
||
|---|---|---|
| config | ||
| contrib | ||
| fixincludes | ||
| gcc | ||
| gnattools | ||
| gotools | ||
| include | ||
| INSTALL | ||
| intl | ||
| libada | ||
| libatomic | ||
| libbacktrace | ||
| libcc1 | ||
| libcpp | ||
| libdecnumber | ||
| libffi | ||
| libgcc | ||
| libgfortran | ||
| libgo | ||
| libgomp | ||
| libhsail-rt | ||
| libiberty | ||
| libitm | ||
| libobjc | ||
| liboffloadmic | ||
| libphobos | ||
| libquadmath | ||
| libsanitizer | ||
| libssp | ||
| libstdc++-v3 | ||
| libvtv | ||
| lto-plugin | ||
| maintainer-scripts | ||
| zlib | ||
| .dir-locals.el | ||
| .gitattributes | ||
| .gitignore | ||
| ABOUT-NLS | ||
| ar-lib | ||
| ChangeLog | ||
| ChangeLog.jit | ||
| ChangeLog.tree-ssa | ||
| compile | ||
| config-ml.in | ||
| config.guess | ||
| config.rpath | ||
| config.sub | ||
| configure | ||
| configure.ac | ||
| COPYING | ||
| COPYING3 | ||
| COPYING3.LIB | ||
| COPYING.LIB | ||
| COPYING.RUNTIME | ||
| depcomp | ||
| install-sh | ||
| libtool-ldflags | ||
| libtool.m4 | ||
| lt~obsolete.m4 | ||
| ltgcc.m4 | ||
| ltmain.sh | ||
| ltoptions.m4 | ||
| ltsugar.m4 | ||
| ltversion.m4 | ||
| MAINTAINERS | ||
| Makefile.def | ||
| Makefile.in | ||
| Makefile.tpl | ||
| missing | ||
| mkdep | ||
| mkinstalldirs | ||
| move-if-change | ||
| multilib.am | ||
| README | ||
| symlink-tree | ||
| test-driver | ||
| ylwrap | ||
This directory contains the GNU Compiler Collection (GCC). The GNU Compiler Collection is free software. See the files whose names start with COPYING for copying permission. The manuals, and some of the runtime libraries, are under different terms; see the individual source files for details. The directory INSTALL contains copies of the installation information as HTML and plain text. The source of this information is gcc/doc/install.texi. The installation information includes details of what is included in the GCC sources and what files GCC installs. See the file gcc/doc/gcc.texi (together with other files that it includes) for usage and porting information. An online readable version of the manual is in the files gcc/doc/gcc.info*. See http://gcc.gnu.org/bugs/ for how to report bugs usefully. Copyright years on GCC source files may be listed using range notation, e.g., 1987-2012, indicating that every year in the range, inclusive, is a copyrightable year that could otherwise be listed individually.