Commit 46ecb6d8 authored by Sylvain Dailler's avatar Sylvain Dailler

ce-bench: Add a test for records with one field and an invariant

parent 97843952
module Ref
use int.Int
type ref = { mutable contents : int}
invariant {contents >= 0 \/ contents <= 0}
function (!) (x: ref) : int = x.contents
let ref1 (v: int) ensures { contents result = 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