Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0006329OCamlOCaml runtime systempublic2014-02-18 10:392014-02-20 12:20
Assigned To 
PlatformOSOS Version
Product Version4.01.0 
Target VersionFixed in Version 
Summary0006329: File "", line 63, characters 6-12: Assertion failed.
DescriptionThere is an assertion failed in the OCaml runtime when dynamically loading a recursive module. Unfortunately, the bug is highly sensitive to conditions: changing the size of the code segment, changing the size of the data segment, changing the size of the read-only data segment, changing the number of relocations, etc, all cause the bug to vanish. As a consequence, we were unable to produce a small testcase, sorry. This bug report is mostly for the record. That said, it is perfectly reproducible and we were able to trigger it on three systems with OCaml 4.01.0 and Coq 8.4pl3.
Steps To Reproducegit clone git:// [^]
cd why3
git checkout a8c13660788c726a134fab9109e384592881e8d7
cat > src/util/ << EOF
let version = "1234567812345678123456781234567812345678123456781234567812345678123456781234567"
let builddate = ""
let libdir = ""
let datadir = ""
let localdir = Some ""
let compile_time_support = [ "", ""; "", "" ]
make src/coq-tactic/.why3-vo-opt
Attached Files

- Relationships

-  Notes
frisch (developer)
2014-02-20 11:36

Could it be the case that two units of the same name where dynlinked in the same process? Do you use -pack?
frisch (developer)
2014-02-20 11:59

$ make src/coq-tactic/.why3-vo-opt
Ocamldep src/util/
Ocamldep src/util/
Ocamldep src/util/
Ocamldep src/util/
Ocamldep src/util/
Ocamldep src/util/
make: *** No rule to make target `src/coq-tactic/.why3-vo-opt'. Stop.

Do we need to install anything else in addition to OCaml itself?
gmelquiond (reporter)
2014-02-20 12:20

I don't think there are two units with the same name. (Any way to make sure?) We are using -pack, so that all our modules are submodules of Why3.

Also, you need Coq, since the dynamically-loaded module is actually a Coq plugin and it depends on various Coq modules. Due to the high sensitivity on the size of the segments and the number of relocations, I was unfortunately not able to remove Coq from the equation.

- Issue History
Date Modified Username Field Change
2014-02-18 10:39 gmelquiond New Issue
2014-02-19 20:46 doligez Tag Attached: recmod
2014-02-20 11:36 frisch Note Added: 0010963
2014-02-20 11:59 frisch Note Added: 0010964
2014-02-20 12:20 gmelquiond Note Added: 0010965

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker