Ocaml 4.04.0 build error
ID0002255: This issue was created automatically from Mantis Issue 2255. Further discussion may take place here.
Id | Project | Category | View | Due Date | Updated |
---|---|---|---|---|---|
ID0002255 | Frama-C | Kernel | public | 2016-11-09 | 2016-12-07 |
Reporter | jamesjer | Assigned To | yakobowski | Resolution | fixed |
Priority | normal | Severity | minor | Reproducibility | always |
Platform | x86_64 | OS | Linux | OS Version | 4.8.6 |
Product Version | Frama-C Aluminium | Target Version | - | Fixed in Version | - |
Description :
Building with ocaml 4.04.0 fails:
File "src/kernel_services/plugin_entry_points/db.ml", line 1: Error: The implementation src/kernel_services/plugin_entry_points/db.ml does not match the interface src/kernel_services/plugin_entry_points/db.cmi: ... In module Properties.Interp.To_zone: Values do not match: val mk_ctx_func_contrat : (Cil_types.kernel_function -> '_a) ref is not included in val mk_ctx_func_contrat : (Cil_types.kernel_function -> state_opt:bool option -> t_ctx) ref File "src/kernel_services/plugin_entry_points/db.ml", line 1074, characters 10-29: Actual declaration
Additional Information :
See https://bugzilla.redhat.com/show_bug.cgi?id=1392552 for the original report, by Richard W. M. Jones. He supplied a patch which, he says, "fixes compilation, but is generally a bit of a hack. Upstream probably will want to make their own better fix." That patch is attached.
Steps To Reproduce :
Build with Frama-C Aluminium with ocaml 4.04.0 on an x86_64 Linux machine.