why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2023-11-13T14:55:01+01:00https://gitlab.inria.fr/why3/why3/-/issues/719`Split_vc` takes a lot of time when used in huge context2023-11-13T14:55:01+01:00François Bobot`Split_vc` takes a lot of time when used in huge context`Split_vc` uses substitution which have a bad behavior with huge context.
```
let simplify_intros =
Trans.compose introduce_premises
(Subst.subst_filtered ~subst_proxy:false subst_filter)
let split_vc =
Trans.compo...`Split_vc` uses substitution which have a bad behavior with huge context.
```
let simplify_intros =
Trans.compose introduce_premises
(Subst.subst_filtered ~subst_proxy:false subst_filter)
let split_vc =
Trans.compose_l
(*** do test:
(Trans.compose Simplify_formula.simplify_trivial_wp_quantification
*)
(Trans.compose generalize_intro Split_goal.split_goal_right)
(Trans.singleton simplify_intros)
```
We are trying to create a toy example, but in any case it seems strange that `split_vc` looks at all the task. What is the goal os this substitution?
The lot of time is that a reload in the IDE can take 14min.1.8.0Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/778Cleaning code2023-07-17T15:06:07+02:00MARCHE ClaudeCleaning codeThis is a minor issue, nothing visible from users, but there are a few possible code reorganization that should be done:
- [ ] module `Model_parser` should be moved from `core` to `driver`
- [ ] attributes and such declared in `Ident` sh...This is a minor issue, nothing visible from users, but there are a few possible code reorganization that should be done:
- [ ] module `Model_parser` should be moved from `core` to `driver`
- [ ] attributes and such declared in `Ident` should be declared in a more appropriate place
- [ ] ?
This issue is a good candidate for hackathon exercises ;-)https://gitlab.inria.fr/why3/why3/-/issues/747extend set of axioms annotated with axioms dependencies2023-09-06T13:45:48+02:00MARCHE Claudeextend set of axioms annotated with axioms dependenciesSet of symbols to annotate:
- [ ] int.Exponentiation.power
- [ ] int.NumOf.numof
- [ ] int.Sum.sum
- [ ] int.Fact.fact
- [ ] int.Iter.iter
- [ ] int.Fibonacci.fib
- [ ] int.WFltof.ltof
- [x] bv.Pow2.pow2
- [ ] bv.BVgen.nth_bv
- [x] bv.BV...Set of symbols to annotate:
- [ ] int.Exponentiation.power
- [ ] int.NumOf.numof
- [ ] int.Sum.sum
- [ ] int.Fact.fact
- [ ] int.Iter.iter
- [ ] int.Fibonacci.fib
- [ ] int.WFltof.ltof
- [x] bv.Pow2.pow2
- [ ] bv.BVgen.nth_bv
- [x] bv.BVgen.uge
- [x] bv.BVgen.ugt
- [x] bv.BVgen.ule
- [x] bv.BVgen.ult
- [x] bv.BVgen.sge
- [x] bv.BVgen.sgt
- [x] bv.BVgen.sle
- [x] bv.BVgen.slt
- [ ] option.Option.is_none
- [ ] option.Map.map
- [ ] to be continued, say with `list.mlw`, etc.1.8.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/741eliminate_if is not robust enough against if in triggers2023-07-18T19:01:30+02:00Guillaume Cluzeleliminate_if is not robust enough against if in triggersWhen Gappa is called, its driver call the transformation `inline_all` and later `eliminate_if`.
```
module M
function f (x : int) : int = if x = 0 then x else x
predicate p (y : bool) = y
axiom x: forall x, y [f x]. p y -> x = f x...When Gappa is called, its driver call the transformation `inline_all` and later `eliminate_if`.
```
module M
function f (x : int) : int = if x = 0 then x else x
predicate p (y : bool) = y
axiom x: forall x, y [f x]. p y -> x = f x
lemma l: forall y. p y
end
```
The combination of the two transformations fails on a such program and we get a message like:
```
internal failure: Failure in transformation eliminate_if
This expression isn't supported:
if x = 0 then x else x
cannot eliminate 'if-then-else' in trigger terms
```
As the transformation fails, it becomes impossible to use Gappa on any program that uses an axiom with a trigger like exposed in the example.
Wouldn't it be possible to remove the trigger in a such case if it is not possible to do something smarter?https://gitlab.inria.fr/why3/why3/-/issues/740Incorrect error message2023-03-20T14:27:54+01:00Xavier DenisIncorrect error messageWhen using function literals, we can get unexpected error messages like with the following program:
```
let x () = [| 0; |]
```
Giving the following error:
```
File "../dummy2.mlw", line 2, characters 14-15: Logical symbol (=) is used...When using function literals, we can get unexpected error messages like with the following program:
```
let x () = [| 0; |]
```
Giving the following error:
```
File "../dummy2.mlw", line 2, characters 14-15: Logical symbol (=) is used in a non-ghost context
```
The solution is to `use int.Int` but it would be better to output a more actionable error instead.https://gitlab.inria.fr/why3/why3/-/issues/726keep less unused symbols2023-09-06T13:46:00+02:00MARCHE Claudekeep less unused symbolsFor the purpose of counterexamples, a lot of variables introduced with `let` that are kept as `let` definition, even if they are substituted in the body of the `let`.
This feature is needed only for some variables, e.g. the ones that st...For the purpose of counterexamples, a lot of variables introduced with `let` that are kept as `let` definition, even if they are substituted in the body of the `let`.
This feature is needed only for some variables, e.g. the ones that store the results of function calls. It should be possible to identify these variables when they are generated in `vc.ml`, say with a specific attribute `keep_even_unused`. If this was done, then the keeping of such "unused" variables could be relaxed and done only when the attribute in question is present.1.8.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/633Review the set of 'old versions' of provers2023-08-29T16:14:53+02:00MARCHE ClaudeReview the set of 'old versions' of proversCurrently, the versions of provers that are NOT considered "old" include Alt-Ergo 2.0.0 to 2.3.3, CVC4 1.5 to 1.7, Gappa 1.0.0 to 1.2.2, Vampire 0.6, Z3 4.5.0 to 4.7.1. CVC3 2.4.1 is not considered old either.
- [ ] Alt-Ergo 2.0.0 to 2....Currently, the versions of provers that are NOT considered "old" include Alt-Ergo 2.0.0 to 2.3.3, CVC4 1.5 to 1.7, Gappa 1.0.0 to 1.2.2, Vampire 0.6, Z3 4.5.0 to 4.7.1. CVC3 2.4.1 is not considered old either.
- [ ] Alt-Ergo 2.0.0 to 2.3.3
- [ ] CVC4 1.5 to 1.7
- [ ] Gappa 1.0.0 to 1.2.2
- [ ] Vampire 0.6
- [ ] Z3 4.5.0 to 4.7.1
- [ ] E prover 1.4 and 1.6 to 2.x
I believe that all those versions (at least) should be considered as "old".
Incidentally, our bench should not include any of those old versions anymore, all sessions should be upgraded to more recent versions of provers. At the same occasion, old versions of provers could be removed from the moloch server.Matteo ManighettiMatteo Manighettihttps://gitlab.inria.fr/why3/why3/-/issues/393type invariant preservation question2019-11-27T13:19:54+01:00DAILLER Sylvaintype invariant preservation questionI have a quite simple question about the behavior of type invariant. In the simple program below, I am asked by the tool to prove a type invariant inside function `g` for variable `e` (after split). I would have expected this invariant t...I have a quite simple question about the behavior of type invariant. In the simple program below, I am asked by the tool to prove a type invariant inside function `g` for variable `e` (after split). I would have expected this invariant to be ensured in the proof for `f`. Is there a way to tell the tool "at this point of program type invariants should hold" ?
```
module Example
type r = { mutable p: int }
invariant { p = 42 }
let f (e: r)
writes {e}
ensures { true }
=
e.p <- 42
let g ()
diverges
=
let e: r = { p = 42 } in
while true do
f (e);
done
end
```https://gitlab.inria.fr/why3/why3/-/issues/315Too much ghostification?2022-03-22T16:55:27+01:00Benedikt BeckerToo much ghostification?In the following example, the ghostification that is introduced by line 16, is expanded to line 12, which results in a compilation error.
The example code works fine when `f` is non-recursive, when the `ghost` keyword is removed from li...In the following example, the ghostification that is introduced by line 16, is expanded to line 12, which results in a compilation error.
The example code works fine when `f` is non-recursive, when the `ghost` keyword is removed from line 16, or when an `; ()` is added after line 16.
```
$ cat test.mlw
module Test
use option.Option
let ref x = ()
exception E
type t = A | B
let rec f (t: t) diverges raises { E -> true } =
match t with
| A ->
x <- () (* Line 12 *)
| B ->
try
f t;
ghost () (* Line 16 *)
with E ->
raise E
end
end
end
$ why3 extract --modular -D ocaml64 -L . test.Test -o /tmp
File "./test.mlw", line 12, characters 6-13:
This expression makes a ghost modification in the non-ghost variable x
```Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/171Extraction of absurd2020-10-23T17:36:51+02:00MARCHE ClaudeExtraction of absurdExtraction of ```absurd``` is currently ```assert false``` which is perfectly fine. Though, during development it happens that ```absurd``` is temporary used on "todo" branches as one uses ``` assert false``` in OCaml. In that case, it w...Extraction of ```absurd``` is currently ```assert false``` which is perfectly fine. Though, during development it happens that ```absurd``` is temporary used on "todo" branches as one uses ``` assert false``` in OCaml. In that case, it would be a very interesting feature if the line number of the original Why3 file be given so that the "Assert_failure" exception raised could point to the proper Why3 file and the proper line. This could be done easily by inserting
```
# <line number> <mlw file name>
```
on the line before ```assert false```PARREIRA PEREIRA Mário JoséPARREIRA PEREIRA Mário Joséhttps://gitlab.inria.fr/why3/why3/-/issues/30Refresh does not reload source view, causing loss of work2019-10-25T15:12:27+02:00Raphaël Rieu-HelftRefresh does not reload source view, causing loss of workRefreshing the session with Ctrl-R does not reload the source view. I lost work from this with the following steps:
1) Open Why3 ide
2) Edit the source file in your favorite editor
3) Reload (source view does not change)
4) Edit the ...Refreshing the session with Ctrl-R does not reload the source view. I lost work from this with the following steps:
1) Open Why3 ide
2) Edit the source file in your favorite editor
3) Reload (source view does not change)
4) Edit the file from Why3 ide (in my case, inadvertently by pressing tab a few times in the ide), save file
5) You lose the work from 2)MARCHE ClaudeMARCHE Claude