Commit def34e58 authored by Andrei Paskevich's avatar Andrei Paskevich


parent 9473d725
library/gallery migration
- check that examples/tests/cvc4-models.mlw can use arrays
instead of ref map (commit dfc90d)
- remove the temporary --type-only from bench/bench (commit 02be08f)
- DISCUSS: why3 prove theories/int.why fails because of a "variant"
clause in one of let functions: this clause requires int.Int
for the order relation, which is not loaded automatically
(program modules are expected to do "use import int.Int")
and, of course, cannot be used explicitly inside int.why.
- expression { e with f2 = e2 } is syntactic sugar for
{ f1 = e.f1; f2 = e2; f3 = e.f3 }
......@@ -15,7 +26,7 @@ typing
is "unbound symbol 'foo'", which is not correct
(is should rather be that "foo" has the wrong type)
- bench/programs/bad-to-keep/at1.mlw
- bench/programs/bad-to-keep/{at1.mlw,old2.mlw}
should at least produce a warning (meaningless 'old')
- no warning on lemma functions
......@@ -23,6 +34,9 @@ typing
- cloning a recursive data type (e.g. clone list.List)
- "old" and "at" in program code gives a syntax error
(bench/programs/bad-to-keep/old3.mlw), we can do better
module M
use import int.Int
use import ref.Ref
let test1 (x: ref int)
ensures { !x >= old !x }
requires { !x >= 0}
= x := !x - 1;
assert { !x >= old !x }
(* old not allowed in programs *)
module Test
use import ref.Refint
let test (x: ref int) =
if !x = old !x then 1 else 2
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment