View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0000224 | Frama-C | Kernel | public | 2009-09-01 13:54 | 2009-09-23 20:22 | ||||
Reporter | mehdi | ||||||||
Assigned To | signoles | ||||||||
Priority | normal | Severity | major | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | Frama-C Beryllium-20090601-beta1 | ||||||||
Target Version | Fixed in Version | Frama-C Beryllium-20090902 | |||||||
Summary | 0000224: Non-exhaustive pattern matching leads to compilation error | ||||||||
Description | 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 | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
signoles (manager) 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. |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2009-09-01 13:54 | mehdi | New Issue | |
2009-09-01 13:54 | mehdi | File Added: 0003-Fix-weak-pattern-matching-in-dynlink_lower_311_byte..patch | |
2009-09-02 10:48 | signoles | Status | new => assigned |
2009-09-02 10:48 | signoles | Assigned To | => signoles |
2009-09-04 16:17 | signoles | Status | assigned => acknowledged |
2009-09-04 17:08 | signoles | Note Added: 0000372 | |
2009-09-04 17:08 | signoles | Status | acknowledged => confirmed |
2009-09-07 10:11 | signoles | Status | confirmed => resolved |
2009-09-07 10:11 | signoles | Fixed in Version | => Frama-C Bore |
2009-09-07 10:11 | signoles | Resolution | open => fixed |
2009-09-23 15:26 | signoles | Fixed in Version | Frama-C Bore => Frama-C Beryllium 2 |
2009-09-23 20:22 | signoles | Status | resolved => closed |