Frama-C Bug Tracking System

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 
PlatformOSOS Version
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 Filespatch file icon 0003-Fix-weak-pattern-matching-in-dynlink_lower_311_byte..patch [^] (836 bytes) 2009-09-01 13:54 [Show Content]

- 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


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker