2021-02-24 18:47 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000224Frama-CKernelpublic2009-09-01 13:542009-09-23 20:22
Reportermehdi 
Assigned Tosignoles 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Beryllium-20090601-beta1 
Target VersionFixed in VersionFrama-C Beryllium-20090902 
Summary0000224: Non-exhaustive pattern matching leads to compilation error
DescriptionHi,

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
TagsNo tags attached.
Attached Files
  • patch file icon 0003-Fix-weak-pattern-matching-in-dynlink_lower_311_byte..patch (836 bytes) 2009-09-01 13:54 - 
    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

-Notes

~0000372

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.
+Notes

-Issue History
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
+Issue History