2014-01-20 Robert Dewar <dewar@adacore.com> * checks.adb: Check SPARK_Mode instead of GNATProve_Mode for converting warnings on inevitable exceptions to errors. * exp_ch4.adb: Check SPARK_Mode instead of GNATProve_Mode for converting warnings on inevitable exceptions to errors. * opt.adb (SPARK_Mode_Config): Handled like other config flags * opt.ads (SPARK_Mode_Type): Moved here from types (renamed from SPARK_Mode_Id) (SPARK_Mode_Type): Add pragma Ordered, remove SPARK_ from names (SPARK_Mode): New flag (SPARK_Mode_Config): New flag (Config_Switches_Type): Add SPARK_Mode field * sem.adb: Minor code reorganization (remove unnecessary with) * sem.ads (Scope_Stack_Entry): Add Save_SPARK_Mode field * sem_aggr.adb: Check SPARK_Mode instead of GNATProve_Mode for converting warnings on inevitable exceptions to errors. * sem_attr.adb: Check SPARK_Mode instead of GNATProve_Mode for converting warnings on inevitable exceptions to errors. * sem_ch3.adb: Check SPARK_Mode instead of GNATProve_Mode for converting warnings on inevitable exceptions to errors. * sem_ch4.adb: Check SPARK_Mode instead of GNATProve_Mode for converting warnings on inevitable exceptions to errors. * sem_ch6.adb (Analyze_Subprogram_Body_Helper): Reset SPARK_Mode from spec if needed * sem_ch7.adb (Analyze_Package_Body_Helper): Reset SPARK_Mode from spec if needed * sem_ch8.adb (Push_Scope): Save SPARK_Mode (Pop_Scope): Restore SPARK_Mode * sem_elab.adb: Check SPARK_Mode instead of GNATProve_Mode for converting warnings on inevitable exceptions to errors. * sem_prag.adb (Get_SPARK_Mode_From_Pragma): New function (Get_SPARK_Mode_Id): Removed (Get_SPARK_Mode_Type): New name of Get_SPARK_Mode_Id * sem_prag.ads (Get_SPARK_Mode_From_Pragma): New function * sem_res.adb: Check SPARK_Mode instead of GNATProve_Mode for converting warnings on inevitable exceptions to errors. * sem_util.adb: Check SPARK_Mode instead of GNATProve_Mode for converting warnings on inevitable exceptions to errors. * types.ads (SPARK_Mode_Id): Moved to opt.ads and renamed SPARK_Mode_Type 2014-01-20 Ed Schonberg <schonberg@adacore.com> * sem_ch13.adb: Add semantic information to rewritten type reference. 2014-01-20 Ed Schonberg <schonberg@adacore.com> * exp_ch5.adb (Expand_N_Assignment_Statement): If both sides are of a type with unknown discriminants, convert both to the underlying view of the type, so that the proper constraint check can be applied to the right-hand side. 2014-01-20 Robert Dewar <dewar@adacore.com> * atree.adb (Copy_Node): Fix failure to copy last component (Exchange_Entities): Fix failure to exchange last entity 2014-01-20 Ed Schonberg <schonberg@adacore.com> * sem_ch12.adb: Code clean up. From-SVN: r206844
Name |
Last commit
|
Last update |
---|---|---|
INSTALL | Loading commit data... | |
boehm-gc | Loading commit data... | |
config | Loading commit data... | |
contrib | Loading commit data... | |
fixincludes | Loading commit data... | |
gcc | Loading commit data... | |
gnattools | Loading commit data... | |
include | Loading commit data... | |
intl | Loading commit data... | |
libada | Loading commit data... | |
libatomic | Loading commit data... | |
libbacktrace | Loading commit data... | |
libcilkrts | Loading commit data... | |
libcpp | Loading commit data... | |
libdecnumber | Loading commit data... | |
libffi | Loading commit data... | |
libgcc | Loading commit data... | |
libgfortran | Loading commit data... | |
libgo | Loading commit data... | |
libgomp | Loading commit data... | |
libiberty | Loading commit data... | |
libitm | Loading commit data... | |
libjava | Loading commit data... | |
libobjc | Loading commit data... | |
libquadmath | Loading commit data... | |
libsanitizer | Loading commit data... | |
libssp | Loading commit data... | |
libstdc++-v3 | Loading commit data... | |
libvtv | Loading commit data... | |
lto-plugin | Loading commit data... | |
maintainer-scripts | Loading commit data... | |
zlib | Loading commit data... | |
.dir-locals.el | Loading commit data... | |
.gitignore | Loading commit data... | |
ABOUT-NLS | Loading commit data... | |
COPYING | Loading commit data... | |
COPYING.LIB | Loading commit data... | |
COPYING.RUNTIME | Loading commit data... | |
COPYING3 | Loading commit data... | |
COPYING3.LIB | Loading commit data... | |
ChangeLog | Loading commit data... | |
ChangeLog.tree-ssa | Loading commit data... | |
MAINTAINERS | Loading commit data... | |
Makefile.def | Loading commit data... | |
Makefile.in | Loading commit data... | |
Makefile.tpl | Loading commit data... | |
README | Loading commit data... | |
compile | Loading commit data... | |
config-ml.in | Loading commit data... | |
config.guess | Loading commit data... | |
config.rpath | Loading commit data... | |
config.sub | Loading commit data... | |
configure | Loading commit data... | |
configure.ac | Loading commit data... | |
depcomp | Loading commit data... | |
install-sh | Loading commit data... | |
libtool-ldflags | Loading commit data... | |
libtool.m4 | Loading commit data... | |
ltgcc.m4 | Loading commit data... | |
ltmain.sh | Loading commit data... | |
ltoptions.m4 | Loading commit data... | |
ltsugar.m4 | Loading commit data... | |
ltversion.m4 | Loading commit data... | |
lt~obsolete.m4 | Loading commit data... | |
missing | Loading commit data... | |
mkdep | Loading commit data... | |
mkinstalldirs | Loading commit data... | |
move-if-change | Loading commit data... | |
symlink-tree | Loading commit data... | |
ylwrap | Loading commit data... |