0000224: Non-exhaustive pattern matching leads to compilation error

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

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 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

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.

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-02 10:52	signoles	Relationship added	related to 0000012
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