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]

[Ada] Check for attempt to bind GNATprove files


If one or more objects is compiled in GNATprove mode (either by using
GNATprove directly, or by using -gnatd.F), then the ALI file is marked
and gnatbind will exit with a message as shown here. Given:

     1. procedure linkdf is
     2. begin
     3.    null;
     4. end;

If we first compile this with

  gcc -c linkdf.adb -gnatd.F

then we try to do a gnatmake, we get

error: one or more files compiled in GNATprove mode
gnatmake: *** bind failed.

Previously this was not detected and the linker bombed
with peculiar error messages.

Tested on x86_64-pc-linux-gnu, committed on trunk

2014-10-10  Robert Dewar  <dewar@adacore.com>

	* ali.adb (Scan_ALI): Read and process new GP flag on ALI P line.
	* ali.ads (GNATprove_Mode): New component in ALI table.
	(GNATprove_Mode_Specified): New global.
	* gnatbind.adb (Gnatbind): Give fatal error if any file compiled
	in GNATProve mode.
	* lib-writ.ads, lib-writ.adb (GP): New flag on P line for
	GNATProve_Mode.

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]