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
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
|
(** Support library for the Micro-C format. *)
module MicroC
use int.Int
use ref.Ref
use array.Array
function length (a: array 'a) : int =
Array.length a
function ([]) (a: array 'a) (i: int) : 'a =
Array.([]) a i
function ([<-]) (a: array 'a) (i: int) (v: 'a) : array 'a =
Array.([<-]) a i v
let ([]) (a: array 'a) (i: int) : 'a
requires { [@expl:index in array bounds] 0 <= i < Array.length a }
ensures { result = a[i] }
= Array.([]) a i
let ([]<-) (a: array 'a) (i: int) (v: 'a) : unit
requires { [@expl:index in array bounds] 0 <= i < Array.length a }
ensures { a = Array.([<-]) (old a) i v }
= Array.([]<-) a i v
use map.Occ
function occurrence (v: 'a) (a: array 'a) : int =
Occ.occ v a.Array.elts 0 a.Array.length
use export int.ComputerDivision
val (/) (x y: int) : int
requires { [@expl:check division by zero] y <> 0 }
ensures { result = div x y }
val (/=) (ref x: int) (y: int) : unit writes {x}
requires { [@expl:check division by zero] y <> 0 }
ensures { x = div (old x) y }
val (%) (x y: int) : int
requires { y <> 0 }
ensures { result = mod x y }
(* operators ++ -- on integers *)
let __postinc (ref r: int) : int
ensures { r = old r + 1 }
ensures { result = old r }
= let v = r in r <- r + 1; v
let __postdec (ref r: int) : int
ensures { r = old r - 1 }
ensures { result = old r }
= let v = r in r <- r - 1; v
let __preinc (ref r: int) : int
ensures { result = r = old r + 1 }
= r <- r + 1; r
let __predec (ref r: int) : int
ensures { result = r = old r - 1 }
= r <- r - 1; r
(* operators ++ -- on array elements *)
let __arrpostinc (a: array int) (i: int) : int
requires { [@expl:index in array bounds] 0 <= i < Array.length a }
ensures { a = (old a)[i <- (old a)[i] + 1] }
ensures { result = old a[i] }
= let v = a[i] in a[i] <- v + 1; v
let __arrpostdec (a: array int) (i: int) : int
requires { [@expl:index in array bounds] 0 <= i < Array.length a }
ensures { a = (old a)[i <- (old a)[i] - 1] }
ensures { result = old a[i] }
= let v = a[i] in a[i] <- v - 1; v
let __arrpreinc (a: array int) (i: int) : int
requires { [@expl:index in array bounds] 0 <= i < Array.length a }
ensures { a = (old a)[i <- (old a)[i] + 1] }
ensures { result = a[i] }
= a[i] <- a[i] + 1; a[i]
let __arrpredec (a: array int) (i: int) : int
requires { [@expl:index in array bounds] 0 <= i < Array.length a }
ensures { a = (old a)[i <- (old a)[i] - 1] }
ensures { result = a[i] }
= a[i] <- a[i] - 1; a[i]
(* operators += -= on array elements *)
let __array_add (a: array int) (i: int) (x: int) : unit
requires { [@expl:index in array bounds] 0 <= i < Array.length a }
ensures { a = (old a)[i <- (old a)[i] + x] }
= a[i] <- a[i] + x
let __array_sub (a: array int) (i: int) (x: int) : unit
requires { [@expl:index in array bounds] 0 <= i < Array.length a }
ensures { a = (old a)[i <- (old a)[i] - x] }
= a[i] <- a[i] - x
let __array_mul (a: array int) (i: int) (x: int) : unit
requires { [@expl:index in array bounds] 0 <= i < Array.length a }
ensures { a = (old a)[i <- (old a)[i] * x] }
= a[i] <- a[i] * x
let __array_div (a: array int) (i: int) (x: int) : unit
requires { [@expl:index in array bounds] 0 <= i < Array.length a }
requires { [@expl:check division by zero] x <> 0 }
ensures { a = (old a)[i <- div (old a)[i] x] }
= a[i] <- a[i] / x
(* to initialize stack-allocated variables *)
val any_int () : int
val alloc_array (n: int) : array int
requires { n >= 0 }
ensures { length result = n }
(* C library *)
val rand () : int
ensures { 0 <= result }
val scanf (ref r: int) : unit
writes { r }
exception Break
exception Return int
end
|
