|Anonymous | Login | Signup for a new account||2014-11-26 00:20 CET|
|Main | My View | View Issues | Change Log | Roadmap|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0006243||OCaml||Misc||public||2013-11-19 09:49||2013-11-28 15:35|
|Target Version||Fixed in Version||4.01.1+dev|
|Summary||0006243: Coq doesn't compile in debug mode|
|Description||Coq trunk compilation in debug mode in 4.01 raises an assertion failure in asmcomp/emitaux.ml at line 226. It seems that CAMLP4 is the faulty one, because it generates dummy locations which break the assertion.|
|Tags||No tags attached.|
|Attached Files||debug-info.diff [^] (641 bytes) 2013-11-19 13:40 [Show Content]|
I haven't looked at where in camlp4 the problem arises, but I think we should maybe do some work on the compiler side as well.
At the moment, the assertion doesn't seem to be appropriate; the condition being checked is not impossible. I think it would probably be better to catch the construction of locations that are not "no location", but have (e.g.) a zero line number, in [Debuginfo]. I'd actually maybe argue that the interface to that module should be changed so that it isn't possible to (e.g.) retrieve a line number when the location is "none"; and also so that it is possible to (e.g.) encode a location consisting of a source filename but not a line number. I wonder if this latter case is what camlp4 is trying to do.
|Tentative fix (against 4.01) attached. This doesn't fix the Camlp4 issue: it just skips the .loc statement if line is 0, instead of bombing out.|
No feedback. Applied proposed patch to 4.01 bugfix branch (r14321) and to trunk (r14322).
|2013-11-19 09:49||ppedrot||New Issue|
|2013-11-19 10:16||shinwell||Note Added: 0010649|
|2013-11-19 13:40||xleroy||File Added: debug-info.diff|
|2013-11-19 13:41||xleroy||Note Added: 0010653|
|2013-11-19 13:41||xleroy||Status||new => feedback|
|2013-11-28 15:35||xleroy||Note Added: 0010676|
|2013-11-28 15:35||xleroy||Status||feedback => resolved|
|2013-11-28 15:35||xleroy||Resolution||open => fixed|
|2013-11-28 15:35||xleroy||Fixed in Version||=> 4.01.1+dev|
|Copyright © 2000 - 2011 MantisBT Group|