| 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 | |
| Platform | | OS | | OS Version | |
| 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 |  0003-Fix-weak-pattern-matching-in-dynlink_lower_311_byte..patch [^] (836 bytes) 2009-09-01 13:54 [Show Content] [Hide Content]From: Mehdi Dogguy <dogguy@pps.jussieu.fr>
Date: Tue, 1 Sep 2009 10:17:52 +0200
Subject: [PATCH] Fix weak pattern-matching in dynlink_lower_311_byte.ml
---
src/lib/dynlink_lower_311_byte.ml | 1 +
1 files changed, 1 insertions(+), 0 deletions(-)
diff --git a/src/lib/dynlink_lower_311_byte.ml b/src/lib/dynlink_lower_311_byte.ml
index 58e0ee5..fc2705e 100644
--- a/src/lib/dynlink_lower_311_byte.ml
+++ b/src/lib/dynlink_lower_311_byte.ml
@@ -84,6 +84,7 @@ let from_dynlink_error = function
| Dynlink.Corrupted_interface s -> Corrupted_interface s
| Dynlink.File_not_found s -> File_not_found s
| Dynlink.Cannot_open_dll s -> Cannot_open_dll s
+ | Dynlink.Inconsistent_implementation s -> Inconsistent_implementation s
let stub_error f x =
try f x with Dynlink.Error e -> raise (Error (from_dynlink_error e))
--
|
|
Relationships 
Relationships