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] |
GNATprove relied on frontend writing cross-references data into the ALI files to synthesize Global contracts. Now this is done by the GNATprove itself. This patch deconstructs the frontend code, that is no longer needed. No test, as only dead code removed. Tested on x86_64-pc-linux-gnu, committed on trunk 2017-11-08 Piotr Trojanek <trojanek@adacore.com> * lib-xref-spark_specific.adb (Add_SPARK_Scope): Remove detection of protected operations. (Add_SPARK_Xrefs): Simplify detection of empty entities. * get_spark_xrefs.ads, get_spark_xrefs.adb, put_spark_xrefs.ads, put_spark_xrefs.adb, spark_xrefs_test.adb: Remove code for writing, reading and testing SPARK cross-references stored in the ALI files. * lib-xref.ads (Output_SPARK_Xrefs): Remove. * lib-writ.adb (Write_ALI): Do not write SPARK cross-references to the ALI file. * spark_xrefs.ads, spark_xrefs.adb (pspark): Remove, together with description of the SPARK xrefs ALI format. * gcc-interface/Make-lang.in (GNAT_ADA_OBJS): Remove get_spark_refs.o and put_spark_refs.o.
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] |