source: Deliverables/D3.1/C-semantics/acc-0.1.spaces.patch @ 648

Last change on this file since 648 was 416, checked in by campbell, 9 years ago

Fix printing of switch statements as matita terms.

File size: 130.1 KB
RevLine 
[292]1diff --git a/cparser/AddCasts.ml b/cparser/AddCasts.ml
2index 9ec128d..5f5184c 100644
3--- a/cparser/AddCasts.ml
4+++ b/cparser/AddCasts.ml
5@@ -39,7 +39,7 @@ let widening_cast env tfrom tto =
[160]6       r1 < r2 || (r1 = r2 && is_signed_ikind k1 = is_signed_ikind k2)
7   | TFloat(k1, _), TFloat(k2, _) ->
8       float_rank k1 <= float_rank k2
9-  | TPtr(ty1, _), TPtr(ty2, _) -> is_void_type env ty2
10+  | TPtr(sp1, ty1, _), TPtr(sp2, ty2, _) when sp1 = sp2 -> is_void_type env ty2
11   | _, _ -> false
12   end
13 
[292]14@@ -52,7 +52,7 @@ let cast_not_needed env tfrom tto =
[160]15 let cast env e tto =
16   if cast_not_needed env e.etyp tto
17   then e
18-  else {edesc = ECast(tto, e); etyp = tto}
19+  else {edesc = ECast(tto, e); etyp = tto; espace = Any}
20 
21 (* Note: this pass applies only to simplified expressions
22    because casts cannot be materialized in op= expressions... *)
[292]23@@ -73,7 +73,7 @@ let rec add_expr env e =
[160]24             EUnop(op, e1')
25         | Opreincr | Opredecr | Opostincr | Opostdecr ->
26             assert false (* not simplified *)
27-      in { edesc = desc; etyp = e.etyp }
28+      in { edesc = desc; etyp = e.etyp; espace = e.espace }
29   | EBinop(op, e1, e2, ty) ->
30       let e1' = add_expr env e1 in
31       let e2' = add_expr env e2 in
[292]32@@ -97,13 +97,14 @@ let rec add_expr env e =
[160]33         | Oadd_assign|Osub_assign|Omul_assign|Odiv_assign|Omod_assign
34         | Oand_assign|Oor_assign|Oxor_assign|Oshl_assign|Oshr_assign ->
35             assert false (* not simplified *)
36-      in { edesc = desc; etyp = e.etyp }
37+      in { edesc = desc; etyp = e.etyp; espace = e.espace }
38   | EConditional(e1, e2, e3) ->
39       { edesc =
40           EConditional(add_expr env e1, add_expr env e2, add_expr env e3);
41-        etyp = e.etyp }
42+        etyp = e.etyp;
43+        espace = e.espace }
44   | ECast(ty, e1) ->
45-      { edesc = ECast(ty, add_expr env e1); etyp = e.etyp }
46+      { edesc = ECast(ty, add_expr env e1); etyp = e.etyp; espace = e.espace }
47   | ECall(e1, el) ->
48       assert false (* not simplified *)
49 
[292]50@@ -132,7 +133,7 @@ let add_arguments env ty_fun args =
[160]51   let ty_args =
52     match unroll env ty_fun with
53     | TFun(res, args, vararg, a) -> args
54-    | TPtr(ty, a) ->
55+    | TPtr(_, ty, a) ->
56         begin match unroll env ty with
57         | TFun(res, args, vararg, a) -> args
58         | _ -> assert false
[292]59@@ -146,10 +147,10 @@ let add_arguments env ty_fun args =
[160]60 
61 let add_topexpr env loc e =
62   match e.edesc with
63-  | EBinop(Oassign, lhs, {edesc = ECall(e1, el); etyp = ty}, _) ->
64+  | EBinop(Oassign, lhs, {edesc = ECall(e1, el); etyp = ty; espace = space}, _) ->
65       let ecall =
66         {edesc = ECall(add_expr env e1, add_arguments env e1.etyp el);
67-         etyp = ty} in
68+         etyp = ty; espace = space} in
69       if cast_not_needed env ty lhs.etyp then
70         sassign loc (add_expr env lhs) ecall
71       else begin
[292]72@@ -162,7 +163,7 @@ let add_topexpr env loc e =
[160]73   | ECall(e1, el) ->
74       let ecall =
75         {edesc = ECall(add_expr env e1, add_arguments env e1.etyp el);
76-         etyp = e.etyp} in
77+         etyp = e.etyp; espace = e.espace} in
78       {sdesc = Sdo ecall; sloc = loc}
79   | _ ->
80       assert false
[292]81@@ -175,7 +176,7 @@ let rec add_init env tto = function
[160]82   | Init_array il ->
83       let ty_elt =
84         match unroll env tto with
85-        | TArray(ty, _, _) -> ty | _ -> assert false in
86+        | TArray(_,ty, _, _) -> ty | _ -> assert false in
87       Init_array (List.map (add_init env ty_elt) il)
88   | Init_struct(id, fil) ->
89       Init_struct (id, List.map
[292]90diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml
91index dea1862..c7dc25f 100644
92--- a/cparser/Bitfields.ml
93+++ b/cparser/Bitfields.ml
94@@ -118,7 +118,7 @@ let insertion_mask bf =
[160]95       (Int64.pred (Int64.shift_left 1L bf.bf_size))
96       bf.bf_pos in
97   (* Give the mask an hexadecimal string representation, nicer to read *)
98-  {edesc = EConst(CInt(m, IUInt, sprintf "0x%LXU" m)); etyp = TInt(IUInt, [])}
99+  {edesc = EConst(CInt(m, IUInt, sprintf "0x%LXU" m)); etyp = TInt(IUInt, []); espace = Code} (* XXX are consts always Code? *)
100 
101 (* Extract the value of a bitfield *)
102 
[292]103@@ -140,12 +140,12 @@ signed int bitfield_signed_extract(unsigned int x, int ofs, int sz)
[160]104 let bitfield_extract bf carrier =
105   let e1 =
106     {edesc = EBinop(Oshl, carrier, left_shift_count bf, TInt(IUInt, []));
107-     etyp = carrier.etyp} in
108+     etyp = carrier.etyp; espace = Any} in
109   let ty = TInt((if bf.bf_signed then IInt else IUInt), []) in
110   let e2 =
111-    {edesc = ECast(ty, e1); etyp = ty} in
112+    {edesc = ECast(ty, e1); etyp = ty; espace = Any} in
113   {edesc = EBinop(Oshr, e2, right_shift_count bf, e2.etyp);
114-   etyp = e2.etyp}
115+   etyp = e2.etyp; espace = Any}
116 
117 (* Assign a bitfield within a carrier *)
118 
[292]119@@ -161,19 +161,21 @@ unsigned int bitfield_insert(unsigned int x, int ofs, int sz, unsigned int y)
[160]120 
121 let bitfield_assign bf carrier newval =
122   let msk = insertion_mask bf in
123-  let notmsk = {edesc = EUnop(Onot, msk); etyp = msk.etyp} in
124+  let notmsk = {edesc = EUnop(Onot, msk); etyp = msk.etyp; espace = Any} in
125   let newval_shifted =
126     {edesc = EBinop(Oshl, newval, intconst (Int64.of_int bf.bf_pos) IUInt,
127                     TInt(IUInt,[]));
128-     etyp = TInt(IUInt,[])} in
129+     etyp = TInt(IUInt,[]);
130+     espace = Any} in
131   let newval_masked =
132     {edesc = EBinop(Oand, newval_shifted, msk, TInt(IUInt,[]));
133-     etyp = TInt(IUInt,[])}
134+     etyp = TInt(IUInt,[]);
135+     espace = Any}
136   and oldval_masked =
137     {edesc = EBinop(Oand, carrier, notmsk, TInt(IUInt,[]));
138-     etyp = TInt(IUInt,[])} in
139+     etyp = TInt(IUInt,[]); espace = Any} in
140   {edesc = EBinop(Oor,  oldval_masked, newval_masked,  TInt(IUInt,[]));
141-   etyp =  TInt(IUInt,[])}
142+   etyp =  TInt(IUInt,[]); espace = Any}
143 
144 (* Expressions *)
145 
[292]146@@ -188,7 +190,7 @@ let transf_expr env e =
[160]147 
148   let is_bitfield_access_ptr ty fieldname =
149     match unroll env ty with
150-    | TPtr(ty', _) -> is_bitfield_access ty' fieldname
151+    | TPtr(_, ty', _) -> is_bitfield_access ty' fieldname
152     | _ -> None in
153 
154   let rec texp e =
[292]155@@ -201,27 +203,28 @@ let transf_expr env e =
[160]156         let e1' = texp e1 in
157         begin match is_bitfield_access e1.etyp fieldname with
158         | None ->
159-            {edesc = EUnop(Odot fieldname, e1'); etyp = e.etyp}
160+            {edesc = EUnop(Odot fieldname, e1'); etyp = e.etyp; espace = e1'.espace}
161         | Some bf ->
162             bitfield_extract bf
163               {edesc = EUnop(Odot bf.bf_carrier, e1');
164-               etyp = bf.bf_carrier_typ}
165+               etyp = bf.bf_carrier_typ;
166+               espace = e1'.espace}
167         end
168 
169     | EUnop(Oarrow fieldname, e1) ->
170         let e1' = texp e1 in
171         begin match is_bitfield_access_ptr e1.etyp fieldname with
172         | None ->
173-            {edesc = EUnop(Oarrow fieldname, e1'); etyp = e.etyp}
174+            {edesc = EUnop(Oarrow fieldname, e1'); etyp = e.etyp; espace = Any}
175         | Some bf ->
176             bitfield_extract bf
177               {edesc = EUnop(Oarrow bf.bf_carrier, e1');
178-               etyp = bf.bf_carrier_typ}
179+               etyp = bf.bf_carrier_typ; espace = Any}
180         end
181 
182     | EUnop(op, e1) ->
183         (* Note: simplified expr, so no ++/-- *)
184-        {edesc = EUnop(op, texp e1); etyp = e.etyp}
185+        {edesc = EUnop(op, texp e1); etyp = e.etyp; espace = e.espace}
186 
187     | EBinop(Oassign, e1, e2, ty) ->
188         begin match e1.edesc with
[292]189@@ -231,17 +234,20 @@ let transf_expr env e =
[160]190             | None ->
191                 {edesc = EBinop(Oassign,
192                                 {edesc = EUnop(Odot fieldname, lhs);
193-                                 etyp = e1.etyp},
194+                                 etyp = e1.etyp; espace = lhs.espace},
195                                 rhs, ty);
196-                 etyp = e.etyp}
197+                 etyp = e.etyp;
198+                 espace = e.espace}
199             | Some bf ->
200                 let carrier =
201                   {edesc = EUnop(Odot bf.bf_carrier, lhs);
202-                   etyp = bf.bf_carrier_typ} in
203+                   etyp = bf.bf_carrier_typ;
204+                   espace = lhs.espace} in
205                 {edesc = EBinop(Oassign, carrier,
206                                 bitfield_assign bf carrier rhs,
207                                 carrier.etyp);
208-                 etyp = carrier.etyp}
209+                 etyp = carrier.etyp;
210+                 espace = lhs.espace}
211             end
212         | EUnop(Oarrow fieldname, e11) ->
213             let lhs = texp e11 in let rhs = texp e2 in
[292]214@@ -249,31 +255,35 @@ let transf_expr env e =
[160]215             | None ->
216                 {edesc = EBinop(Oassign,
217                                 {edesc = EUnop(Oarrow fieldname, lhs);
218-                                 etyp = e1.etyp},
219+                                 etyp = e1.etyp;
220+                                 espace = e1.espace},
221                                 rhs, ty);
222-                 etyp = e.etyp}
223+                 etyp = e.etyp;
224+                 espace = e.espace}
225             | Some bf ->
226                 let carrier =
227                   {edesc = EUnop(Oarrow bf.bf_carrier, lhs);
228-                   etyp = bf.bf_carrier_typ} in
229+                   etyp = bf.bf_carrier_typ;
230+                   espace = Any} in
231                 {edesc = EBinop(Oassign, carrier,
232                                 bitfield_assign bf carrier rhs,
233                                 carrier.etyp);
234-                 etyp = carrier.etyp}
235+                 etyp = carrier.etyp;
236+                 espace = Any}
237             end
238         | _ ->
239-            {edesc = EBinop(Oassign, texp e1, texp e2, e1.etyp); etyp = e1.etyp}
240+            {edesc = EBinop(Oassign, texp e1, texp e2, e1.etyp); etyp = e1.etyp; espace = e1.espace}
241         end
242 
243     | EBinop(op, e1, e2, ty) ->
244         (* Note: simplified expr assumed, so no assign-op *)
245-        {edesc = EBinop(op, texp e1, texp e2, ty); etyp = e.etyp}
246+        {edesc = EBinop(op, texp e1, texp e2, ty); etyp = e.etyp; espace = e.espace}
247     | EConditional(e1, e2, e3) ->
248-        {edesc = EConditional(texp e1, texp e2, texp e3); etyp = e.etyp}
249+        {edesc = EConditional(texp e1, texp e2, texp e3); etyp = e.etyp; espace = e.espace}
250     | ECast(ty, e1) ->
251-        {edesc = ECast(ty, texp e1); etyp = e.etyp}
252+        {edesc = ECast(ty, texp e1); etyp = e.etyp; espace = e.espace}
253     | ECall(e1, el) ->
254-        {edesc = ECall(texp e1, List.map texp el); etyp = e.etyp}
255+        {edesc = ECall(texp e1, List.map texp el); etyp = e.etyp; espace = e.espace}
256 
257   in texp e
258 
[292]259@@ -325,13 +335,16 @@ let bitfield_initializer bf i =
[160]260       let m = Int64.pred (Int64.shift_left 1L bf.bf_size) in
261       let e_mask =
262         {edesc = EConst(CInt(m, IUInt, sprintf "0x%LXU" m));
263-         etyp = TInt(IUInt, [])} in
264+         etyp = TInt(IUInt, []);
265+         espace = Any} in
266       let e_and =
267         {edesc = EBinop(Oand, e, e_mask, TInt(IUInt,[]));
268-         etyp = TInt(IUInt,[])} in
269+         etyp = TInt(IUInt,[]);
270+         espace = Any} in
271       {edesc = EBinop(Oshl, e_and, intconst (Int64.of_int bf.bf_pos) IInt,
272                       TInt(IUInt, []));
273-       etyp = TInt(IUInt, [])}
274+       etyp = TInt(IUInt, []);
275+       espace = Any}
276   | _ -> assert false
277 
278 let rec pack_bitfield_init id carrier fld_init_list =
[292]279@@ -354,7 +367,8 @@ let rec or_expr_list = function
[160]280   | [e] -> e
281   | e1 :: el ->
282       {edesc = EBinop(Oor, e1, or_expr_list el, TInt(IUInt,[]));
283-       etyp = TInt(IUInt,[])}
284+       etyp = TInt(IUInt,[]);
285+       espace = Any}
286 
287 let rec transf_struct_init id fld_init_list =
288   match fld_init_list with
[292]289@@ -367,7 +381,8 @@ let rec transf_struct_init id fld_init_list =
[160]290         ({fld_name = bf.bf_carrier; fld_typ = bf.bf_carrier_typ;
291           fld_bitfield = None},
292          Init_single {edesc = ECast(bf.bf_carrier_typ, or_expr_list el);
293-                      etyp = bf.bf_carrier_typ})
294+                      etyp = bf.bf_carrier_typ;
295+                      espace = Any})
296         :: transf_struct_init id rem'
297       with Not_found ->
298         (fld, i) :: transf_struct_init id rem
[292]299diff --git a/cparser/Builtins.ml b/cparser/Builtins.ml
300index 8eb1abf..aa243fd 100644
301--- a/cparser/Builtins.ml
302+++ b/cparser/Builtins.ml
303@@ -37,10 +37,10 @@ let add_function (s, (res, args, va)) =
[160]304     TFun(res,
305          Some (List.map (fun ty -> (Env.fresh_ident "", ty)) args),
306          va, []) in
307-  let (id, env') = Env.enter_ident !env s Storage_extern ty in
308+  let (id, env') = Env.enter_ident !env s Storage_extern ty Code in
309   env := env';
310   idents := id :: !idents;
311-  decls := {gdesc = Gdecl(Storage_extern, id, ty, None); gloc = no_loc} :: !decls
312+  decls := {gdesc = Gdecl(Code, (Storage_extern, id, ty, None)); gloc = no_loc} :: !decls
313 
314 type t = {
315   typedefs: (string * C.typ) list;
[292]316diff --git a/cparser/C.mli b/cparser/C.mli
317index d477acd..90df378 100644
318--- a/cparser/C.mli
319+++ b/cparser/C.mli
320@@ -124,12 +124,20 @@ type binary_operator =
321 
322 (** Types *)
323 
324+type memory_space =
325+  | Any
326+  | Data
327+  | IData
328+  | PData
329+  | XData
330+  | Code
331+
332 type typ =
333   | TVoid of attributes
334   | TInt of ikind * attributes
335   | TFloat of fkind * attributes
336-  | TPtr of typ * attributes
337-  | TArray of typ * int64 option * attributes
338+  | TPtr of memory_space * typ * attributes
339+  | TArray of memory_space * typ * int64 option * attributes
340   | TFun of typ * (ident * typ) list option * bool * attributes
341   | TNamed of ident * attributes
342   | TStruct of ident * attributes
343@@ -137,7 +145,7 @@ type typ =
344 
345 (** Expressions *)
346 
347-type exp = { edesc: exp_desc; etyp: typ }
348+type exp = { edesc: exp_desc; etyp: typ; espace: memory_space }
349 
350 and exp_desc =
351   | EConst of constant
352@@ -220,7 +228,7 @@ type globdecl =
353   { gdesc: globdecl_desc; gloc: location }
354 
355 and globdecl_desc =
356-  | Gdecl of decl           (* variable declaration, function prototype *)
357+  | Gdecl of memory_space * decl  (* variable declaration, function prototype *)
358   | Gfundef of fundef                   (* function definition *)
359   | Gcompositedecl of struct_or_union * ident (* struct/union declaration *)
360   | Gcompositedef of struct_or_union * ident * field list
361diff --git a/cparser/Ceval.ml b/cparser/Ceval.ml
362index 0e22852..acf84aa 100644
363--- a/cparser/Ceval.ml
364+++ b/cparser/Ceval.ml
365@@ -99,11 +99,11 @@ let cast env ty_to ty_from v =
[160]366       if is_signed env ty_from
367       then F(normalize_float (Int64.to_float n) fk)
368       else F(normalize_float (int64_unsigned_to_float n) fk)
369-  | TPtr(ty, _), I n ->
370+  | TPtr(_, ty, _), I n ->
371       I (normalize_int n ptr_t_ikind)
372-  | TPtr(ty, _), F n ->
373+  | TPtr(_, ty, _), F n ->
374       if n = 0.0 then I 0L else raise Notconst
375-  | TPtr(ty, _), (S _ | WS _) ->
376+  | TPtr(_, ty, _), (S _ | WS _) ->
377       v
378   | _, _ ->
379       raise Notconst
[292]380@@ -270,8 +270,8 @@ let constant_expr env ty e =
[160]381     match unroll env ty, cast env e.etyp ty (expr env e) with
382     | TInt(ik, _), I n -> Some(CInt(n, ik, ""))
383     | TFloat(fk, _), F n -> Some(CFloat(n, fk, ""))
384-    | TPtr(_, _), I 0L -> Some(CInt(0L, IInt, ""))
385-    | TPtr(_, _), S s -> Some(CStr s)
386-    | TPtr(_, _), WS s -> Some(CWStr s)
387+    | TPtr(_, _, _), I 0L -> Some(CInt(0L, IInt, ""))
388+    | TPtr(_, _, _), S s -> Some(CStr s)
389+    | TPtr(_, _, _), WS s -> Some(CWStr s)
390     | _   -> None
391   with Notconst -> None
[292]392diff --git a/cparser/Cleanup.ml b/cparser/Cleanup.ml
393index be28989..9644654 100644
394--- a/cparser/Cleanup.ml
395+++ b/cparser/Cleanup.ml
396@@ -40,8 +40,8 @@ let needed id =
[160]397 (* Iterate [addref] on all syntactic categories. *)
398 
399 let rec add_typ = function
400-  | TPtr(ty, _) -> add_typ ty
401-  | TArray(ty, _, _) -> add_typ ty
402+  | TPtr(_, ty, _) -> add_typ ty
403+  | TArray(_, ty, _, _) -> add_typ ty
404   | TFun(res, None, _, _) -> add_typ res
405   | TFun(res, Some params, _, _) -> add_typ res; add_vars params
406   | TNamed(id, _) -> addref id
[292]407@@ -120,7 +120,7 @@ let rec add_init_globdecls accu = function
[160]408   | [] -> accu
409   | g :: rem ->
410       match g.gdesc with
411-      | Gdecl decl when visible_decl decl ->
412+      | Gdecl (_,decl) when visible_decl decl ->
413           add_decl decl; add_init_globdecls accu rem
414       | Gfundef({fd_storage = Storage_default} as f) ->
415           add_fundef f; add_init_globdecls accu rem
[292]416@@ -135,7 +135,7 @@ let rec add_needed_globdecls accu = function
[160]417   | [] -> accu
418   | g :: rem ->
419       match g.gdesc with
420-      | Gdecl((sto, id, ty, init) as decl) ->
421+      | Gdecl(_, ((sto, id, ty, init) as decl)) ->
422           if needed id
423           then (add_decl decl; add_needed_globdecls accu rem)
424           else add_needed_globdecls (g :: accu) rem
[292]425@@ -174,7 +174,7 @@ let rec simpl_globdecls accu = function
[160]426   | g :: rem ->
427       let need =
428         match g.gdesc with
429-        | Gdecl((sto, id, ty, init) as decl) -> visible_decl decl || needed id
430+        | Gdecl(_, ((sto, id, ty, init) as decl)) -> visible_decl decl || needed id
431         | Gfundef f -> f.fd_storage = Storage_default || needed f.fd_name
432         | Gcompositedecl(_, id) -> needed id
433         | Gcompositedef(_, id, flds) -> needed id
[292]434diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml
435index 7d8f2b3..70aba81 100644
436--- a/cparser/Cprint.ml
437+++ b/cparser/Cprint.ml
438@@ -67,13 +67,13 @@ let rec dcl pp ty n =
[160]439       fprintf pp "%s%a%t" (name_of_ikind k) attributes a n
440   | TFloat(k, a) ->
441       fprintf pp "%s%a%t" (name_of_fkind k) attributes a n
442-  | TPtr(t, a) ->
443+  | TPtr(_, t, a) -> (* XXX *)
444       let n' pp =
445         match t with
446         | TFun _ | TArray _ -> fprintf pp " (*%a%t)" attributes a n
447         | _ -> fprintf pp " *%a%t" attributes a n in
448       dcl pp t n'
449-  | TArray(t, sz, a) ->
450+  | TArray(_, t, sz, a) -> (* XXX *)
451       let n' pp =
452         begin match a with
453         | [] -> n pp
[292]454@@ -353,10 +353,12 @@ let rec exp_of_stmt s =
[160]455   | Sdo e -> e
456   | Sseq(s1, s2) ->
457       {edesc = EBinop(Ocomma, exp_of_stmt s1, exp_of_stmt s2, TVoid []);
458-       etyp = TVoid []}
459+       etyp = TVoid [];
460+       espace = Any}
461   | Sif(e, s1, s2) ->
462       {edesc = EConditional(e, exp_of_stmt s1, exp_of_stmt s2);
463-       etyp = TVoid []}
464+       etyp = TVoid [];
465+       espace = Any}
466   | _ ->
467       raise Not_expr
468 
[292]469@@ -373,7 +375,7 @@ let rec stmt pp s =
[160]470       fprintf pp "@[<v 2>if (%a) {@ %a@;<0 -2>}@]"
471               exp (0, e) stmt_block s1
472   | Sif(e, {sdesc = Sskip}, s2) ->
473-      let not_e = {edesc = EUnop(Olognot, e); etyp = TInt(IInt, [])} in
474+      let not_e = {edesc = EUnop(Olognot, e); etyp = TInt(IInt, []); espace = Any} in
475       fprintf pp "@[<v 2>if (%a) {@ %a@;<0 -2>}@]"
476               exp (0, not_e) stmt_block s2
477   | Sif(e, s1, s2) ->
[292]478@@ -455,7 +457,7 @@ let field pp f =
[160]479 let globdecl pp g =
480   location pp g.gloc;
481   match g.gdesc with
482-  | Gdecl d ->
483+  | Gdecl (_, d) -> (* XXX *)
484       fprintf pp "%a@ @ " full_decl d
485   | Gfundef f ->
486       fundef pp f
[292]487diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
488index 49b25a2..4a43d09 100644
489--- a/cparser/Cutil.ml
490+++ b/cparser/Cutil.ml
491@@ -71,8 +71,8 @@ let rec add_attributes_type attr t =
[160]492   | TVoid a -> TVoid (add_attributes attr a)
493   | TInt(ik, a) -> TInt(ik, add_attributes attr a)
494   | TFloat(fk, a) -> TFloat(fk, add_attributes attr a)
495-  | TPtr(ty, a) -> TPtr(ty, add_attributes attr a)
496-  | TArray(ty, sz, a) -> TArray(add_attributes_type attr ty, sz, a)
497+  | TPtr(sp, ty, a) -> TPtr(sp, ty, add_attributes attr a)
498+  | TArray(sp, ty, sz, a) -> TArray(sp, add_attributes_type attr ty, sz, a)
499   | TFun(ty, params, vararg, a) -> TFun(ty, params, vararg, add_attributes attr
500 a)
501   | TNamed(s, a) -> TNamed(s, add_attributes attr a)
[292]502@@ -95,8 +95,8 @@ let rec attributes_of_type env t =
[160]503   | TVoid a -> a
504   | TInt(ik, a) -> a
505   | TFloat(fk, a) -> a
506-  | TPtr(ty, a) -> a
507-  | TArray(ty, sz, a) -> a              (* correct? *)
508+  | TPtr(_, ty, a) -> a
509+  | TArray(_, ty, sz, a) -> a              (* correct? *)
510   | TFun(ty, params, vararg, a) -> a
511   | TNamed(s, a) -> attributes_of_type env (unroll env t)
512   | TStruct(s, a) -> a
[292]513@@ -110,9 +110,9 @@ let rec change_attributes_type env (f: attributes -> attributes) t =
[160]514   | TVoid a -> TVoid (f a)
515   | TInt(ik, a) -> TInt(ik, f a)
516   | TFloat(fk, a) -> TFloat(fk, f a)
517-  | TPtr(ty, a) -> TPtr(ty, f a)
518-  | TArray(ty, sz, a) ->
519-      TArray(change_attributes_type env f ty, sz, a)
520+  | TPtr(sp, ty, a) -> TPtr(sp, ty, f a)
521+  | TArray(sp, ty, sz, a) ->
522+      TArray(sp, change_attributes_type env f ty, sz, a)
523   | TFun(ty, params, vararg, a) -> TFun(ty, params, vararg, f a)
524   | TNamed(s, a) ->
525       let t1 = unroll env t in
[292]526@@ -166,10 +166,10 @@ let combine_types ?(noattrs = false) env t1 t2 =
[160]527         TInt(comp_base ik1 ik2, comp_attr a1 a2)
528     | TFloat(fk1, a1), TFloat(fk2, a2) ->
529         TFloat(comp_base fk1 fk2, comp_attr a1 a2)
530-    | TPtr(ty1, a1), TPtr(ty2, a2) ->
531-        TPtr(comp ty1 ty2, comp_attr a1 a2)
532-    | TArray(ty1, sz1, a1), TArray(ty2, sz2, a2) ->
533-        TArray(comp ty1 ty2, comp_array_size sz1 sz2, comp_attr a1 a2)
534+    | TPtr(sp1, ty1, a1), TPtr(sp2, ty2, a2) when sp1 = sp2 ->
535+        TPtr(sp1, comp ty1 ty2, comp_attr a1 a2)
536+    | TArray(sp1, ty1, sz1, a1), TArray(sp2, ty2, sz2, a2) when sp1 = sp2 ->
537+        TArray(sp1, comp ty1 ty2, comp_array_size sz1 sz2, comp_attr a1 a2)
538     | TFun(ty1, params1, vararg1, a1), TFun(ty2, params2, vararg2, a2) ->
539         let (params, vararg) =
540           match params1, params2 with
[292]541@@ -244,8 +244,8 @@ let rec alignof env t =
[160]542   | TVoid _ -> !config.alignof_void
543   | TInt(ik, _) -> Some(alignof_ikind ik)
544   | TFloat(fk, _) -> Some(alignof_fkind fk)
545-  | TPtr(_, _) -> Some(!config.alignof_ptr)
546-  | TArray(ty, _, _) -> alignof env ty
547+  | TPtr(_, _, _) -> Some(!config.alignof_ptr)
548+  | TArray(_, ty, _, _) -> alignof env ty
549   | TFun(_, _, _, _) -> !config.alignof_fun
550   | TNamed(_, _) -> alignof env (unroll env t)
551   | TStruct(name, _) ->
[292]552@@ -302,9 +302,9 @@ let rec sizeof env t =
[160]553   | TVoid _ -> !config.sizeof_void
554   | TInt(ik, _) -> Some(sizeof_ikind ik)
555   | TFloat(fk, _) -> Some(sizeof_fkind fk)
556-  | TPtr(_, _) -> Some(!config.sizeof_ptr)
557-  | TArray(ty, None, _) -> None
558-  | TArray(ty, Some n, _) as t' ->
559+  | TPtr(_, _, _) -> Some(!config.sizeof_ptr) (* FIXME *)
560+  | TArray(_, ty, None, _) -> None
561+  | TArray(_, ty, Some n, _) as t' ->
562       begin match sizeof env ty with
563       | None -> None
564       | Some s ->
[292]565@@ -343,7 +343,7 @@ let sizeof_union env members =
[160]566 
567 let sizeof_struct env members =
568   let rec sizeof_rec ofs = function
569-  | [] | [ { fld_typ = TArray(_, None, _) } ] ->
570+  | [] | [ { fld_typ = TArray(_, _, None, _) } ] ->
571       (* C99: ty[] allowed as last field *)
572       begin match alignof_struct_union env members with
573       | None -> None                    (* should not happen? *)
[292]574@@ -472,8 +472,8 @@ let float_rank = function
[160]575 
576 let pointer_decay env t =
577   match unroll env t with
578-  | TArray(ty, _, _) -> TPtr(ty, [])
579-  | TFun _ as ty -> TPtr(ty, [])
580+  | TArray(sp, ty, _, _) -> TPtr(sp, ty, [])
581+  | TFun _ as ty -> TPtr(Code, ty, [])
582   | t -> t
583 
584 (* The usual unary conversions (H&S 6.3.3) *)
[292]585@@ -489,8 +489,8 @@ let unary_conversion env t =
[160]586           TInt(kind, attr)
587       end
588   (* Arrays and functions decay automatically to pointers *)
589-  | TArray(ty, _, _) -> TPtr(ty, [])
590-  | TFun _ as ty -> TPtr(ty, [])
591+  | TArray(sp, ty, _, _) -> TPtr(sp, ty, [])
592+  | TFun _ as ty -> TPtr(Code, ty, [])
593   (* Other types are not changed *)
594   | t -> t
595 
[292]596@@ -540,8 +540,8 @@ let argument_conversion env t =
[160]597   (* Arrays and functions degrade automatically to pointers *)
598   (* Other types are not changed *)
599   match unroll env t with
600-  | TArray(ty, _, _) -> TPtr(ty, [])
601-  | TFun _ as ty -> TPtr(ty, [])
602+  | TArray(sp, ty, _, _) -> TPtr(sp, ty, [])
603+  | TFun _ as ty -> TPtr(Code, ty, [])
604   | _ -> t (* preserve typedefs *)
605 
606 (* Conversion on function arguments (old-style unprototyped, or vararg *)
[292]607@@ -584,8 +584,8 @@ let enum_ikind = IInt
[160]608 let type_of_constant = function
609   | CInt(_, ik, _) -> TInt(ik, [])
610   | CFloat(_, fk, _) -> TFloat(fk, [])
611-  | CStr _ -> TPtr(TInt(IChar, []), [])          (* XXX or array? const? *)
612-  | CWStr _ -> TPtr(TInt(wchar_ikind, []), [])   (* XXX or array? const? *)
613+  | CStr _ -> TPtr(Code, TInt(IChar, []), [])          (* XXX or array? const? *)
614+  | CWStr _ -> TPtr(Code, TInt(wchar_ikind, []), [])   (* XXX or array? const? *)
615   | CEnum(_, _) -> TInt(IInt, [])
616 
617 (* Check that a C expression is a lvalue *)
[292]618@@ -612,12 +612,19 @@ let is_literal_0 e =
[160]619 
620 (* Check that an assignment is allowed *)
621 
622+let valid_pointer_conv from tto =
623+  match from, tto with
624+  | Any, _
625+  | _, Any -> true
626+  | f, t -> f = t
627+
628 let valid_assignment env from tto =
629   match pointer_decay env from.etyp, pointer_decay env tto with
630   | (TInt _ | TFloat _), (TInt _ | TFloat _) -> true
631   | TInt _, TPtr _ -> is_literal_0 from
632-  | TPtr(ty, _), TPtr(ty', _) ->
633-      incl_attributes (attributes_of_type env ty) (attributes_of_type env ty')
634+  | TPtr(sp, ty, _), TPtr(sp', ty', _) ->
635+      valid_pointer_conv sp sp'
636+      && incl_attributes (attributes_of_type env ty) (attributes_of_type env ty')
637       && (is_void_type env ty || is_void_type env ty'
638           || compatible_types env
639                (erase_attributes_type env ty)
[292]640@@ -643,17 +650,17 @@ let valid_cast env tfrom tto =
[160]641 (* Construct an integer constant *)
642 
643 let intconst v ik =
644-  { edesc = EConst(CInt(v, ik, "")); etyp = TInt(ik, []) }
645+  { edesc = EConst(CInt(v, ik, "")); etyp = TInt(ik, []); espace = Code }
646 
647 (* Construct a float constant *)
648 
649 let floatconst v fk =
650-  { edesc = EConst(CFloat(v, fk, "")); etyp = TFloat(fk, []) }
651+  { edesc = EConst(CFloat(v, fk, "")); etyp = TFloat(fk, []); espace = Code }
652 
653 (* Construct the literal "0" with void * type *)
654 
655 let nullconst =
656-  { edesc = EConst(CInt(0L, ptr_t_ikind, "0")); etyp = TPtr(TVoid [], []) }
657+  { edesc = EConst(CInt(0L, ptr_t_ikind, "0")); etyp = TPtr(Any, TVoid [], []); espace = Code } (* XXX *)
658 
659 (* Construct a sequence *)
660 
[292]661@@ -667,7 +674,7 @@ let sseq loc s1 s2 =
[160]662 (* Construct an assignment statement *)
663 
664 let sassign loc lv rv =
665-  { sdesc = Sdo {edesc = EBinop(Oassign, lv, rv, lv.etyp); etyp = lv.etyp};
666+  { sdesc = Sdo {edesc = EBinop(Oassign, lv, rv, lv.etyp); etyp = lv.etyp; espace = lv.espace};
667     sloc = loc }
668 
669 (* Empty location *)
[292]670diff --git a/cparser/Elab.ml b/cparser/Elab.ml
671index 7204508..1978b6b 100644
672--- a/cparser/Elab.ml
673+++ b/cparser/Elab.ml
674@@ -270,6 +270,28 @@ let rec elab_attributes loc = function
[160]675       | None -> elab_attributes loc al
676       | Some a -> add_attributes [a] (elab_attributes loc al)
677 
678+let elab_attribute_space = function
679+  | ("data", []) -> Some Data
680+  | ("idata", []) -> Some IData
681+  | ("pdata", []) -> Some PData
682+  | ("xdata", []) -> Some XData
683+  | ("code", []) -> Some Code
684+  | _ -> None
685+
686+let rec elab_attributes_space loc attrs =
687+  let rec aux = function
688+    | [] -> None
689+    | h::t -> (match elab_attribute_space h with
690+                | None -> aux t
691+                | Some v -> Some (v,t))
692+  in match aux attrs with
693+    | None -> Any
694+    | Some (space, rest) ->
695+       (match aux rest with
696+         | None -> ()
697+         | Some _ -> warning loc "Multiple memory spaces given");
698+       space
699+
700 (* Auxiliary for typespec elaboration *)
701 
702 let typespec_rank = function (* Don't change this *)
[292]703@@ -288,6 +310,7 @@ let typespec_rank = function (* Don't change this *)
[160]704 
705 let typespec_order t1 t2 = compare (typespec_rank t1) (typespec_rank t2)
706 
707+
708 (* Elaboration of a type specifier.  Returns 4-tuple:
709      (storage class, "inline" flag, elaborated type, new env)
710    Optional argument "only" is true if this is a standalone
[292]711@@ -302,7 +325,8 @@ let rec elab_specifier ?(only = false) loc env specifier =
[160]712   let sto = ref Storage_default
713   and inline = ref false
714   and attr = ref []
715-  and tyspecs = ref [] in
716+  and tyspecs = ref []
717+  and space = ref Any in
718 
719   let do_specifier = function
720   | SpecTypedef -> ()
[292]721@@ -314,7 +338,13 @@ let rec elab_specifier ?(only = false) loc env specifier =
[160]722         | CV_RESTRICT -> ARestrict in
723       attr := add_attributes [a] !attr
724   | SpecAttr a ->
725-      attr := add_attributes (elab_attributes loc [a]) !attr
726+      attr := add_attributes (elab_attributes loc [a]) !attr;
727+      (match elab_attribute_space a with
728+        | None -> ()
729+        | Some sp ->
730+           if !space <> Any then
731+             error loc "multiple memory space specifiers";
732+           space := sp)
733   | SpecStorage st ->
734       if !sto <> Storage_default then
735         error loc "multiple storage specifiers";
[292]736@@ -330,7 +360,7 @@ let rec elab_specifier ?(only = false) loc env specifier =
[160]737 
738   List.iter do_specifier specifier;
739 
740-  let simple ty = (!sto, !inline, add_attributes_type !attr ty, env) in
741+  let simple ty = (!space, !sto, !inline, add_attributes_type !attr ty, env) in
742 
743   (* Now interpret the list of type specifiers.  Much of this code
744      is stolen from CIL. *)
[292]745@@ -394,19 +424,19 @@ let rec elab_specifier ?(only = false) loc env specifier =
[160]746         let (id', env') =
747           elab_struct_or_union only Struct loc id optmembers env in
748         let attr' = add_attributes !attr (elab_attributes loc a) in
749-        (!sto, !inline, TStruct(id', attr'), env')
750+        (!space, !sto, !inline, TStruct(id', attr'), env')
751 
752     | [Cabs.Tunion(id, optmembers, a)] ->
753         let (id', env') =
754           elab_struct_or_union only Union loc id optmembers env in
755         let attr' = add_attributes !attr (elab_attributes loc a) in
756-        (!sto, !inline, TUnion(id', attr'), env')
757+        (!space, !sto, !inline, TUnion(id', attr'), env')
758 
759     | [Cabs.Tenum(id, optmembers, a)] ->
760         let env' =
761           elab_enum loc id optmembers env in
762         let attr' = add_attributes !attr (elab_attributes loc a) in
763-        (!sto, !inline, TInt(enum_ikind, attr'), env')
764+        (!space, !sto, !inline, TInt(enum_ikind, attr'), env')
765 
766     | [Cabs.TtypeofE _] ->
767         fatal_error loc "GCC __typeof__ not supported"
[292]768@@ -419,13 +449,14 @@ let rec elab_specifier ?(only = false) loc env specifier =
[160]769 
770 (* Elaboration of a type declarator.  *)
771 
772-and elab_type_declarator loc env ty = function
773+and elab_type_declarator loc env space ty = function
774   | Cabs.JUSTBASE ->
775-      (ty, env)
776+      (space, ty, env)
777   | Cabs.PARENTYPE(attr1, d, attr2) ->
778       (* XXX ignoring the distinction between attrs after and before *)
779       let a = elab_attributes loc (attr1 @ attr2) in
780-      elab_type_declarator loc env (add_attributes_type a ty) d
781+      (* XXX ought to use space from attrs? *)
782+      elab_type_declarator loc env space (add_attributes_type a ty) d
783   | Cabs.ARRAY(d, attr, sz) ->
784       let a = elab_attributes loc attr in
785       let sz' =
[292]786@@ -440,10 +471,11 @@ and elab_type_declarator loc env ty = function
[160]787             | None ->
788                 error loc "array size is not a compile-time constant";
789                 Some 1L in (* produces better error messages later *)
790-       elab_type_declarator loc env (TArray(ty, sz', a)) d
791+       elab_type_declarator loc env space (TArray(space, ty, sz', a)) d
792   | Cabs.PTR(attr, d) ->
793       let a = elab_attributes loc attr in
794-       elab_type_declarator loc env (TPtr(ty, a)) d
795+      let space' = elab_attributes_space loc attr in
796+       elab_type_declarator loc env space' (TPtr(space, ty, a)) d
797   | Cabs.PROTO(d, params, vararg) ->
798        begin match unroll env ty with
799        | TArray _ | TFun _ ->
[292]800@@ -451,7 +483,7 @@ and elab_type_declarator loc env ty = function
[160]801        | _ -> ()
802        end;
803        let params' = elab_parameters env params in
804-       elab_type_declarator loc env (TFun(ty, params', vararg, [])) d
805+       elab_type_declarator loc env space (TFun(ty, params', vararg, [])) d
806 
807 (* Elaboration of parameters in a prototype *)
808 
[292]809@@ -476,25 +508,25 @@ and elab_parameter env (spec, name) =
[160]810       "'extern' or 'static' storage not supported for function parameter";
811   (* replace array and function types by pointer types *)
812   let ty1 = argument_conversion env1 ty in
813-  let (id', env2) = Env.enter_ident env1 id sto ty1 in
814+  let (id', env2) = Env.enter_ident env1 id sto ty1 Any (* stack *) in
815   ( (id', ty1) , env2 )
816 
817 (* Elaboration of a (specifier, Cabs "name") pair *)
818 
819 and elab_name env spec (id, decl, attr, loc) =
820-  let (sto, inl, bty, env') = elab_specifier loc env spec in
821-  let (ty, env'') = elab_type_declarator loc env' bty decl in
822+  let (space, sto, inl, bty, env') = elab_specifier loc env spec in
823+  let (_, ty, env'') = elab_type_declarator loc env' space bty decl in
824   let a = elab_attributes loc attr in
825   (id, sto, inl, add_attributes_type a ty, env'')
826 
827 (* Elaboration of a name group *)
828 
829 and elab_name_group env (spec, namelist) =
830-  let (sto, inl, bty, env') =
831+  let (space, sto, inl, bty, env') =
832     elab_specifier (loc_of_namelist namelist) env spec in
833   let elab_one_name env (id, decl, attr, loc) =
834-    let (ty, env1) =
835-      elab_type_declarator loc env bty decl in
836+    let (_, ty, env1) =
837+      elab_type_declarator loc env space bty decl in
838     let a = elab_attributes loc attr in
839     ((id, sto, add_attributes_type a ty), env1) in
840   mmap elab_one_name env' namelist
[292]841@@ -502,13 +534,13 @@ and elab_name_group env (spec, namelist) =
[160]842 (* Elaboration of an init-name group *)
843 
844 and elab_init_name_group env (spec, namelist) =
845-  let (sto, inl, bty, env') =
846+  let (space, sto, inl, bty, env') =
847     elab_specifier (loc_of_init_name_list namelist) env spec in
848   let elab_one_name env ((id, decl, attr, loc), init) =
849-    let (ty, env1) =
850-      elab_type_declarator loc env bty decl in
851+    let (space', ty, env1) =
852+      elab_type_declarator loc env space bty decl in
853     let a = elab_attributes loc attr in
854-    ((id, sto, add_attributes_type a ty, init), env1) in
855+    ((space', id, sto, add_attributes_type a ty, init), env1) in
856   mmap elab_one_name env' namelist
857 
858 (* Elaboration of a field group *)
[292]859@@ -558,7 +590,7 @@ and elab_struct_or_union_info kind loc env members =
[160]860   (* Check for incomplete types *)
861   let rec check_incomplete = function
862   | [] -> ()
863-  | [ { fld_typ = TArray(ty_elt, None, _) } ] when kind = Struct -> ()
864+  | [ { fld_typ = TArray(_, ty_elt, None, _) } ] when kind = Struct -> ()
865         (* C99: ty[] allowed as last field of a struct *)
866   | fld :: rem ->
867       if incomplete_type env' fld.fld_typ then
[292]868@@ -663,12 +695,16 @@ and elab_enum loc tag optmembers env =
[160]869 (* Elaboration of a naked type, e.g. in a cast *)
870 
871 let elab_type loc env spec decl =
872-  let (sto, inl, bty, env') = elab_specifier loc env spec in
873-  let (ty, env'') = elab_type_declarator loc env' bty decl in
874+  let (space, sto, inl, bty, env') = elab_specifier loc env spec in
875+  let (_, ty, env'') = elab_type_declarator loc env' space bty decl in
876   if sto <> Storage_default || inl then
877     error loc "'extern', 'static', 'register' and 'inline' are meaningless in cast";
878   ty
879 
880+
881+let join_spaces s1 s2 =
882+if s1 = s2 then s1 else Any
883+
884 
885 (* Elaboration of expressions *)
886 
[292]887@@ -687,15 +723,15 @@ let elab_expr loc env a =
[160]888 
889   | VARIABLE s ->
890       begin match wrap Env.lookup_ident loc env s with
891-      | (id, II_ident(sto, ty)) ->
892-          { edesc = EVar id; etyp = ty }
893+      | (id, II_ident(sto, ty, spc)) ->
894+          { edesc = EVar id; etyp = ty; espace=spc }
895       | (id, II_enum v) ->
896-          { edesc = EConst(CEnum(id, v)); etyp = TInt(enum_ikind, []) }
897+          { edesc = EConst(CEnum(id, v)); etyp = TInt(enum_ikind, []); espace = Code }
898       end
899 
900   | CONSTANT cst ->
901       let cst' = elab_constant loc cst in
902-      { edesc = EConst cst'; etyp = type_of_constant cst' }
903+      { edesc = EConst cst'; etyp = type_of_constant cst'; espace = Code }
904 
905   | PAREN e ->
906       elab e
[292]907@@ -704,12 +740,12 @@ let elab_expr loc env a =
[160]908 
909   | INDEX(a1, a2) ->            (* e1[e2] *)
910       let b1 = elab a1 in let b2 = elab a2 in
911-      let tres =
912+      let space, tres =
913         match (unroll env b1.etyp, unroll env b2.etyp) with
914-        | (TPtr(t, _) | TArray(t, _, _)), TInt _ -> t
915-        | TInt _, (TPtr(t, _) | TArray(t, _, _)) -> t
916+        | (TPtr(space, t, _) | TArray(space, t, _, _)), TInt _ -> space, t
917+        | TInt _, (TPtr(space, t, _) | TArray(space, t, _, _)) -> space, t
918         | t1, t2 -> error "incorrect types for array subscripting" in
919-      { edesc = EBinop(Oindex, b1, b2, TPtr(tres, [])); etyp = tres }
920+      { edesc = EBinop(Oindex, b1, b2, TPtr(space, tres, [])); etyp = tres; espace = space }
921 
922   | MEMBEROF(a1, fieldname) ->
923       let b1 = elab a1 in
[292]924@@ -723,25 +759,27 @@ let elab_expr loc env a =
[160]925             error "left-hand side of '.' is not a struct or union" in
926       (* A field of a const/volatile struct or union is itself const/volatile *)
927       { edesc = EUnop(Odot fieldname, b1);
928-        etyp = add_attributes_type attrs fld.fld_typ }
929+        etyp = add_attributes_type attrs fld.fld_typ;
930+        espace = b1.espace }
931 
932   | MEMBEROFPTR(a1, fieldname) ->
933       let b1 = elab a1 in
934-      let (fld, attrs) =
935+      let (space, fld, attrs) =
936         match unroll env b1.etyp with
937-        | TPtr(t, _) ->
938+        | TPtr(space, t, _) ->
939             begin match unroll env t with
940             | TStruct(id, attrs) ->
941-                (wrap Env.find_struct_member loc env (id, fieldname), attrs)
942+                (space, wrap Env.find_struct_member loc env (id, fieldname), attrs)
943             | TUnion(id, attrs) ->
944-                (wrap Env.find_union_member loc env (id, fieldname), attrs)
945+                (space, wrap Env.find_union_member loc env (id, fieldname), attrs)
946             | _ ->
947                 error "left-hand side of '->' is not a pointer to a struct or union"
948             end
949         | _ ->
950             error "left-hand side of '->' is not a pointer " in
951       { edesc = EUnop(Oarrow fieldname, b1);
952-        etyp = add_attributes_type attrs fld.fld_typ }
953+        etyp = add_attributes_type attrs fld.fld_typ;
954+        espace = space }
955 
956 (* Hack to treat vararg.h functions the GCC way.  Helps with testing.
957     va_start(ap,n)
[292]958@@ -754,13 +792,15 @@ let elab_expr loc env a =
[160]959   | CALL((VARIABLE "__builtin_va_start" as a1), [a2; a3]) ->
960       let b1 = elab a1 and b2 = elab a2 and b3 = elab a3 in
961       { edesc = ECall(b1, [b2; {edesc = EUnop(Oaddrof, b3);
962-                                etyp = TPtr(b3.etyp, [])}]);
963-        etyp = TVoid [] }
964+                                etyp = TPtr(b3.espace, b3.etyp, []);
965+                                espace = Any }]);
966+        etyp = TVoid [];
967+        espace = Any (* XXX ? *) }
968   | CALL((VARIABLE "__builtin_va_arg" as a1),
969          [a2; (TYPE_SIZEOF _) as a3]) ->
970       let b1 = elab a1 and b2 = elab a2 and b3 = elab a3 in
971       let ty = match b3.edesc with ESizeof ty -> ty | _ -> assert false in
972-      { edesc = ECall(b1, [b2; b3]); etyp = ty }
973+      { edesc = ECall(b1, [b2; b3]); etyp = ty; espace = Any (* XXX ? *) }
974 
975   | CALL(a1, al) ->
976       let b1 =
[292]977@@ -771,15 +811,15 @@ let elab_expr loc env a =
[160]978             let ty = TFun(TInt(IInt, []), None, false, []) in
979             (* Emit an extern declaration for it *)
980             let id = Env.fresh_ident n in
981-            emit_elab (elab_loc loc) (Gdecl(Storage_extern, id, ty, None));
982-            { edesc = EVar id; etyp = ty }
983+            emit_elab (elab_loc loc) (Gdecl(Code, (Storage_extern, id, ty, None)));
984+            { edesc = EVar id; etyp = ty; espace = Any }
985         | _ -> elab a1 in
986       let bl = List.map elab al in
987       (* Extract type information *)
988       let (res, args, vararg) =
989         match unroll env b1.etyp with
990         | TFun(res, args, vararg, a) -> (res, args, vararg)
991-        | TPtr(ty, a) ->
992+        | TPtr(_, ty, a) ->
993             begin match unroll env ty with
994             | TFun(res, args, vararg, a) -> (res, args, vararg)
995             | _ -> error "the function part of a call does not have a function type"
[292]996@@ -791,7 +831,7 @@ let elab_expr loc env a =
[160]997         match args with
998         | None -> bl
999         | Some proto -> elab_arguments 1 bl proto vararg in
1000-      { edesc = ECall(b1, bl'); etyp = res }
1001+      { edesc = ECall(b1, bl'); etyp = res; espace = Any (* Stack *) }
1002 
1003   | UNARY(POSINCR, a1) ->
1004       elab_pre_post_incr_decr Opostincr "postfix '++'" a1
[292]1005@@ -805,50 +845,50 @@ let elab_expr loc env a =
[160]1006       let b1 = elab a1 in
1007       if not (valid_cast env b1.etyp ty) then
1008         err "illegal cast from %a@ to %a" Cprint.typ b1.etyp Cprint.typ ty;
1009-      { edesc = ECast(ty, b1); etyp = ty }
1010+      { edesc = ECast(ty, b1); etyp = ty; espace = b1.espace }
1011 
1012   | CAST ((spec, dcl), _) ->
1013       error "cast of initializer expression is not supported"
1014 
1015   | EXPR_SIZEOF(CONSTANT(CONST_STRING s)) ->
1016       let cst = CInt(Int64.of_int (String.length s), size_t_ikind, "") in
1017-      { edesc = EConst cst; etyp = type_of_constant cst }
1018+      { edesc = EConst cst; etyp = type_of_constant cst; espace = Code }
1019 
1020   | EXPR_SIZEOF a1 ->
1021       let b1 = elab a1 in
1022       if sizeof env b1.etyp = None then
1023         err "incomplete type %a" Cprint.typ b1.etyp;
1024-      { edesc = ESizeof b1.etyp; etyp = TInt(size_t_ikind, []) }
1025+      { edesc = ESizeof b1.etyp; etyp = TInt(size_t_ikind, []); espace = Code }
1026 
1027   | TYPE_SIZEOF (spec, dcl) ->
1028       let ty = elab_type loc env spec dcl in
1029       if sizeof env ty = None then
1030         err "incomplete type %a" Cprint.typ ty;
1031-      { edesc = ESizeof ty; etyp = TInt(size_t_ikind, []) }
1032+      { edesc = ESizeof ty; etyp = TInt(size_t_ikind, []); espace = Code }
1033 
1034   | UNARY(PLUS, a1) ->
1035       let b1 = elab a1 in
1036       if not (is_arith_type env b1.etyp) then
1037         error "argument of unary '+' is not an arithmetic type";
1038-      { edesc = EUnop(Oplus, b1); etyp = unary_conversion env b1.etyp }
1039+      { edesc = EUnop(Oplus, b1); etyp = unary_conversion env b1.etyp; espace = Any }
1040 
1041   | UNARY(MINUS, a1) ->
1042       let b1 = elab a1 in
1043       if not (is_arith_type env b1.etyp) then
1044         error "argument of unary '-' is not an arithmetic type";
1045-      { edesc = EUnop(Ominus, b1); etyp = unary_conversion env b1.etyp }
1046+      { edesc = EUnop(Ominus, b1); etyp = unary_conversion env b1.etyp; espace = Any }
1047 
1048   | UNARY(BNOT, a1) ->
1049       let b1 = elab a1 in
1050       if not (is_integer_type env b1.etyp) then
1051         error "argument of '~' is not an integer type";
1052-      { edesc = EUnop(Onot, b1); etyp = unary_conversion env b1.etyp }
1053+      { edesc = EUnop(Onot, b1); etyp = unary_conversion env b1.etyp; espace = Any }
1054 
1055   | UNARY(NOT, a1) ->
1056       let b1 = elab a1 in
1057       if not (is_scalar_type env b1.etyp) then
1058         error "argument of '!' is not a scalar type";
1059-      { edesc = EUnop(Olognot, b1); etyp = TInt(IInt, []) }
1060+      { edesc = EUnop(Olognot, b1); etyp = TInt(IInt, []); espace = Any }
1061 
1062   | UNARY(ADDROF, a1) ->
1063       let b1 = elab a1 in
[292]1064@@ -857,15 +897,15 @@ let elab_expr loc env a =
[160]1065       | _ ->
1066         if not (is_lvalue env b1) then err "argument of '&' is not a l-value"
1067       end;
1068-      { edesc = EUnop(Oaddrof, b1); etyp = TPtr(b1.etyp, []) }
1069+      { edesc = EUnop(Oaddrof, b1); etyp = TPtr(b1.espace, b1.etyp, []); espace = Any }
1070 
1071   | UNARY(MEMOF, a1) ->
1072       let b1 = elab a1 in
1073       begin match unroll env b1.etyp with
1074       (* '*' applied to a function type has no effect *)
1075       | TFun _ -> b1
1076-      | TPtr(ty, _) | TArray(ty, _, _) ->
1077-          { edesc = EUnop(Oderef, b1); etyp = ty }
1078+      | TPtr(space, ty, _) | TArray(space, ty, _, _) ->
1079+          { edesc = EUnop(Oderef, b1); etyp = ty; espace = space }
1080       | _ ->
1081           error "argument of unary '*' is not a pointer"
1082       end
[292]1083@@ -893,16 +933,16 @@ let elab_expr loc env a =
[160]1084         if is_arith_type env b1.etyp && is_arith_type env b2.etyp then
1085           binary_conversion env b1.etyp b2.etyp
1086         else begin
1087-          let (ty, attr) =
1088+          let (space, ty, attr) =
1089             match unroll env b1.etyp, unroll env b2.etyp with
1090-            | (TPtr(ty, a) | TArray(ty, _, a)), TInt _ -> (ty, a)
1091-            | TInt _, (TPtr(ty, a) | TArray(ty, _, a)) -> (ty, a)
1092+            | (TPtr(space, ty, a) | TArray(space, ty, _, a)), TInt _ -> (space, ty, a)
1093+            | TInt _, (TPtr(space, ty, a) | TArray(space, ty, _, a)) -> (space, ty, a)
1094             | _, _ -> error "type error in binary '+'" in
1095           if not (pointer_arithmetic_ok env ty) then
1096             err "illegal pointer arithmetic in binary '+'";
1097-          TPtr(ty, attr)
1098+          TPtr(space, ty, attr)
1099         end in
1100-      { edesc = EBinop(Oadd, b1, b2, tyres); etyp = tyres }
1101+      { edesc = EBinop(Oadd, b1, b2, tyres); etyp = tyres; espace = Any }
1102 
1103   | BINARY(SUB, a1, a2) ->
1104       let b1 = elab a1 in
[292]1105@@ -913,24 +953,25 @@ let elab_expr loc env a =
[160]1106           (tyres, tyres)
1107         end else begin
1108           match unroll env b1.etyp, unroll env b2.etyp with
1109-          | (TPtr(ty, a) | TArray(ty, _, a)), TInt _ ->
1110+          | (TPtr(space, ty, a) | TArray(space, ty, _, a)), TInt _ ->
1111               if not (pointer_arithmetic_ok env ty) then
1112                 err "illegal pointer arithmetic in binary '-'";
1113-              (TPtr(ty, a), TPtr(ty, a))
1114-          | TInt _, (TPtr(ty, a) | TArray(ty, _, a)) ->
1115+              (TPtr(space, ty, a), TPtr(space, ty, a))
1116+          | TInt _, (TPtr(space, ty, a) | TArray(space, ty, _, a)) ->
1117               if not (pointer_arithmetic_ok env ty) then
1118                 err "illegal pointer arithmetic in binary '-'";
1119-              (TPtr(ty, a), TPtr(ty, a))
1120-          | (TPtr(ty1, a1) | TArray(ty1, _, a1)),
1121-            (TPtr(ty2, a2) | TArray(ty2, _, a2)) ->
1122-              if not (compatible_types ~noattrs:true env ty1 ty2) then
1123+              (TPtr(space, ty, a), TPtr(space, ty, a))
1124+          | (TPtr(space1, ty1, a1) | TArray(space1, ty1, _, a1)),
1125+            (TPtr(space2, ty2, a2) | TArray(space2, ty2, _, a2)) ->
1126+(* TODO: automatic cast on space mismatch? *)
1127+              if not (compatible_types ~noattrs:true env ty1 ty2) || space1 != space2 then
1128                 err "mismatch between pointer types in binary '-'";
1129               if not (pointer_arithmetic_ok env ty1) then
1130                 err "illegal pointer arithmetic in binary '-'";
1131-              (TPtr(ty1, []), TInt(ptrdiff_t_ikind, []))
1132+              (TPtr(space1, ty1, []), TInt(ptrdiff_t_ikind, []))
1133           | _, _ -> error "type error in binary '-'"
1134         end in
1135-      { edesc = EBinop(Osub, b1, b2, tyop); etyp = tyres }
1136+      { edesc = EBinop(Osub, b1, b2, tyop); etyp = tyres; espace = Any }
1137 
1138   | BINARY(SHL, a1, a2) ->
1139       elab_shift "<<" Oshl a1 a2
[292]1140@@ -970,35 +1011,38 @@ let elab_expr loc env a =
[160]1141       let b1 = elab a1 in
1142       let b2 = elab a2 in
1143       let b3 = elab a3 in
1144+      let space = join_spaces b2.espace b3.espace in
1145       if not (is_scalar_type env b1.etyp) then
1146         err ("the first argument of '? :' is not a scalar type");
1147       begin match pointer_decay env b2.etyp, pointer_decay env b3.etyp with
1148       | (TInt _ | TFloat _), (TInt _ | TFloat _) ->
1149           { edesc = EConditional(b1, b2, b3);
1150-            etyp = binary_conversion env b2.etyp b3.etyp }
1151-      | TPtr(ty1, a1), TPtr(ty2, a2) ->
1152+            etyp = binary_conversion env b2.etyp b3.etyp;
1153+            espace = space }
1154+      (* TODO: maybe we should automatically cast to a generic pointer when the spaces don't match? *)
1155+      | TPtr(sp1, ty1, a1), TPtr(sp2, ty2, a2) ->
1156           let tyres =
1157-            if is_void_type env ty1 || is_void_type env ty2 then
1158-              TPtr(TVoid [], add_attributes a1 a2)
1159+            if (is_void_type env ty1 || is_void_type env ty2) && sp1 = sp2 then
1160+              TPtr(sp1, TVoid [], add_attributes a1 a2)
1161             else
1162               match combine_types ~noattrs:true env
1163-                                  (TPtr(ty1, a1)) (TPtr(ty2, a2)) with
1164+                                  (TPtr(sp1, ty1, a1)) (TPtr(sp2, ty2, a2)) with
1165               | None ->
1166                   error "the second and third arguments of '? :' \
1167                          have incompatible pointer types"
1168               | Some ty -> ty
1169             in
1170-          { edesc = EConditional(b1, b2, b3); etyp = tyres }
1171-      | TPtr(ty1, a1), TInt _ when is_literal_0 b3 ->
1172-          { edesc = EConditional(b1, b2, nullconst); etyp = TPtr(ty1, a1) }
1173-      | TInt _, TPtr(ty2, a2) when is_literal_0 b2 ->
1174-          { edesc = EConditional(b1, nullconst, b3); etyp = TPtr(ty2, a2) }
1175+          { edesc = EConditional(b1, b2, b3); etyp = tyres; espace = space }
1176+      | TPtr(sp1, ty1, a1), TInt _ when is_literal_0 b3 ->
1177+          { edesc = EConditional(b1, b2, nullconst); etyp = TPtr(sp1, ty1, a1); espace = space }
1178+      | TInt _, TPtr(sp2, ty2, a2) when is_literal_0 b2 ->
1179+          { edesc = EConditional(b1, nullconst, b3); etyp = TPtr(sp2, ty2, a2); espace = space }
1180       | ty1, ty2 ->
1181           match combine_types env ty1 ty2 with
1182           | None ->
1183               error ("the second and third arguments of '? :' have incompatible types")
1184           | Some tyres ->
1185-              { edesc = EConditional(b1, b2, b3); etyp = tyres }
1186+              { edesc = EConditional(b1, b2, b3); etyp = tyres; espace = space }
1187       end
1188 
1189 (* 7.9 Assignment expressions *)
[292]1190@@ -1018,7 +1062,7 @@ let elab_expr loc env a =
[160]1191           err "assigning a value of type@ %a@ to a lvalue of type@ %a"
1192                   Cprint.typ b2.etyp Cprint.typ b1.etyp;
1193       end;
1194-      { edesc = EBinop(Oassign, b1, b2, b1.etyp); etyp = b1.etyp }
1195+      { edesc = EBinop(Oassign, b1, b2, b1.etyp); etyp = b1.etyp; espace = b1.espace }
1196 
1197   | BINARY((ADD_ASSIGN | SUB_ASSIGN | MUL_ASSIGN | DIV_ASSIGN | MOD_ASSIGN
1198             | BAND_ASSIGN | BOR_ASSIGN | XOR_ASSIGN | SHL_ASSIGN | SHR_ASSIGN
[292]1199@@ -1050,7 +1094,7 @@ let elab_expr loc env a =
[160]1200               err "assigning a value of type@ %a@ to a lvalue of type@ %a"
1201                       Cprint.typ ty Cprint.typ b1.etyp;
1202           end;
1203-          { edesc = EBinop(top, b1, b2, ty); etyp = b1.etyp }
1204+          { edesc = EBinop(top, b1, b2, ty); etyp = b1.etyp; espace = b1.espace }
1205       | _ -> assert false
1206       end
1207 
[292]1208@@ -1063,7 +1107,7 @@ let elab_expr loc env a =
[160]1209       | [] -> accu
1210       | a :: l ->
1211           let b = elab a in
1212-          elab_comma { edesc = EBinop(Ocomma, accu, b, b.etyp); etyp = b.etyp } l
1213+          elab_comma { edesc = EBinop(Ocomma, accu, b, b.etyp); etyp = b.etyp; espace = b.espace } l
1214       in elab_comma (elab a1) al
1215 
1216 (* Extensions that we do not handle *)
[292]1217@@ -1099,7 +1143,7 @@ let elab_expr loc env a =
[160]1218         err "the argument of %s is not a l-value" msg;
1219       if not (is_scalar_type env b1.etyp) then
1220         err "the argument of %s must be an arithmetic or pointer type" msg;
1221-      { edesc = EUnop(op, b1); etyp = b1.etyp }
1222+      { edesc = EUnop(op, b1); etyp = b1.etyp; espace = b1.espace }
1223 
1224 (* Elaboration of binary operators over integers *)
1225   and elab_binary_integer msg op a1 a2 =
[292]1226@@ -1110,7 +1154,7 @@ let elab_expr loc env a =
[160]1227       if not (is_integer_type env b2.etyp) then
1228         error "the second argument of '%s' is not an integer type" msg;
1229       let tyres = binary_conversion env b1.etyp b2.etyp in
1230-      { edesc = EBinop(op, b1, b2, tyres); etyp = tyres }
1231+      { edesc = EBinop(op, b1, b2, tyres); etyp = tyres; espace = Any }
1232 
1233 (* Elaboration of binary operators over arithmetic types *)
1234   and elab_binary_arithmetic msg op a1 a2 =
[292]1235@@ -1121,7 +1165,7 @@ let elab_expr loc env a =
[160]1236       if not (is_arith_type env b2.etyp) then
1237         error "the second argument of '%s' is not an arithmetic type" msg;
1238       let tyres = binary_conversion env b1.etyp b2.etyp in
1239-      { edesc = EBinop(op, b1, b2, tyres); etyp = tyres }
1240+      { edesc = EBinop(op, b1, b2, tyres); etyp = tyres; espace = Any }
1241 
1242 (* Elaboration of shift operators *)
1243   and elab_shift msg op a1 a2 =
[292]1244@@ -1132,7 +1176,7 @@ let elab_expr loc env a =
[160]1245       if not (is_integer_type env b2.etyp) then
1246         error "the second argument of '%s' is not an integer type" msg;
1247       let tyres = unary_conversion env b1.etyp in
1248-      { edesc = EBinop(op, b1, b2, tyres); etyp = tyres }
1249+      { edesc = EBinop(op, b1, b2, tyres); etyp = tyres; espace = Any }
1250 
1251 (* Elaboration of comparisons *)
1252   and elab_comparison op a1 a2 =
[292]1253@@ -1142,28 +1186,28 @@ let elab_expr loc env a =
[160]1254         match pointer_decay env b1.etyp, pointer_decay env b2.etyp with
1255         | (TInt _ | TFloat _), (TInt _ | TFloat _) ->
1256             EBinop(op, b1, b2, binary_conversion env b1.etyp b2.etyp)
1257-        | TInt _, TPtr(ty, _) when is_literal_0 b1 ->
1258-            EBinop(op, nullconst, b2, TPtr(ty, []))
1259-        | TPtr(ty, _), TInt _ when is_literal_0 b2 ->
1260-            EBinop(op, b1, nullconst, TPtr(ty, []))
1261-        | TPtr(ty1, _), TPtr(ty2, _)
1262+        | TInt _, TPtr(sp, ty, _) when is_literal_0 b1 ->
1263+            EBinop(op, nullconst, b2, TPtr(sp, ty, []))
1264+        | TPtr(sp, ty, _), TInt _ when is_literal_0 b2 ->
1265+            EBinop(op, b1, nullconst, TPtr(sp, ty, []))
1266+        | TPtr(sp1, ty1, _), TPtr(sp2, ty2, _)
1267           when is_void_type env ty1 ->
1268-            EBinop(op, b1, b2, TPtr(ty2, []))
1269-        | TPtr(ty1, _), TPtr(ty2, _)
1270+            EBinop(op, b1, b2, TPtr(sp2, ty2, []))  (* XXX sp1? *)
1271+        | TPtr(sp1, ty1, _), TPtr(sp2, ty2, _)
1272           when is_void_type env ty2 ->
1273-            EBinop(op, b1, b2, TPtr(ty1, []))
1274-        | TPtr(ty1, _), TPtr(ty2, _) ->
1275+            EBinop(op, b1, b2, TPtr(sp1, ty1, []))  (* XXX sp2? *)
1276+        | TPtr(sp1, ty1, _), TPtr(sp2, ty2, _) ->
1277             if not (compatible_types ~noattrs:true env ty1 ty2) then
1278               warning "comparison between incompatible pointer types";
1279-            EBinop(op, b1, b2, TPtr(ty1, []))
1280-        | TPtr _, TInt _
1281-        | TInt _, TPtr _ ->
1282+            EBinop(op, b1, b2, TPtr(sp1, ty1, []))  (* XXX sp1? *)
1283+        | TPtr (sp,_,_), TInt _
1284+        | TInt _, TPtr (sp,_,_) ->
1285             warning "comparison between integer and pointer";
1286-            EBinop(op, b1, b2, TPtr(TVoid [], []))
1287+            EBinop(op, b1, b2, TPtr(sp,TVoid [], []))
1288         | ty1, ty2 ->
1289             error "illegal comparison between types@ %a@ and %a"
1290                   Cprint.typ b1.etyp Cprint.typ b2.etyp in
1291-      { edesc = resdesc; etyp = TInt(IInt, []) }
1292+      { edesc = resdesc; etyp = TInt(IInt, []); espace = Any }
1293 
1294 (* Elaboration of && and || *)
1295   and elab_logical_operator msg op a1 a2 =
[292]1296@@ -1173,7 +1217,7 @@ let elab_expr loc env a =
[160]1297       let b2 = elab a2 in
1298       if not (is_scalar_type env b2.etyp) then
1299         err "the second argument of '%s' is not a scalar type" msg;
1300-      { edesc = EBinop(op, b1, b2, TInt(IInt, [])); etyp = TInt(IInt, []) }
1301+      { edesc = EBinop(op, b1, b2, TInt(IInt, [])); etyp = TInt(IInt, []); espace = Any }
1302 
1303 (* Type-checking of function arguments *)
1304   and elab_arguments argno args params vararg =
[292]1305@@ -1271,7 +1315,7 @@ let check_init_type loc env a ty =
[160]1306 
1307 let rec elab_init loc env ty ile =
1308   match unroll env ty with
1309-  | TArray(ty_elt, opt_sz, _) ->
1310+  | TArray(space, ty_elt, opt_sz, _) ->
1311       let rec elab_init_array n accu rem =
1312         match opt_sz, rem with
1313         | Some sz, _ when n >= sz ->
[292]1314@@ -1390,8 +1434,8 @@ let elab_initial loc env ty ie =
[160]1315 
1316 let fixup_typ env ty init =
1317   match unroll env ty, init with
1318-  | TArray(ty_elt, None, attr), Init_array il ->
1319-      TArray(ty_elt, Some(Int64.of_int(List.length il)), attr)
1320+  | TArray(space, ty_elt, None, attr), Init_array il ->
1321+      TArray(space, ty_elt, Some(Int64.of_int(List.length il)), attr)
1322   | _ -> ty
1323 
1324 (* Entry point *)
[292]1325@@ -1416,9 +1460,9 @@ let enter_typedef loc env (s, sto, ty) =
[160]1326   emit_elab (elab_loc loc) (Gtypedef(id, ty));
1327   env'
1328 
1329-let enter_or_refine_ident local loc env s sto ty =
1330+let enter_or_refine_ident local loc env s sto ty space =
1331   match redef Env.lookup_ident env s with
1332-  | Some(id, II_ident(old_sto, old_ty)) ->
1333+  | Some(id, II_ident(old_sto, old_ty, old_space)) ->
1334       let new_ty =
1335         if local then begin
1336           error loc "redefinition of local variable '%s'" s;
[292]1337@@ -1437,17 +1481,18 @@ let enter_or_refine_ident local loc env s sto ty =
[160]1338           warning loc "redefinition of '%s' with incompatible storage class" s;
1339           sto
1340         end in
1341-      (id, Env.add_ident env id new_sto new_ty)
1342+      let new_space = join_spaces old_space space (* XXX: incompatible? *) in
1343+      (id, Env.add_ident env id new_sto new_ty new_space)
1344   | Some(id, II_enum v) ->
1345       error loc "illegal redefinition of enumerator '%s'" s;
1346-      (id, Env.add_ident env id sto ty)
1347+      (id, Env.add_ident env id sto ty space)
1348   | _ ->
1349-      Env.enter_ident env s sto ty
1350+      Env.enter_ident env s sto ty space
1351 
1352 let rec enter_decdefs local loc env = function
1353   | [] ->
1354       ([], env)
1355-  | (s, sto, ty, init) :: rem ->
1356+  | (space, s, sto, ty, init) :: rem ->
1357       (* Sanity checks on storage class *)
1358       begin match sto with
1359       | Storage_extern ->
[292]1360@@ -1462,11 +1507,11 @@ let rec enter_decdefs local loc env = function
[160]1361         match unroll env ty with TFun _ -> Storage_extern | _ -> sto in
1362       (* enter ident in environment with declared type, because
1363          initializer can refer to the ident *)
1364-      let (id, env1) = enter_or_refine_ident local loc env s sto' ty in
1365+      let (id, env1) = enter_or_refine_ident local loc env s sto' ty space in
1366       (* process the initializer *)
1367       let (ty', init') = elab_initializer loc env1 ty init in
1368       (* update environment with refined type *)
1369-      let env2 = Env.add_ident env1 id sto' ty' in
1370+      let env2 = Env.add_ident env1 id sto' ty' space in
1371       (* check for incomplete type *)
1372       if sto' <> Storage_extern && incomplete_type env ty' then
1373         warning loc "'%s' has incomplete type" s;
[292]1374@@ -1476,7 +1521,7 @@ let rec enter_decdefs local loc env = function
[160]1375         ((sto', id, ty', init') :: decls, env3)
1376       end else begin
1377         (* Global definition *)
1378-        emit_elab (elab_loc loc) (Gdecl(sto, id, ty', init'));
1379+        emit_elab (elab_loc loc) (Gdecl(space, (sto, id, ty', init')));
1380         enter_decdefs local loc env2 rem
1381       end
1382 
[292]1383@@ -1496,10 +1541,10 @@ let elab_fundef env (spec, name) body loc1 loc2 =
[160]1384     | TFun(ty_ret, Some params, vararg, attr) -> (ty_ret, params, vararg)
1385     | _ -> fatal_error loc1 "wrong type for function definition" in
1386   (* Enter function in the environment, for recursive references *)
1387-  let (fun_id, env1) = enter_or_refine_ident false loc1 env s sto ty in
1388+  let (fun_id, env1) = enter_or_refine_ident false loc1 env s sto ty Code in
1389   (* Enter parameters in the environment *)
1390   let env2 =
1391-    List.fold_left (fun e (id, ty) -> Env.add_ident e id Storage_default ty)
1392+    List.fold_left (fun e (id, ty) -> Env.add_ident e id Storage_default ty Any)
1393                    (Env.new_scope env1) params in
1394   (* Elaborate function body *)
1395   let body' = !elab_block_f loc2 ty_ret env2 body in
[292]1396@@ -1538,7 +1583,7 @@ let rec elab_definition (local: bool) (env: Env.t) (def: Cabs.definition)
[160]1397 
1398   (* "struct s { ...};" or "union u;" *)
1399   | ONLYTYPEDEF(spec, loc) ->
1400-      let (sto, inl, ty, env') = elab_specifier ~only:true loc env spec in
1401+      let (space, sto, inl, ty, env') = elab_specifier ~only:true loc env spec in
1402       if sto <> Storage_default || inl then
1403         error loc "Non-default storage or 'inline' on 'struct' or 'union' declaration";
1404       ([], env')
[292]1405diff --git a/cparser/Env.ml b/cparser/Env.ml
1406index 777b3e1..1f41c0c 100644
1407--- a/cparser/Env.ml
1408+++ b/cparser/Env.ml
1409@@ -70,7 +70,7 @@ type composite_info = {
[160]1410 (* Infos associated with an ordinary identifier *)
1411 
1412 type ident_info =
1413-  | II_ident of storage * typ
1414+  | II_ident of storage * typ * memory_space
1415   | II_enum of int64                    (* value of the enum *)
1416 
1417 (* Infos associated with a typedef *)
[292]1418@@ -201,10 +201,10 @@ let find_typedef env id =
[160]1419 
1420 (* Inserting things by source name, with generation of a translated name *)
1421 
1422-let enter_ident env s sto ty =
1423+let enter_ident env s sto ty sp =
1424   let id = fresh_ident s in
1425   (id,
1426-   { env with env_ident = IdentMap.add id (II_ident(sto, ty)) env.env_ident })
1427+   { env with env_ident = IdentMap.add id (II_ident(sto, ty, sp)) env.env_ident })
1428 
1429 let enter_composite env s ci =
1430   let id = fresh_ident s in
[292]1431@@ -220,8 +220,8 @@ let enter_typedef env s info =
[160]1432 
1433 (* Inserting things by translated name *)
1434 
1435-let add_ident env id sto ty =
1436-  { env with env_ident = IdentMap.add id (II_ident(sto, ty)) env.env_ident }
1437+let add_ident env id sto ty sp =
1438+  { env with env_ident = IdentMap.add id (II_ident(sto, ty, sp)) env.env_ident }
1439 
1440 let add_composite env id ci =
1441   { env with env_tag = IdentMap.add id ci env.env_tag }
[292]1442diff --git a/cparser/Env.mli b/cparser/Env.mli
1443index e7a74af..a9daa21 100644
1444--- a/cparser/Env.mli
1445+++ b/cparser/Env.mli
1446@@ -31,7 +31,7 @@ type composite_info = {
[160]1447   ci_sizeof: int option;                (* size; None if incomplete *)
1448 }
1449 
1450-type ident_info = II_ident of C.storage * C.typ | II_enum of int64
1451+type ident_info = II_ident of C.storage * C.typ * C.memory_space | II_enum of int64
1452 
1453 type typedef_info = C.typ
1454 
[292]1455@@ -60,11 +60,11 @@ val find_struct_member : t -> C.ident * string -> C.field
[160]1456 val find_union_member : t -> C.ident * string -> C.field
1457 val find_typedef : t -> C.ident -> typedef_info
1458 
1459-val enter_ident : t -> string -> C.storage -> C.typ -> C.ident * t
1460+val enter_ident : t -> string -> C.storage -> C.typ -> C.memory_space -> C.ident * t
1461 val enter_composite : t -> string -> composite_info -> C.ident * t
1462 val enter_enum_item : t -> string -> int64 -> C.ident * t
1463 val enter_typedef : t -> string -> typedef_info -> C.ident * t
1464 
1465-val add_ident : t -> C.ident -> C.storage -> C.typ -> t
1466+val add_ident : t -> C.ident -> C.storage -> C.typ -> C.memory_space -> t
1467 val add_composite : t -> C.ident -> composite_info -> t
1468 val add_typedef : t -> C.ident -> typedef_info -> t
[292]1469diff --git a/cparser/GCC.ml b/cparser/GCC.ml
1470index 9f864dc..17f3cfa 100644
1471--- a/cparser/GCC.ml
1472+++ b/cparser/GCC.ml
1473@@ -30,11 +30,11 @@ let ulongLongType = TInt(IULongLong, [])
[160]1474 let floatType = TFloat(FFloat, [])
1475 let doubleType = TFloat(FDouble, [])
1476 let longDoubleType = TFloat (FLongDouble, [])
1477-let voidPtrType = TPtr(TVoid [], [])
1478-let voidConstPtrType = TPtr(TVoid [AConst], [])
1479-let charPtrType = TPtr(TInt(IChar, []), [])
1480-let charConstPtrType = TPtr(TInt(IChar, [AConst]), [])
1481-let intPtrType = TPtr(TInt(IInt, []), [])
1482+let voidPtrType = TPtr(Any,TVoid [], [])
1483+let voidConstPtrType = TPtr(Any,TVoid [AConst], [])
1484+let charPtrType = TPtr(Any,TInt(IChar, []), [])
1485+let charConstPtrType = TPtr(Any,TInt(IChar, [AConst]), [])
1486+let intPtrType = TPtr(Any,TInt(IInt, []), [])
1487 let sizeType = TInt(size_t_ikind, [])
1488 
1489 let builtins = {
[292]1490@@ -150,9 +150,9 @@ let builtins = {
[160]1491   "__builtin_log10l",  (longDoubleType, [ longDoubleType ], false);
1492 
1493   "__builtin_modff",  (floatType, [ floatType;
1494-                                          TPtr(floatType,[]) ], false);
1495+                                          TPtr(Any,floatType,[]) ], false);
1496   "__builtin_modfl",  (longDoubleType, [ longDoubleType;
1497-                                               TPtr(longDoubleType, []) ],
1498+                                               TPtr(Any,longDoubleType, []) ],
1499                              false);
1500 
1501   "__builtin_nan",  (doubleType, [ charConstPtrType ], false);
[292]1502diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll
1503index d4947ad..d3f3958 100644
1504--- a/cparser/Lexer.mll
1505+++ b/cparser/Lexer.mll
1506@@ -181,7 +181,13 @@ let init_lexicon _ =
[160]1507       ("__builtin_types_compatible_p", fun loc -> BUILTIN_TYPES_COMPAT loc);
1508       ("__builtin_offsetof", fun loc -> BUILTIN_OFFSETOF loc);
1509       (* On some versions of GCC __thread is a regular identifier *)
1510-      ("__thread", fun loc -> THREAD loc)
1511+      ("__thread", fun loc -> THREAD loc);
1512+      (* 8051 memory space extensions *)
1513+      ("__data", fun loc -> DATA loc);
1514+      ("__idata", fun loc -> IDATA loc);
1515+      ("__pdata", fun loc -> PDATA loc);
1516+      ("__xdata", fun loc -> XDATA loc);
1517+      ("__code", fun loc -> CODE loc);
1518     ]
1519 
1520 (* Mark an identifier as a type name. The old mapping is preserved and will
[292]1521diff --git a/cparser/Parser.mly b/cparser/Parser.mly
1522index 0eebb84..abec574 100644
1523--- a/cparser/Parser.mly
1524+++ b/cparser/Parser.mly
1525@@ -221,6 +221,8 @@ let transformOffsetOf (speclist, dtype) member =
[160]1526 %token<Cabs.cabsloc> VOLATILE EXTERN STATIC CONST RESTRICT AUTO REGISTER
1527 %token<Cabs.cabsloc> THREAD
1528 
1529+%token<Cabs.cabsloc> DATA IDATA PDATA XDATA CODE
1530+
1531 %token<Cabs.cabsloc> SIZEOF ALIGNOF
1532 
1533 %token EQ PLUS_EQ MINUS_EQ STAR_EQ SLASH_EQ PERCENT_EQ
[292]1534@@ -1249,6 +1251,12 @@ attribute_nocv:
[160]1535 |   MSATTR                              { (fst $1, []), snd $1 }
1536                                         /* ISO 6.7.3 */
1537 |   THREAD                              { ("__thread",[]), $1 }
1538+
1539+|   DATA                                { ("data",[]), $1 }
1540+|   IDATA                               { ("idata",[]), $1 }
1541+|   PDATA                               { ("pdata",[]), $1 }
1542+|   XDATA                               { ("xdata",[]), $1 }
1543+|   CODE                                { ("code",[]), $1 }
1544 ;
1545 
1546 attribute_nocv_list:
[292]1547diff --git a/cparser/Rename.ml b/cparser/Rename.ml
1548index 4b2f350..b6de8cd 100644
1549--- a/cparser/Rename.ml
1550+++ b/cparser/Rename.ml
1551@@ -75,8 +75,8 @@ let ident env id =
[160]1552                        id.name id.stamp
1553 
1554 let rec typ env = function
1555-  | TPtr(ty, a) -> TPtr(typ env ty, a)
1556-  | TArray(ty, sz, a) -> TArray(typ env ty, sz, a)
1557+  | TPtr(sp, ty, a) -> TPtr(sp, typ env ty, a)
1558+  | TArray(sp, ty, sz, a) -> TArray(sp, typ env ty, sz, a)
1559   | TFun(res, None, va, a) -> TFun(typ env res, None, va, a)
1560   | TFun(res, Some p, va, a) ->
1561       let (p', _) = mmap param env p in
[292]1562@@ -97,7 +97,7 @@ let constant env = function
[160]1563   | cst -> cst
1564 
1565 let rec exp env e =
1566-  { edesc = exp_desc env e.edesc; etyp = typ env e.etyp }
1567+  { edesc = exp_desc env e.edesc; etyp = typ env e.etyp; espace = e.espace }
1568 
1569 and exp_desc env = function
1570   | EConst cst -> EConst(constant env cst)
[292]1571@@ -191,9 +191,9 @@ let rec globdecl env g =
[160]1572   ( { gdesc = desc'; gloc = g.gloc }, env' )
1573 
1574 and globdecl_desc env = function
1575-  | Gdecl d ->
1576+  | Gdecl (sp,d) ->
1577       let (d', env') = decl env d in
1578-      (Gdecl d', env')
1579+      (Gdecl (sp,d'), env')
1580   | Gfundef fd ->
1581       let (fd', env') = fundef env fd in
1582       (Gfundef fd', env')
[292]1583@@ -230,7 +230,7 @@ let rec reserve_public env = function
[160]1584   | dcl :: rem ->
1585       let env' =
1586         match dcl.gdesc with
1587-        | Gdecl(sto, id, _, _) ->
1588+        | Gdecl (_, (sto, id, _, _)) ->
1589             begin match sto with
1590             | Storage_default | Storage_extern -> enter_global env id
1591             | Storage_static -> env
[292]1592diff --git a/cparser/SimplExpr.ml b/cparser/SimplExpr.ml
1593index 330b184..8202cb2 100644
1594--- a/cparser/SimplExpr.ml
1595+++ b/cparser/SimplExpr.ml
1596@@ -92,12 +92,13 @@ let simpl_expr loc env e act =
[160]1597 
1598   let eboolvalof e =
1599     { edesc = EBinop(One, e, intconst 0L IInt, TInt(IInt, []));
1600-      etyp = TInt(IInt, []) } in
1601+      etyp = TInt(IInt, []);
1602+      espace = Any } in
1603 
1604   let sseq s1 s2 = Cutil.sseq loc s1 s2 in
1605 
1606   let sassign e1 e2 =
1607-    { sdesc = Sdo {edesc = EBinop(Oassign, e1, e2, e1.etyp); etyp = e1.etyp};
1608+    { sdesc = Sdo {edesc = EBinop(Oassign, e1, e2, e1.etyp); etyp = e1.etyp; espace = e1.espace};
1609       sloc = loc } in
1610 
1611   let sif e s1 s2 =
[292]1612@@ -149,15 +150,15 @@ let simpl_expr loc env e act =
[160]1613 
1614         | Ominus | Oplus | Olognot | Onot | Oderef | Oarrow _ ->
1615             let (s1, e1') = simpl e1 RHS in
1616-            finish act s1 {edesc = EUnop(op, e1'); etyp = e.etyp}
1617+            finish act s1 {edesc = EUnop(op, e1'); etyp = e.etyp; espace = e.espace}
1618 
1619         | Oaddrof ->
1620             let (s1, e1') = simpl e1 LHS in
1621-            finish act s1 {edesc = EUnop(op, e1'); etyp = e.etyp}
1622+            finish act s1 {edesc = EUnop(op, e1'); etyp = e.etyp; espace = e.espace}
1623 
1624         | Odot _ ->
1625             let (s1, e1') = simpl e1 (if act = LHS then LHS else RHS) in
1626-            finish act s1 {edesc = EUnop(op, e1'); etyp = e.etyp}
1627+            finish act s1 {edesc = EUnop(op, e1'); etyp = e.etyp; espace = e.espace}
1628 
1629         | Opreincr | Opredecr ->
1630             let (s1, e1') = simpl e1 LHS in
[292]1631@@ -165,7 +166,7 @@ let simpl_expr loc env e act =
[160]1632             let op' = match op with Opreincr -> Oadd | _ -> Osub in
1633             let ty = unary_conversion env e.etyp in
1634             let e3 =
1635-              {edesc = EBinop(op', e2', intconst 1L IInt, ty); etyp = ty} in
1636+              {edesc = EBinop(op', e2', intconst 1L IInt, ty); etyp = ty; espace = Any} in
1637             begin match act with
1638             | Drop ->
1639                 (sseq s1 (sseq s2 (sassign e1' e3)), voidconst)
[292]1640@@ -184,12 +185,12 @@ let simpl_expr loc env e act =
[160]1641             | Drop ->
1642                 let (s2, e2') = lhs_to_rhs e1' in
1643                 let e3 =
1644-                  {edesc = EBinop(op', e2', intconst 1L IInt, ty); etyp = ty} in
1645+                  {edesc = EBinop(op', e2', intconst 1L IInt, ty); etyp = ty; espace = Any} in
1646                 (sseq s1 (sseq s2 (sassign e1' e3)), voidconst)
1647             | _ ->
1648                 let tmp = new_temp e.etyp in
1649                 let e3 =
1650-                  {edesc = EBinop(op', tmp, intconst 1L IInt, ty); etyp = ty} in
1651+                  {edesc = EBinop(op', tmp, intconst 1L IInt, ty); etyp = ty; espace = Any} in
1652                 finish act (sseq s1 (sseq (sassign tmp e1') (sassign e1' e3)))
1653                        tmp
1654             end
[292]1655@@ -205,7 +206,7 @@ let simpl_expr loc env e act =
[160]1656             let (s1, e1') = simpl e1 RHS in
1657             let (s2, e2') = simpl e2 RHS in
1658             finish act (sseq s1 s2)
1659-                       {edesc = EBinop(op, e1', e2', ty); etyp = e.etyp}
1660+                       {edesc = EBinop(op, e1', e2', ty); etyp = e.etyp; espace = Any}
1661 
1662         | Oassign ->
1663             if act = Drop && is_simpl_expr e1 then
[292]1664@@ -239,7 +240,7 @@ let simpl_expr loc env e act =
[160]1665               | Oshl_assign -> Oshl    | Oshr_assign -> Oshr
1666               | _ -> assert false in
1667             let e3 =
1668-              { edesc = EBinop(op', e11', e2', ty); etyp = ty } in
1669+              { edesc = EBinop(op', e11', e2', ty); etyp = ty; espace = Any } in
1670             begin match act with
1671             | Drop ->
1672                 (sseq s1 (sseq s11 (sseq s2 (sassign e1' e3))), voidconst)
[292]1673@@ -259,7 +260,7 @@ let simpl_expr loc env e act =
[160]1674             let (s1, e1') = simpl e1 RHS in
1675             if is_simpl_expr e2 then begin
1676               finish act s1
1677-                     {edesc = EBinop(Ologand, e1', e2, ty); etyp = e.etyp}
1678+                     {edesc = EBinop(Ologand, e1', e2, ty); etyp = e.etyp; espace = e.espace}
1679             end else begin
1680               match act with
1681               | Drop ->
[292]1682@@ -284,7 +285,7 @@ let simpl_expr loc env e act =
[160]1683             let (s1, e1') = simpl e1 RHS in
1684             if is_simpl_expr e2 then begin
1685               finish act s1
1686-                     {edesc = EBinop(Ologor, e1', e2, ty); etyp = e.etyp}
1687+                     {edesc = EBinop(Ologor, e1', e2, ty); etyp = e.etyp; espace = e.espace}
1688             end else begin
1689               match act with
1690               | Drop ->
[292]1691@@ -310,7 +311,7 @@ let simpl_expr loc env e act =
[160]1692     | EConditional(e1, e2, e3) ->
1693         let (s1, e1') = simpl e1 RHS in
1694         if is_simpl_expr e2 && is_simpl_expr e3 then begin
1695-          finish act s1 {edesc = EConditional(e1', e2, e3); etyp = e.etyp}
1696+          finish act s1 {edesc = EConditional(e1', e2, e3); etyp = e.etyp; espace = e.espace}
1697         end else begin
1698           match act with
1699           | Drop ->
[292]1700@@ -336,13 +337,13 @@ let simpl_expr loc env e act =
[160]1701             simpl e1 act
1702         end else begin
1703           let (s1, e1') = simpl e1 RHS in
1704-          finish act s1 {edesc = ECast(ty, e1'); etyp = e.etyp}
1705+          finish act s1 {edesc = ECast(ty, e1'); etyp = e.etyp; espace = e.espace}
1706         end
1707 
1708     | ECall(e1, el) ->
1709         let (s1, e1') = simpl e1 RHS in
1710         let (s2, el') = simpl_list el in
1711-        let e2 = { edesc = ECall(e1', el'); etyp = e.etyp } in
1712+        let e2 = { edesc = ECall(e1', el'); etyp = e.etyp; espace = e.espace } in
1713         begin match act with
1714         | Drop ->
1715             (sseq s1 (sseq s2 {sdesc = Sdo e2; sloc=loc}), voidconst)
[292]1716@@ -481,7 +482,7 @@ let simpl_statement env s =
[160]1717         let (s', _) = simpl_expr s.sloc env e (Set tmp) in
1718         let s_init =
1719           {sdesc = Sdo {edesc = EBinop(Oassign, tmp, intconst 1L IInt, tmp.etyp);
1720-                        etyp = tmp.etyp};
1721+                        etyp = tmp.etyp; espace = tmp.espace};
1722            sloc = s.sloc} in
1723         {sdesc = Sfor(s_init, tmp, s', simpl_stmt s1); sloc = s.sloc}
1724       end
[292]1725diff --git a/cparser/StructAssign.ml b/cparser/StructAssign.ml
1726index f5cecfc..5af7bed 100644
1727--- a/cparser/StructAssign.ml
1728+++ b/cparser/StructAssign.ml
1729@@ -28,9 +28,9 @@ let maxsize = ref 8
[160]1730 let need_memcpy = ref (None: ident option)
1731 
1732 let memcpy_type =
1733-  TFun(TPtr(TVoid [], []),
1734-       Some [(Env.fresh_ident "", TPtr(TVoid [], []));
1735-             (Env.fresh_ident "", TPtr(TVoid [AConst], []));
1736+  TFun(TPtr(Any,TVoid [], []),
1737+       Some [(Env.fresh_ident "", TPtr(Any,TVoid [], []));
1738+             (Env.fresh_ident "", TPtr(Any,TVoid [AConst], []));
1739              (Env.fresh_ident "", TInt(size_t_ikind, []))],
1740        false, [])
1741 
[292]1742@@ -43,6 +43,11 @@ let memcpy_ident () =
[160]1743   | Some id ->
1744       id
1745 
1746+let space_of_ty = function
1747+| TArray(space, _, _, _)
1748+| TPtr(space, _, _) -> space
1749+| _ -> Any
1750+
1751 let transf_assign env loc lhs rhs =
1752 
1753   let num_assign = ref 0 in
[292]1754@@ -62,9 +67,9 @@ let transf_assign env loc lhs rhs =
[160]1755         transf_struct l r ci.ci_members
1756     | TUnion(id, attr) ->
1757         raise Exit
1758-    | TArray(ty_elt, Some sz, attr) ->
1759-        transf_array l r ty_elt 0L sz
1760-    | TArray(ty_elt, None, attr) ->
1761+    | TArray(space, ty_elt, Some sz, attr) ->
1762+        transf_array space l (space_of_ty (unroll env r.etyp)) r ty_elt 0L sz
1763+    | TArray(space, ty_elt, None, attr) ->
1764         error "%a: Error: array of unknown size" formatloc loc;
1765         sskip                           (* will be ignored later *)
1766     | _ ->
[292]1767@@ -73,28 +78,29 @@ let transf_assign env loc lhs rhs =
[160]1768   and transf_struct l r = function
1769     | [] -> sskip
1770     | f :: fl ->
1771-        sseq loc (transf {edesc = EUnop(Odot f.fld_name, l); etyp = f.fld_typ}
1772-                         {edesc = EUnop(Odot f.fld_name, r); etyp = f.fld_typ})
1773+        sseq loc (transf {edesc = EUnop(Odot f.fld_name, l); etyp = f.fld_typ; espace = l.espace}
1774+                         {edesc = EUnop(Odot f.fld_name, r); etyp = f.fld_typ; espace = r.espace})
1775                  (transf_struct l r fl)
1776 
1777-  and transf_array l r ty idx sz =
1778+  and transf_array lsp l rsp r ty idx sz =
1779     if idx >= sz then sskip else begin
1780       let e = intconst idx size_t_ikind in
1781-      sseq loc (transf {edesc = EBinop(Oindex, l, e, ty); etyp = ty}
1782-                       {edesc = EBinop(Oindex, r, e, ty); etyp = ty})
1783-               (transf_array l r ty (Int64.add idx 1L) sz)
1784+      sseq loc (transf {edesc = EBinop(Oindex, l, e, ty); etyp = ty; espace = lsp}
1785+                       {edesc = EBinop(Oindex, r, e, ty); etyp = ty; espace = rsp})
1786+               (transf_array lsp l rsp r ty (Int64.add idx 1L) sz)
1787     end
1788   in
1789 
1790   try
1791     transf lhs rhs
1792   with Exit ->
1793-    let memcpy = {edesc = EVar(memcpy_ident()); etyp = memcpy_type} in
1794-    let e_lhs = {edesc = EUnop(Oaddrof, lhs); etyp = TPtr(lhs.etyp, [])} in
1795-    let e_rhs = {edesc = EUnop(Oaddrof, rhs); etyp = TPtr(rhs.etyp, [])} in
1796-    let e_size = {edesc = ESizeof(lhs.etyp); etyp = TInt(size_t_ikind, [])} in
1797+    let memcpy = {edesc = EVar(memcpy_ident()); etyp = memcpy_type; espace = Any} in
1798+    (* XXX: casts required? *)
1799+    let e_lhs = {edesc = EUnop(Oaddrof, lhs); etyp = TPtr(Any, lhs.etyp, []); espace = Any} in
1800+    let e_rhs = {edesc = EUnop(Oaddrof, rhs); etyp = TPtr(Any, rhs.etyp, []); espace = Any} in
1801+    let e_size = {edesc = ESizeof(lhs.etyp); etyp = TInt(size_t_ikind, []); espace = Any} in
1802     {sdesc = Sdo {edesc = ECall(memcpy, [e_lhs; e_rhs; e_size]);
1803-                  etyp = TVoid[]};
1804+                  etyp = TVoid[]; espace = Any};
1805      sloc = loc}
1806 
1807 let rec transf_stmt env s =
[292]1808@@ -136,7 +142,7 @@ let program p =
[160]1809   match !need_memcpy with
1810   | None -> p'
1811   | Some id ->
1812-      {gdesc = Gdecl(Storage_extern, id, memcpy_type, None); gloc = no_loc}
1813+      {gdesc = Gdecl(Code, (Storage_extern, id, memcpy_type, None)); gloc = no_loc}
1814       :: p'
1815 
1816 (* Horrible hack *)
[292]1817diff --git a/cparser/StructByValue.ml b/cparser/StructByValue.ml
1818index de79737..60e088b 100644
1819--- a/cparser/StructByValue.ml
1820+++ b/cparser/StructByValue.ml
1821@@ -38,21 +38,21 @@ let rec transf_type env t =
[160]1822       let tres' = transf_type env tres in
1823       if is_composite_type env tres then begin
1824         let res = Env.fresh_ident "_res" in
1825-        TFun(TVoid [], Some((res, TPtr(tres', [])) :: args'), vararg, attr)
1826+        TFun(TVoid [], Some((res, TPtr(Any, tres', [])) :: args'), vararg, attr)
1827       end else
1828         TFun(tres', Some args', vararg, attr)
1829-  | TPtr(t1, attr) ->
1830+  | TPtr(sp, t1, attr) ->
1831       let t1' = transf_type env t1 in
1832-      if t1' = t1 then t else TPtr(transf_type env t1, attr)
1833-  | TArray(t1, sz, attr) ->
1834+      if t1' = t1 then t else TPtr(sp, transf_type env t1, attr)
1835+  | TArray(sp, t1, sz, attr) ->
1836       let t1' = transf_type env t1 in
1837-      if t1' = t1 then t else TArray(transf_type env t1, sz, attr)
1838+      if t1' = t1 then t else TArray(sp, transf_type env t1, sz, attr)
1839   | _ -> t
1840 
1841 and transf_funarg env (id, t) =
1842   let t = transf_type env t in
1843   if is_composite_type env t
1844-  then (id, TPtr(add_attributes_type [AConst] t, []))
1845+  then (id, TPtr(Any, add_attributes_type [AConst] t, []))
1846   else (id, t)
1847 
1848 (* Simple exprs: no change in structure, since calls cannot occur within,
[292]1849@@ -60,6 +60,7 @@ and transf_funarg env (id, t) =
[160]1850 
1851 let rec transf_expr env e =
1852   { etyp = transf_type env e.etyp;
1853+    espace = e.espace;
1854     edesc = match e.edesc with
1855       | EConst c -> EConst c
1856       | ESizeof ty -> ESizeof (transf_type env ty)
[292]1857@@ -104,7 +105,7 @@ and transf_expr e = transf_expr env e in
[160]1858 let transf_arg e =
1859   let e' = transf_expr e in
1860   if is_composite_type env e'.etyp
1861-  then {edesc = EUnop(Oaddrof, e'); etyp = TPtr(e'.etyp, [])}
1862+  then {edesc = EUnop(Oaddrof, e'); etyp = TPtr(Any, e'.etyp, []); espace = Any} (* XXX: this might require a cast? *)
1863   else e'
1864 in
1865 
[292]1866@@ -118,25 +119,25 @@ in
[160]1867 let rec transf_stmt s =
1868   match s.sdesc with
1869   | Sskip -> s
1870-  | Sdo {edesc = ECall(fn, args); etyp = ty} ->
1871+  | Sdo {edesc = ECall(fn, args); etyp = ty; espace = space} ->
1872       let fn = transf_expr fn in
1873       let args = List.map transf_arg args in
1874       if is_composite_type env ty then begin
1875         let tmp = new_temp ~name:"_res" ty in
1876-        let arg0 = {edesc = EUnop(Oaddrof, tmp); etyp = TPtr(ty, [])} in
1877-        {s with sdesc = Sdo {edesc = ECall(fn, arg0 :: args); etyp = TVoid []}}
1878+        let arg0 = {edesc = EUnop(Oaddrof, tmp); etyp = TPtr(Any, ty, []); espace = Any} in
1879+        {s with sdesc = Sdo {edesc = ECall(fn, arg0 :: args); etyp = TVoid []; espace = Any}}
1880       end else
1881-        {s with sdesc = Sdo {edesc = ECall(fn, args); etyp = ty}}
1882-  | Sdo {edesc = EBinop(Oassign, dst, {edesc = ECall(fn, args); etyp = ty}, _)} ->
1883+        {s with sdesc = Sdo {edesc = ECall(fn, args); etyp = ty; espace = space}}
1884+  | Sdo {edesc = EBinop(Oassign, dst, {edesc = ECall(fn, args); etyp = ty; espace = space}, _)} ->
1885       let dst = transf_expr dst in
1886       let fn = transf_expr fn in
1887       let args = List.map transf_arg args in
1888       let ty = transf_type ty in
1889       if is_composite_type env ty then begin
1890-        let arg0 = {edesc = EUnop(Oaddrof, dst); etyp = TPtr(dst.etyp, [])} in
1891-        {s with sdesc = Sdo {edesc = ECall(fn, arg0 :: args); etyp = TVoid []}}
1892+        let arg0 = {edesc = EUnop(Oaddrof, dst); etyp = TPtr(Any, dst.etyp, []); espace = Any} in
1893+        {s with sdesc = Sdo {edesc = ECall(fn, arg0 :: args); etyp = TVoid []; espace = Any}}
1894       end else
1895-        sassign s.sloc dst {edesc = ECall(fn, args); etyp = ty}
1896+        sassign s.sloc dst {edesc = ECall(fn, args); etyp = ty; espace = space}
1897   | Sdo e ->
1898       {s with sdesc = Sdo(transf_expr e)}
1899   | Sseq(s1, s2) ->
[292]1900@@ -184,14 +185,15 @@ let transf_params loc env params =
[160]1901       let ty = transf_type env ty in
1902       if is_composite_type env ty then begin
1903         let id' = Env.fresh_ident id.name in
1904-        let ty' = TPtr(add_attributes_type [AConst] ty, []) in
1905+        let ty' = TPtr(Any, add_attributes_type [AConst] ty, []) in
1906         let (params', decls, init) = transf_prm params in
1907         ((id', ty') :: params',
1908          (Storage_default, id, ty, None) :: decls,
1909          sseq loc
1910-          (sassign loc {edesc = EVar id; etyp = ty}
1911-                       {edesc = EUnop(Oderef, {edesc = EVar id'; etyp = ty'});
1912-                        etyp = ty})
1913+          (sassign loc {edesc = EVar id; etyp = ty; espace = Any}
1914+                       {edesc = EUnop(Oderef, {edesc = EVar id'; etyp = ty'; espace = Any});
1915+                        etyp = ty;
1916+                        espace = Any})
1917           init)
1918       end else begin
1919         let (params', decls, init) = transf_prm params in
[292]1920@@ -206,9 +208,9 @@ let transf_fundef env f =
[160]1921   let (ret1, params1, body1) =
1922     if is_composite_type env ret then begin
1923       let vres = Env.fresh_ident "_res" in
1924-      let tres = TPtr(ret, []) in
1925-      let eres = {edesc = EVar vres; etyp = tres} in
1926-      let eeres = {edesc = EUnop(Oderef, eres); etyp = ret} in
1927+      let tres = TPtr(Any, ret, []) in
1928+      let eres = {edesc = EVar vres; etyp = tres; espace = Any} in
1929+      let eeres = {edesc = EUnop(Oderef, eres); etyp = ret; espace = Any} in
1930       (TVoid [],
1931        (vres, tres) :: params,
1932        transf_funbody env f.fd_body (Some eeres))
[292]1933diff --git a/cparser/Transform.ml b/cparser/Transform.ml
1934index b7f57f3..1a9dd20 100644
1935--- a/cparser/Transform.ml
1936+++ b/cparser/Transform.ml
1937@@ -33,7 +33,7 @@ let new_temp_var ?(name = "t") ty =
[160]1938 
1939 let new_temp ?(name = "t") ty =
1940   let id = new_temp_var ~name ty in
1941-  { edesc = EVar id; etyp = ty }
1942+  { edesc = EVar id; etyp = ty; espace = Any (* Always stack allocated? *) }
1943 
1944 let get_temps () =
1945   let temps = !temporaries in
[292]1946@@ -58,11 +58,11 @@ let program
[160]1947   | g :: gl ->
1948       let (desc', env') =
1949         match g.gdesc with
1950-        | Gdecl((sto, id, ty, init) as d) ->
1951-           (Gdecl(decl env d), Env.add_ident env id sto ty)
1952+        | Gdecl (sp, ((sto, id, ty, init) as d)) ->
1953+           (Gdecl(sp, decl env d), Env.add_ident env id sto ty sp)
1954         | Gfundef f ->
1955            (Gfundef(fundef env f),
1956-            Env.add_ident env f.fd_name f.fd_storage (fundef_typ f))
1957+            Env.add_ident env f.fd_name f.fd_storage (fundef_typ f) Code)
1958         | Gcompositedecl(su, id) ->
1959             (Gcompositedecl(su, id),
1960              Env.add_composite env id (composite_info_decl env su))
[292]1961diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml
1962index fa304b7..d19940a 100644
1963--- a/cparser/Unblock.ml
1964+++ b/cparser/Unblock.ml
1965@@ -32,32 +32,33 @@ let rec local_initializer loc env path init k =
[160]1966   match init with
1967   | Init_single e ->
1968       sdoseq loc
1969-        { edesc = EBinop(Oassign, path, e, path.etyp); etyp = path.etyp }
1970+        { edesc = EBinop(Oassign, path, e, path.etyp); etyp = path.etyp; espace = path.espace }
1971         k
1972   | Init_array il ->
1973-      let ty_elt =
1974+      let space, ty_elt =
1975         match unroll env path.etyp with
1976-        | TArray(ty_elt, _, _) -> ty_elt
1977+        | TArray(space, ty_elt, _, _) -> space, ty_elt
1978         | _ -> fatal_error "%aWrong type for array initializer"
1979                            formatloc loc in
1980       let rec array_init pos = function
1981         | [] -> k
1982         | i :: il ->
1983             local_initializer loc env
1984-              { edesc = EBinop(Oindex, path, intconst pos IInt, TPtr(ty_elt, []));
1985-                etyp = ty_elt }
1986+              { edesc = EBinop(Oindex, path, intconst pos IInt, TPtr(space, ty_elt, []));
1987+                etyp = ty_elt;
1988+                espace = Any }
1989               i
1990               (array_init (Int64.succ pos) il) in
1991       array_init 0L il
1992   | Init_struct(id, fil) ->
1993       let field_init (fld, i) k =
1994         local_initializer loc env
1995-          { edesc = EUnop(Odot fld.fld_name, path); etyp = fld.fld_typ }
1996+          { edesc = EUnop(Odot fld.fld_name, path); etyp = fld.fld_typ; espace = Any }
1997           i k in
1998       List.fold_right field_init fil k
1999   | Init_union(id, fld, i) ->
2000       local_initializer loc env
2001-        { edesc = EUnop(Odot fld.fld_name, path); etyp = fld.fld_typ }
2002+        { edesc = EUnop(Odot fld.fld_name, path); etyp = fld.fld_typ; espace = Any }
2003         i k
2004 
2005 (* Record new variables to be locally defined *)
[292]2006@@ -82,7 +83,7 @@ let process_decl loc env (sto, id, ty, optinit) k =
[160]2007   match optinit with
2008   | None -> k
2009   | Some init ->
2010-      local_initializer loc env { edesc = EVar id; etyp = ty' } init k
2011+      local_initializer loc env { edesc = EVar id; etyp = ty'; espace = Any } init k
2012 
2013 (* Simplification of blocks within a statement *)
2014 
[292]2015diff --git a/src/acc.ml b/src/acc.ml
2016index c8f6592..e2f782c 100644
2017--- a/src/acc.ml
2018+++ b/src/acc.ml
2019@@ -33,11 +33,15 @@ let process filename =
[160]2020       src_language tgt_language input_ast
2021   in
2022   let final_ast, intermediate_asts = Misc.ListExt.cut_last target_asts in
2023-  let annotated_input_ast =  Languages.annotate input_ast final_ast in
2024-  Languages.save filename annotated_input_ast;
2025+  if Options.annotation_requested () then begin
2026+    let annotated_input_ast =  Languages.annotate input_ast final_ast in
2027+    Languages.save filename annotated_input_ast
2028+  end;
2029   Languages.save filename final_ast;
2030   if Options.is_debug_enabled () then
2031     List.iter (Languages.save filename) intermediate_asts;
2032+  if Options.is_matita_output_enabled () then
2033+    Languages.save_matita filename (input_ast :: target_asts);
2034   if Options.interpretation_requested () || Options.is_debug_enabled () then begin
2035     let asts = input_ast :: target_asts in
2036     let label_traces = List.map Languages.interpret asts in
[292]2037diff --git a/src/clight/clight.mli b/src/clight/clight.mli
2038index 4c9d638..b831ef0 100644
2039--- a/src/clight/clight.mli
2040+++ b/src/clight/clight.mli
2041@@ -7,6 +7,8 @@ open AST
2042 
2043 (** ** Types *)
2044 
2045+type memory_space = Any | Data | IData | PData | XData | Code
2046+
2047 (** Clight types are similar to those of C.  They include numeric types,
2048   pointers, arrays, function types, and composite types (struct and
2049   union).  Numeric types (integers and floats) fully specify the
2050@@ -61,8 +63,8 @@ type ctype =
2051   | Tvoid                                      (**r the [void] type *)
2052   | Tint of intsize*signedness                 (**r integer types *)
2053   | Tfloat of floatsize                                (**r floating-point types *)
2054-  | Tpointer of ctype                          (**r pointer types ([*ty]) *)
2055-  | Tarray of ctype*int                                (**r array types ([ty[len]]) *)
2056+  | Tpointer of memory_space * ctype           (**r pointer types ([*ty]) *)
2057+  | Tarray of memory_space * ctype*int         (**r array types ([ty[len]]) *)
2058   | Tfunction of ctype list*ctype              (**r function types *)
2059   | Tstruct of ident*(ident*ctype) list
2060   (**r struct types *)
2061@@ -199,5 +201,5 @@ type init_data =
2062 type program = {
2063   prog_funct: (ident * fundef) list ;
2064   prog_main: ident;
2065-  prog_vars: ((ident * init_data list) * ctype) list
2066+  prog_vars: (((ident * init_data list) * memory_space) * ctype) list
2067 }
2068diff --git a/src/clight/clightFromC.ml b/src/clight/clightFromC.ml
2069index 0aacbce..0a4b947 100644
2070--- a/src/clight/clightFromC.ml
2071+++ b/src/clight/clightFromC.ml
2072@@ -19,7 +19,7 @@ let rec alignof = function
[160]2073   | Tfloat F32 -> 4
2074   | Tfloat F64 -> 8
2075   | Tpointer _ -> 4
2076-  | Tarray (t',n) -> alignof t'
2077+  | Tarray (_,t',n) -> alignof t'
2078   | Tfunction (_,_) -> 1
2079   | Tstruct (_,fld) -> alignof_fields fld
2080   | Tunion (_,fld) -> alignof_fields fld
[292]2081@@ -42,7 +42,7 @@ let rec sizeof t =
[160]2082     | Tfloat F32 -> 4
2083     | Tfloat F64 -> 8
2084     | Tpointer _ -> 4
2085-    | Tarray (t',n) -> sizeof t' * max 1 n
2086+    | Tarray (_,t',n) -> sizeof t' * max 1 n
2087     | Tfunction (_,_) -> 1
2088     | Tstruct (_,fld) -> align (max 1 (sizeof_struct fld 0)) (alignof t)
2089     | Tunion (_,fld) -> align (max 1 (sizeof_union fld)) (alignof t)
[292]2090@@ -102,14 +102,14 @@ let name_for_string_literal env s =
[160]2091     Hashtbl.add decl_atom id
2092       (env, (C.Storage_static,
2093              Env.fresh_ident name,
2094-             C.TPtr(C.TInt(C.IChar,[C.AConst]),[]),
2095+             C.TPtr(C.Any,C.TInt(C.IChar,[C.AConst]),[]),
2096              None));
2097     !define_stringlit_hook id;
2098     Hashtbl.add stringTable s id;
2099     id
2100 
2101 let typeStringLiteral s =
2102-  Tarray(Tint(I8, Unsigned), String.length s + 1)
2103+  Tarray(Code, Tint(I8, Unsigned), String.length s + 1)
2104 
2105 let global_for_string s id =
2106   let init = ref [] in
[292]2107@@ -119,7 +119,7 @@ let global_for_string s id =
[160]2108        :: !init in
2109   add_char '\000';
2110   for i = String.length s - 1 downto 0 do add_char s.[i] done;
2111-  ((id, !init), typeStringLiteral s)
2112+  (((id, !init), Code), typeStringLiteral s)
2113 
2114 let globals_for_strings globs =
2115   Hashtbl.fold
[292]2116@@ -143,7 +143,7 @@ let register_stub_function name tres targs =
[160]2117     let rec types_of_types = function
2118       | [] -> []
2119       | Tfloat(_)::tl -> Tfloat(F64)::(types_of_types tl)
2120-      | _::tl -> Tpointer(Tvoid)::(types_of_types tl) in
2121+      | _::tl -> Tpointer(Any,Tvoid)::(types_of_types tl) in
2122     let stub_type = Tfunction (types_of_types targs, tres) in
2123     Hashtbl.add stub_function_table stub_name stub_type;
2124     (stub_name, stub_type)
[292]2125@@ -193,6 +193,14 @@ let convertFkind = function
[160]2126       if not !ClightFlags.option_flonglong then unsupported "'long double' type";
2127       F64
2128 
2129+let convertSpace = function
2130+  | C.Any -> Any
2131+  | C.Data -> Data
2132+  | C.IData -> IData
2133+  | C.PData -> PData
2134+  | C.XData -> XData
2135+  | C.Code -> Code
2136+
2137 let convertTyp env t =
2138 
2139   let rec convertTyp seen t =
[292]2140@@ -202,19 +210,19 @@ let convertTyp env t =
[160]2141         let (sg, sz) = convertIkind ik in Tint(sz, sg)
2142     | C.TFloat(fk, a) ->
2143         Tfloat(convertFkind fk)
2144-    | C.TPtr(C.TStruct(id, _), _) when List.mem id seen ->
2145+    | C.TPtr(_,C.TStruct(id, _), _) when List.mem id seen ->
2146         Tcomp_ptr("struct " ^ id.name)
2147-    | C.TPtr(C.TUnion(id, _), _) when List.mem id seen ->
2148+    | C.TPtr(_,C.TUnion(id, _), _) when List.mem id seen ->
2149         Tcomp_ptr("union " ^ id.name)
2150-    | C.TPtr(ty, a) ->
2151-        Tpointer(convertTyp seen ty)
2152-    | C.TArray(ty, None, a) ->
2153+    | C.TPtr(sp,ty, a) ->
2154+        Tpointer(convertSpace sp, convertTyp seen ty)
2155+    | C.TArray(sp, ty, None, a) ->
2156         (* Cparser verified that the type ty[] occurs only in
2157            contexts that are safe for Clight, so just treat as ty[0]. *)
2158         (* warning "array type of unspecified size"; *)
2159-        Tarray(convertTyp seen ty, 0)
2160-    | C.TArray(ty, Some sz, a) ->
2161-        Tarray(convertTyp seen ty, convertInt sz )
2162+        Tarray(convertSpace sp, convertTyp seen ty, 0)
2163+    | C.TArray(sp, ty, Some sz, a) ->
2164+        Tarray(convertSpace sp, convertTyp seen ty, convertInt sz )
2165     | C.TFun(tres, targs, va, a) ->
2166         if va then unsupported "variadic function type";
2167         if Cutil.is_composite_type env tres then
[292]2168@@ -298,7 +306,7 @@ let rec convertExpr env e =
[160]2169       let e1' = convertExpr env e1 in
2170       let ty1 =
2171         match typeof e1' with
2172-        | Tpointer t -> t
2173+        | Tpointer (_,t) -> t
2174         | _ -> error ("wrong type for ->" ^ id ^ " access"); Tvoid in
2175       Expr(Efield(Expr(Ederef(convertExpr env e1), ty1),
2176                    id), ty)
[292]2177@@ -315,7 +323,7 @@ let rec convertExpr env e =
[160]2178 
2179   | C.EBinop(C.Oindex, e1, e2, _) ->
2180       Expr(Ederef(Expr(Ebinop(Oadd, convertExpr env e1, convertExpr env e2),
2181-                       Tpointer ty)), ty)
2182+                       convertTyp env e1.etyp)), ty)
2183   | C.EBinop(C.Ologand, e1, e2, _) ->
2184       Expr(Eandbool(convertExpr env e1, convertExpr env e2), ty)
2185   | C.EBinop(C.Ologor, e1, e2, _) ->
[292]2186@@ -354,7 +362,7 @@ let rec convertExpr env e =
[160]2187 let rec projFunType env ty =
2188   match Cutil.unroll env ty with
2189   | TFun(res, args, vararg, attr) -> Some(res, vararg)
2190-  | TPtr(ty', attr) -> projFunType env ty'
2191+  | TPtr(_, ty', attr) -> projFunType env ty'
2192   | _ -> None
2193 
2194 let convertFuncall env lhs fn args =
[292]2195@@ -400,19 +408,19 @@ let volatile_fun_suffix_type ty =
[160]2196   | Tfloat F32 -> ("float32", ty)
2197   | Tfloat F64 -> ("float64", ty)
2198   | Tpointer _ | Tarray _ | Tfunction _ | Tcomp_ptr _ ->
2199-      ("pointer", Tpointer Tvoid)
2200+      ("pointer", Tpointer (Any, Tvoid)) (* XXX: what is the pointer is to a different space? *)
2201   | _ ->
2202       unsupported "operation on volatile struct or union"; ("", Tvoid)
2203 
2204 let volatile_read_fun ty =
2205   let (suffix, ty') = volatile_fun_suffix_type ty in
2206   Expr(Evar( ("__builtin_volatile_read_" ^ suffix)),
2207-       Tfunction((Tpointer Tvoid)::[], ty'))
2208+       Tfunction((Tpointer (Any,Tvoid))::[], ty'))
2209 
2210 let volatile_write_fun ty =
2211   let (suffix, ty') = volatile_fun_suffix_type ty in
2212   Expr(Evar( ("__builtin_volatile_write_" ^ suffix)),
2213-       Tfunction((Tpointer Tvoid)::(ty'::[]), Tvoid))
2214+       Tfunction((Tpointer (Any,Tvoid))::(ty'::[]), Tvoid))
2215 
2216 (* Toplevel expression, argument of an Sdo *)
2217 
[292]2218@@ -432,11 +440,11 @@ let convertTopExpr env e =
[160]2219       | false, true ->                  (* volatile read *)
2220           Scall(Some lhs',
2221                 volatile_read_fun (typeof rhs'),
2222-                [ Expr (Eaddrof rhs', Tpointer (typeof rhs')) ])
2223+                [ Expr (Eaddrof rhs', Tpointer (Any (* XXX ? *), typeof rhs')) ])
2224       | true, false ->                  (* volatile write *)
2225           Scall(None,
2226                 volatile_write_fun (typeof lhs'),
2227-                [ Expr(Eaddrof lhs', Tpointer (typeof lhs')); rhs' ])
2228+                [ Expr(Eaddrof lhs', Tpointer (Any (* XXX ? *), typeof lhs')); rhs' ])
2229       | false, false ->                 (* regular assignment *)
2230           Sassign(convertExpr env lhs, convertExpr env rhs)
2231       end
[292]2232@@ -663,7 +671,7 @@ let convertInit env ty init =
[160]2233   | Init_array il ->
2234       let ty_elt =
2235         match Cutil.unroll env ty with
2236-        | C.TArray(t, _, _) -> t
2237+        | C.TArray(_, t, _, _) -> t
2238         | _ -> error "array type expected in initializer"; C.TVoid [] in
2239       List.iter (cvtInit ty_elt) il
2240   | Init_struct(_, flds) ->
[292]2241@@ -690,7 +698,7 @@ let convertInit env ty init =
[160]2242 
2243 (** Global variable *)
2244 
2245-let convertGlobvar env (sto, id, ty, optinit as decl) =
2246+let convertGlobvar env space (sto, id, ty, optinit as decl) =
2247   let id' =  id.name in
2248   let ty' = convertTyp env ty in
2249   let init' =
[292]2250@@ -701,7 +709,7 @@ let convertGlobvar env (sto, id, ty, optinit as decl) =
[160]2251         convertInit env ty i in
2252   Hashtbl.add decl_atom id' (env, decl);
2253   !define_variable_hook id' decl;
2254-  ((id', init'), ty')
2255+  (((id', init'), convertSpace space), ty')
2256 
2257 (** Convert a list of global declarations.
2258   Result is a pair [(funs, vars)] where [funs] are
[292]2259@@ -714,7 +722,7 @@ let rec convertGlobdecls env funs vars gl =
[160]2260   | g :: gl' ->
2261       updateLoc g.gloc;
2262       match g.gdesc with
2263-      | C.Gdecl((sto, id, ty, optinit) as d) ->
2264+      | C.Gdecl(space, ((sto, id, ty, optinit) as d)) ->
2265           (* Prototyped functions become external declarations.
2266              Variadic functions are skipped.
2267              Other types become variable declarations. *)
[292]2268@@ -727,7 +735,7 @@ let rec convertGlobdecls env funs vars gl =
[160]2269           | TFun(_, _, true, _) ->
2270               convertGlobdecls env funs vars gl'
2271           | _ ->
2272-              convertGlobdecls env funs (convertGlobvar env d :: vars) gl'
2273+              convertGlobdecls env funs (convertGlobvar env space d :: vars) gl'
2274           end
2275       | C.Gfundef fd ->
2276           convertGlobdecls env (convertFundef env fd :: funs) vars gl'
[292]2277@@ -769,11 +777,11 @@ let cleanupGlobals p =
[160]2278     | g :: gl ->
2279         updateLoc g.gloc;
2280         match g.gdesc with
2281-        | C.Gdecl(sto, id, ty, None) ->
2282+        | C.Gdecl(_, (sto, id, ty, None)) ->
2283             if IdentSet.mem id defs
2284             then clean defs accu gl
2285             else clean (IdentSet.add id defs) (g :: accu) gl
2286-        | C.Gdecl(_, id, ty, _) ->
2287+        | C.Gdecl(_, (_, id, ty, _)) ->
2288             if IdentSet.mem id defs then
2289               error ("multiple definitions of " ^ id.name);
2290             clean (IdentSet.add id defs) (g :: accu) gl
[292]2291@@ -815,7 +823,7 @@ let rec type_is_readonly env t =
[160]2292   if List.mem C.AVolatile a then false else
2293   if List.mem C.AConst a then true else
2294   match Cutil.unroll env t with
2295-  | C.TArray(t', _, _) -> type_is_readonly env t'
2296+  | C.TArray(_, t', _, _) -> type_is_readonly env t'
2297   | _ -> false
2298 
2299 let atom_is_static a =
[292]2300@@ -853,42 +861,42 @@ open Builtins
[160]2301 let builtins_generic = {
2302   typedefs = [
2303     (* keeps GCC-specific headers happy, harmless for others *)
2304-    "__builtin_va_list", C.TPtr(C.TVoid [], [])
2305+    "__builtin_va_list", C.TPtr(C.Any, C.TVoid [], [])
2306   ];
2307   functions = [
2308     (* The volatile read/volatile write functions *)
2309     "__builtin_volatile_read_int8unsigned",
2310-        (TInt(IUChar, []), [TPtr(TVoid [], [])], false);
2311+        (TInt(IUChar, []), [TPtr(C.Any, TVoid [], [])], false);
2312     "__builtin_volatile_read_int8signed",
2313-        (TInt(ISChar, []), [TPtr(TVoid [], [])], false);
2314+        (TInt(ISChar, []), [TPtr(C.Any, TVoid [], [])], false);
2315     "__builtin_volatile_read_int16unsigned",
2316-        (TInt(IUShort, []), [TPtr(TVoid [], [])], false);
2317+        (TInt(IUShort, []), [TPtr(C.Any, TVoid [], [])], false);
2318     "__builtin_volatile_read_int16signed",
2319-        (TInt(IShort, []), [TPtr(TVoid [], [])], false);
2320+        (TInt(IShort, []), [TPtr(C.Any, TVoid [], [])], false);
2321     "__builtin_volatile_read_int32",
2322-        (TInt(IInt, []), [TPtr(TVoid [], [])], false);
2323+        (TInt(IInt, []), [TPtr(C.Any, TVoid [], [])], false);
2324     "__builtin_volatile_read_float32",
2325-        (TFloat(FFloat, []), [TPtr(TVoid [], [])], false);
2326+        (TFloat(FFloat, []), [TPtr(C.Any, TVoid [], [])], false);
2327     "__builtin_volatile_read_float64",
2328-         (TFloat(FDouble, []), [TPtr(TVoid [], [])], false);
2329+         (TFloat(FDouble, []), [TPtr(C.Any, TVoid [], [])], false);
2330     "__builtin_volatile_read_pointer",
2331-         (TPtr(TVoid [], []), [TPtr(TVoid [], [])], false);
2332+         (TPtr(C.Any, TVoid [], []), [TPtr(C.Any, TVoid [], [])], false);
2333     "__builtin_volatile_write_int8unsigned",
2334-        (TVoid [], [TPtr(TVoid [], []); TInt(IUChar, [])], false);
2335+        (TVoid [], [TPtr(C.Any, TVoid [], []); TInt(IUChar, [])], false);
2336     "__builtin_volatile_write_int8signed",
2337-        (TVoid [], [TPtr(TVoid [], []); TInt(ISChar, [])], false);
2338+        (TVoid [], [TPtr(C.Any, TVoid [], []); TInt(ISChar, [])], false);
2339     "__builtin_volatile_write_int16unsigned",
2340-        (TVoid [], [TPtr(TVoid [], []); TInt(IUShort, [])], false);
2341+        (TVoid [], [TPtr(C.Any, TVoid [], []); TInt(IUShort, [])], false);
2342     "__builtin_volatile_write_int16signed",
2343-        (TVoid [], [TPtr(TVoid [], []); TInt(IShort, [])], false);
2344+        (TVoid [], [TPtr(C.Any, TVoid [], []); TInt(IShort, [])], false);
2345     "__builtin_volatile_write_int32",
2346-        (TVoid [], [TPtr(TVoid [], []); TInt(IInt, [])], false);
2347+        (TVoid [], [TPtr(C.Any, TVoid [], []); TInt(IInt, [])], false);
2348     "__builtin_volatile_write_float32",
2349-        (TVoid [], [TPtr(TVoid [], []); TFloat(FFloat, [])], false);
2350+        (TVoid [], [TPtr(C.Any, TVoid [], []); TFloat(FFloat, [])], false);
2351     "__builtin_volatile_write_float64",
2352-         (TVoid [], [TPtr(TVoid [], []); TFloat(FDouble, [])], false);
2353+         (TVoid [], [TPtr(C.Any, TVoid [], []); TFloat(FDouble, [])], false);
2354     "__builtin_volatile_write_pointer",
2355-         (TVoid [], [TPtr(TVoid [], []); TPtr(TVoid [], [])], false)
2356+         (TVoid [], [TPtr(C.Any, TVoid [], []); TPtr(C.Any, TVoid [], [])], false)
2357   ]
2358 }
2359 
[292]2360diff --git a/src/clight/clightInterpret.ml b/src/clight/clightInterpret.ml
2361index 32b9884..b744932 100644
2362--- a/src/clight/clightInterpret.ml
2363+++ b/src/clight/clightInterpret.ml
2364@@ -29,7 +29,7 @@ let rec sizeof = function
[160]2365   | Tfloat F32 -> 4
2366   | Tfloat F64 -> 8
2367   | Tpointer _ -> 4                   
2368-  | Tarray (_,_) -> 4                   
2369+  | Tarray _ -> 4                       
2370   | Tfunction (_,_) -> assert false
2371   | Tstruct (_,_) -> assert false
2372   | Tunion (_,_) -> assert false
[292]2373@@ -46,7 +46,7 @@ let rec mq_of_ty = function
[160]2374   | Tfloat F32 -> assert false
2375   | Tfloat F64 -> Memory.MQ_float64
2376   | Tpointer _ -> Memory.MQ_int32                     
2377-  | Tarray (c,s) -> Memory.MQ_int32
2378+  | Tarray (_,c,s) -> Memory.MQ_int32
2379   | Tfunction (_,_) -> assert false
2380   | Tstruct (_,_) -> assert false
2381   | Tunion (_,_) -> assert false
[292]2382@@ -207,7 +207,7 @@ let eval_cast = function
[160]2383   | (Value.Val_float f,_,Tfloat F64) -> Value.Val_float f
2384   (* Cast pointeur *)
2385   | (Value.Val_ptr (b,o),_,Tpointer _) -> Value.Val_ptr (b,o)
2386-  | (Value.Val_ptr (b,o),_,Tarray(_,_)) -> Value.Val_ptr (b,o)
2387+  | (Value.Val_ptr (b,o),_,Tarray _) -> Value.Val_ptr (b,o)
2388   (* no cast *)
2389   | (e,a,b) when a=b -> e
2390   (* error *)
[292]2391@@ -232,13 +232,13 @@ let eval_add = function
[160]2392       Value.Val_int (cast_int (i1+i2) t1)     
2393   | ((Value.Val_float i1,Tfloat F64) , (Value.Val_float i2,Tfloat F64)) ->
2394       Value.Val_float (i1+.i2)
2395-  | ((Value.Val_int i,_) , (Value.Val_ptr (b,o),Tarray(t,_))) ->
2396+  | ((Value.Val_int i,_) , (Value.Val_ptr (b,o),Tarray(_,t,_))) ->
2397       Value.Val_ptr (b,o+(i*(sizeof t)))
2398-  | ((Value.Val_ptr (b,o),Tarray(t,_)) , (Value.Val_int i,_)) ->
2399+  | ((Value.Val_ptr (b,o),Tarray(_,t,_)) , (Value.Val_int i,_)) ->
2400       Value.Val_ptr (b,o+(i*(sizeof t)))
2401-  | ((Value.Val_int i,_) , (Value.Val_ptr (b,o),Tpointer t)) ->
2402+  | ((Value.Val_int i,_) , (Value.Val_ptr (b,o),Tpointer (_,t))) ->
2403       Value.Val_ptr (b,o+(i*(sizeof t)))
2404-  | ((Value.Val_ptr (b,o),Tpointer t) , (Value.Val_int i,_)) ->
2405+  | ((Value.Val_ptr (b,o),Tpointer (_,t)) , (Value.Val_int i,_)) ->
2406       Value.Val_ptr (b,o+(i*(sizeof t)))
2407   | ((v1,_),(v2,_)) ->
2408       print_string ("Debug: add "^(Value.string_of_value v1)^" with "
[292]2409@@ -250,13 +250,13 @@ let eval_sub = function
[160]2410       Value.Val_int (cast_int (i1-i2) t1)   
2411   | ((Value.Val_float i1,Tfloat F64) , (Value.Val_float i2,Tfloat F64)) ->
2412       Value.Val_float (i1-.i2)
2413-  | ((Value.Val_int i,_) , (Value.Val_ptr (b,o),Tarray(t,_))) ->
2414+  | ((Value.Val_int i,_) , (Value.Val_ptr (b,o),Tarray(_,t,_))) ->
2415       Value.Val_ptr (b,o-(i*(sizeof t)))
2416-  | ((Value.Val_ptr (b,o),Tarray(t,_)) , (Value.Val_int i,_)) ->
2417+  | ((Value.Val_ptr (b,o),Tarray(_,t,_)) , (Value.Val_int i,_)) ->
2418       Value.Val_ptr (b,o-(i*(sizeof t)))
2419-  | ((Value.Val_int i,_) , (Value.Val_ptr (b,o),Tpointer t)) ->
2420+  | ((Value.Val_int i,_) , (Value.Val_ptr (b,o),Tpointer (_,t))) ->
2421       Value.Val_ptr (b,o-(i*(sizeof t)))
2422-  | ((Value.Val_ptr (b,o),Tpointer t) , (Value.Val_int i,_)) ->
2423+  | ((Value.Val_ptr (b,o),Tpointer (_,t)) , (Value.Val_int i,_)) ->
2424       Value.Val_ptr (b,o-(i*(sizeof t)))
2425   | _ -> assert false
2426 
[292]2427@@ -475,9 +475,9 @@ let bind_parameters m (param_l:(ident*ctype) list) (arg_l:Value.t list) (var_l:(
[160]2428     | _ -> assert false
2429   and treat_v (m,e) = function
2430     | [] -> (m,e)
2431-    | (id,Tarray(c,n))::l ->
2432+    | (id,Tarray(s,c,n))::l ->
2433         (match alloc m 0 (n*(sizeof c)) with
2434-           | Some(b,m') -> treat_v (bind m' e (id,Tarray(c,n)) (Value.Val_ptr(b,0)) ) l
2435+           | Some(b,m') -> treat_v (bind m' e (id,Tarray(s,c,n)) (Value.Val_ptr(b,0)) ) l
2436            | None -> assert false)
2437     | var::l -> treat_v (bind m e var Value.Val_undef) l
2438   in treat_v (treat_p (m,(Hashtbl.create 11)) (param_l,arg_l)) var_l
[292]2439diff --git a/src/clight/clightPrintMatita.ml b/src/clight/clightPrintMatita.ml
2440new file mode 100644
[416]2441index 0000000..948ef87
[292]2442--- /dev/null
2443+++ b/src/clight/clightPrintMatita.ml
2444@@ -0,0 +1,483 @@
[160]2445+(* *********************************************************************)
2446+(*                                                                     *)
2447+(*              The Compcert verified compiler                         *)
2448+(*                                                                     *)
2449+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
2450+(*                                                                     *)
2451+(*  Copyright Institut National de Recherche en Informatique et en     *)
2452+(*  Automatique.  All rights reserved.  This file is distributed       *)
2453+(*  under the terms of the GNU General Public License as published by  *)
2454+(*  the Free Software Foundation, either version 2 of the License, or  *)
2455+(*  (at your option) any later version.  This file is also distributed *)
2456+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
2457+(*                                                                     *)
2458+(* *********************************************************************)
2459+
2460+(** Pretty-printer for Csyntax *)
2461+
2462+open Format
2463+open AST
2464+open Clight
2465+
2466+(* If there's name hiding this might get us into trouble. *)
2467+let ident_map = Hashtbl.create 13;;
2468+let ident_next = ref 0;;
2469+let id_i n =
2470+  try Hashtbl.find ident_map n
2471+  with Not_found ->
2472+    let i = !ident_next in
2473+    Hashtbl.add ident_map n i;
2474+    ident_next := i+1;
2475+    i
2476+let id_s n = string_of_int (id_i n)
2477+
2478+let print_list f fmt l =
2479+  let rec aux fmt = function
2480+      | [] -> ()
2481+      | [x] -> f fmt x
2482+      | h::t -> f fmt h; fprintf fmt ";@ "; aux fmt t
2483+  in
2484+  fprintf fmt "@[[%a]@]" aux l
2485+
2486+let name_unop = function
2487+  | Onotbool -> "Onotbool"
2488+  | Onotint  -> "Onotint"
2489+  | Oneg     -> "Oneg"
2490+
2491+
2492+let name_binop = function
2493+  | Oadd -> "Oadd"
2494+  | Osub -> "Osub"
2495+  | Omul -> "Omul"
2496+  | Odiv -> "Odiv"
2497+  | Omod -> "Omod"
2498+  | Oand -> "Oand"
2499+  | Oor  -> "Oor"
2500+  | Oxor -> "Oxor"
2501+  | Oshl -> "Oshl"
2502+  | Oshr -> "Oshr"
2503+  | Oeq  -> "Oeq"
2504+  | One  -> "One"
2505+  | Olt  -> "Olt"
2506+  | Ogt  -> "Ogt"
2507+  | Ole  -> "Ole"
2508+  | Oge  -> "Oge"
2509+
2510+let name_inttype sz sg =
2511+  match sz, sg with
2512+  | I8, Signed    -> "I8 Signed   "
2513+  | I8, Unsigned  -> "I8 Unsigned "
2514+  | I16, Signed   -> "I16 Signed  "
2515+  | I16, Unsigned -> "I16 Unsigned"
2516+  | I32, Signed   -> "I32 Signed  "
2517+  | I32, Unsigned -> "I32 Unsigned"
2518+
2519+let name_floattype sz =
2520+  match sz with
2521+  | F32 -> "F32"
2522+  | F64 -> "F64"
2523+
2524+(* Collecting the names and fields of structs and unions *)
2525+
2526+module StructUnionSet = Set.Make(struct
2527+  type t = string * (ident*ctype) list
2528+  let compare (n1, _ : t) (n2, _ : t) = compare n1 n2
2529+end)
2530+
2531+let struct_unions = ref StructUnionSet.empty
2532+
2533+let register_struct_union id fld =
2534+  struct_unions := StructUnionSet.add (id, fld) !struct_unions
2535+
2536+(* Declarator (identifier + type) *)
2537+
2538+let name_optid id =
2539+  if id = "" then "" else " " ^ id
2540+
2541+let parenthesize_if_pointer id =
2542+  if String.length id > 0 && id.[0] = '*' then "(" ^ id ^ ")" else id
2543+
2544+let rec name_cdecl id ty =
2545+  match ty with
2546+  | Tvoid ->
2547+      "void" ^ name_optid id
2548+  | Tint(sz, sg) ->
2549+      name_inttype sz sg ^ name_optid id
2550+  | Tfloat sz ->
2551+      name_floattype sz ^ name_optid id
2552+  | Tpointer (s,t) -> (* XXX *)
2553+      name_cdecl ("*" ^ id) t
2554+  | Tarray(s, t, n) -> (* XXX *)
2555+      name_cdecl
2556+        (sprintf "%s[%d]" (parenthesize_if_pointer id) n)
2557+        t
2558+  | Tfunction(args, res) ->
2559+      let b = Buffer.create 20 in
2560+      if id = ""
2561+      then Buffer.add_string b "(*)"
2562+      else Buffer.add_string b (parenthesize_if_pointer id);
2563+      Buffer.add_char b '(';
2564+      begin match args with
2565+      | [] ->
2566+          Buffer.add_string b "void"
2567+      | _ ->
2568+          let rec add_args first = function
2569+          | [] -> ()
2570+          | t1::tl ->
2571+              if not first then Buffer.add_string b ", ";
2572+              Buffer.add_string b (name_cdecl "" t1);
2573+              add_args false tl in
2574+          add_args true args
2575+      end;
2576+      Buffer.add_char b ')';
2577+      name_cdecl (Buffer.contents b) res
2578+  | Tstruct(name, fld) ->
2579+      name ^ name_optid id
2580+  | Tunion(name, fld) ->
2581+      name ^ name_optid id
2582+  | Tcomp_ptr name ->
2583+      name ^ " *" ^ id
2584+
2585+(* Type *)
2586+
2587+let sspace = function
2588+| Any -> "Any"
2589+| Data -> "Data"
2590+| IData -> "IData"
2591+| PData -> "PData"
2592+| XData -> "XData"
2593+| Code -> "Code"
2594+
2595+let rec stype ty =
2596+  match ty with
2597+  | Tvoid -> "Tvoid"
2598+  | Tint(sz, sg) -> "(Tint " ^ name_inttype sz sg ^ ")"
2599+  | Tfloat sz -> "(Tfloat " ^ name_floattype sz ^ ")"
2600+  | Tpointer (sp, t) -> "(Tpointer " ^ sspace sp ^ " " ^ stype t ^ ")"
2601+  | Tarray(sp, t, n) -> "(Tarray " ^ sspace sp ^ " " ^ stype t ^ " " ^ (string_of_int n) ^ ")"
2602+  | Tfunction(args, res) -> "(Tfunction " ^ typelist args ^ " " ^ stype res ^ ")"
2603+  | Tstruct(name, fld) ->
2604+      fieldlist "(Tstruct (succ_pos_of_nat " name fld
2605+  | Tunion(name, fld) ->
2606+      fieldlist "(Tunion (succ_pos_of_nat " name fld
2607+  | Tcomp_ptr name ->
2608+      "(Tcomp_ptr (succ_pos_of_nat " ^ id_s name ^ "))"
2609+ and typelist l =
2610+    let b = Buffer.create 20 in
2611+      let rec add_types = function
2612+        | [] -> Buffer.add_string b "Tnil"
2613+        | t1::tl ->
2614+            Buffer.add_string b "(Tcons ";
2615+            Buffer.add_string b (stype t1);
2616+            Buffer.add_char b ' ';
2617+            add_types tl;
2618+            Buffer.add_char b ')'
2619+      in add_types l;
2620+        Buffer.contents b
2621+ and fieldlist s name l =
2622+    let b = Buffer.create 20 in
2623+      Buffer.add_string b s;
2624+      Buffer.add_string b (id_s name);
2625+      Buffer.add_string b ") ";
2626+      let rec add_fields = function
2627+        | [] -> Buffer.add_string b "Fnil"
2628+        | (id, ty)::tl ->
2629+            Buffer.add_string b "(Fcons (succ_pos_of_nat ";
2630+            Buffer.add_string b (id_s id);
2631+            Buffer.add_string b ") ";
2632+            Buffer.add_string b (stype ty);
2633+            Buffer.add_char b ' ';
2634+            add_fields tl;
2635+            Buffer.add_char b ')'
2636+      in add_fields l;
2637+        Buffer.add_char b ')';
2638+        Buffer.contents b
2639+
2640+let name_type ty = name_cdecl "" ty
2641+
2642+(* Expressions *)
2643+
2644+let rec print_expr p (Expr (eb, ty)) =
[292]2645+  fprintf p "@[<hov 2>(Expr %a@ %s)@]" print_expr_descr eb (stype ty)
2646+and print_expr_descr p eb =
[160]2647+  match eb with
[292]2648+  | Ecost (_, Expr (e, _)) -> print_expr_descr p e
[160]2649+  | Econst_int n ->
2650+      fprintf p "(Econst_int (repr %d))" n
2651+  | Econst_float f ->
2652+      fprintf p "(Econst_float %F)" f
2653+  | Evar id ->
2654+      fprintf p "(Evar (succ_pos_of_nat %d))" (id_i id)
2655+  | Eunop(op, e1) ->
2656+      fprintf p "(Eunop %s %a)" (name_unop op) print_expr e1
2657+  | Ederef e ->
2658+      fprintf p "(Ederef@ %a)" print_expr e
2659+  | Eaddrof e ->
2660+      fprintf p "(Eaddrof@ %a)" print_expr e
2661+  | Ebinop(op, e1, e2) ->
2662+      fprintf p "(Ebinop@ %s@ %a@ %a)"
2663+                (name_binop op)
2664+                print_expr e1
2665+                print_expr e2
2666+  | Ecast(ty, e1) ->
2667+      fprintf p "(Ecast %s@ %a)"
2668+                (stype ty)
2669+                print_expr e1
2670+  | Econdition(e1, e2, e3) ->
2671+      fprintf p "(Econdition %a@ %a@ %a)"
2672+                print_expr e1
2673+                print_expr e2
2674+                print_expr e3
2675+  | Eandbool(e1, e2) ->
2676+      fprintf p "(Eandbool %a@ %a)"
2677+                print_expr e1
2678+                print_expr e2
2679+  | Eorbool(e1, e2) ->
2680+      fprintf p "(Eorbool %a@ %a)"
2681+                print_expr e1
2682+                print_expr e2
2683+  | Esizeof ty ->
2684+      fprintf p "(Esizeof %s)" (stype ty)
2685+  | Efield(e1, id) ->
2686+      fprintf p "(Efield %a (succ_pos_of_nat %i))" print_expr e1 (id_i id)
2687+
2688+let rec print_expr_list p (first, el) =
2689+  match el with
2690+  | [] -> ()
2691+  | e1 :: et ->
2692+      if not first then fprintf p ",@ ";
2693+      print_expr p e1;
2694+      print_expr_list p (false, et)
2695+
2696+let rec print_stmt p s =
2697+  match s with
2698+  | Scost (_, s') -> print_stmt p s'
2699+  | Sskip ->
2700+      fprintf p "Sskip"
2701+  | Sassign(e1, e2) ->
2702+      fprintf p "@[<hv 2>(Sassign %a@ %a)@]" print_expr e1 print_expr e2
2703+  | Scall(None, e1, el) ->
2704+      fprintf p "@[<hv 2>(Scall (None ?) %a @[<hov 0>%a@])@]"
2705+                print_expr e1
2706+                (print_list print_expr) el
2707+  | Scall(Some lhs, e1, el) ->
2708+      fprintf p "@[<hv 2>(Scall (Some ? %a)@ %a@ @[<hov 0>%a@])@]"
2709+                print_expr lhs
2710+                print_expr e1
2711+                (print_list print_expr) el
2712+  | Ssequence(s1, s2) ->
2713+      fprintf p "(Ssequence@ %a@ %a)" print_stmt s1 print_stmt s2
2714+  | Sifthenelse(e, s1, s2) ->
2715+      fprintf p "@[<v 2>(Sifthenelse %a@ %a@ %a)@]"
2716+              print_expr e
2717+              print_stmt s1
2718+              print_stmt s2
2719+  | Swhile(e, s) ->
2720+      fprintf p "@[<v 2>(Swhile %a@ %a)@]"
2721+              print_expr e
2722+              print_stmt s
2723+  | Sdowhile(e, s) ->
2724+      fprintf p "@[<v 2>S(dowhile %a@ %a)@]"
2725+              print_expr e
2726+              print_stmt s
2727+  | Sfor(s_init, e, s_iter, s_body) ->
2728+      fprintf p "@[<v 2>(Sfor %a@ %a@ %a@\n%a@;<0 -2>)@]"
2729+              print_stmt s_init
2730+              print_expr e
2731+              print_stmt s_iter
2732+              print_stmt s_body
2733+  | Sbreak ->
2734+      fprintf p "Sbreak"
2735+  | Scontinue ->
2736+      fprintf p "Scontinue"
2737+  | Sswitch(e, cases) ->
2738+      fprintf p "@[<v 2>(Sswitch %a (@ %a@;<0 -2>))@]"
2739+              print_expr e
2740+              print_cases cases
2741+  | Sreturn None ->
2742+      fprintf p "(Sreturn (None ?))"
2743+  | Sreturn (Some e) ->
2744+      fprintf p "(Sreturn (Some ? %a))" print_expr e
2745+  | Slabel(lbl, s1) ->
2746+      fprintf p "(Slabel (succ_pos_of_nat %i)@ %a)" (id_i lbl) print_stmt s1
2747+  | Sgoto lbl ->
2748+      fprintf p "(Sgoto (succ_pos_of_nat %i))" (id_i lbl)
2749+
2750+and print_cases p cases =
2751+  match cases with
2752+  | LSdefault s ->
[416]2753+      fprintf p "@[<v 2>(LSdefault@ %a)@]" print_stmt s
[160]2754+  | LScase(lbl, s, rem) ->
[416]2755+      fprintf p "@[<v 2>(LScase (repr %d)@ %a@ %a)@]"
[160]2756+              lbl
2757+              print_stmt s
2758+              print_cases rem
2759+
2760+let name_function_parameters params =
2761+  let b = Buffer.create 20 in
2762+  Buffer.add_char b '[';
2763+    let rec add_params first = function
2764+      | [] -> ()
2765+      | (id, ty) :: rem ->
2766+          if not first then Buffer.add_string b "; ";
2767+          Buffer.add_string b "mk_pair ?? (succ_pos_of_nat ";
2768+          Buffer.add_string b (id_s id);
2769+          Buffer.add_string b ") ";
2770+          Buffer.add_string b (stype ty);
2771+          add_params false rem in
2772+      add_params true params;
2773+      Buffer.add_char b ']';
2774+      Buffer.contents b
2775+
2776+let print_function p f =
2777+  fprintf p "@[<v 2>mk_function %s %s %s@ " (stype f.fn_return)
2778+    (name_function_parameters f.fn_params)
2779+    (name_function_parameters f.fn_vars);
2780+  print_stmt p f.fn_body;
2781+  fprintf p "@;<0 -2>@]@ @ "
2782+
2783+let print_fundef p (id, fd) =
2784+  fprintf p "@[<v 2>mk_pair ?? (succ_pos_of_nat %i (* %s *)) " (id_i id) id;
2785+  match fd with
2786+  | External(id', args, res) ->
2787+      fprintf p "(External (succ_pos_of_nat %i) %s %s)@]" (id_i id) (typelist args) (stype res)
2788+  | Internal f ->
2789+      fprintf p "(Internal (@ %a@;<0 -2>))@]" print_function f
2790+
2791+let string_of_init id =
2792+  let b = Buffer.create (List.length id) in
2793+  let add_init = function
2794+  | Init_int8 c ->
2795+      if c >= 32 && c <= 126 && c <> Char.code '\"' && c <> Char.code '\\'
2796+      then Buffer.add_char b (Char.chr c)
2797+      else Buffer.add_string b (Printf.sprintf "\\%03o" c)
2798+  | _ ->
2799+      assert false
2800+  in List.iter add_init id; Buffer.contents b
2801+
2802+let chop_last_nul id =
2803+  match List.rev id with
2804+  | Init_int8 0 :: tl -> List.rev tl
2805+  | _ -> id
2806+
2807+let print_init p = function
2808+  | Init_int8 n -> fprintf p "(Init_int8 (repr %d))@ " n
2809+  | Init_int16 n -> fprintf p "(Init_int16 (repr %d))@ " n
2810+  | Init_int32 n -> fprintf p "(Init_int32 (repr %d))@ " n
2811+  | Init_float32 n -> fprintf p "(Init_float32 %F)@ " n
2812+  | Init_float64 n -> fprintf p "(Iinit_float64 %F)@ " n
2813+  | Init_space n -> fprintf p "(Init_space %d)@ " n
2814+  | Init_addrof(symb, ofs) -> fprintf p "(Init_addrof %d (repr %d))" (id_i symb) ofs
2815+
2816+let re_string_literal = Str.regexp "__stringlit_[0-9]+"
2817+
2818+let print_globvar p ((((id, init), sp), ty)) =
2819+  fprintf p "@[<hov 2>(mk_pair ?? (mk_pair ?? (mk_pair ?? (succ_pos_of_nat %i (* %s *))@ %a)@ %s)@ %s)@]"
2820+    (id_i id)
2821+    id
2822+    (print_list print_init) init
2823+    (sspace sp)
2824+    (stype ty)
2825+
2826+(* Collect struct and union types *)
2827+
2828+let rec collect_type = function
2829+  | Tvoid -> ()
2830+  | Tint(sz, sg) -> ()
2831+  | Tfloat sz -> ()
2832+  | Tpointer (_,t) -> collect_type t
2833+  | Tarray(_, t, n) -> collect_type t
2834+  | Tfunction(args, res) -> List.iter collect_type args; collect_type res
2835+  | Tstruct(id, fld) -> register_struct_union id fld; List.iter collect_field fld
2836+  | Tunion(id, fld) -> register_struct_union id fld; List.iter collect_field fld
2837+  | Tcomp_ptr _ -> ()
2838+
2839+and collect_field f = collect_type (snd f)
2840+
2841+let rec collect_expr (Expr(ed, ty)) =
2842+  match ed with
2843+  | Ecost (_, e) -> collect_expr e
2844+  | Econst_int n -> ()
2845+  | Econst_float f -> ()
2846+  | Evar id -> ()
2847+  | Eunop(op, e1) -> collect_expr e1
2848+  | Ederef e -> collect_expr e
2849+  | Eaddrof e -> collect_expr e
2850+  | Ebinop(op, e1, e2) -> collect_expr e1; collect_expr e2
2851+  | Ecast(ty, e1) -> collect_type ty; collect_expr e1
2852+  | Econdition(e1, e2, e3) -> collect_expr e1; collect_expr e2; collect_expr e3
2853+  | Eandbool(e1, e2) -> collect_expr e1; collect_expr e2
2854+  | Eorbool(e1, e2) -> collect_expr e1; collect_expr e2
2855+  | Esizeof ty -> collect_type ty
2856+  | Efield(e1, id) -> collect_expr e1
2857+
2858+let rec collect_expr_list = function
2859+  | [] -> ()
2860+  | hd :: tl -> collect_expr hd; collect_expr_list tl
2861+
2862+let rec collect_stmt = function
2863+  | Scost (_, s) -> collect_stmt s
2864+  | Sskip -> ()
2865+  | Sassign(e1, e2) -> collect_expr e1; collect_expr e2
2866+  | Scall(None, e1, el) -> collect_expr e1; collect_expr_list el
2867+  | Scall(Some lhs, e1, el) -> collect_expr lhs; collect_expr e1; collect_expr_list el
2868+  | Ssequence(s1, s2) -> collect_stmt s1; collect_stmt s2
2869+  | Sifthenelse(e, s1, s2) -> collect_expr e; collect_stmt s1; collect_stmt s2
2870+  | Swhile(e, s) -> collect_expr e; collect_stmt s
2871+  | Sdowhile(e, s) -> collect_stmt s; collect_expr e
2872+  | Sfor(s_init, e, s_iter, s_body) ->
2873+      collect_stmt s_init; collect_expr e;
2874+      collect_stmt s_iter; collect_stmt s_body
2875+  | Sbreak -> ()
2876+  | Scontinue -> ()
2877+  | Sswitch(e, cases) -> collect_expr e; collect_cases cases
2878+  | Sreturn None -> ()
2879+  | Sreturn (Some e) -> collect_expr e
2880+  | Slabel(lbl, s) -> collect_stmt s
2881+  | Sgoto lbl -> ()
2882+
2883+and collect_cases = function
2884+  | LSdefault s -> collect_stmt s
2885+  | LScase(lbl, s, rem) -> collect_stmt s; collect_cases rem
2886+
2887+let collect_function f =
2888+  collect_type f.fn_return;
2889+  List.iter (fun (id, ty) -> collect_type ty) f.fn_params;
2890+  List.iter (fun (id, ty) -> collect_type ty) f.fn_vars;
2891+  collect_stmt f.fn_body
2892+
2893+let collect_fundef (id, fd) =
2894+  match fd with
2895+  | External(_, args, res) -> List.iter collect_type args; collect_type res
2896+  | Internal f -> collect_function f
2897+
2898+let collect_globvar ((id, init), ty) =
2899+  collect_type ty
2900+
2901+let collect_program p =
2902+  List.iter collect_globvar p.prog_vars;
2903+  List.iter collect_fundef p.prog_funct
2904+
2905+let declare_struct_or_union p (name, fld) =
2906+  fprintf p "%s;@ @ " name
2907+
2908+let print_struct_or_union p (name, fld) =
2909+  fprintf p "@[<v 2>%s {" name;
2910+  let rec print_field (id, ty) =
2911+    fprintf p "@ %s;" (name_cdecl id ty) in
2912+  List.iter print_field fld;
2913+  fprintf p "@;<0 -2>};@]@ "
2914+
2915+let print_program p prog =
2916+  struct_unions := StructUnionSet.empty;
2917+  collect_program prog;
2918+  fprintf p "include \"Csyntax.ma\".@\n@\n";
2919+  fprintf p "@[<v 2>ndefinition myprog := mk_program fundef type@ ";
2920+(*  StructUnionSet.iter (declare_struct_or_union p) !struct_unions;
2921+  StructUnionSet.iter (print_struct_or_union p) !struct_unions;*)
2922+  print_list print_fundef p prog.prog_funct;
2923+  fprintf p "@\n(succ_pos_of_nat %i)@\n" (id_i "main");
2924+  print_list print_globvar p prog.prog_vars;
2925+  fprintf p "@;<0 -2>.@]@."
2926+
2927+
[292]2928diff --git a/src/clight/clightPrinter.ml b/src/clight/clightPrinter.ml
2929index c458e36..b1efd87 100644
2930--- a/src/clight/clightPrinter.ml
2931+++ b/src/clight/clightPrinter.ml
2932@@ -19,6 +19,15 @@ open Format
2933 open AST
2934 open Clight
2935 
2936+let name_space = function
2937+  | Any -> ""
2938+  | Data -> "__data "
2939+  | IData -> "__idata "
2940+  | PData -> "__pdata "
2941+  | XData -> "__xdata "
2942+  | Code -> "__code "
2943+
2944+
2945 let name_unop = function
2946   | Onotbool -> "!"
2947   | Onotint  -> "~"
2948@@ -77,22 +86,28 @@ let name_optid id =
2949 let parenthesize_if_pointer id =
2950   if String.length id > 0 && id.[0] = '*' then "(" ^ id ^ ")" else id
2951 
2952-let rec name_cdecl id ty =
2953+(* Use Any for the space when nothing should appear. *)
2954+
2955+let rec name_cdecl sp id ty =
2956+  let ssp = name_space sp in
2957   match ty with
2958   | Tvoid ->
2959-      "void" ^ name_optid id
2960+      ssp ^ "void" ^ name_optid id
2961   | Tint(sz, sg) ->
2962-      name_inttype sz sg ^ name_optid id
2963+      ssp ^ name_inttype sz sg ^ name_optid id
2964   | Tfloat sz ->
2965-      name_floattype sz ^ name_optid id
2966-  | Tpointer t ->
2967-      name_cdecl ("*" ^ id) t
2968-  | Tarray(t, n) ->
2969+      ssp ^ name_floattype sz ^ name_optid id
2970+  | Tpointer (sp',t) ->
2971+      name_cdecl sp' ("* " ^ ssp ^ id) t
2972+  | Tarray(sp', t, n) ->
2973+      if sp <> sp' then eprintf "Array %s has wrong memory space.\n%!" id;
2974       name_cdecl
2975+        sp'
2976         (sprintf "%s[%ld]" (parenthesize_if_pointer id) (Int32.of_int n))
2977         t
2978   | Tfunction(args, res) ->
2979       let b = Buffer.create 20 in
2980+      Buffer.add_string b ssp;
2981       if id = ""
2982       then Buffer.add_string b "(*)"
2983       else Buffer.add_string b (parenthesize_if_pointer id);
2984@@ -105,22 +120,22 @@ let rec name_cdecl id ty =
2985           | [] -> ()
2986           | t1::tl ->
2987               if not first then Buffer.add_string b ", ";
2988-              Buffer.add_string b (name_cdecl "" t1);
2989+              Buffer.add_string b (name_cdecl Any "" t1);
2990               add_args false tl in
2991           add_args true args
2992       end;
2993       Buffer.add_char b ')';
2994-      name_cdecl (Buffer.contents b) res
2995+      name_cdecl Any (Buffer.contents b) res
2996   | Tstruct(name, fld) ->
2997-      name ^ name_optid id
2998+      ssp ^ name ^ name_optid id
2999   | Tunion(name, fld) ->
3000-      name ^ name_optid id
3001+      ssp ^ name ^ name_optid id
3002   | Tcomp_ptr name ->
3003-      name ^ " *" ^ id
3004+      ssp ^ name ^ " *" ^ id
3005 
3006 (* Type *)
3007 
3008-let name_type ty = name_cdecl "" ty
3009+let name_type ty = name_cdecl Any "" ty
3010 
3011 (* Expressions *)
3012 
3013@@ -318,7 +333,7 @@ let name_function_parameters fun_name params =
3014       | [] -> ()
3015       | (id, ty) :: rem ->
3016           if not first then Buffer.add_string b ", ";
3017-          Buffer.add_string b (name_cdecl id ty);
3018+          Buffer.add_string b (name_cdecl Any id ty);
3019           add_params false rem in
3020       add_params true params
3021   end;
3022@@ -327,12 +342,13 @@ let name_function_parameters fun_name params =
3023 
3024 let print_function p id f =
3025   fprintf p "%s@ "
3026-            (name_cdecl (name_function_parameters id f.fn_params)
3027+            (name_cdecl Any
3028+                        (name_function_parameters id f.fn_params)
3029                         f.fn_return);
3030   fprintf p "@[<v 2>{@ ";
3031   List.iter
3032     (fun ((id, ty)) ->
3033-      fprintf p "%s;@ " (name_cdecl id ty))
3034+      fprintf p "%s;@ " (name_cdecl Any id ty))
3035     f.fn_vars;
3036   print_stmt p f.fn_body;
3037   fprintf p "@;<0 -2>}@]@ @ "
3038@@ -341,7 +357,7 @@ let print_fundef p (id, fd) =
3039   match fd with
3040   | External(_, args, res) ->
3041       fprintf p "extern %s;@ @ "
3042-                (name_cdecl id (Tfunction(args, res)))
3043+                (name_cdecl Any id (Tfunction(args, res)))
3044   | Internal f ->
3045       print_function p id f
3046 
3047@@ -376,17 +392,17 @@ let print_init p = function
3048 
3049 let re_string_literal = Str.regexp "__stringlit_[0-9]+"
3050 
3051-let print_globvar p (((id, init), ty)) =
3052+let print_globvar p ((((id, init), sp), ty)) =
3053   match init with
3054   | [] ->
3055       fprintf p "extern %s;@ @ "
3056-              (name_cdecl id ty)
3057+              (name_cdecl sp id ty)
3058   | [Init_space _] ->
3059       fprintf p "%s;@ @ "
3060-              (name_cdecl id ty)
3061+              (name_cdecl sp id ty)
3062   | _ ->
3063       fprintf p "@[<hov 2>%s = "
3064-              (name_cdecl id ty);
3065+              (name_cdecl sp id ty);
3066       if Str.string_match re_string_literal id 0
3067       && List.for_all (function Init_int8 _ -> true | _ -> false) init
3068       then
3069@@ -404,8 +420,8 @@ let rec collect_type = function
3070   | Tvoid -> ()
3071   | Tint(sz, sg) -> ()
3072   | Tfloat sz -> ()
3073-  | Tpointer t -> collect_type t
3074-  | Tarray(t, n) -> collect_type t
3075+  | Tpointer (_,t) -> collect_type t
3076+  | Tarray(_, t, n) -> collect_type t
3077   | Tfunction(args, res) -> collect_type_list args; collect_type res
3078   | Tstruct(id, fld) -> register_struct_union id fld; collect_fields fld
3079   | Tunion(id, fld) -> register_struct_union id fld; collect_fields fld
3080@@ -491,7 +507,7 @@ let print_struct_or_union p (name, fld) =
3081   let rec print_fields = function
3082   | [] -> ()
3083   | (id, ty)::rem ->
3084-      fprintf p "@ %s;" (name_cdecl id ty);
3085+      fprintf p "@ %s;" (name_cdecl Any id ty);
3086       print_fields rem in
3087   print_fields fld;
3088   fprintf p "@;<0 -2>};@]@ "
3089diff --git a/src/clight/clightToCminor.ml b/src/clight/clightToCminor.ml
3090index 956239e..8b76ff8 100644
3091--- a/src/clight/clightToCminor.ml
3092+++ b/src/clight/clightToCminor.ml
3093@@ -7,7 +7,7 @@ let rec ctype_to_type_return t = match t with
[160]3094   | Tint (_,_) -> Type_ret Sig_int
3095   | Tfloat _ -> Type_ret Sig_float
3096   | Tpointer _ -> Type_ret Sig_int
3097-  | Tarray (_,_) -> Type_ret Sig_int
3098+  | Tarray _ -> Type_ret Sig_int
3099   | Tfunction (_,_) | Tstruct (_,_)
3100   | Tunion (_,_) | Tcomp_ptr _ -> assert false
3101 
[292]3102@@ -15,7 +15,7 @@ let rec ctype_to_sig_type t = match t with
[160]3103   | Tint (_,_) -> Sig_int
3104   | Tfloat _ -> Sig_float
3105   | Tpointer _ -> Sig_int
3106-  | Tarray (_,_) -> Sig_int
3107+  | Tarray _ -> Sig_int
3108   | Tvoid -> assert false
3109   | Tfunction (_,_) | Tstruct (_,_)| Tunion (_,_) | Tcomp_ptr _ ->
3110       assert false
[292]3111@@ -31,7 +31,7 @@ let rec mq_of_ty = function
[160]3112   | Tfloat F32 -> assert false
3113   | Tfloat F64 -> Memory.MQ_float64
3114   | Tpointer _ -> Memory.MQ_int32                     
3115-  | Tarray (c,s) -> Memory.MQ_int32
3116+  | Tarray _ -> Memory.MQ_int32
3117   | Tfunction (_,_) -> assert false
3118   | Tstruct (_,_) -> assert false
3119   | Tunion (_,_) -> assert false
[292]3120@@ -59,15 +59,15 @@ let rec size_of_ctype t = match t with
[160]3121   | Tfloat F32 -> 8
3122   | Tfloat F64 -> 8
3123   | Tpointer _ -> 4                   
3124-  | Tarray (c,s) -> s*(size_of_ctype c)                         
3125+  | Tarray (_,c,s) -> s*(size_of_ctype c)                       
3126   | Tfunction (_,_) | Tstruct (_,_) | Tunion (_,_)  | Tcomp_ptr _ ->
3127       assert false
3128 
3129 let rec translate_vars v =
3130-  let ((id,lst),cty) = v in
3131+  let (((id,lst),space),cty) = v in
3132     match cty with
3133       | Tint (_,_) | Tfloat _ | Tpointer _ -> (id,init_data_to_data_rec lst)
3134-      | Tarray(c,_) -> translate_vars ((id,lst),c)
3135+      | Tarray(_,c,_) -> translate_vars (((id,lst),space),c)
3136       | Tvoid | Tfunction (_,_) | Tstruct (_,_) | Tunion (_,_) | Tcomp_ptr _ ->
3137           assert false
3138 
[292]3139@@ -95,13 +95,13 @@ let translate_binop t1 e1 t2 e2 = function
[160]3140       (match (t1,t2) with
3141          | (Tint(_,_),Tint(_,_)) -> Op2 (Op_add,e1,e2)
3142          | (Tfloat _,Tfloat _) -> Op2 (Op_addf,e1,e2)
3143-         | (Tpointer t,Tint(_,_)) ->
3144+         | (Tpointer (_,t),Tint(_,_)) ->
3145              Op2 (Op_add,e1, Op2 (Op_mul,e2,Cst (Cst_int (size_of_ctype t))))
3146-         | (Tint(_,_),Tpointer t) ->
3147+         | (Tint(_,_),Tpointer (_,t)) ->
3148              Op2 (Op_add,Op2 (Op_mul,e1,Cst (Cst_int (size_of_ctype t))),e2)
3149-         | (Tarray (t,_),Tint(_,_)) ->
3150+         | (Tarray (_,t,_),Tint(_,_)) ->
3151              Op2 (Op_add,e1,Op2 (Op_mul,e2,(Cst (Cst_int (size_of_ctype t)))))
3152-         | (Tint(_,_),Tarray(t,_)) ->
3153+         | (Tint(_,_),Tarray(_,t,_)) ->
3154              Op2 (Op_add,e2,Op2 (Op_mul,e1,(Cst (Cst_int (size_of_ctype t)))))
3155          | _ -> assert false
3156       )
[292]3157@@ -109,13 +109,13 @@ let translate_binop t1 e1 t2 e2 = function
[160]3158       (match (t1,t2) with
3159          | (Tint(_,_),Tint(_,_)) -> Op2 (Op_sub,e1,e2)
3160          | (Tfloat _,Tfloat _) -> Op2 (Op_subf,e1,e2)
3161-         | (Tpointer t,Tint(_,_)) ->
3162+         | (Tpointer (_,t),Tint(_,_)) ->
3163              Op2 (Op_sub,e1,Op2 (Op_mul,e2,(Cst (Cst_int (size_of_ctype t)))))
3164-         | (Tint(_,_),Tpointer t) ->
3165+         | (Tint(_,_),Tpointer (_,t)) ->
3166              Op2 (Op_sub,Op2 (Op_mul,e1,(Cst (Cst_int (size_of_ctype t)))),e2)
3167-         | (Tarray (t,_),Tint(_,_)) ->
3168+         | (Tarray (_,t,_),Tint(_,_)) ->
3169              Op2 (Op_sub,e1,Op2 (Op_mul,e2,(Cst (Cst_int (size_of_ctype t)))))
3170-         | (Tint(_,_),Tarray(t,_)) ->
3171+         | (Tint(_,_),Tarray(_,t,_)) ->
3172              Op2 (Op_sub,e2,Op2 (Op_mul,e1,(Cst (Cst_int (size_of_ctype t)))))
3173          | _ -> assert false
3174       )
[292]3175@@ -310,7 +310,7 @@ let compute_stack f =
[160]3176   and stck = ref 0 in
3177   let treat_var v = match snd v with 
3178     | Tvoid | Tint (_,_) | Tfloat _ | Tpointer _ -> ()
3179-    | Tarray (_,_)  ->
3180+    | Tarray _  ->
3181         let size = size_of_ctype (snd v) in
3182           if size > 0 then (
3183             (Hashtbl.add addr_of_id (fst v) !stck);
[292]3184@@ -400,7 +400,7 @@ let translate_funct globals = function
[160]3185   | (id,External (i,p,r)) -> (id, F_ext (translate_external i p r))
3186 
3187 let translate p =
3188-  let globals = List.map (fun p -> fst (fst p)) p.prog_vars in
3189+  let globals = List.map (fun p -> fst (fst (fst p))) p.prog_vars in
3190     {Cminor.vars   = List.map translate_vars p.prog_vars;
3191      Cminor.functs = List.map (translate_funct globals) p.prog_funct;
3192      Cminor.main = p.prog_main }
[292]3193diff --git a/src/common/cminorMemory.ml b/src/common/cminorMemory.ml
3194index 1b3e509..813be71 100644
3195--- a/src/common/cminorMemory.ml
3196+++ b/src/common/cminorMemory.ml
3197@@ -204,7 +204,7 @@ let rec sizeof = function
[160]3198   | Tfloat F32 -> 4
3199   | Tfloat F64 -> 8
3200   | Tpointer _ -> 4                   
3201-  | Tarray (_,_) -> 4                   
3202+  | Tarray _ -> 4                       
3203   | Tfunction (_,_) -> assert false
3204   | Tstruct (_,_) -> assert false
3205   | Tunion (_,_) -> assert false
[292]3206@@ -227,7 +227,7 @@ let vk_of_init_list = function (*FIXME*)
[160]3207 let cast t v = v (*TODO*)
3208 
3209 let init m b lst = function
3210-  | Tarray (c,n) ->
3211+  | Tarray (_,c,n) ->
3212       (match alloc m 0 (n*(sizeof c)) with
3213          | Some(b',m') ->
3214              (match store m' Memory.MQ_int32 b 0 (Val_ptr(b',0)) with
[292]3215@@ -253,7 +253,7 @@ let initmem_clight p =
[160]3216   let b_of_id = Hashtbl.create 11
3217   and fd_of_b = Hashtbl.create 11
3218   and i = ref (-1) in
3219-  let update_mem m ((id,lst),cty) =
3220+  let update_mem m (((id,lst),_),cty) =
3221     (match alloc m 0 (sizeof cty) with
3222        | Some(b,m') ->
3223            Hashtbl.add b_of_id id b;
[292]3224diff --git a/src/languages.ml b/src/languages.ml
3225index 4317d19..12ffdd2 100644
3226--- a/src/languages.ml
3227+++ b/src/languages.ml
3228@@ -230,6 +230,27 @@ let save filename ast =
[160]3229   flush cout;
3230   close_out cout
3231 
3232+let rec find_clight = function
3233+| [] -> None
3234+| AstClight p :: t -> Some p
3235+| _::t -> find_clight t
3236+
3237+let save_matita filename asts =
3238+  match find_clight asts with
3239+  | None -> Error.warning "during matita output" "No Clight AST."
3240+  | Some prog -> begin
3241+    let output_filename =
3242+      Misc.SysExt.alternative
3243+        (Filename.chop_extension filename
3244+         ^ ".ma")
3245+    in
3246+    let cout = open_out output_filename in
3247+    let fout = Format.formatter_of_out_channel cout in
3248+    ClightPrintMatita.print_program fout prog;
3249+    flush cout;
3250+    close_out cout
3251+  end
3252+
3253 let interpret = function
3254   | AstClight p ->
3255     ClightInterpret.interpret true p
[292]3256diff --git a/src/languages.mli b/src/languages.mli
3257index 3dfc31a..f5d8e45 100644
3258--- a/src/languages.mli
3259+++ b/src/languages.mli
3260@@ -75,6 +75,11 @@ val interpret : ast -> AST.label list
[160]3261     is deduced from the language of the AST. *)
3262 val save : string -> ast -> unit
3263 
3264+(** [save_matita filename asts] pretty prints the first Clight AST in
3265+    [asts] in a fresh file whose name is prefixed by [filename] and whose
3266+    extension is .ma. *)
3267+val save_matita : string -> ast list -> unit
3268+
3269 (** [from_string s] parses [s] as an intermediate language name. *)
3270 val from_string : string -> name
3271 
[292]3272diff --git a/src/options.ml b/src/options.ml
3273index 061f7d0..d47e558 100644
3274--- a/src/options.ml
3275+++ b/src/options.ml
3276@@ -39,6 +39,9 @@ let debug_flag                        = ref false
[160]3277 let set_debug                  = (:=) debug_flag
3278 let is_debug_enabled ()                = !debug_flag
3279 
3280+let matita_output_flag          = ref false
3281+let is_matita_output_enabled () = !matita_output_flag
3282+
3283 let options = OptionsParsing.register [
3284   "-s", Arg.String set_source_language,
3285   " Choose the source language between:";
[292]3286@@ -58,4 +61,7 @@ let options = OptionsParsing.register [
[160]3287 
3288   "-d", Arg.Set debug_flag,
3289   " Debugging mode.";
3290+
3291+  "-ma", Arg.Set matita_output_flag,
3292+  " Output matita formatted Clight program.";
3293 ]
[292]3294diff --git a/src/options.mli b/src/options.mli
3295index 4517400..ec6b020 100644
3296--- a/src/options.mli
3297+++ b/src/options.mli
3298@@ -22,3 +22,6 @@ val input_files          : unit -> string list
[160]3299 
3300 (** {2 Verbose mode} *)
3301 val is_debug_enabled : unit -> bool
3302+
3303+(** {2 Matita output of Clight programs} *)
3304+val is_matita_output_enabled : unit -> bool
Note: See TracBrowser for help on using the repository browser.