1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
|
module WithInt32
use int.Int
use mach.int.Int32
let f (n min max:int32) : int32
ensures { min <= result <= max }
=
let _x = min + max in
if n < min then min else if n > max then max else n
end
(** same version with (signed) bit-vectors *)
module WithBV32
use int.Int
use bv.BV32
use mach.bv.BVCheck32
let f (n min max:BV32.t) : BV32.t
ensures { ule min result /\ ule result max }
(* ensures { BV32.t'int min <= BV32.t'int result <= BV32.t'int max } *)
=
let _x = u_add min max in
if u_lt n min then min else if u_gt n max then max else n
end
|
