why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2018-10-02T16:14:42+02:00https://gitlab.inria.fr/why3/why3/-/issues/190Unhandled exceptions should be displayed more prominently in IDE2018-10-02T16:14:42+02:00Raphaël Rieu-HelftUnhandled exceptions should be displayed more prominently in IDE1.1.0https://gitlab.inria.fr/why3/why3/-/issues/189Fix encoding of maps2018-10-01T17:37:52+02:00Guillaume MelquiondFix encoding of mapsWe need to understand what went wrong in the encoding of [stdlib/array.mlw](stdlib/array.mlw) for SMT-LIB after 68effd1441dba7a2b914ae606321d5b4e02ac10f.We need to understand what went wrong in the encoding of [stdlib/array.mlw](stdlib/array.mlw) for SMT-LIB after 68effd1441dba7a2b914ae606321d5b4e02ac10f.1.1.0Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/188Modify split_vc to not use simplify_trivial_quantification2018-10-04T15:07:54+02:00Raphaël Rieu-HelftModify split_vc to not use simplify_trivial_quantification1.1.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/182Unsound termination check2018-10-05T13:56:19+02:00Guillaume MelquiondUnsound termination checkConsider the following snippet:
let rec function f () : unit = f ()
let main () = f ()
According to Why3, this is a terminating function, which gets extracted to a non-terminating one:
let rec f (_: unit) : unit = f ()
...Consider the following snippet:
let rec function f () : unit = f ()
let main () = f ()
According to Why3, this is a terminating function, which gets extracted to a non-terminating one:
let rec f (_: unit) : unit = f ()
let main (_: unit) : unit = f ()1.1.0Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/181Invalid extraction of disjunction patterns2018-09-14T14:19:19+02:00Benedikt BeckerInvalid extraction of disjunction patternsThe extraction of the following program to OCaml contains a type error: `cat pattern.mlw`
```ocaml
module Pattern
type s = A
type t = B | C
let f x =
match x with
| A, (B | C) -> ()
end
end
```
In fact, the parentheses...The extraction of the following program to OCaml contains a type error: `cat pattern.mlw`
```ocaml
module Pattern
type s = A
type t = B | C
let f x =
match x with
| A, (B | C) -> ()
end
end
```
In fact, the parentheses around the disjunction seem to be lost on the way, or different associativity is assumed with respect to the comma: `why3 extract -D ocaml64 -o pattern.ml pattern.mlw`
```ocaml
type s =
| A
type t =
| B
| C
let f (x: s * t) : unit = let (A, B | C) = x in ()
```
OCaml surely complains: `ocamlc pattern.ml`
```
File "pattern.ml", line 8, characters 38-39:
Error: This pattern matches values of type t
but a pattern was expected which matches values of type s * t
```1.1.0PARREIRA PEREIRA Mário JoséPARREIRA PEREIRA Mário Joséhttps://gitlab.inria.fr/why3/why3/-/issues/177Release of Why3 1.1.02018-10-19T14:06:48+02:00Guillaume MelquiondRelease of Why3 1.1.0- [x] decide in GT whether this version is 1.00.1 or 1.01.0 or 1.1.0 : it is 1.1.0
- [x] decide in GT whether we drop compatibility with Alt-Ergo < 2.0.0, because
they are unsound on examples/tests-provers/div
- [x] support of Alt-...- [x] decide in GT whether this version is 1.00.1 or 1.01.0 or 1.1.0 : it is 1.1.0
- [x] decide in GT whether we drop compatibility with Alt-Ergo < 2.0.0, because
they are unsound on examples/tests-provers/div
- [x] support of Alt-Ergo 2.1.0 and 2.2.0
- [x] support of Isabelle 2018 (discards Isabelle 2016 support, but keep Isabelle2017)
- [x] [POSTPONED] support Vampire (SMT-LIB2 input)
- [x] fix or discard handcrafted messages (see issues #150 and #172)
- [x] [POSTPONED] fix issue with ghost refinement (see issues #42 and #168)
- [x] check issue #166
- [x] fix issue #159
- [x] fix issue #188
- [x] fix issue #157
- [x] fix broken examples of gallery : fix stdlib/array
- [x] fix issue #149
- [x] fix issue #147
- [x] fix issue #134
- [x] fix issue #190
- [x] [POSTPONED] fix issue #133
- [ ] fix issue #127
- [x] fix issue #181
- [x] fix issue #182
- [x] some fixes of the installation and so that frama-c wp could use why3 api for next version. !21
- [x] fill the changelog
- [x] fix issue #186
- [x] fix issue #189
- [x] fix issue #195
- [x] discuss !22
1.1.0https://gitlab.inria.fr/why3/why3/-/issues/172Unknown syntax error2019-09-20T11:23:55+02:00Benedikt BeckerUnknown syntax errorThe following program has an obvious syntax error but its compilation fails with the
message `This is an unknown syntax error (79). Please report`, so here we go:
```
module Unknown
lemma err: x1 = (fun x2 -> let x3 = x4 in let x5 x6)...The following program has an obvious syntax error but its compilation fails with the
message `This is an unknown syntax error (79). Please report`, so here we go:
```
module Unknown
lemma err: x1 = (fun x2 -> let x3 = x4 in let x5 x6) -> true
end
```1.1.0https://gitlab.inria.fr/why3/why3/-/issues/168Cloning function with bad ghost status raises Invalid_argument("Expr.let_rec")2020-03-17T01:18:26+01:00PARREIRA PEREIRA Mário JoséCloning function with bad ghost status raises Invalid_argument("Expr.let_rec")The following fails with anomaly: Invalid_argument("Expr.let_rec")
```
module A
type t
val f (ghost x: t) : t
let rec ff (ghost x: t) = f x
end
module B
let f (x: int) = 42
clone A with val f, type t = int
end
```
The...The following fails with anomaly: Invalid_argument("Expr.let_rec")
```
module A
type t
val f (ghost x: t) : t
let rec ff (ghost x: t) = f x
end
module B
let f (x: int) = 42
clone A with val f, type t = int
end
```
The error message points to the `clone` line. Removing the `rec` keyword from the definition of `ff`, or stating the argument `x`, of function `f` in module B, as ghost removes the problem.
The error message is a little cryptic, and I don't fully understand why this only happens when we call `f` inside a `let rec` definition.1.3.0Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/166non val logic symbols should not be usable in programs2018-08-30T13:43:21+02:00MARCHE Claudenon val logic symbols should not be usable in programsIn the following code
```
type t
constant a : t
val function f t : int
use ref.Ref
let test (x:ref int) : unit = x := f a
```
why3 answers:
```
why3 prove ghost.mlw
File "ghost.mlw", line 5, characters 37-38:
warning: Logical symbol a is...In the following code
```
type t
constant a : t
val function f t : int
use ref.Ref
let test (x:ref int) : unit = x := f a
```
why3 answers:
```
why3 prove ghost.mlw
File "ghost.mlw", line 5, characters 37-38:
warning: Logical symbol a is used in a non-ghost context
File "ghost.mlw", line 5, characters 32-34:
This expression makes a ghost modification in the non-ghost variable x
```
I'm surprised that the first message is a warning and not an error.
To tell all, it was in a much larger context where it appeared to be quite hard to figure out the reason of the dreadful message ``This expression makes a ghost modification in the non-ghost variable``
at the beginning I thought that ``f`` was assumed ghost, turning the first message into an error would have been helpful1.1.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/159Handling of concurrent events in the server2018-09-14T14:19:19+02:00Guillaume MelquiondHandling of concurrent events in the server@bobot has been trying to run the regression suite on the CI slaves and the jobs sometimes get stuck. So, I have been looking at `src/server/server-unix.c` to try to understand why. I don't think it is related, but the code looks a bit s...@bobot has been trying to run the regression suite on the CI slaves and the jobs sometimes get stuck. So, I have been looking at `src/server/server-unix.c` to try to understand why. I don't think it is related, but the code looks a bit strange.
What happens when several events happen at once in the main loop? For example, a client connects and a child exits. It seems to me that the code will first handle `cur->fd == server_sock` and then breaks out of the inner loop. As a consequence, the child death will not be handled until another child dies (or never if it was the last child). Am I missing something?
Another potential issue is that `close_client` (and thus `read_on_client`) modifies `poll_list`. So, the code should be modified to break out of the inner loop, so as to avoid use-after-free. But then, we are back to the previous issue. If several events happen at once, some of them might be lost in the process.1.1.0Johannes KanigJohannes Kanighttps://gitlab.inria.fr/why3/why3/-/issues/157controller_itp : Whyconf.CPU_duplicate not handled2018-09-10T15:42:03+02:00François Bobotcontroller_itp : Whyconf.CPU_duplicate not handledA TODO (assert false) remains for CPU_duplicate in controller_itp.A TODO (assert false) remains for CPU_duplicate in controller_itp.1.1.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/150custom Menhir error reporting does not work in TryWhy32019-09-20T11:23:55+02:00Andrei Paskevichcustom Menhir error reporting does not work in TryWhy3report.ml uses functions from Str (search_forward), which are not implemented in js_of_ocaml. Thus, instead of "syntax error", TryWhy3 shows "Failure: re_search_forward not implemented". Removing the call to Report.report from lexer.mll ...report.ml uses functions from Str (search_forward), which are not implemented in js_of_ocaml. Thus, instead of "syntax error", TryWhy3 shows "Failure: re_search_forward not implemented". Removing the call to Report.report from lexer.mll fixes the problem, but we need a proper solution to this.
(I am amazed that TryWhy3 manages to avoid other uses of Str regexps — we seem to have quite a number of them in Why3.)1.1.0https://gitlab.inria.fr/why3/why3/-/issues/149Flocq 3.0.0 cannot be recognized2018-09-04T10:45:56+02:00Ghost UserFlocq 3.0.0 cannot be recognizedWhy3 version: 1.0.0
`./configure` can't recognize flocq 3.0.0.
It seems that `./configure` check `Require Import Flocq.Flocq_version` on Coq.
But `Flocq.Flocq_version` module has been replaced with `Flocq.Version` module from version...Why3 version: 1.0.0
`./configure` can't recognize flocq 3.0.0.
It seems that `./configure` check `Require Import Flocq.Flocq_version` on Coq.
But `Flocq.Flocq_version` module has been replaced with `Flocq.Version` module from version 3.0.0.
(P.S. Congratulations for new major release!)1.1.0Guillaume MelquiondGuillaume Melquiondhttps://gitlab.inria.fr/why3/why3/-/issues/147Session is always considered as outdated on startup2018-09-04T10:45:56+02:00Guillaume MelquiondSession is always considered as outdated on startupI suppose that is because I pass an `.mlw` file to `why3 ide`, which causes it to send an `Add_file_req` request to the server, which causes the session to be marked as "needs saving".I suppose that is because I pass an `.mlw` file to `why3 ide`, which causes it to send an `Add_file_req` request to the server, which causes the session to be marked as "needs saving".1.1.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/138Remaining TODOs for Range and Float2018-08-14T14:24:32+02:00François BobotRemaining TODOs for Range and FloatSome todos remain in pretty.ml and theory.ml aboute Range and Float constructorSome todos remain in pretty.ml and theory.ml aboute Range and Float constructor1.0.0https://gitlab.inria.fr/why3/why3/-/issues/137Readd smoke detector2018-06-18T18:11:46+02:00François BobotReadd smoke detectorReadd the functionnality of smoke detector in why3 replay. Removed in commit 57de2a1485e5d2d29c71d8205a33838ffee6fba3Readd the functionnality of smoke detector in why3 replay. Removed in commit 57de2a1485e5d2d29c71d8205a33838ffee6fba31.0.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/136Make `any ... ensures` less error-prone2018-06-22T11:28:03+02:00Guillaume MelquiondMake `any ... ensures` less error-proneI didn't know that `any ... ensures` introduces an axiom. And I was not the only developer to get it wrong. We really should limit the number of language constructions that introduce axioms.
There are only three occurrences of this cons...I didn't know that `any ... ensures` introduces an axiom. And I was not the only developer to get it wrong. We really should limit the number of language constructions that introduce axioms.
There are only three occurrences of this construction in the gallery:
- `unraveling_a_card_trick`: `any int ensures { 0 <= result <= n*m }`
- `white_and_black_balls`: `any (x: int, y: int) ensures { 0 <= x && 0 <= y && x + y = 2 && x <= !b && y <= !w }`
- `vstte12_bfs`: `any B.t ensures { !!result = succ v }`
The first two occurrences are actually provable, so I am not sure their authors intended them to generate axioms. The last one is an actual axiom, but it should ideally have been `val`, so that the user could instantiate it to obtain an effective algorithm.
Thus, I suggest that this construction be repurposed so that it generates a verification condition.1.0.0https://gitlab.inria.fr/why3/why3/-/issues/134bisect should not raise Invalid_argument2018-10-04T15:07:54+02:00Guillaume Melquiondbisect should not raise Invalid_argument1.1.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/133Finalize the use of prover alternative "counterexamples" to get counterexamples2018-12-21T13:51:33+01:00Guillaume MelquiondFinalize the use of prover alternative "counterexamples" to get counterexamples1.2.0https://gitlab.inria.fr/why3/why3/-/issues/128Transformation `split_vc` and term shapes2018-06-13T16:56:30+02:00Guillaume MelquiondTransformation `split_vc` and term shapesThe transformation `split_vc` splits the goals, simplifies trivial quantifications, and then introduces premises. Unfortunately, it means that we might end up with several proof tasks that have exactly the same shape as children of a sin...The transformation `split_vc` splits the goals, simplifies trivial quantifications, and then introduces premises. Unfortunately, it means that we might end up with several proof tasks that have exactly the same shape as children of a single node of the proof tree. As a consequence, pairing gets completely confused as soon as the code is modified.
A solution would be to change the shape algorithm so that it also hashes the premises that have been marked by `introduce_premises`. This might considerably increase the size of the shapes, but that will also make the pairing algorithm more reliable.
I mark this issue as blocking, since `split_vc` is the recommended transformation for newcomers.1.0.0Raphaël Rieu-HelftRaphaël Rieu-Helft