Merge branch 'cleaning_again_example_sin_cos' into 'master'
[why3.git] / stdlib / microc.mlw
blob2d293aba8d27d7e982a5a098ce64acf1c9af19e7
2 (** Support library for the Micro-C format. *)
4 module MicroC
6   use int.Int
7   use ref.Ref
8   use array.Array
10   function length (a: array 'a) : int =
11     Array.length a
13   function ([]) (a: array 'a) (i: int) : 'a =
14     Array.([]) a i
16   function ([<-]) (a: array 'a) (i: int) (v: 'a) : array 'a =
17     Array.([<-]) a i v
19   let ([]) (a: array 'a) (i: int) : 'a
20     requires { [@expl:index in array bounds] 0 <= i < Array.length a }
21     ensures  { result = a[i] }
22   = Array.([]) a i
24   let ([]<-) (a: array 'a) (i: int) (v: 'a) : unit
25     requires { [@expl:index in array bounds] 0 <= i < Array.length a }
26     ensures  { a = Array.([<-]) (old a) i v }
27   = Array.([]<-) a i v
29   use map.Occ
31   function occurrence (v: 'a) (a: array 'a) : int =
32     Occ.occ v a.Array.elts 0 a.Array.length
34   use export int.ComputerDivision
36   val (/) (x y: int) : int
37     requires { [@expl:check division by zero] y <> 0 }
38     ensures  { result = div x y }
40   val (/=) (ref x: int) (y: int) : unit writes {x}
41     requires { [@expl:check division by zero] y <> 0 }
42     ensures  { x = div (old x) y }
44   val (%) (x y: int) : int
45     requires { y <> 0 }
46     ensures  { result = mod x y }
48   (* operators ++ -- on integers *)
49   let __postinc (ref r: int) : int
50     ensures { r = old r + 1 }
51     ensures { result = old r }
52   = let v = r in r <- r + 1; v
54   let __postdec (ref r: int) : int
55     ensures { r = old r - 1 }
56     ensures { result = old r }
57   = let v = r in r <- r - 1; v
59   let __preinc (ref r: int) : int
60     ensures { result = r = old r + 1 }
61   = r <- r + 1; r
63   let __predec (ref r: int) : int
64     ensures { result = r = old r - 1 }
65   = r <- r - 1; r
67   (* operators ++ -- on array elements *)
68   let __arrpostinc (a: array int) (i: int) : int
69     requires { [@expl:index in array bounds] 0 <= i < Array.length a }
70     ensures  { a = (old a)[i <- (old a)[i] + 1] }
71     ensures  { result = old a[i] }
72   = let v = a[i] in a[i] <- v + 1; v
74   let __arrpostdec (a: array int) (i: int) : int
75     requires { [@expl:index in array bounds] 0 <= i < Array.length a }
76     ensures  { a = (old a)[i <- (old a)[i] - 1] }
77     ensures  { result = old a[i] }
78   = let v = a[i] in a[i] <- v - 1; v
80   let __arrpreinc (a: array int) (i: int) : int
81     requires { [@expl:index in array bounds] 0 <= i < Array.length a }
82     ensures  { a = (old a)[i <- (old a)[i] + 1] }
83     ensures  { result = a[i] }
84   = a[i] <- a[i] + 1; a[i]
86   let __arrpredec (a: array int) (i: int) : int
87     requires { [@expl:index in array bounds] 0 <= i < Array.length a }
88     ensures  { a = (old a)[i <- (old a)[i] - 1] }
89     ensures  { result = a[i] }
90   = a[i] <- a[i] - 1; a[i]
92   (* operators += -= on array elements *)
93   let __array_add (a: array int) (i: int) (x: int) : unit
94     requires { [@expl:index in array bounds] 0 <= i < Array.length a }
95     ensures  { a = (old a)[i <- (old a)[i] + x] }
96   = a[i] <- a[i] + x
98   let __array_sub (a: array int) (i: int) (x: int) : unit
99     requires { [@expl:index in array bounds] 0 <= i < Array.length a }
100     ensures  { a = (old a)[i <- (old a)[i] - x] }
101   = a[i] <- a[i] - x
103   let __array_mul (a: array int) (i: int) (x: int) : unit
104     requires { [@expl:index in array bounds] 0 <= i < Array.length a }
105     ensures  { a = (old a)[i <- (old a)[i] * x] }
106   = a[i] <- a[i] * x
108   let __array_div (a: array int) (i: int) (x: int) : unit
109     requires { [@expl:index in array bounds] 0 <= i < Array.length a }
110     requires { [@expl:check division by zero] x <> 0 }
111     ensures  { a = (old a)[i <- div (old a)[i] x] }
112   = a[i] <- a[i] / x
114   (* to initialize stack-allocated variables *)
116   val any_int () : int
118   val alloc_array (n: int) : array int
119     requires { n >= 0 }
120     ensures  { length result = n }
122   (* C library *)
124   val rand () : int
125     ensures  { 0 <= result }
127   val scanf (ref r: int) : unit
128     writes { r }
130   exception Break
132   exception Return int