MARCHE Claude (33a58e17) at 28 Mar 16:12
constrains the type of argument for meta model_projection
Closes #841
MARCHE Claude (f8a7b300) at 28 Mar 15:51
BONNOT Paul (8aca4387) at 28 Mar 15:49
MARCHE Claude (f8a7b300) at 28 Mar 15:49
Merge branch '839-forward_propagation-strategy-sin-and-cos-support-...
... and 1 more commit
Closes #839
BONNOT Paul (8aca4387) at 28 Mar 13:33
Add sin and cos support
Closes #839
BONNOT Paul (4db33118) at 28 Mar 12:37
It needs some cleanup before, I'm on it.
Still pertinent, I think it could be useful for the forward_propagation strategy when we try to be smarter in our analysis of the task.
The bug is still present in master branch, and is not a known bug as far as I know. Thanks for reporting it
Is this MR still pertinent @pbonnot ? or should it be abandoned ?
What is the status of this MR @pbonnot ? Could it be marked as ready and reviewed?
Andrei Paskevich (212b5fab) at 27 Mar 23:55
coma: do not precompute unneeded subVCs
I came across a surprising behavior of the why3 execute
command (why3 plateform 1.6.0).
Here's a shrinked example, to help reproducing the error.
module Issue
use bintree.Tree
use bintree.Inorder
use list.List
let issue () =
let l = inorder Empty in
assert { l = Nil }
end
With why3 ide
, it behaves as excepted : one VC is generated, and the assertion is easily discharged automatically.
With why3 execute
, I get the following error message :
$ why3 execute issue.mlw --use=Issue 'issue ()'
Type mismatch between bintree.Tree.tree 'a and bintree.Tree.tree 'xi
Is this a known issue for version 1.6.0 of why3 ?
I have tried to provide more guidance to type inference using type annotations, but this doesn't solve the problem.
Thanks
the meta model_projection
has the following form
meta "model_projection" function f
where f
is a unary function say from some type t
. It allows to obtain values in counterexamples say when t
is an abstract type. It can also be used when t
is not abstract. Yet, when t
is an alias type then the current implementation produces some unexpected behavior, and indeed it is unclear what should be done in such a case. It is thus preferable that Why3 simply signals an error when t
is an alias type.
executing why3 session create
displays spurious debug messages regarding the directory and the session file created. They should be visible only when some debug flag is set
I noticed that we did not took into account the possibilities of !680 (merged) in the typing.ml
code for the content of interfaces from !557 (merged). I just added a commit extending it.
It means logic definitions are now refined as intended, and we can include inductives and exceptions without problems