Bug 1392552 - Frama-C FTBFS in Rawhide
Summary: Frama-C FTBFS in Rawhide
Keywords:
Status: CLOSED RAWHIDE
Alias: None
Product: Fedora
Classification: Fedora
Component: frama-c
Version: rawhide
Hardware: Unspecified
OS: Unspecified
unspecified
unspecified
Target Milestone: ---
Assignee: Jerry James
QA Contact: Fedora Extras Quality Assurance
URL:
Whiteboard:
Depends On:
Blocks:
TreeView+ depends on / blocked
 
Reported: 2016-11-07 17:58 UTC by Richard W.M. Jones
Modified: 2016-11-09 02:22 UTC (History)
2 users (show)

Fixed In Version: frama-c-1.13-5.fc26
Doc Type: If docs needed, set a value
Doc Text:
Clone Of:
Environment:
Last Closed: 2016-11-08 15:13:53 UTC
Type: Bug
Embargoed:


Attachments (Terms of Use)
build.log (712.00 KB, text/plain)
2016-11-07 17:58 UTC, Richard W.M. Jones
no flags Details
frama-c-ocaml-4.04.patch (4.17 KB, patch)
2016-11-08 14:21 UTC, Richard W.M. Jones
no flags Details | Diff

Description Richard W.M. Jones 2016-11-07 17:58:16 UTC
Created attachment 1218170 [details]
build.log

Description of problem:

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

This seems unrelated to the upgrade to OCaml 4.04.0 also in Rawhide.

Version-Release number of selected component (if applicable):

frama-c-1.13-5.fc26

How reproducible:

100%

Steps to Reproduce:
1. Build frama-c in Rawhide.

Comment 1 Richard W.M. Jones 2016-11-08 14:21:23 UTC
Created attachment 1218529 [details]
frama-c-ocaml-4.04.patch

I added the attached patch which fixes compilation, but is
generally a bit of a hack.  Upstream probably will want to
make their own better fix.

Comment 2 Jerry James 2016-11-09 02:22:22 UTC
Thank you again for the diagnosis and fix, Richard.  Upstream bug report: https://bts.frama-c.com/view.php?id=2255


Note You need to log in before you can comment on or make changes to this bug.