Frama-C Bug Tracking System - Frama-C
View Issue Details
0000224Frama-CKernelpublic2009-09-01 13:542009-09-23 20:22
mehdi 
signoles 
normalmajoralways
closedfixed 
Frama-C Beryllium-20090601-beta1 
Frama-C Beryllium-20090902 
0000224: Non-exhaustive pattern matching leads to compilation error
Hi, 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/dynlink_common_interface.ml Ocamlc src/lib/dynlink_common_interface.cmo File "src/lib/dynlink_common_interface.ml", 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/dynlink_common_interface.ml", 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, -- Mehdi
No tags attached.
patch 0003-Fix-weak-pattern-matching-in-dynlink_lower_311_byte..patch (836) 2009-09-01 13:54
https://bts.frama-c.com/file_download.php?file_id=14&type=bug
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-02 10:52signolesRelationship addedrelated to 0000012
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

Notes
(0000372)
signoles   
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.