You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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
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
The text was updated successfully, but these errors were encountered:
(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.)
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
The text was updated successfully, but these errors were encountered: