Bug 1392552

Summary: Frama-C FTBFS in Rawhide
Product: [Fedora] Fedora Reporter: Richard W.M. Jones <rjones>
Component: frama-cAssignee: Jerry James <loganjerry>
Status: CLOSED RAWHIDE QA Contact: Fedora Extras Quality Assurance <extras-qa>
Severity: unspecified Docs Contact:
Priority: unspecified    
Version: rawhideCC: loganjerry, msrader
Target Milestone: ---   
Target Release: ---   
Hardware: Unspecified   
OS: Unspecified   
Whiteboard:
Fixed In Version: frama-c-1.13-5.fc26 Doc Type: If docs needed, set a value
Doc Text:
Story Points: ---
Clone Of: Environment:
Last Closed: 2016-11-08 15:13:53 UTC Type: Bug
Regression: --- Mount Type: ---
Documentation: --- CRM:
Verified Versions: Category: ---
oVirt Team: --- RHEL 7.3 requirements from Atomic Host:
Cloudforms Team: --- Target Upstream Version:
Attachments:
Description Flags
build.log
none
frama-c-ocaml-4.04.patch none

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