contracts.adb (Analyze_Entry_Or_Subprogram_Body_Contract): Remove the guard concerning entry bodies as it is spurious. 2015-11-12 Hristian Kirtchev <kirtchev@adacore.com> * contracts.adb (Analyze_Entry_Or_Subprogram_Body_Contract): Remove the guard concerning entry bodies as it is spurious. (Analyze_Entry_Or_Subprogram_Contract): Skip the analysis of Contract_Cases when not annotating the tree. * einfo.adb: Node25 is now used as Contract_Wrapper. (Contract_Wrapper): New routine. (PPC_Wrapper): Removed. (Set_Contract_Wrapper): New routine. (Set_PPC_Wrapper): Removed. (Write_Field25_Name): Add output for Contract_Wrapper. Remove output for PPC_Wrapper. * einfo.ads: New attribute Contract_Wrapper along with usage in entities. Remove attribute PPC_Wrapper along with usage in nodes. (Contract_Wrapper): New routine along with pragma Inline. (PPC_Wrapper): Removed along with pragma Inline. (Set_Contract_Wrapper): New routine along with pragma Inline. (Set_PPC_Wrapper): Removed along with pragma Inline. * exp_ch9.adb (Build_Contract_Wrapper): New routine. (Build_PPC_Wrapper): Removed. (Build_Protected_Entry): Code cleanup. (Expand_Entry_Declaration): Create a contract wrapper which now verifies Contract_Cases along with pre/postconditions. (Expand_N_Task_Type_Declaration): There is no need to check whether an entry has pre/postconditions as this is now done in Build_Contract_Wrapper. * sem_ch13.adb (Analyze_Aspect_Specifications): Pragma Refined_Post is now properly inserted in entry bodies. (Insert_Pragma): Add circuitry to insert in an entry body. Redo the instance "header" circuitry. Remove the now obsolete special case of inserting pre- conditions. * sem_prag.adb (Analyze_Pragma): Pragma Contract_Cases now applies to entries. * sem_res.adb (Resolve_Entry_Call): Update the calls to PPC_Wrapper. From-SVN: r230236
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... | |
gotools | Loading commit data... | |
include | Loading commit data... | |
intl | Loading commit data... | |
libada | Loading commit data... | |
libatomic | Loading commit data... | |
libbacktrace | Loading commit data... | |
libcc1 | 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... | |
libmpx | Loading commit data... | |
libobjc | Loading commit data... | |
liboffloadmic | 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.jit | 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... |