Commit 97843952 authored by Sylvain Dailler's avatar Sylvain Dailler

ce-bench add example with a record with invariant

parent 80334a31
(*****************************************
** Getting counterexamples for records **
*****************************************)
module M
use ref.Ref
use int.Int
(*** In all cases, records are decomposed using match eval ***)
type r = {f [@model_trace:.my_field_f] :int; g:bool}
invariant { f = 0 }
let record_match_eval_test1 (x : r) : int
ensures { result = 1 }
=
if x.g then
x.f
else
1
let record_match_eval_test2 (x : r ) : int
ensures { result = 1 }
=
x.f
let record_match_eval_test3 (x : ref r) : unit
ensures { !x.g }
=
x := { !x with f = 6}
let record_match_eval_test4 (x : ref r) : r
ensures { result.g }
=
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
let test_record_match_eval_test5 (x : ref r) : r
ensures { result = !re }
=
x := { !x with f = 6 };
!x
end
module Mutable
use int.Int
type r = {mutable f [@model_trace:.my_field_f] :int; mutable g:bool}
let record_match_eval_test1 (x : r) : int
ensures { result = 1 }
=
if x.g then
x.f
else
1
let record_match_eval_test2 (x : r ) : int
ensures { result = 1 }
=
x.f
let record_match_eval_test3 (x : r) : unit
ensures { x.g }
=
x.f <- 6
let record_match_eval_test4 (x : r) : r
ensures { result.g }
=
x.f <- 6;
x
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