Commit e8a6fe0f authored by Sylvain Dailler's avatar Sylvain Dailler

ce-bench: Add new tests

parent 99f12932
module Array
use int.Int
use map.Map
type array = private {
mutable ghost elts : int -> int;
length : int
} invariant { 0 <= length }
function ([]) (a: array) (i: int) : int = a.elts i
val ([]) (a: array) (i: int) : int
requires { [@expl:index in array bounds] 0 <= i < length a }
ensures { result = a[i] }
val ghost function ([<-]) (a: array) (i: int) (v: int): array
ensures { result.length = a.length }
ensures { result.elts = Map.set a.elts i v }
val ([]<-) (a: array) (i: int) (v: int) : unit writes {a}
requires { [@expl:index in array bounds] 0 <= i < length a }
ensures { a.elts = Map.set (old a).elts i v }
ensures { a = (old a)[i <- v] }
end
module A
use int.Int
use Array
let f1 (a:array) : int
= a[0]
let f2 (a:array) : unit
requires { a.length >= 2 }
ensures { a[0] <> a[1] }
= a[0] <- 42
end
(*
module B
use int.Int
use array.Array
clone array.Sorted with
type elt=int,
predicate le=(<=)
let f1 (a:array int) : unit
ensures { sorted a }
= ()
let f2 (a:array int) : array int
ensures { sorted result }
= a
end
*)
\ No newline at end of file
......@@ -34,6 +34,13 @@ module M
=
x := { !x with f = 6 };
!x
let record_match_eval_test44 (x : ref r) : r
ensures { result.g }
= [@vc:sp]
x := { !x with f = 6 };
assert { !x.f = 12};
!x
val re : ref r
......@@ -78,4 +85,18 @@ module Mutable
x.f <- 6;
x
let record_old_test1 (x : r) : unit
ensures { old x.f = x.f}
=
x.f <- 6
let record_at_test2 (x : r) : unit
=
label L in
x.f <- 6;
label M in
x.f <- 12;
assert { x at L = x at M}
end
module Ref
type ref = { mutable contents [@model_trace:] : int }
function (!) (x: ref) : int = x.contents
let ref (v: int) ensures { result = { contents = v } } = { contents = v }
let (!) (r:ref) ensures { result = !r } = r.contents
let (:=) (r:ref) (v:int) ensures { !r = v } = r.contents <- v
end
module M
use list.List
use int.Int
use Ref
let test_post (x: int) (y: ref): unit
ensures { old !y >= x }
=
y := x - 1 + !y
let test_post2 (x: int) (y: ref): unit
requires { x > 42 }
ensures { old !y > !y + x }
=
y := x - 1 + !y
(**********************************************************
** Getting counterexamples for terms of primitive types **
**********************************************************)
val y :ref
let incr (x23: ref): unit
ensures { !x23 = old !x23 + 2 + !y }
=
(*#"random_path.random" 62 27 32#*)
y := !y + 1;
x23 := !x23 + 1;
x23 := !x23 + 1
let test_loop (x: ref): unit
ensures { !x < old !x }
=
label L in
incr x;
label M in
while !x > 0 do
invariant { !x > !x at L + !x at M }
variant { !x }
x := !x - 1
done
end
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