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 modifies the contract freezing mechanism to suppress freezing when the trigger is the body of an instantiated package. This effectively prevents a spurious attempt to freeze because a) the body instantiation pass does not have all semantic information and b) freezing has already taken place. ------------ -- Source -- ------------ -- gp.ads generic type T is private; package GP with SPARK_Mode => On, Elaborate_Body, Abstract_State => (State, (Atomic_State with External)) is end GP; -- gp.adb package body GP with SPARK_Mode => On, Refined_State => (State => GG1, Atomic_State => GG2) is GG1 : T; GG2 : T with Volatile; end GP; -- base.ads package Base with SPARK_Mode => On is end Base; -- base-a.ads package Base.A with SPARK_Mode => On, Elaborate_Body, Abstract_State => (State, (Atomic_State with External)) is end Base.A; -- base-a.adb with Base.A.B; package body Base.A with SPARK_Mode => On, Refined_State => (State => Base.A.B.State, Atomic_State => Base.A.B.Atomic_State) is end Base.A; -- base-a-b.ads private package Base.A.B with SPARK_Mode => On, Elaborate_Body, Abstract_State => ((State with Part_Of => Base.A.State), (Atomic_State with External, Part_Of => Base.A.Atomic_State)) is end Base.A.B; -- base-a-b.adb with GP; pragma Elaborate_All (GP); package body Base.A.B with SPARK_Mode => On, Refined_State => (State => (G1, P.State), Atomic_State => P.Atomic_State) is G1 : Boolean := False; package P is new GP (T => Boolean); end Base.A.B; ----------------- -- Compilation -- ----------------- $ gcc -c base-a-b.adb Tested on x86_64-pc-linux-gnu, committed on trunk 2016-04-27 Hristian Kirtchev <kirtchev@adacore.com> * sem_ch7.adb (Analyze_Package_Body_Helper): The body of an instantiated package should not cause freezing of previous contracts.
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] |