This is the mail archive of the gcc-patches@gcc.gnu.org mailing list for the GCC project.
Index Nav: | [Date Index] [Subject Index] [Author Index] [Thread Index] | |
---|---|---|
Message Nav: | [Date Prev] [Date Next] | [Thread Prev] [Thread Next] |
Other format: | [Raw text] |
This patch implements two predicates that allow for state revinement queries while ignoring the region over which a state refinement is visible. No test possible as this requires an external client of the compiler. Tested on x86_64-pc-linux-gnu, committed on trunk 2015-11-18 Hristian Kirtchev <kirtchev@adacore.com> * einfo.adb (Has_Non_Null_Refinement): Rename to Has_Non_Null_Visible_Refinement. (Has_Null_Refinement): Rename to Has_Null_Visible_Refinement. * einfo.ads Update the documentation of attribute Has_Non_Null_Refinement and attribute Has_Null_Refinement. (Has_Non_Null_Refinement): Rename to Has_Non_Null_Visible_Refinement and update occurrences in entities. (Has_Null_Refinement): Rename to Has_Null_Visible_Refinement and update occurrences in entities. * sem_prag.adb (Check_In_Out_States): Update the calls to Has_[Non_]Null_Refinement. (Check_Input_States): Update the calls to Has_[Non_]Null_Refinement. (Check_Output_States): Update the calls to Has_[Non_]Null_Refinement. (Check_Proof_In_States): Update the calls to Has_[Non_]Null_Refinement. (Collect_Global_Item): Update the calls to Has_[Non_]Null_Refinement. (Is_Null_Refined_State): Update the calls to Has_[Non_]Null_Refinement. (Match_Item): Update the calls to Has_[Non_]Null_Refinement. * sem_util.adb (Has_Non_Null_Refinement): New routine. (Has_Null_Refinement): New routine. * sem_util.ads (Has_Non_Null_Refinement): New routine. (Has_Null_Refinement): New routine.
Attachment:
difs
Description: Text document
Index Nav: | [Date Index] [Subject Index] [Author Index] [Thread Index] | |
---|---|---|
Message Nav: | [Date Prev] [Date Next] | [Thread Prev] [Thread Next] |