Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0006243OCamlMiscpublic2013-11-19 09:492013-11-28 15:35
Reporterppedrot 
Assigned To 
PrioritynormalSeveritymajorReproducibilityalways
StatusresolvedResolutionfixed 
PlatformOSOS Version
Product Version4.01.0 
Target VersionFixed in Version4.01.1+dev 
Summary0006243: Coq doesn't compile in debug mode
DescriptionCoq 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.
TagsNo tags attached.
Attached Filesdiff file icon debug-info.diff [^] (641 bytes) 2013-11-19 13:40 [Show Content]

- Relationships

-  Notes
(0010649)
shinwell (developer)
2013-11-19 10:16

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.
(0010653)
xleroy (administrator)
2013-11-19 13:41

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.
(0010676)
xleroy (administrator)
2013-11-28 15:35

No feedback. Applied proposed patch to 4.01 bugfix branch (r14321) and to trunk (r14322).

- Issue History
Date Modified Username Field Change
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
Powered by Mantis Bugtracker