Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

New version of compiler doesn't handle Why3 library correctly: #7659

Closed
vicuna opened this issue Oct 18, 2017 · 3 comments
Closed

New version of compiler doesn't handle Why3 library correctly: #7659

vicuna opened this issue Oct 18, 2017 · 3 comments

Comments

@vicuna
Copy link

vicuna commented Oct 18, 2017

Original bug ID: 7659
Reporter: msk
Status: resolved (set by @xavierleroy on 2017-12-20T17:00:41Z)
Resolution: unable to duplicate
Priority: normal
Severity: major
Platform: x64
OS: LUbuntu
OS Version: 16.04
Category: compiler driver

Bug description

Why3 0.83.3 module core/term.mli contains declaration:

val t_const : Number.constant -> term

and in core/term.ml:

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 reproduce

Simply try to use Term.t_const function from Why3 library

@vicuna
Copy link
Author

vicuna commented Oct 18, 2017

Comment author: @gasche

(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.)

@vicuna
Copy link
Author

vicuna commented Nov 26, 2017

Comment author: @xavierleroy

Dear user "msk", we need your feedback and a repro case in order to investigate. Otherwise we'll close this report as not reproducible.

@vicuna
Copy link
Author

vicuna commented Dec 20, 2017

Comment author: @xavierleroy

Closing as not reproducible.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

1 participant