2013-10-10 Hristian Kirtchev <kirtchev@adacore.com> * aspects.adb: Add entries in table Canonical_Aspects for aspects Refined_Depends and Refined_Global. * aspects.ads: Add entries in tables Aspect_Id, Aspect_Argument, Aspect_Names, Aspect_Declay, Aspect_On_Body_Or_Stub_OK for aspects Refined_Depends and Refined_Global. * einfo.adb (Contract): Subprogram bodies are now valid owners of contracts. (Set_Contract): Subprogram bodies are now valid owners of contracts. (Write_Field24_Name): Output the contract attribute for subprogram bodies. * exp_ch6.adb (Expand_Subprogram_Contract): New routine. * exp_ch6.ads (Expand_Subprogram_Contract): New routine. * par-prag.adb: Pragmas Refined_Depends and Refined_Global do not require any special processing by the parser. * sem_ch3.adb (Adjust_D): Renamed to Adjust_Decl. (Analyze_Declarations): Code reformatting. Analyze the contract of a subprogram body at the end of the declarative region. * sem_ch6.adb (Analyze_Generic_Subprogram_Body): Subprogram bodies can now have contracts. Use Expand_Subprogram_Contract to handle the various contract assertions. (Analyze_Subprogram_Body_Contract): New null routine. (Analyze_Subprogram_Body_Helper): Subprogram bodies can now have contracts. Use Expand_Subprogram_Contract to handle the various contract assertions. (Analyze_Subprogram_Contract): Add local variable Nam. Update the call to Analyze_PPC_In_Decl_Part. Capture the pragma name in Nam. (Process_PPCs): Removed. * sem_ch6.ads (Analyze_Subprogram_Body_Contract): New routine. (Analyze_Subprogram_Contract): Update the comment on usage. * sem_ch13.adb (Analyze_Aspect_Specifications): Add null implementations for aspects Refined_Depends and Refined_Global. (Check_Aspect_At_Freeze_Point): Aspects Refined_Depends and Refined_Global do not need to be checked at the freeze point. * sem_prag.adb: Add entries in table Sig_Flags for pragmas Refined_Depends and Refined_Global. (Analyze_Contract_Cases_In_Decl_Part): Add local variable Restore. Use Restore to pop the scope. (Analyze_Depends_In_Decl_Part): Add local variable Restore. Use Restore to pop the scope. (Analyze_Global_In_Decl_List): Add local variable Restore. Use Restore to pop the scope. (Analyze_PPC_In_Decl_Part): Renamed to Analyze_Pre_Post_Condition_In_Decl_Part. (Analyze_Pragma): Add null implementations for pragmas Refined_Depends and Refined_Global. Refined_Pre and Refined_Post are now handled by routine Analyze_Refined_Pre_Post_Condition exclusively. (Analyze_Refined_Depends_In_Decl_Part): New null routine. (Analyze_Refined_Global_In_Decl_Part): New null routine. (Analyze_Refined_Pre_Post): Renamed to Analyze_Refined_Pre_Post_Condition. (Analyze_Refined_Pre_Post_Condition): Analyze the boolean expression. (Check_Precondition_Postcondition): Update the call to Analyze_PPC_In_Decl_Part. * sem_prag.ads: Add entries in table Pragma_On_Body_Or_Stub_OK for pragmas Refined_Depends and Refined_Global. (Analyze_PPC_In_Decl_Part): Renamed to Analyze_Pre_Post_Condition_In_Decl_Part. Update the comment on usage. (Analyze_Refined_Depends_In_Decl_Part): New routine. (Analyze_Refined_Global_In_Decl_Part): New routine. (Analyze_Test_Case_In_Decl_Part): Update the comment on usage. * sem_util.adb (Add_Contract_Item): Rename formal Item to Prag and update all occurrences. Subprogram body contracts can now contain pragmas Refined_Depends and Refined_Global. * sem_util.ads (Add_Contract_Item): Rename formal Item to Prag. Update the comment on usage. * sinfo.ads: Update the comment on structure and usage of N_Contract. * snames.ads-tmpl: Add new predefined names for Refined_Depends and Refined_Global. Add entries in table Pragma_Id for Refined_Depends and Refined_Global. 2013-10-10 Robert Dewar <dewar@adacore.com> * types.ads: Minor reformatting. From-SVN: r203365
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... | |
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... | |
libmudflap | 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... | |
.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... |