Commit bb743fab authored by Andrei Paskevich's avatar Andrei Paskevich

fix WhyML warnings about unused variables in examples

parent b67fb7c0
......@@ -62,7 +62,7 @@ let p12 () ensures { result = 2 }
= try
begin raise E; raise (F 1); 1 end
with E -> 2
| F x -> 3
| F _ -> 3
end
let p13 () ensures { !x = 2 }
......
......@@ -10,7 +10,7 @@ val f () : unit writes {x} ensures { !x = 1 - old !x }
let p () =
'Init:
begin
let t = () in ();
let _t = () in ();
(f ());
(f ());
assert { !x = at !x 'Init };
......
......@@ -252,8 +252,8 @@ use export list.List
function type_value (v:value) : datatype =
match v with
| Vvoid -> TYunit
| Vint int -> TYint
| Vbool bool -> TYbool
| Vint _ -> TYint
| Vbool _ -> TYbool
end
inductive type_operator (op:operator) (ty1 ty2 ty: datatype) =
......@@ -452,7 +452,7 @@ predicate fresh_in_fmla (id:ident) (f:fmla) =
fresh_in_fmla id f1 /\ fresh_in_fmla id f2
| Fnot f -> fresh_in_fmla id f
| Flet y t f -> id <> y /\ fresh_in_term id t /\ fresh_in_fmla id f
| Fforall y ty f -> id <> y /\ fresh_in_fmla id f
| Fforall y _ f -> id <> y /\ fresh_in_fmla id f
end
......
......@@ -114,7 +114,7 @@ predicate fresh_in_fmla (id:ident) (f:fmla) =
fresh_in_fmla id f1 /\ fresh_in_fmla id f2
| Fnot f -> fresh_in_fmla id f
| Flet y t f -> id <> y /\ fresh_in_term id t /\ fresh_in_fmla id f
| Fforall y ty f -> id <> y /\ fresh_in_fmla id f
| Fforall y _ f -> id <> y /\ fresh_in_fmla id f
end
function subst (f:fmla) (x:ident) (v:ident) : fmla =
......
This diff is collapsed.
......@@ -166,7 +166,6 @@ module M
invariant { reverse (model (old_next) (old_p)) =
reverse (model !next !p) ++ model !next !q }
let tmp = !next[!p] in
let bak_next = !next in
next := !next[!p <- !q];
assert { (reverse (Cons !p (model !next tmp))) ++ (model !next !q) =
(reverse (model !next tmp)) ++ (Cons !p (model !next !q))};
......@@ -328,8 +327,7 @@ module M2
requires { is_list !next !p }
ensures { is_list !next !result }
ensures { reverse (model (old !next) (old !p)) = model !next !result }
= let old_next = !next in
let old_p = !p in
= let old_p = !p in
let q = ref null in
'Init:
while !p <> null do
......@@ -338,7 +336,6 @@ module M2
invariant { reverse (model (at !next 'Init) (old_p)) =
reverse (model !next !p) ++ model !next !q }
let tmp = !next[!p] in
let bak_next = !next in
next := !next[!p <- !q];
(* assert { (reverse (Cons p (model !next tmp))) ++ (model !next q) = *)
(* (reverse (model !next tmp)) ++ (Cons p (model !next q))}; *)
......
......@@ -85,7 +85,7 @@ module RedBlackTree
predicate bst (t : tree) =
match t with
| Leaf -> true
| Node _ l k v r -> bst l /\ bst r /\ lt_tree k l /\ gt_tree k r
| Node _ l k _ r -> bst l /\ bst r /\ lt_tree k l /\ gt_tree k r
end
lemma bst_Leaf : bst Leaf
......
......@@ -238,8 +238,8 @@ module ZipperBased
requires { (* list [left] satisfies the invariant *)
g left /\
(* when [left] has one element, it can't be a solution *)
match left with Cons (d1, t1) Nil -> d1 <> 0 \/ right <> Nil
| _ -> true end /\
match left with Cons (d1, _) Nil -> d1 <> 0 \/ right <> Nil
| _ -> true end /\
(* apart (possibly) from its head, all elements in [right] are leaves;
moreover the left branch of [right]'s head already satisfies
invariant [g] when consed to [left] *)
......
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