Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007659OCamlcompiler driverpublic2017-10-18 15:342017-12-20 18:00
Assigned To 
StatusresolvedResolutionunable to reproduce 
Platformx64OSLUbuntuOS Version16.04
Product Version 
Target VersionFixed in Version 
Summary0007659: New version of compiler doesn't handle Why3 library correctly:
DescriptionWhy3 0.83.3 module core/term.mli contains declaration:

val t_const : Number.constant -> term

and in core/

let t_const c ty = mk_term (Tconst c) (Some ty)
let t_const c = match c with
  | Number.ConstInt _ -> t_const c ty_int
  | Number.ConstReal _ -> t_const c ty_real

in ocaml 4.04.2 all works ok, in 4.05.0 real exported type of t_const is the type of first t_const definition in .ml:

Number.constant -> Ty.ty -> Term.term (instead of Number.constant -> Term.term)
Steps To ReproduceSimply try to use Term.t_const function from Why3 library
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
gasche (administrator)
2017-10-18 16:09
edited on: 2017-10-18 16:10

(I don't know of a 0.83.3 release, do you mean 0.86.3 ?)

Are you sure? If you were correct, then all the uses of t_constr outside the Term module in the why3 codebase should be ill-typed (there are several), but why3 0.86.3 seems to build correctly under 4.05. Could this be an error on your part?

(Would you have a simpler reproduction case, a short OCaml module or pair of files that would exhibit the issue? It is much easier to test self-contained reproduction cases.)

xleroy (administrator)
2017-11-26 17:50

Dear user "msk", we need your feedback and a repro case in order to investigate. Otherwise we'll close this report as not reproducible.
xleroy (administrator)
2017-12-20 18:00

Closing as not reproducible.

- Issue History
Date Modified Username Field Change
2017-10-18 15:34 msk New Issue
2017-10-18 16:09 gasche Note Added: 0018586
2017-10-18 16:10 gasche Note Edited: 0018586 View Revisions
2017-10-18 16:10 gasche Status new => feedback
2017-11-26 17:50 xleroy Note Added: 0018693
2017-12-20 18:00 xleroy Note Added: 0018760
2017-12-20 18:00 xleroy Status feedback => resolved
2017-12-20 18:00 xleroy Resolution open => unable to reproduce

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker