programs: more tests

parent 850d3a26
(* side effects in tests *)
parameter x : int ref
parameter set_and_test_zero :
v:int ->
{} bool writes x { !x = v and if result=True then !x = 0 else !x <> 0 }
let p () = {} if set_and_test_zero 0 then 1 else 2 { result = 1 }
parameter set_and_test_nzero :
v:int ->
{} bool writes x { !x = v and if result=True then !x <> 0 else !x = 0 }
let p2 (y:int ref) =
{ !y >= 0 }
while set_and_test_nzero !y do
invariant { !y >= 0 } variant { !y }
y := !y - 1
done
{ !y = 0 }
let p3 (y:int ref) =
{ !y >= 0 }
while let b = set_and_test_nzero !y in b do
invariant { !y >= 0 } variant { !y }
y := !y - 1
done
{ !y = 0 }
let p4 (y:int ref) =
{ !y >= 1 }
while begin y := !y - 1; (set_and_test_nzero !y) end do
invariant { !y >= 1 } variant { !y }
()
done
{ !y = 0 }
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/set"
End:
*)
../programs/good/set.mlw
\ No newline at end of file
......@@ -511,7 +511,7 @@ let variant loc env (t, ps) =
| [t1; _] when Ty.ty_equal t1 t.t_ty ->
t, ps
| [t1; _] ->
errorm ~loc "variant has type %a, but is expected to have type %a"
errorm ~loc "@[variant has type %a, but is expected to have type %a@]"
Pretty.print_ty t.t_ty Pretty.print_ty t1
| _ ->
assert false
......
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