Frama-C Bug Tracking System - Frama-C
View Issue Details
0000224Frama-CKernelpublic2009-09-01 13:542009-09-23 20:22
Assigned Tosignoles 
PlatformOSOS Version
Product VersionFrama-C Beryllium-20090601-beta1 
Target VersionFixed in VersionFrama-C Beryllium-20090902 
Summary0000224: Non-exhaustive pattern matching leads to compilation error

When compiling frama-c in bytecode on a non-native architecture (even if OCaml 3.11.1 is available), compilation fails due to a non-exhaustive pattern matching.

The relevant lines are:

Ocamlc src/lib/dynlink_common_interface.cmi
Generating src/lib/
Ocamlc src/lib/dynlink_common_interface.cmo
File "src/lib/", line 77, characters 25-491:
Warning P: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
Inconsistent_implementation _
File "src/lib/", line 1, characters 0-1:
Error: Error-enabled warnings (1 occurrences)

Please find attached a (trivial) patch that fixes this bug.

OCaml 3.11.1 is available on those architectures (e.g., hppa, mips, s390) with only the bytecode backend. So why do not activate the dynlink option or those too? In the configure script, you seem to rely on the presence of dynlink.cmxa. But dynlink.cma is also present when compiling in bytecode. I hope this will be fixed too.

Best regards,

TagsNo tags attached.
Attached Filespatch 0003-Fix-weak-pattern-matching-in-dynlink_lower_311_byte..patch (836) 2009-09-01 13:54

2009-09-04 17:08   
Possible to reproduce the issue with ocaml >= 3.11 when no native dynlink available. Thank's for the report.

However your patch is not correct since it breaks compatibility with ocaml < 3.11. I'm working for correctly fixing this issue.

Furthermore, Frama-C always links against dynlink.cma in bytecode. The test in the configure script is for generating the native version of frama-c.

Issue History
2009-09-01 13:54mehdiNew Issue
2009-09-01 13:54mehdiFile Added: 0003-Fix-weak-pattern-matching-in-dynlink_lower_311_byte..patch
2009-09-02 10:48signolesStatusnew => assigned
2009-09-02 10:48signolesAssigned To => signoles
2009-09-04 16:17signolesStatusassigned => acknowledged
2009-09-04 17:08signolesNote Added: 0000372
2009-09-04 17:08signolesStatusacknowledged => confirmed
2009-09-07 10:11signolesStatusconfirmed => resolved
2009-09-07 10:11signolesFixed in Version => Frama-C Bore
2009-09-07 10:11signolesResolutionopen => fixed
2009-09-23 15:26signolesFixed in VersionFrama-C Bore => Frama-C Beryllium 2
2009-09-23 20:22signolesStatusresolved => closed