source: src/Clight/acc-0.1.spaces.patch @ 2745

cparser/AddCasts.ml

@@ -39 +39 @@
       r1 < r2 || (r1 = r2 && is_signed_ikind k1 = is_signed_ikind k2)
   | TFloat(k1, _), TFloat(k2, _) ->
       float_rank k1 <= float_rank k2
-  | TPtr(ty1, _), TPtr(ty2, _) -> is_void_type env ty2
+  | TPtr(sp1, ty1, _), TPtr(sp2, ty2, _) when sp1 = sp2 -> is_void_type env ty2
   | _, _ -> false
   end
 
@@ -52 +52 @@
 let cast env e tto =
   if cast_not_needed env e.etyp tto
   then e
-  else {edesc = ECast(tto, e); etyp = tto}
+  else {edesc = ECast(tto, e); etyp = tto; espace = Any}
 
 (* Note: this pass applies only to simplified expressions 
    because casts cannot be materialized in op= expressions... *)
@@ -73 +73 @@
             EUnop(op, e1')
         | Opreincr | Opredecr | Opostincr | Opostdecr ->
             assert false (* not simplified *)
-      in { edesc = desc; etyp = e.etyp }
+      in { edesc = desc; etyp = e.etyp; espace = e.espace }
   | EBinop(op, e1, e2, ty) ->
       let e1' = add_expr env e1 in
       let e2' = add_expr env e2 in
@@ -97 +97 @@
         | Oadd_assign|Osub_assign|Omul_assign|Odiv_assign|Omod_assign
         | Oand_assign|Oor_assign|Oxor_assign|Oshl_assign|Oshr_assign ->
             assert false (* not simplified *)
-      in { edesc = desc; etyp = e.etyp }
+      in { edesc = desc; etyp = e.etyp; espace = e.espace }
   | EConditional(e1, e2, e3) ->
       { edesc = 
           EConditional(add_expr env e1, add_expr env e2, add_expr env e3);
-        etyp = e.etyp }
+        etyp = e.etyp;
+        espace = e.espace }
   | ECast(ty, e1) ->
-      { edesc = ECast(ty, add_expr env e1); etyp = e.etyp }
+      { edesc = ECast(ty, add_expr env e1); etyp = e.etyp; espace = e.espace }
   | ECall(e1, el) ->
       assert false (* not simplified *)
 
@@ -132 +133 @@
   let ty_args =
     match unroll env ty_fun with
     | TFun(res, args, vararg, a) -> args
-    | TPtr(ty, a) ->
+    | TPtr(_, ty, a) ->
         begin match unroll env ty with
         | TFun(res, args, vararg, a) -> args
         | _ -> assert false
@@ -146 +147 @@
 
 let add_topexpr env loc e =
   match e.edesc with
-  | EBinop(Oassign, lhs, {edesc = ECall(e1, el); etyp = ty}, _) ->
+  | EBinop(Oassign, lhs, {edesc = ECall(e1, el); etyp = ty; espace = space}, _) ->
       let ecall =
         {edesc = ECall(add_expr env e1, add_arguments env e1.etyp el);
-         etyp = ty} in
+         etyp = ty; espace = space} in
       if cast_not_needed env ty lhs.etyp then
         sassign loc (add_expr env lhs) ecall
       else begin
@@ -162 +163 @@
   | ECall(e1, el) ->
       let ecall =
         {edesc = ECall(add_expr env e1, add_arguments env e1.etyp el);
-         etyp = e.etyp} in
+         etyp = e.etyp; espace = e.espace} in
       {sdesc = Sdo ecall; sloc = loc}
   | _ ->
       assert false
@@ -175 +176 @@
   | Init_array il ->
       let ty_elt =
         match unroll env tto with
-        | TArray(ty, _, _) -> ty | _ -> assert false in
+        | TArray(_,ty, _, _) -> ty | _ -> assert false in
       Init_array (List.map (add_init env ty_elt) il)
   | Init_struct(id, fil) ->
       Init_struct (id, List.map

cparser/Bitfields.ml

@@ -118 +118 @@
       (Int64.pred (Int64.shift_left 1L bf.bf_size))
       bf.bf_pos in
   (* Give the mask an hexadecimal string representation, nicer to read *)
-  {edesc = EConst(CInt(m, IUInt, sprintf "0x%LXU" m)); etyp = TInt(IUInt, [])}
+  {edesc = EConst(CInt(m, IUInt, sprintf "0x%LXU" m)); etyp = TInt(IUInt, []); espace = Code} (* XXX are consts always Code? *)
 
 (* Extract the value of a bitfield *)
 
@@ -140 +140 @@
 let bitfield_extract bf carrier =
   let e1 =
     {edesc = EBinop(Oshl, carrier, left_shift_count bf, TInt(IUInt, []));
-     etyp = carrier.etyp} in
+     etyp = carrier.etyp; espace = Any} in
   let ty = TInt((if bf.bf_signed then IInt else IUInt), []) in
   let e2 =
-    {edesc = ECast(ty, e1); etyp = ty} in
+    {edesc = ECast(ty, e1); etyp = ty; espace = Any} in
   {edesc = EBinop(Oshr, e2, right_shift_count bf, e2.etyp);
-   etyp = e2.etyp}
+   etyp = e2.etyp; espace = Any}
 
 (* Assign a bitfield within a carrier *)
 
@@ -161 +161 @@
 
 let bitfield_assign bf carrier newval =
   let msk = insertion_mask bf in
-  let notmsk = {edesc = EUnop(Onot, msk); etyp = msk.etyp} in
+  let notmsk = {edesc = EUnop(Onot, msk); etyp = msk.etyp; espace = Any} in
   let newval_shifted =
     {edesc = EBinop(Oshl, newval, intconst (Int64.of_int bf.bf_pos) IUInt,
                     TInt(IUInt,[]));
-     etyp = TInt(IUInt,[])} in
+     etyp = TInt(IUInt,[]);
+     espace = Any} in
   let newval_masked =
     {edesc = EBinop(Oand, newval_shifted, msk, TInt(IUInt,[]));
-     etyp = TInt(IUInt,[])}
+     etyp = TInt(IUInt,[]);
+     espace = Any}
   and oldval_masked =
     {edesc = EBinop(Oand, carrier, notmsk, TInt(IUInt,[]));
-     etyp = TInt(IUInt,[])} in
+     etyp = TInt(IUInt,[]); espace = Any} in
   {edesc = EBinop(Oor,  oldval_masked, newval_masked,  TInt(IUInt,[]));
-   etyp =  TInt(IUInt,[])}
+   etyp =  TInt(IUInt,[]); espace = Any}
 
 (* Expressions *)
 
@@ -188 +190 @@
 
   let is_bitfield_access_ptr ty fieldname =
     match unroll env ty with
-    | TPtr(ty', _) -> is_bitfield_access ty' fieldname
+    | TPtr(_, ty', _) -> is_bitfield_access ty' fieldname
     | _ -> None in 
 
   let rec texp e =
@@ -201 +203 @@
         let e1' = texp e1 in
         begin match is_bitfield_access e1.etyp fieldname with
         | None ->
-            {edesc = EUnop(Odot fieldname, e1'); etyp = e.etyp}
+            {edesc = EUnop(Odot fieldname, e1'); etyp = e.etyp; espace = e1'.espace}
         | Some bf ->
             bitfield_extract bf
               {edesc = EUnop(Odot bf.bf_carrier, e1');
-               etyp = bf.bf_carrier_typ}
+               etyp = bf.bf_carrier_typ;
+               espace = e1'.espace}
         end
 
     | EUnop(Oarrow fieldname, e1) ->
         let e1' = texp e1 in
         begin match is_bitfield_access_ptr e1.etyp fieldname with
         | None ->
-            {edesc = EUnop(Oarrow fieldname, e1'); etyp = e.etyp}
+            {edesc = EUnop(Oarrow fieldname, e1'); etyp = e.etyp; espace = Any}
         | Some bf ->
             bitfield_extract bf
               {edesc = EUnop(Oarrow bf.bf_carrier, e1');
-               etyp = bf.bf_carrier_typ}
+               etyp = bf.bf_carrier_typ; espace = Any}
         end
 
     | EUnop(op, e1) ->
         (* Note: simplified expr, so no ++/-- *)
-        {edesc = EUnop(op, texp e1); etyp = e.etyp}
+        {edesc = EUnop(op, texp e1); etyp = e.etyp; espace = e.espace}
 
     | EBinop(Oassign, e1, e2, ty) ->
         begin match e1.edesc with
@@ -231 +234 @@
             | None ->
                 {edesc = EBinop(Oassign,
                                 {edesc = EUnop(Odot fieldname, lhs);
-                                 etyp = e1.etyp},
+                                 etyp = e1.etyp; espace = lhs.espace},
                                 rhs, ty);
-                 etyp = e.etyp}
+                 etyp = e.etyp;
+                 espace = e.espace}
             | Some bf ->
                 let carrier =
                   {edesc = EUnop(Odot bf.bf_carrier, lhs);
-                   etyp = bf.bf_carrier_typ} in
+                   etyp = bf.bf_carrier_typ;
+                   espace = lhs.espace} in
                 {edesc = EBinop(Oassign, carrier,
                                 bitfield_assign bf carrier rhs,
                                 carrier.etyp);
-                 etyp = carrier.etyp}
+                 etyp = carrier.etyp;
+                 espace = lhs.espace}
             end
         | EUnop(Oarrow fieldname, e11) ->
             let lhs = texp e11 in let rhs = texp e2 in
@@ -249 +255 @@
             | None ->
                 {edesc = EBinop(Oassign,
                                 {edesc = EUnop(Oarrow fieldname, lhs);
-                                 etyp = e1.etyp},
+                                 etyp = e1.etyp;
+                                 espace = e1.espace},
                                 rhs, ty);
-                 etyp = e.etyp}
+                 etyp = e.etyp;
+                 espace = e.espace}
             | Some bf ->
                 let carrier =
                   {edesc = EUnop(Oarrow bf.bf_carrier, lhs);
-                   etyp = bf.bf_carrier_typ} in
+                   etyp = bf.bf_carrier_typ;
+                   espace = Any} in
                 {edesc = EBinop(Oassign, carrier,
                                 bitfield_assign bf carrier rhs,
                                 carrier.etyp);
-                 etyp = carrier.etyp}
+                 etyp = carrier.etyp;
+                 espace = Any}
             end
         | _ ->
-            {edesc = EBinop(Oassign, texp e1, texp e2, e1.etyp); etyp = e1.etyp}
+            {edesc = EBinop(Oassign, texp e1, texp e2, e1.etyp); etyp = e1.etyp; espace = e1.espace}
         end
 
     | EBinop(op, e1, e2, ty) ->
         (* Note: simplified expr assumed, so no assign-op *)
-        {edesc = EBinop(op, texp e1, texp e2, ty); etyp = e.etyp}
+        {edesc = EBinop(op, texp e1, texp e2, ty); etyp = e.etyp; espace = e.espace}
     | EConditional(e1, e2, e3) ->
-        {edesc = EConditional(texp e1, texp e2, texp e3); etyp = e.etyp}
+        {edesc = EConditional(texp e1, texp e2, texp e3); etyp = e.etyp; espace = e.espace}
     | ECast(ty, e1) ->
-        {edesc = ECast(ty, texp e1); etyp = e.etyp}
+        {edesc = ECast(ty, texp e1); etyp = e.etyp; espace = e.espace}
     | ECall(e1, el) ->
-        {edesc = ECall(texp e1, List.map texp el); etyp = e.etyp}
+        {edesc = ECall(texp e1, List.map texp el); etyp = e.etyp; espace = e.espace}
 
   in texp e
 
@@ -325 +335 @@
       let m = Int64.pred (Int64.shift_left 1L bf.bf_size) in
       let e_mask =
         {edesc = EConst(CInt(m, IUInt, sprintf "0x%LXU" m));
-         etyp = TInt(IUInt, [])} in
+         etyp = TInt(IUInt, []);
+         espace = Any} in
       let e_and =
         {edesc = EBinop(Oand, e, e_mask, TInt(IUInt,[]));
-         etyp = TInt(IUInt,[])} in
+         etyp = TInt(IUInt,[]);
+         espace = Any} in
       {edesc = EBinop(Oshl, e_and, intconst (Int64.of_int bf.bf_pos) IInt,
                       TInt(IUInt, []));
-       etyp = TInt(IUInt, [])}
+       etyp = TInt(IUInt, []);
+       espace = Any}
   | _ -> assert false
 
 let rec pack_bitfield_init id carrier fld_init_list =
@@ -354 +367 @@
   | [e] -> e
   | e1 :: el ->
       {edesc = EBinop(Oor, e1, or_expr_list el, TInt(IUInt,[]));
-       etyp = TInt(IUInt,[])}
+       etyp = TInt(IUInt,[]);
+       espace = Any}
 
 let rec transf_struct_init id fld_init_list =
   match fld_init_list with
@@ -367 +381 @@
         ({fld_name = bf.bf_carrier; fld_typ = bf.bf_carrier_typ;
           fld_bitfield = None},
          Init_single {edesc = ECast(bf.bf_carrier_typ, or_expr_list el);
-                      etyp = bf.bf_carrier_typ})
+                      etyp = bf.bf_carrier_typ;
+                      espace = Any})
         :: transf_struct_init id rem'
       with Not_found ->
         (fld, i) :: transf_struct_init id rem

cparser/Builtins.ml

@@ -37 +37 @@
     TFun(res,
          Some (List.map (fun ty -> (Env.fresh_ident "", ty)) args),
          va, []) in
-  let (id, env') = Env.enter_ident !env s Storage_extern ty in
+  let (id, env') = Env.enter_ident !env s Storage_extern ty Code in
   env := env';
   idents := id :: !idents;
-  decls := {gdesc = Gdecl(Storage_extern, id, ty, None); gloc = no_loc} :: !decls
+  decls := {gdesc = Gdecl(Code, (Storage_extern, id, ty, None)); gloc = no_loc} :: !decls
 
 type t = {
   typedefs: (string * C.typ) list;

cparser/C.mli

@@ -124 +124 @@
 
 (** Types *)
 
+type memory_space =
+  | Any
+  | Data
+  | IData
+  | PData
+  | XData
+  | Code
+
 type typ =
   | TVoid of attributes
   | TInt of ikind * attributes
   | TFloat of fkind * attributes
-  | TPtr of typ * attributes
-  | TArray of typ * int64 option * attributes
+  | TPtr of memory_space * typ * attributes
+  | TArray of memory_space * typ * int64 option * attributes
   | TFun of typ * (ident * typ) list option * bool * attributes
   | TNamed of ident * attributes
   | TStruct of ident * attributes
@@ -137 +145 @@
 
 (** Expressions *)
 
-type exp = { edesc: exp_desc; etyp: typ }
+type exp = { edesc: exp_desc; etyp: typ; espace: memory_space }
 
 and exp_desc =
   | EConst of constant
@@ -220 +228 @@
   { gdesc: globdecl_desc; gloc: location }
 
 and globdecl_desc =
-  | Gdecl of decl           (* variable declaration, function prototype *)
+  | Gdecl of memory_space * decl  (* variable declaration, function prototype *)
   | Gfundef of fundef                   (* function definition *)
   | Gcompositedecl of struct_or_union * ident (* struct/union declaration *)
   | Gcompositedef of struct_or_union * ident * field list

cparser/Ceval.ml

@@ -99 +99 @@
       if is_signed env ty_from
       then F(normalize_float (Int64.to_float n) fk)
       else F(normalize_float (int64_unsigned_to_float n) fk)
-  | TPtr(ty, _), I n ->
+  | TPtr(_, ty, _), I n ->
       I (normalize_int n ptr_t_ikind)
-  | TPtr(ty, _), F n ->
+  | TPtr(_, ty, _), F n ->
       if n = 0.0 then I 0L else raise Notconst
-  | TPtr(ty, _), (S _ | WS _) ->
+  | TPtr(_, ty, _), (S _ | WS _) ->
       v
   | _, _ ->
       raise Notconst
@@ -270 +270 @@
     match unroll env ty, cast env e.etyp ty (expr env e) with
     | TInt(ik, _), I n -> Some(CInt(n, ik, ""))
     | TFloat(fk, _), F n -> Some(CFloat(n, fk, ""))
-    | TPtr(_, _), I 0L -> Some(CInt(0L, IInt, ""))
-    | TPtr(_, _), S s -> Some(CStr s)
-    | TPtr(_, _), WS s -> Some(CWStr s)
+    | TPtr(_, _, _), I 0L -> Some(CInt(0L, IInt, ""))
+    | TPtr(_, _, _), S s -> Some(CStr s)
+    | TPtr(_, _, _), WS s -> Some(CWStr s)
     | _   -> None
   with Notconst -> None

cparser/Cleanup.ml

@@ -40 +40 @@
 (* Iterate [addref] on all syntactic categories. *)
 
 let rec add_typ = function
-  | TPtr(ty, _) -> add_typ ty
-  | TArray(ty, _, _) -> add_typ ty
+  | TPtr(_, ty, _) -> add_typ ty
+  | TArray(_, ty, _, _) -> add_typ ty
   | TFun(res, None, _, _) -> add_typ res
   | TFun(res, Some params, _, _) -> add_typ res; add_vars params
   | TNamed(id, _) -> addref id
@@ -120 +120 @@
   | [] -> accu
   | g :: rem ->
       match g.gdesc with
-      | Gdecl decl when visible_decl decl ->
+      | Gdecl (_,decl) when visible_decl decl ->
           add_decl decl; add_init_globdecls accu rem
       | Gfundef({fd_storage = Storage_default} as f) ->
           add_fundef f; add_init_globdecls accu rem
@@ -135 +135 @@
   | [] -> accu
   | g :: rem ->
       match g.gdesc with
-      | Gdecl((sto, id, ty, init) as decl) ->
+      | Gdecl(_, ((sto, id, ty, init) as decl)) ->
           if needed id
           then (add_decl decl; add_needed_globdecls accu rem)
           else add_needed_globdecls (g :: accu) rem
@@ -174 +174 @@
   | g :: rem ->
       let need =
         match g.gdesc with
-        | Gdecl((sto, id, ty, init) as decl) -> visible_decl decl || needed id
+        | Gdecl(_, ((sto, id, ty, init) as decl)) -> visible_decl decl || needed id
         | Gfundef f -> f.fd_storage = Storage_default || needed f.fd_name
         | Gcompositedecl(_, id) -> needed id
         | Gcompositedef(_, id, flds) -> needed id

cparser/Cprint.ml

@@ -67 +67 @@
       fprintf pp "%s%a%t" (name_of_ikind k) attributes a n
   | TFloat(k, a) ->
       fprintf pp "%s%a%t" (name_of_fkind k) attributes a n
-  | TPtr(t, a) ->
+  | TPtr(_, t, a) -> (* XXX *)
       let n' pp =
         match t with
         | TFun _ | TArray _ -> fprintf pp " (*%a%t)" attributes a n
         | _ -> fprintf pp " *%a%t" attributes a n in
       dcl pp t n'
-  | TArray(t, sz, a) ->
+  | TArray(_, t, sz, a) -> (* XXX *)
       let n' pp =
         begin match a with
         | [] -> n pp
@@ -353 +353 @@
   | Sdo e -> e
   | Sseq(s1, s2) -> 
       {edesc = EBinop(Ocomma, exp_of_stmt s1, exp_of_stmt s2, TVoid []);
-       etyp = TVoid []}
+       etyp = TVoid [];
+       espace = Any}
   | Sif(e, s1, s2) ->
       {edesc = EConditional(e, exp_of_stmt s1, exp_of_stmt s2);
-       etyp = TVoid []}
+       etyp = TVoid [];
+       espace = Any}
   | _ ->
       raise Not_expr
 
@@ -373 +375 @@
       fprintf pp "@[<v 2>if (%a) {@ %a@;<0 -2>}@]"
               exp (0, e) stmt_block s1
   | Sif(e, {sdesc = Sskip}, s2) ->
-      let not_e = {edesc = EUnop(Olognot, e); etyp = TInt(IInt, [])} in
+      let not_e = {edesc = EUnop(Olognot, e); etyp = TInt(IInt, []); espace = Any} in
       fprintf pp "@[<v 2>if (%a) {@ %a@;<0 -2>}@]"
               exp (0, not_e) stmt_block s2
   | Sif(e, s1, s2) ->
@@ -455 +457 @@
 let globdecl pp g =
   location pp g.gloc;
   match g.gdesc with
-  | Gdecl d ->
+  | Gdecl (_, d) -> (* XXX *)
       fprintf pp "%a@ @ " full_decl d
   | Gfundef f ->
       fundef pp f

cparser/Cutil.ml

@@ -71 +71 @@
   | TVoid a -> TVoid (add_attributes attr a)
   | TInt(ik, a) -> TInt(ik, add_attributes attr a)
   | TFloat(fk, a) -> TFloat(fk, add_attributes attr a)
-  | TPtr(ty, a) -> TPtr(ty, add_attributes attr a)
-  | TArray(ty, sz, a) -> TArray(add_attributes_type attr ty, sz, a)
+  | TPtr(sp, ty, a) -> TPtr(sp, ty, add_attributes attr a)
+  | TArray(sp, ty, sz, a) -> TArray(sp, add_attributes_type attr ty, sz, a)
   | TFun(ty, params, vararg, a) -> TFun(ty, params, vararg, add_attributes attr 
 a)
   | TNamed(s, a) -> TNamed(s, add_attributes attr a)
@@ -95 +95 @@
   | TVoid a -> a
   | TInt(ik, a) -> a
   | TFloat(fk, a) -> a
-  | TPtr(ty, a) -> a
-  | TArray(ty, sz, a) -> a              (* correct? *)
+  | TPtr(_, ty, a) -> a
+  | TArray(_, ty, sz, a) -> a              (* correct? *)
   | TFun(ty, params, vararg, a) -> a
   | TNamed(s, a) -> attributes_of_type env (unroll env t)
   | TStruct(s, a) -> a
@@ -110 +110 @@
   | TVoid a -> TVoid (f a)
   | TInt(ik, a) -> TInt(ik, f a)
   | TFloat(fk, a) -> TFloat(fk, f a)
-  | TPtr(ty, a) -> TPtr(ty, f a)
-  | TArray(ty, sz, a) ->
-      TArray(change_attributes_type env f ty, sz, a)
+  | TPtr(sp, ty, a) -> TPtr(sp, ty, f a)
+  | TArray(sp, ty, sz, a) ->
+      TArray(sp, change_attributes_type env f ty, sz, a)
   | TFun(ty, params, vararg, a) -> TFun(ty, params, vararg, f a)
   | TNamed(s, a) ->
       let t1 = unroll env t in
@@ -166 +166 @@
         TInt(comp_base ik1 ik2, comp_attr a1 a2)
     | TFloat(fk1, a1), TFloat(fk2, a2) ->
         TFloat(comp_base fk1 fk2, comp_attr a1 a2)
-    | TPtr(ty1, a1), TPtr(ty2, a2) ->
-        TPtr(comp ty1 ty2, comp_attr a1 a2)
-    | TArray(ty1, sz1, a1), TArray(ty2, sz2, a2) ->
-        TArray(comp ty1 ty2, comp_array_size sz1 sz2, comp_attr a1 a2)
+    | TPtr(sp1, ty1, a1), TPtr(sp2, ty2, a2) when sp1 = sp2 ->
+        TPtr(sp1, comp ty1 ty2, comp_attr a1 a2)
+    | TArray(sp1, ty1, sz1, a1), TArray(sp2, ty2, sz2, a2) when sp1 = sp2 ->
+        TArray(sp1, comp ty1 ty2, comp_array_size sz1 sz2, comp_attr a1 a2)
     | TFun(ty1, params1, vararg1, a1), TFun(ty2, params2, vararg2, a2) ->
         let (params, vararg) =
           match params1, params2 with
@@ -244 +244 @@
   | TVoid _ -> !config.alignof_void
   | TInt(ik, _) -> Some(alignof_ikind ik)
   | TFloat(fk, _) -> Some(alignof_fkind fk)
-  | TPtr(_, _) -> Some(!config.alignof_ptr)
-  | TArray(ty, _, _) -> alignof env ty
+  | TPtr(_, _, _) -> Some(!config.alignof_ptr)
+  | TArray(_, ty, _, _) -> alignof env ty
   | TFun(_, _, _, _) -> !config.alignof_fun
   | TNamed(_, _) -> alignof env (unroll env t)
   | TStruct(name, _) ->
@@ -302 +302 @@
   | TVoid _ -> !config.sizeof_void
   | TInt(ik, _) -> Some(sizeof_ikind ik)
   | TFloat(fk, _) -> Some(sizeof_fkind fk)
-  | TPtr(_, _) -> Some(!config.sizeof_ptr)
-  | TArray(ty, None, _) -> None
-  | TArray(ty, Some n, _) as t' ->
+  | TPtr(_, _, _) -> Some(!config.sizeof_ptr) (* FIXME *)
+  | TArray(_, ty, None, _) -> None
+  | TArray(_, ty, Some n, _) as t' ->
       begin match sizeof env ty with
       | None -> None
       | Some s ->
@@ -343 +343 @@
 
 let sizeof_struct env members =
   let rec sizeof_rec ofs = function
-  | [] | [ { fld_typ = TArray(_, None, _) } ] ->
+  | [] | [ { fld_typ = TArray(_, _, None, _) } ] ->
       (* C99: ty[] allowed as last field *)
       begin match alignof_struct_union env members with
       | None -> None                    (* should not happen? *)
@@ -472 +472 @@
 
 let pointer_decay env t =
   match unroll env t with
-  | TArray(ty, _, _) -> TPtr(ty, [])
-  | TFun _ as ty -> TPtr(ty, [])
+  | TArray(sp, ty, _, _) -> TPtr(sp, ty, [])
+  | TFun _ as ty -> TPtr(Code, ty, [])
   | t -> t
 
 (* The usual unary conversions (H&S 6.3.3) *) 
@@ -489 +489 @@
           TInt(kind, attr)
       end
   (* Arrays and functions decay automatically to pointers *)
-  | TArray(ty, _, _) -> TPtr(ty, [])
-  | TFun _ as ty -> TPtr(ty, [])
+  | TArray(sp, ty, _, _) -> TPtr(sp, ty, [])
+  | TFun _ as ty -> TPtr(Code, ty, [])
   (* Other types are not changed *)
   | t -> t
 
@@ -540 +540 @@
   (* Arrays and functions degrade automatically to pointers *)
   (* Other types are not changed *)
   match unroll env t with
-  | TArray(ty, _, _) -> TPtr(ty, [])
-  | TFun _ as ty -> TPtr(ty, [])
+  | TArray(sp, ty, _, _) -> TPtr(sp, ty, [])
+  | TFun _ as ty -> TPtr(Code, ty, [])
   | _ -> t (* preserve typedefs *)
 
 (* Conversion on function arguments (old-style unprototyped, or vararg *)
@@ -584 +584 @@
 let type_of_constant = function
   | CInt(_, ik, _) -> TInt(ik, [])
   | CFloat(_, fk, _) -> TFloat(fk, [])
-  | CStr _ -> TPtr(TInt(IChar, []), [])          (* XXX or array? const? *)
-  | CWStr _ -> TPtr(TInt(wchar_ikind, []), [])   (* XXX or array? const? *)
+  | CStr _ -> TPtr(Code, TInt(IChar, []), [])          (* XXX or array? const? *)
+  | CWStr _ -> TPtr(Code, TInt(wchar_ikind, []), [])   (* XXX or array? const? *)
   | CEnum(_, _) -> TInt(IInt, [])
 
 (* Check that a C expression is a lvalue *)
@@ -612 +612 @@
 
 (* Check that an assignment is allowed *)
 
+let valid_pointer_conv from tto =
+  match from, tto with
+  | Any, _
+  | _, Any -> true
+  | f, t -> f = t
+
 let valid_assignment env from tto =
   match pointer_decay env from.etyp, pointer_decay env tto with
   | (TInt _ | TFloat _), (TInt _ | TFloat _) -> true
   | TInt _, TPtr _ -> is_literal_0 from
-  | TPtr(ty, _), TPtr(ty', _) ->
-      incl_attributes (attributes_of_type env ty) (attributes_of_type env ty')
+  | TPtr(sp, ty, _), TPtr(sp', ty', _) ->
+      valid_pointer_conv sp sp'
+      && incl_attributes (attributes_of_type env ty) (attributes_of_type env ty')
       && (is_void_type env ty || is_void_type env ty'
           || compatible_types env
                (erase_attributes_type env ty)
@@ -643 +650 @@
 (* Construct an integer constant *)
 
 let intconst v ik =
-  { edesc = EConst(CInt(v, ik, "")); etyp = TInt(ik, []) }
+  { edesc = EConst(CInt(v, ik, "")); etyp = TInt(ik, []); espace = Code }
 
 (* Construct a float constant *)
 
 let floatconst v fk =
-  { edesc = EConst(CFloat(v, fk, "")); etyp = TFloat(fk, []) }
+  { edesc = EConst(CFloat(v, fk, "")); etyp = TFloat(fk, []); espace = Code }
 
 (* Construct the literal "0" with void * type *)
 
 let nullconst =
-  { edesc = EConst(CInt(0L, ptr_t_ikind, "0")); etyp = TPtr(TVoid [], []) }
+  { edesc = EConst(CInt(0L, ptr_t_ikind, "0")); etyp = TPtr(Any, TVoid [], []); espace = Code } (* XXX *)
 
 (* Construct a sequence *)
 
@@ -667 +674 @@
 (* Construct an assignment statement *)
 
 let sassign loc lv rv =
-  { sdesc = Sdo {edesc = EBinop(Oassign, lv, rv, lv.etyp); etyp = lv.etyp};
+  { sdesc = Sdo {edesc = EBinop(Oassign, lv, rv, lv.etyp); etyp = lv.etyp; espace = lv.espace};
     sloc = loc }
 
 (* Empty location *)

cparser/Elab.ml

@@ -270 +270 @@
       | None -> elab_attributes loc al
       | Some a -> add_attributes [a] (elab_attributes loc al)
 
+let elab_attribute_space = function
+  | ("data", []) -> Some Data
+  | ("idata", []) -> Some IData
+  | ("pdata", []) -> Some PData
+  | ("xdata", []) -> Some XData
+  | ("code", []) -> Some Code
+  | _ -> None
+
+let rec elab_attributes_space loc attrs =
+  let rec aux = function
+    | [] -> None
+    | h::t -> (match elab_attribute_space h with
+                | None -> aux t
+                | Some v -> Some (v,t))
+  in match aux attrs with
+    | None -> Any
+    | Some (space, rest) ->
+       (match aux rest with 
+         | None -> ()
+         | Some _ -> warning loc "Multiple memory spaces given");
+       space
+
 (* Auxiliary for typespec elaboration *)
 
 let typespec_rank = function (* Don't change this *)
@@ -288 +310 @@
 
 let typespec_order t1 t2 = compare (typespec_rank t1) (typespec_rank t2)
 
+
 (* Elaboration of a type specifier.  Returns 4-tuple:
      (storage class, "inline" flag, elaborated type, new env)
    Optional argument "only" is true if this is a standalone
@@ -302 +325 @@
   let sto = ref Storage_default
   and inline = ref false
   and attr = ref []
-  and tyspecs = ref [] in
+  and tyspecs = ref []
+  and space = ref Any in
 
   let do_specifier = function
   | SpecTypedef -> ()
@@ -314 +338 @@
         | CV_RESTRICT -> ARestrict in
       attr := add_attributes [a] !attr
   | SpecAttr a ->
-      attr := add_attributes (elab_attributes loc [a]) !attr
+      attr := add_attributes (elab_attributes loc [a]) !attr;
+      (match elab_attribute_space a with
+        | None -> ()
+        | Some sp ->
+           if !space <> Any then
+             error loc "multiple memory space specifiers";
+           space := sp)
   | SpecStorage st ->
       if !sto <> Storage_default then
         error loc "multiple storage specifiers";
@@ -330 +360 @@
 
   List.iter do_specifier specifier;
 
-  let simple ty = (!sto, !inline, add_attributes_type !attr ty, env) in
+  let simple ty = (!space, !sto, !inline, add_attributes_type !attr ty, env) in
 
   (* Now interpret the list of type specifiers.  Much of this code
      is stolen from CIL. *)
@@ -394 +424 @@
         let (id', env') =
           elab_struct_or_union only Struct loc id optmembers env in
         let attr' = add_attributes !attr (elab_attributes loc a) in
-        (!sto, !inline, TStruct(id', attr'), env')
+        (!space, !sto, !inline, TStruct(id', attr'), env')
 
     | [Cabs.Tunion(id, optmembers, a)] ->
         let (id', env') =
           elab_struct_or_union only Union loc id optmembers env in
         let attr' = add_attributes !attr (elab_attributes loc a) in
-        (!sto, !inline, TUnion(id', attr'), env')
+        (!space, !sto, !inline, TUnion(id', attr'), env')
 
     | [Cabs.Tenum(id, optmembers, a)] ->
         let env' = 
           elab_enum loc id optmembers env in
         let attr' = add_attributes !attr (elab_attributes loc a) in
-        (!sto, !inline, TInt(enum_ikind, attr'), env')
+        (!space, !sto, !inline, TInt(enum_ikind, attr'), env')
 
     | [Cabs.TtypeofE _] ->
         fatal_error loc "GCC __typeof__ not supported"
@@ -419 +449 @@
 
 (* Elaboration of a type declarator.  *)
 
-and elab_type_declarator loc env ty = function
+and elab_type_declarator loc env space ty = function
   | Cabs.JUSTBASE ->
-      (ty, env)
+      (space, ty, env)
   | Cabs.PARENTYPE(attr1, d, attr2) ->
       (* XXX ignoring the distinction between attrs after and before *)
       let a = elab_attributes loc (attr1 @ attr2) in
-      elab_type_declarator loc env (add_attributes_type a ty) d
+      (* XXX ought to use space from attrs? *)
+      elab_type_declarator loc env space (add_attributes_type a ty) d
   | Cabs.ARRAY(d, attr, sz) ->
       let a = elab_attributes loc attr in
       let sz' =
@@ -440 +471 @@
             | None ->
                 error loc "array size is not a compile-time constant";
                 Some 1L in (* produces better error messages later *)
-       elab_type_declarator loc env (TArray(ty, sz', a)) d
+       elab_type_declarator loc env space (TArray(space, ty, sz', a)) d
   | Cabs.PTR(attr, d) ->
       let a = elab_attributes loc attr in
-       elab_type_declarator loc env (TPtr(ty, a)) d
+      let space' = elab_attributes_space loc attr in
+       elab_type_declarator loc env space' (TPtr(space, ty, a)) d
   | Cabs.PROTO(d, params, vararg) ->
        begin match unroll env ty with
        | TArray _ | TFun _ ->
@@ -451 +483 @@
        | _ -> ()
        end;
        let params' = elab_parameters env params in
-       elab_type_declarator loc env (TFun(ty, params', vararg, [])) d
+       elab_type_declarator loc env space (TFun(ty, params', vararg, [])) d
 
 (* Elaboration of parameters in a prototype *)
 
@@ -476 +508 @@
       "'extern' or 'static' storage not supported for function parameter";
   (* replace array and function types by pointer types *)
   let ty1 = argument_conversion env1 ty in
-  let (id', env2) = Env.enter_ident env1 id sto ty1 in
+  let (id', env2) = Env.enter_ident env1 id sto ty1 Any (* stack *) in
   ( (id', ty1) , env2 )
 
 (* Elaboration of a (specifier, Cabs "name") pair *)
 
 and elab_name env spec (id, decl, attr, loc) =
-  let (sto, inl, bty, env') = elab_specifier loc env spec in
-  let (ty, env'') = elab_type_declarator loc env' bty decl in 
+  let (space, sto, inl, bty, env') = elab_specifier loc env spec in
+  let (_, ty, env'') = elab_type_declarator loc env' space bty decl in 
   let a = elab_attributes loc attr in
   (id, sto, inl, add_attributes_type a ty, env'')
 
 (* Elaboration of a name group *)
 
 and elab_name_group env (spec, namelist) =
-  let (sto, inl, bty, env') =
+  let (space, sto, inl, bty, env') =
     elab_specifier (loc_of_namelist namelist) env spec in
   let elab_one_name env (id, decl, attr, loc) =
-    let (ty, env1) =
-      elab_type_declarator loc env bty decl in 
+    let (_, ty, env1) =
+      elab_type_declarator loc env space bty decl in 
     let a = elab_attributes loc attr in
     ((id, sto, add_attributes_type a ty), env1) in
   mmap elab_one_name env' namelist
@@ -502 +534 @@
 (* Elaboration of an init-name group *)
 
 and elab_init_name_group env (spec, namelist) =
-  let (sto, inl, bty, env') =
+  let (space, sto, inl, bty, env') =
     elab_specifier (loc_of_init_name_list namelist) env spec in
   let elab_one_name env ((id, decl, attr, loc), init) =
-    let (ty, env1) =
-      elab_type_declarator loc env bty decl in 
+    let (space', ty, env1) =
+      elab_type_declarator loc env space bty decl in 
     let a = elab_attributes loc attr in
-    ((id, sto, add_attributes_type a ty, init), env1) in
+    ((space', id, sto, add_attributes_type a ty, init), env1) in
   mmap elab_one_name env' namelist
 
 (* Elaboration of a field group *)
@@ -558 +590 @@
   (* Check for incomplete types *)
   let rec check_incomplete = function
   | [] -> ()
-  | [ { fld_typ = TArray(ty_elt, None, _) } ] when kind = Struct -> ()
+  | [ { fld_typ = TArray(_, ty_elt, None, _) } ] when kind = Struct -> ()
         (* C99: ty[] allowed as last field of a struct *)
   | fld :: rem ->
       if incomplete_type env' fld.fld_typ then
@@ -663 +695 @@
 (* Elaboration of a naked type, e.g. in a cast *)
 
 let elab_type loc env spec decl =
-  let (sto, inl, bty, env') = elab_specifier loc env spec in
-  let (ty, env'') = elab_type_declarator loc env' bty decl in 
+  let (space, sto, inl, bty, env') = elab_specifier loc env spec in
+  let (_, ty, env'') = elab_type_declarator loc env' space bty decl in 
   if sto <> Storage_default || inl then
     error loc "'extern', 'static', 'register' and 'inline' are meaningless in cast";
   ty
 
+
+let join_spaces s1 s2 =
+if s1 = s2 then s1 else Any
+
 
 
 (* Elaboration of expressions *)

cparser/Env.ml

@@ -70 +70 @@
 (* Infos associated with an ordinary identifier *)
 
 type ident_info =
-  | II_ident of storage * typ
+  | II_ident of storage * typ * memory_space
   | II_enum of int64                    (* value of the enum *)
 
 (* Infos associated with a typedef *)
@@ -201 +201 @@
 
 (* Inserting things by source name, with generation of a translated name *)
 
-let enter_ident env s sto ty =
+let enter_ident env s sto ty sp =
   let id = fresh_ident s in
   (id,
-   { env with env_ident = IdentMap.add id (II_ident(sto, ty)) env.env_ident })
+   { env with env_ident = IdentMap.add id (II_ident(sto, ty, sp)) env.env_ident })
 
 let enter_composite env s ci =
   let id = fresh_ident s in
@@ -220 +220 @@
 
 (* Inserting things by translated name *)
 
-let add_ident env id sto ty =
-  { env with env_ident = IdentMap.add id (II_ident(sto, ty)) env.env_ident }
+let add_ident env id sto ty sp =
+  { env with env_ident = IdentMap.add id (II_ident(sto, ty, sp)) env.env_ident }
 
 let add_composite env id ci =
   { env with env_tag = IdentMap.add id ci env.env_tag }

cparser/Env.mli

@@ -31 +31 @@
   ci_sizeof: int option;                (* size; None if incomplete *)
 }
 
-type ident_info = II_ident of C.storage * C.typ | II_enum of int64
+type ident_info = II_ident of C.storage * C.typ * C.memory_space | II_enum of int64
 
 type typedef_info = C.typ
 
@@ -60 +60 @@
 val find_union_member : t -> C.ident * string -> C.field
 val find_typedef : t -> C.ident -> typedef_info
 
-val enter_ident : t -> string -> C.storage -> C.typ -> C.ident * t
+val enter_ident : t -> string -> C.storage -> C.typ -> C.memory_space -> C.ident * t
 val enter_composite : t -> string -> composite_info -> C.ident * t
 val enter_enum_item : t -> string -> int64 -> C.ident * t
 val enter_typedef : t -> string -> typedef_info -> C.ident * t
 
-val add_ident : t -> C.ident -> C.storage -> C.typ -> t
+val add_ident : t -> C.ident -> C.storage -> C.typ -> C.memory_space -> t
 val add_composite : t -> C.ident -> composite_info -> t
 val add_typedef : t -> C.ident -> typedef_info -> t

cparser/GCC.ml

@@ -30 +30 @@
 let floatType = TFloat(FFloat, [])
 let doubleType = TFloat(FDouble, [])
 let longDoubleType = TFloat (FLongDouble, [])
-let voidPtrType = TPtr(TVoid [], [])
-let voidConstPtrType = TPtr(TVoid [AConst], [])
-let charPtrType = TPtr(TInt(IChar, []), [])
-let charConstPtrType = TPtr(TInt(IChar, [AConst]), [])
-let intPtrType = TPtr(TInt(IInt, []), [])
+let voidPtrType = TPtr(Any,TVoid [], [])
+let voidConstPtrType = TPtr(Any,TVoid [AConst], [])
+let charPtrType = TPtr(Any,TInt(IChar, []), [])
+let charConstPtrType = TPtr(Any,TInt(IChar, [AConst]), [])
+let intPtrType = TPtr(Any,TInt(IInt, []), [])
 let sizeType = TInt(size_t_ikind, [])
 
 let builtins = {
@@ -150 +150 @@
   "__builtin_log10l",  (longDoubleType, [ longDoubleType ], false);
 
   "__builtin_modff",  (floatType, [ floatType; 
-                                          TPtr(floatType,[]) ], false);
+                                          TPtr(Any,floatType,[]) ], false);
   "__builtin_modfl",  (longDoubleType, [ longDoubleType; 
-                                               TPtr(longDoubleType, []) ], 
+                                               TPtr(Any,longDoubleType, []) ], 
                              false);
 
   "__builtin_nan",  (doubleType, [ charConstPtrType ], false);

cparser/Lexer.mll

@@ -181 +181 @@
       ("__builtin_types_compatible_p", fun loc -> BUILTIN_TYPES_COMPAT loc);
       ("__builtin_offsetof", fun loc -> BUILTIN_OFFSETOF loc);
       (* On some versions of GCC __thread is a regular identifier *)
-      ("__thread", fun loc -> THREAD loc)
+      ("__thread", fun loc -> THREAD loc);
+      (* 8051 memory space extensions *)
+      ("__data", fun loc -> DATA loc);
+      ("__idata", fun loc -> IDATA loc);
+      ("__pdata", fun loc -> PDATA loc);
+      ("__xdata", fun loc -> XDATA loc);
+      ("__code", fun loc -> CODE loc);
     ]
 
 (* Mark an identifier as a type name. The old mapping is preserved and will 

cparser/Parser.mly

@@ -221 +221 @@
 %token<Cabs.cabsloc> VOLATILE EXTERN STATIC CONST RESTRICT AUTO REGISTER
 %token<Cabs.cabsloc> THREAD
 
+%token<Cabs.cabsloc> DATA IDATA PDATA XDATA CODE
+
 %token<Cabs.cabsloc> SIZEOF ALIGNOF
 
 %token EQ PLUS_EQ MINUS_EQ STAR_EQ SLASH_EQ PERCENT_EQ
@@ -1249 +1251 @@
 |   MSATTR                              { (fst $1, []), snd $1 }
                                         /* ISO 6.7.3 */
 |   THREAD                              { ("__thread",[]), $1 }
+
+|   DATA                                { ("data",[]), $1 }
+|   IDATA                               { ("idata",[]), $1 }
+|   PDATA                               { ("pdata",[]), $1 }
+|   XDATA                               { ("xdata",[]), $1 }
+|   CODE                                { ("code",[]), $1 }
 ;
 
 attribute_nocv_list:

cparser/Rename.ml

@@ -75 +75 @@
                        id.name id.stamp
 
 let rec typ env = function
-  | TPtr(ty, a) -> TPtr(typ env ty, a)
-  | TArray(ty, sz, a) -> TArray(typ env ty, sz, a)
+  | TPtr(sp, ty, a) -> TPtr(sp, typ env ty, a)
+  | TArray(sp, ty, sz, a) -> TArray(sp, typ env ty, sz, a)
   | TFun(res, None, va, a) -> TFun(typ env res, None, va, a)
   | TFun(res, Some p, va, a) ->
       let (p', _) = mmap param env p in
@@ -97 +97 @@
   | cst -> cst
 
 let rec exp env e =
-  { edesc = exp_desc env e.edesc; etyp = typ env e.etyp }
+  { edesc = exp_desc env e.edesc; etyp = typ env e.etyp; espace = e.espace }
 
 and exp_desc env = function
   | EConst cst -> EConst(constant env cst)
@@ -191 +191 @@
   ( { gdesc = desc'; gloc = g.gloc }, env' )
 
 and globdecl_desc env = function
-  | Gdecl d ->
+  | Gdecl (sp,d) ->
       let (d', env') = decl env d in
-      (Gdecl d', env')
+      (Gdecl (sp,d'), env')
   | Gfundef fd ->
       let (fd', env') = fundef env fd in
       (Gfundef fd', env')
@@ -230 +230 @@
   | dcl :: rem ->
       let env' =
         match dcl.gdesc with
-        | Gdecl(sto, id, _, _) ->
+        | Gdecl (_, (sto, id, _, _)) ->
             begin match sto with
             | Storage_default | Storage_extern -> enter_global env id
             | Storage_static -> env

cparser/SimplExpr.ml

@@ -92 +92 @@
 
   let eboolvalof e =
     { edesc = EBinop(One, e, intconst 0L IInt, TInt(IInt, []));
-      etyp = TInt(IInt, []) } in
+      etyp = TInt(IInt, []);
+      espace = Any } in
 
   let sseq s1 s2 = Cutil.sseq loc s1 s2 in
 
   let sassign e1 e2 =
-    { sdesc = Sdo {edesc = EBinop(Oassign, e1, e2, e1.etyp); etyp = e1.etyp}; 
+    { sdesc = Sdo {edesc = EBinop(Oassign, e1, e2, e1.etyp); etyp = e1.etyp; espace = e1.espace}; 
       sloc = loc } in
 
   let sif e s1 s2 =
@@ -149 +150 @@
 
         | Ominus | Oplus | Olognot | Onot | Oderef | Oarrow _ ->
             let (s1, e1') = simpl e1 RHS in
-            finish act s1 {edesc = EUnop(op, e1'); etyp = e.etyp}
+            finish act s1 {edesc = EUnop(op, e1'); etyp = e.etyp; espace = e.espace}
 
         | Oaddrof ->
             let (s1, e1') = simpl e1 LHS in
-            finish act s1 {edesc = EUnop(op, e1'); etyp = e.etyp}
+            finish act s1 {edesc = EUnop(op, e1'); etyp = e.etyp; espace = e.espace}
 
         | Odot _ ->
             let (s1, e1') = simpl e1 (if act = LHS then LHS else RHS) in
-            finish act s1 {edesc = EUnop(op, e1'); etyp = e.etyp}
+            finish act s1 {edesc = EUnop(op, e1'); etyp = e.etyp; espace = e.espace}
 
         | Opreincr | Opredecr ->
             let (s1, e1') = simpl e1 LHS in
@@ -165 +166 @@
             let op' = match op with Opreincr -> Oadd | _ -> Osub in
             let ty = unary_conversion env e.etyp in
             let e3 =
-              {edesc = EBinop(op', e2', intconst 1L IInt, ty); etyp = ty} in
+              {edesc = EBinop(op', e2', intconst 1L IInt, ty); etyp = ty; espace = Any} in
             begin match act with
             | Drop ->
                 (sseq s1 (sseq s2 (sassign e1' e3)), voidconst)
@@ -184 +185 @@
             | Drop ->
                 let (s2, e2') = lhs_to_rhs e1' in
                 let e3 =
-                  {edesc = EBinop(op', e2', intconst 1L IInt, ty); etyp = ty} in
+                  {edesc = EBinop(op', e2', intconst 1L IInt, ty); etyp = ty; espace = Any} in
                 (sseq s1 (sseq s2 (sassign e1' e3)), voidconst)
             | _ ->
                 let tmp = new_temp e.etyp in
                 let e3 =
-                  {edesc = EBinop(op', tmp, intconst 1L IInt, ty); etyp = ty} in
+                  {edesc = EBinop(op', tmp, intconst 1L IInt, ty); etyp = ty; espace = Any} in
                 finish act (sseq s1 (sseq (sassign tmp e1') (sassign e1' e3))) 
                        tmp
             end
@@ -205 +206 @@
             let (s1, e1') = simpl e1 RHS in
             let (s2, e2') = simpl e2 RHS in
             finish act (sseq s1 s2)
-                       {edesc = EBinop(op, e1', e2', ty); etyp = e.etyp}
+                       {edesc = EBinop(op, e1', e2', ty); etyp = e.etyp; espace = Any}
 
         | Oassign ->
             if act = Drop && is_simpl_expr e1 then
@@ -239 +240 @@
               | Oshl_assign -> Oshl    | Oshr_assign -> Oshr
               | _ -> assert false in
             let e3 =
-              { edesc = EBinop(op', e11', e2', ty); etyp = ty } in
+              { edesc = EBinop(op', e11', e2', ty); etyp = ty; espace = Any } in
             begin match act with
             | Drop ->
                 (sseq s1 (sseq s11 (sseq s2 (sassign e1' e3))), voidconst)
@@ -259 +260 @@
             let (s1, e1') = simpl e1 RHS in
             if is_simpl_expr e2 then begin
               finish act s1
-                     {edesc = EBinop(Ologand, e1', e2, ty); etyp = e.etyp}
+                     {edesc = EBinop(Ologand, e1', e2, ty); etyp = e.etyp; espace = e.espace}
             end else begin
               match act with
               | Drop ->
@@ -284 +285 @@
             let (s1, e1') = simpl e1 RHS in
             if is_simpl_expr e2 then begin
               finish act s1
-                     {edesc = EBinop(Ologor, e1', e2, ty); etyp = e.etyp}
+                     {edesc = EBinop(Ologor, e1', e2, ty); etyp = e.etyp; espace = e.espace}
             end else begin
               match act with
               | Drop ->
@@ -310 +311 @@
     | EConditional(e1, e2, e3) ->
         let (s1, e1') = simpl e1 RHS in
         if is_simpl_expr e2 && is_simpl_expr e3 then begin
-          finish act s1 {edesc = EConditional(e1', e2, e3); etyp = e.etyp}
+          finish act s1 {edesc = EConditional(e1', e2, e3); etyp = e.etyp; espace = e.espace}
         end else begin
           match act with
           | Drop ->
@@ -336 +337 @@
             simpl e1 act
         end else begin
           let (s1, e1') = simpl e1 RHS in
-          finish act s1 {edesc = ECast(ty, e1'); etyp = e.etyp}
+          finish act s1 {edesc = ECast(ty, e1'); etyp = e.etyp; espace = e.espace}
         end
 
     | ECall(e1, el) ->
         let (s1, e1') = simpl e1 RHS in
         let (s2, el') = simpl_list el in
-        let e2 = { edesc = ECall(e1', el'); etyp = e.etyp } in
+        let e2 = { edesc = ECall(e1', el'); etyp = e.etyp; espace = e.espace } in
         begin match act with
         | Drop ->
             (sseq s1 (sseq s2 {sdesc = Sdo e2; sloc=loc}), voidconst)
@@ -481 +482 @@
         let (s', _) = simpl_expr s.sloc env e (Set tmp) in
         let s_init =
           {sdesc = Sdo {edesc = EBinop(Oassign, tmp, intconst 1L IInt, tmp.etyp);
-                        etyp = tmp.etyp};
+                        etyp = tmp.etyp; espace = tmp.espace};
            sloc = s.sloc} in
         {sdesc = Sfor(s_init, tmp, s', simpl_stmt s1); sloc = s.sloc}
       end

cparser/StructAssign.ml

@@ -28 +28 @@
 let need_memcpy = ref (None: ident option)
 
 let memcpy_type =
-  TFun(TPtr(TVoid [], []),
-       Some [(Env.fresh_ident "", TPtr(TVoid [], []));
-             (Env.fresh_ident "", TPtr(TVoid [AConst], []));
+  TFun(TPtr(Any,TVoid [], []),
+       Some [(Env.fresh_ident "", TPtr(Any,TVoid [], []));
+             (Env.fresh_ident "", TPtr(Any,TVoid [AConst], []));
              (Env.fresh_ident "", TInt(size_t_ikind, []))],
        false, [])
 
@@ -43 +43 @@
   | Some id ->
       id 
 
+let space_of_ty = function
+| TArray(space, _, _, _)
+| TPtr(space, _, _) -> space
+| _ -> Any
+
 let transf_assign env loc lhs rhs =
 
   let num_assign = ref 0 in
@@ -62 +67 @@
         transf_struct l r ci.ci_members
     | TUnion(id, attr) ->
         raise Exit
-    | TArray(ty_elt, Some sz, attr) ->
-        transf_array l r ty_elt 0L sz
-    | TArray(ty_elt, None, attr) ->
+    | TArray(space, ty_elt, Some sz, attr) ->
+        transf_array space l (space_of_ty (unroll env r.etyp)) r ty_elt 0L sz
+    | TArray(space, ty_elt, None, attr) ->
         error "%a: Error: array of unknown size" formatloc loc;
         sskip                           (* will be ignored later *)
     | _ ->
@@ -73 +78 @@
   and transf_struct l r = function
     | [] -> sskip
     | f :: fl ->
-        sseq loc (transf {edesc = EUnop(Odot f.fld_name, l); etyp = f.fld_typ}
-                         {edesc = EUnop(Odot f.fld_name, r); etyp = f.fld_typ})
+        sseq loc (transf {edesc = EUnop(Odot f.fld_name, l); etyp = f.fld_typ; espace = l.espace}
+                         {edesc = EUnop(Odot f.fld_name, r); etyp = f.fld_typ; espace = r.espace})
                  (transf_struct l r fl)
 
-  and transf_array l r ty idx sz =
+  and transf_array lsp l rsp r ty idx sz =
     if idx >= sz then sskip else begin
       let e = intconst idx size_t_ikind in
-      sseq loc (transf {edesc = EBinop(Oindex, l, e, ty); etyp = ty}
-                       {edesc = EBinop(Oindex, r, e, ty); etyp = ty})
-               (transf_array l r ty (Int64.add idx 1L) sz)
+      sseq loc (transf {edesc = EBinop(Oindex, l, e, ty); etyp = ty; espace = lsp}
+                       {edesc = EBinop(Oindex, r, e, ty); etyp = ty; espace = rsp})
+               (transf_array lsp l rsp r ty (Int64.add idx 1L) sz)
     end
   in
 
   try
     transf lhs rhs
   with Exit ->
-    let memcpy = {edesc = EVar(memcpy_ident()); etyp = memcpy_type} in
-    let e_lhs = {edesc = EUnop(Oaddrof, lhs); etyp = TPtr(lhs.etyp, [])} in
-    let e_rhs = {edesc = EUnop(Oaddrof, rhs); etyp = TPtr(rhs.etyp, [])} in
-    let e_size = {edesc = ESizeof(lhs.etyp); etyp = TInt(size_t_ikind, [])} in
+    let memcpy = {edesc = EVar(memcpy_ident()); etyp = memcpy_type; espace = Any} in
+    (* XXX: casts required? *)
+    let e_lhs = {edesc = EUnop(Oaddrof, lhs); etyp = TPtr(Any, lhs.etyp, []); espace = Any} in
+    let e_rhs = {edesc = EUnop(Oaddrof, rhs); etyp = TPtr(Any, rhs.etyp, []); espace = Any} in
+    let e_size = {edesc = ESizeof(lhs.etyp); etyp = TInt(size_t_ikind, []); espace = Any} in
     {sdesc = Sdo {edesc = ECall(memcpy, [e_lhs; e_rhs; e_size]);
-                  etyp = TVoid[]};
+                  etyp = TVoid[]; espace = Any};
      sloc = loc}
 
 let rec transf_stmt env s =
@@ -136 +142 @@
   match !need_memcpy with
   | None -> p'
   | Some id ->
-      {gdesc = Gdecl(Storage_extern, id, memcpy_type, None); gloc = no_loc}
+      {gdesc = Gdecl(Code, (Storage_extern, id, memcpy_type, None)); gloc = no_loc}
       :: p'
 
 (* Horrible hack *)

cparser/StructByValue.ml

@@ -38 +38 @@
       let tres' = transf_type env tres in
       if is_composite_type env tres then begin
         let res = Env.fresh_ident "_res" in
-        TFun(TVoid [], Some((res, TPtr(tres', [])) :: args'), vararg, attr)
+        TFun(TVoid [], Some((res, TPtr(Any, tres', [])) :: args'), vararg, attr)
       end else
         TFun(tres', Some args', vararg, attr)
-  | TPtr(t1, attr) ->
+  | TPtr(sp, t1, attr) ->
       let t1' = transf_type env t1 in
-      if t1' = t1 then t else TPtr(transf_type env t1, attr)
-  | TArray(t1, sz, attr) ->
+      if t1' = t1 then t else TPtr(sp, transf_type env t1, attr)
+  | TArray(sp, t1, sz, attr) ->
       let t1' = transf_type env t1 in
-      if t1' = t1 then t else TArray(transf_type env t1, sz, attr)
+      if t1' = t1 then t else TArray(sp, transf_type env t1, sz, attr)
   | _ -> t
 
 and transf_funarg env (id, t) =
   let t = transf_type env t in
   if is_composite_type env t
-  then (id, TPtr(add_attributes_type [AConst] t, []))
+  then (id, TPtr(Any, add_attributes_type [AConst] t, []))
   else (id, t)
 
 (* Simple exprs: no change in structure, since calls cannot occur within,
@@ -60 +60 @@
 
 let rec transf_expr env e =
   { etyp = transf_type env e.etyp;
+    espace = e.espace;
     edesc = match e.edesc with
       | EConst c -> EConst c
       | ESizeof ty -> ESizeof (transf_type env ty)
@@ -104 +105 @@
 let transf_arg e =
   let e' = transf_expr e in
   if is_composite_type env e'.etyp
-  then {edesc = EUnop(Oaddrof, e'); etyp = TPtr(e'.etyp, [])}
+  then {edesc = EUnop(Oaddrof, e'); etyp = TPtr(Any, e'.etyp, []); espace = Any} (* XXX: this might require a cast? *)
   else e'
 in
 
@@ -118 +119 @@
 let rec transf_stmt s =
   match s.sdesc with
   | Sskip -> s
-  | Sdo {edesc = ECall(fn, args); etyp = ty} ->
+  | Sdo {edesc = ECall(fn, args); etyp = ty; espace = space} ->
       let fn = transf_expr fn in
       let args = List.map transf_arg args in
       if is_composite_type env ty then begin
         let tmp = new_temp ~name:"_res" ty in
-        let arg0 = {edesc = EUnop(Oaddrof, tmp); etyp = TPtr(ty, [])} in
-        {s with sdesc = Sdo {edesc = ECall(fn, arg0 :: args); etyp = TVoid []}}
+        let arg0 = {edesc = EUnop(Oaddrof, tmp); etyp = TPtr(Any, ty, []); espace = Any} in
+        {s with sdesc = Sdo {edesc = ECall(fn, arg0 :: args); etyp = TVoid []; espace = Any}}
       end else
-        {s with sdesc = Sdo {edesc = ECall(fn, args); etyp = ty}}
-  | Sdo {edesc = EBinop(Oassign, dst, {edesc = ECall(fn, args); etyp = ty}, _)} ->
+        {s with sdesc = Sdo {edesc = ECall(fn, args); etyp = ty; espace = space}}
+  | Sdo {edesc = EBinop(Oassign, dst, {edesc = ECall(fn, args); etyp = ty; espace = space}, _)} ->
       let dst = transf_expr dst in
       let fn = transf_expr fn in
       let args = List.map transf_arg args in
       let ty = transf_type ty in
       if is_composite_type env ty then begin
-        let arg0 = {edesc = EUnop(Oaddrof, dst); etyp = TPtr(dst.etyp, [])} in
-        {s with sdesc = Sdo {edesc = ECall(fn, arg0 :: args); etyp = TVoid []}}
+        let arg0 = {edesc = EUnop(Oaddrof, dst); etyp = TPtr(Any, dst.etyp, []); espace = Any} in
+        {s with sdesc = Sdo {edesc = ECall(fn, arg0 :: args); etyp = TVoid []; espace = Any}}
       end else
-        sassign s.sloc dst {edesc = ECall(fn, args); etyp = ty}
+        sassign s.sloc dst {edesc = ECall(fn, args); etyp = ty; espace = space}
   | Sdo e ->
       {s with sdesc = Sdo(transf_expr e)}
   | Sseq(s1, s2) ->
@@ -184 +185 @@
       let ty = transf_type env ty in
       if is_composite_type env ty then begin
         let id' = Env.fresh_ident id.name in
-        let ty' = TPtr(add_attributes_type [AConst] ty, []) in
+        let ty' = TPtr(Any, add_attributes_type [AConst] ty, []) in
         let (params', decls, init) = transf_prm params in
         ((id', ty') :: params',
          (Storage_default, id, ty, None) :: decls,
          sseq loc
-          (sassign loc {edesc = EVar id; etyp = ty}
-                       {edesc = EUnop(Oderef, {edesc = EVar id'; etyp = ty'});
-                        etyp = ty})
+          (sassign loc {edesc = EVar id; etyp = ty; espace = Any}
+                       {edesc = EUnop(Oderef, {edesc = EVar id'; etyp = ty'; espace = Any});
+                        etyp = ty;
+                        espace = Any})
           init)
       end else begin
         let (params', decls, init) = transf_prm params in
@@ -206 +208 @@
   let (ret1, params1, body1) =
     if is_composite_type env ret then begin
       let vres = Env.fresh_ident "_res" in
-      let tres = TPtr(ret, []) in
-      let eres = {edesc = EVar vres; etyp = tres} in
-      let eeres = {edesc = EUnop(Oderef, eres); etyp = ret} in
+      let tres = TPtr(Any, ret, []) in
+      let eres = {edesc = EVar vres; etyp = tres; espace = Any} in
+      let eeres = {edesc = EUnop(Oderef, eres); etyp = ret; espace = Any} in
       (TVoid [],
        (vres, tres) :: params,
        transf_funbody env f.fd_body (Some eeres))

cparser/Transform.ml

@@ -33 +33 @@
 
 let new_temp ?(name = "t") ty =
   let id = new_temp_var ~name ty in
-  { edesc = EVar id; etyp = ty }
+  { edesc = EVar id; etyp = ty; espace = Any (* Always stack allocated? *) }
 
 let get_temps () =
   let temps = !temporaries in
@@ -58 +58 @@
   | g :: gl ->
       let (desc', env') =
         match g.gdesc with
-        | Gdecl((sto, id, ty, init) as d) ->
-           (Gdecl(decl env d), Env.add_ident env id sto ty)
+        | Gdecl (sp, ((sto, id, ty, init) as d)) ->
+           (Gdecl(sp, decl env d), Env.add_ident env id sto ty sp)
         | Gfundef f ->
            (Gfundef(fundef env f),
-            Env.add_ident env f.fd_name f.fd_storage (fundef_typ f))
+            Env.add_ident env f.fd_name f.fd_storage (fundef_typ f) Code)
         | Gcompositedecl(su, id) ->
             (Gcompositedecl(su, id),
              Env.add_composite env id (composite_info_decl env su))

cparser/Unblock.ml

@@ -32 +32 @@
   match init with
   | Init_single e ->
       sdoseq loc
-        { edesc = EBinop(Oassign, path, e, path.etyp); etyp = path.etyp }
+        { edesc = EBinop(Oassign, path, e, path.etyp); etyp = path.etyp; espace = path.espace }
         k
   | Init_array il ->
-      let ty_elt =
+      let space, ty_elt =
         match unroll env path.etyp with
-        | TArray(ty_elt, _, _) -> ty_elt
+        | TArray(space, ty_elt, _, _) -> space, ty_elt
         | _ -> fatal_error "%aWrong type for array initializer" 
                            formatloc loc in
       let rec array_init pos = function
         | [] -> k
         | i :: il ->
             local_initializer loc env
-              { edesc = EBinop(Oindex, path, intconst pos IInt, TPtr(ty_elt, []));
-                etyp = ty_elt }
+              { edesc = EBinop(Oindex, path, intconst pos IInt, TPtr(space, ty_elt, []));
+                etyp = ty_elt;
+                espace = Any }
               i
               (array_init (Int64.succ pos) il) in
       array_init 0L il
   | Init_struct(id, fil) ->
       let field_init (fld, i) k =
         local_initializer loc env
-          { edesc = EUnop(Odot fld.fld_name, path); etyp = fld.fld_typ } 
+          { edesc = EUnop(Odot fld.fld_name, path); etyp = fld.fld_typ; espace = Any } 
           i k in
       List.fold_right field_init fil k
   | Init_union(id, fld, i) ->
       local_initializer loc env
-        { edesc = EUnop(Odot fld.fld_name, path); etyp = fld.fld_typ }
+        { edesc = EUnop(Odot fld.fld_name, path); etyp = fld.fld_typ; espace = Any }
         i k
 
 (* Record new variables to be locally defined *)
@@ -82 +83 @@
   match optinit with
   | None -> k
   | Some init ->
-      local_initializer loc env { edesc = EVar id; etyp = ty' } init k
+      local_initializer loc env { edesc = EVar id; etyp = ty'; espace = Any } init k
 
 (* Simplification of blocks within a statement *)
 

src/acc.ml

@@ -33 +33 @@
       src_language tgt_language input_ast
   in
   let final_ast, intermediate_asts = Misc.ListExt.cut_last target_asts in
-  let annotated_input_ast =  Languages.annotate input_ast final_ast in
-  Languages.save filename annotated_input_ast;
+  if Options.annotation_requested () then begin
+    let annotated_input_ast =  Languages.annotate input_ast final_ast in
+    Languages.save filename annotated_input_ast
+  end;
   Languages.save filename final_ast;
   if Options.is_debug_enabled () then 
     List.iter (Languages.save filename) intermediate_asts;
+  if Options.is_matita_output_enabled () then
+    Languages.save_matita filename (input_ast :: target_asts);
   if Options.interpretation_requested () || Options.is_debug_enabled () then begin
     let asts = input_ast :: target_asts in
     let label_traces = List.map Languages.interpret asts in

src/clight/clight.mli

@@ -7 +7 @@
 
 (** ** Types *)
 
+type memory_space = Any | Data | IData | PData | XData | Code
+
 (** Clight types are similar to those of C.  They include numeric types,
   pointers, arrays, function types, and composite types (struct and 
   union).  Numeric types (integers and floats) fully specify the
@@ -61 +63 @@
   | Tvoid                                       (**r the [void] type *)
   | Tint of intsize*signedness                  (**r integer types *)
   | Tfloat of floatsize                         (**r floating-point types *)
-  | Tpointer of ctype                           (**r pointer types ([*ty]) *)
-  | Tarray of ctype*int                         (**r array types ([ty[len]]) *)
+  | Tpointer of memory_space * ctype            (**r pointer types ([*ty]) *)
+  | Tarray of memory_space * ctype*int          (**r array types ([ty[len]]) *)
   | Tfunction of ctype list*ctype               (**r function types *)
   | Tstruct of ident*(ident*ctype) list
   (**r struct types *)
@@ -199 +201 @@
 type program = {
   prog_funct: (ident * fundef) list ;
   prog_main: ident;
-  prog_vars: ((ident * init_data list) * ctype) list
+  prog_vars: (((ident * init_data list) * memory_space) * ctype) list
 }

src/clight/clightFromC.ml

@@ -19 +19 @@
   | Tfloat F32 -> 4
   | Tfloat F64 -> 8
   | Tpointer _ -> 4
-  | Tarray (t',n) -> alignof t'
+  | Tarray (_,t',n) -> alignof t'
   | Tfunction (_,_) -> 1
   | Tstruct (_,fld) -> alignof_fields fld
   | Tunion (_,fld) -> alignof_fields fld
@@ -42 +42 @@
     | Tfloat F32 -> 4
     | Tfloat F64 -> 8
     | Tpointer _ -> 4
-    | Tarray (t',n) -> sizeof t' * max 1 n
+    | Tarray (_,t',n) -> sizeof t' * max 1 n
     | Tfunction (_,_) -> 1
     | Tstruct (_,fld) -> align (max 1 (sizeof_struct fld 0)) (alignof t)
     | Tunion (_,fld) -> align (max 1 (sizeof_union fld)) (alignof t)
@@ -102 +102 @@
     Hashtbl.add decl_atom id
       (env, (C.Storage_static,
              Env.fresh_ident name,
-             C.TPtr(C.TInt(C.IChar,[C.AConst]),[]),
+             C.TPtr(C.Any,C.TInt(C.IChar,[C.AConst]),[]),
              None));
     !define_stringlit_hook id;
     Hashtbl.add stringTable s id;
     id
 
 let typeStringLiteral s =
-  Tarray(Tint(I8, Unsigned), String.length s + 1)
+  Tarray(Code, Tint(I8, Unsigned), String.length s + 1)
 
 let global_for_string s id =
   let init = ref [] in
@@ -119 +119 @@
        :: !init in
   add_char '\000';
   for i = String.length s - 1 downto 0 do add_char s.[i] done;
-  ((id, !init), typeStringLiteral s)
+  (((id, !init), Code), typeStringLiteral s)
 
 let globals_for_strings globs =
   Hashtbl.fold
@@ -143 +143 @@
     let rec types_of_types = function
       | [] -> []
       | Tfloat(_)::tl -> Tfloat(F64)::(types_of_types tl)
-      | _::tl -> Tpointer(Tvoid)::(types_of_types tl) in
+      | _::tl -> Tpointer(Any,Tvoid)::(types_of_types tl) in
     let stub_type = Tfunction (types_of_types targs, tres) in
     Hashtbl.add stub_function_table stub_name stub_type;
     (stub_name, stub_type)
@@ -193 +193 @@
       if not !ClightFlags.option_flonglong then unsupported "'long double' type";
       F64
 
+let convertSpace = function
+  | C.Any -> Any
+  | C.Data -> Data
+  | C.IData -> IData
+  | C.PData -> PData
+  | C.XData -> XData
+  | C.Code -> Code
+
 let convertTyp env t =
 
   let rec convertTyp seen t =
@@ -202 +210 @@
         let (sg, sz) = convertIkind ik in Tint(sz, sg)
     | C.TFloat(fk, a) ->
         Tfloat(convertFkind fk)
-    | C.TPtr(C.TStruct(id, _), _) when List.mem id seen ->
+    | C.TPtr(_,C.TStruct(id, _), _) when List.mem id seen ->
         Tcomp_ptr("struct " ^ id.name)
-    | C.TPtr(C.TUnion(id, _), _) when List.mem id seen ->
+    | C.TPtr(_,C.TUnion(id, _), _) when List.mem id seen ->
         Tcomp_ptr("union " ^ id.name)
-    | C.TPtr(ty, a) ->
-        Tpointer(convertTyp seen ty)
-    | C.TArray(ty, None, a) ->
+    | C.TPtr(sp,ty, a) ->
+        Tpointer(convertSpace sp, convertTyp seen ty)
+    | C.TArray(sp, ty, None, a) ->
         (* Cparser verified that the type ty[] occurs only in
            contexts that are safe for Clight, so just treat as ty[0]. *)
         (* warning "array type of unspecified size"; *)
-        Tarray(convertTyp seen ty, 0)
-    | C.TArray(ty, Some sz, a) ->
-        Tarray(convertTyp seen ty, convertInt sz )
+        Tarray(convertSpace sp, convertTyp seen ty, 0)
+    | C.TArray(sp, ty, Some sz, a) ->
+        Tarray(convertSpace sp, convertTyp seen ty, convertInt sz )
     | C.TFun(tres, targs, va, a) ->
         if va then unsupported "variadic function type";
         if Cutil.is_composite_type env tres then
@@ -298 +306 @@
       let e1' = convertExpr env e1 in
       let ty1 =
         match typeof e1' with
-        | Tpointer t -> t
+        | Tpointer (_,t) -> t
         | _ -> error ("wrong type for ->" ^ id ^ " access"); Tvoid in
       Expr(Efield(Expr(Ederef(convertExpr env e1), ty1),
                    id), ty)
@@ -315 +323 @@
 
   | C.EBinop(C.Oindex, e1, e2, _) ->
       Expr(Ederef(Expr(Ebinop(Oadd, convertExpr env e1, convertExpr env e2),
-                       Tpointer ty)), ty)
+                       convertTyp env e1.etyp)), ty)
   | C.EBinop(C.Ologand, e1, e2, _) ->
       Expr(Eandbool(convertExpr env e1, convertExpr env e2), ty)
   | C.EBinop(C.Ologor, e1, e2, _) ->
@@ -354 +362 @@
 let rec projFunType env ty =
   match Cutil.unroll env ty with
   | TFun(res, args, vararg, attr) -> Some(res, vararg)
-  | TPtr(ty', attr) -> projFunType env ty'
+  | TPtr(_, ty', attr) -> projFunType env ty'
   | _ -> None
 
 let convertFuncall env lhs fn args =
@@ -400 +408 @@
   | Tfloat F32 -> ("float32", ty)
   | Tfloat F64 -> ("float64", ty)
   | Tpointer _ | Tarray _ | Tfunction _ | Tcomp_ptr _ ->
-      ("pointer", Tpointer Tvoid)
+      ("pointer", Tpointer (Any, Tvoid)) (* XXX: what is the pointer is to a different space? *)
   | _ ->
       unsupported "operation on volatile struct or union"; ("", Tvoid)
 
 let volatile_read_fun ty =
   let (suffix, ty') = volatile_fun_suffix_type ty in
   Expr(Evar( ("__builtin_volatile_read_" ^ suffix)),
-       Tfunction((Tpointer Tvoid)::[], ty'))
+       Tfunction((Tpointer (Any,Tvoid))::[], ty'))
 
 let volatile_write_fun ty =
   let (suffix, ty') = volatile_fun_suffix_type ty in
   Expr(Evar( ("__builtin_volatile_write_" ^ suffix)),
-       Tfunction((Tpointer Tvoid)::(ty'::[]), Tvoid))
+       Tfunction((Tpointer (Any,Tvoid))::(ty'::[]), Tvoid))
 
 (* Toplevel expression, argument of an Sdo *)
 
@@ -432 +440 @@
       | false, true ->                  (* volatile read *)
           Scall(Some lhs',
                 volatile_read_fun (typeof rhs'),
-                [ Expr (Eaddrof rhs', Tpointer (typeof rhs')) ])
+                [ Expr (Eaddrof rhs', Tpointer (Any (* XXX ? *), typeof rhs')) ])
       | true, false ->                  (* volatile write *)
           Scall(None,
                 volatile_write_fun (typeof lhs'),
-                [ Expr(Eaddrof lhs', Tpointer (typeof lhs')); rhs' ])
+                [ Expr(Eaddrof lhs', Tpointer (Any (* XXX ? *), typeof lhs')); rhs' ])
       | false, false ->                 (* regular assignment *)
           Sassign(convertExpr env lhs, convertExpr env rhs)
       end
@@ -663 +671 @@
   | Init_array il ->
       let ty_elt =
         match Cutil.unroll env ty with
-        | C.TArray(t, _, _) -> t
+        | C.TArray(_, t, _, _) -> t
         | _ -> error "array type expected in initializer"; C.TVoid [] in
       List.iter (cvtInit ty_elt) il
   | Init_struct(_, flds) ->
@@ -690 +698 @@
 
 (** Global variable *)
 
-let convertGlobvar env (sto, id, ty, optinit as decl) =
+let convertGlobvar env space (sto, id, ty, optinit as decl) =
   let id' =  id.name in
   let ty' = convertTyp env ty in 
   let init' =
@@ -701 +709 @@
         convertInit env ty i in
   Hashtbl.add decl_atom id' (env, decl);
   !define_variable_hook id' decl;
-  ((id', init'), ty')
+  (((id', init'), convertSpace space), ty')
 
 (** Convert a list of global declarations.
   Result is a pair [(funs, vars)] where [funs] are 
@@ -714 +722 @@
   | g :: gl' ->
       updateLoc g.gloc;
       match g.gdesc with
-      | C.Gdecl((sto, id, ty, optinit) as d) ->
+      | C.Gdecl(space, ((sto, id, ty, optinit) as d)) ->
           (* Prototyped functions become external declarations.
              Variadic functions are skipped.
              Other types become variable declarations. *)
@@ -727 +735 @@
           | TFun(_, _, true, _) ->
               convertGlobdecls env funs vars gl'
           | _ ->
-              convertGlobdecls env funs (convertGlobvar env d :: vars) gl'
+              convertGlobdecls env funs (convertGlobvar env space d :: vars) gl'
           end
       | C.Gfundef fd ->
           convertGlobdecls env (convertFundef env fd :: funs) vars gl'
@@ -769 +777 @@
     | g :: gl ->
         updateLoc g.gloc;
         match g.gdesc with
-        | C.Gdecl(sto, id, ty, None) ->
+        | C.Gdecl(_, (sto, id, ty, None)) ->
             if IdentSet.mem id defs
             then clean defs accu gl
             else clean (IdentSet.add id defs) (g :: accu) gl
-        | C.Gdecl(_, id, ty, _) ->
+        | C.Gdecl(_, (_, id, ty, _)) ->
             if IdentSet.mem id defs then
               error ("multiple definitions of " ^ id.name);
             clean (IdentSet.add id defs) (g :: accu) gl
@@ -815 +823 @@
   if List.mem C.AVolatile a then false else
   if List.mem C.AConst a then true else
   match Cutil.unroll env t with
-  | C.TArray(t', _, _) -> type_is_readonly env t'
+  | C.TArray(_, t', _, _) -> type_is_readonly env t'
   | _ -> false
 
 let atom_is_static a =
@@ -853 +861 @@
 let builtins_generic = {
   typedefs = [
     (* keeps GCC-specific headers happy, harmless for others *)
-    "__builtin_va_list", C.TPtr(C.TVoid [], [])
+    "__builtin_va_list", C.TPtr(C.Any, C.TVoid [], [])
   ];
   functions = [
     (* The volatile read/volatile write functions *)
     "__builtin_volatile_read_int8unsigned",
-        (TInt(IUChar, []), [TPtr(TVoid [], [])], false);
+        (TInt(IUChar, []), [TPtr(C.Any, TVoid [], [])], false);
     "__builtin_volatile_read_int8signed",
-        (TInt(ISChar, []), [TPtr(TVoid [], [])], false);
+        (TInt(ISChar, []), [TPtr(C.Any, TVoid [], [])], false);
     "__builtin_volatile_read_int16unsigned",
-        (TInt(IUShort, []), [TPtr(TVoid [], [])], false);
+        (TInt(IUShort, []), [TPtr(C.Any, TVoid [], [])], false);
     "__builtin_volatile_read_int16signed",
-        (TInt(IShort, []), [TPtr(TVoid [], [])], false);
+        (TInt(IShort, []), [TPtr(C.Any, TVoid [], [])], false);
     "__builtin_volatile_read_int32",
-        (TInt(IInt, []), [TPtr(TVoid [], [])], false);
+        (TInt(IInt, []), [TPtr(C.Any, TVoid [], [])], false);
     "__builtin_volatile_read_float32",
-        (TFloat(FFloat, []), [TPtr(TVoid [], [])], false);
+        (TFloat(FFloat, []), [TPtr(C.Any, TVoid [], [])], false);
     "__builtin_volatile_read_float64",
-         (TFloat(FDouble, []), [TPtr(TVoid [], [])], false);
+         (TFloat(FDouble, []), [TPtr(C.Any, TVoid [], [])], false);
     "__builtin_volatile_read_pointer",
-         (TPtr(TVoid [], []), [TPtr(TVoid [], [])], false);
+         (TPtr(C.Any, TVoid [], []), [TPtr(C.Any, TVoid [], [])], false);
     "__builtin_volatile_write_int8unsigned",
-        (TVoid [], [TPtr(TVoid [], []); TInt(IUChar, [])], false);
+        (TVoid [], [TPtr(C.Any, TVoid [], []); TInt(IUChar, [])], false);
     "__builtin_volatile_write_int8signed",
-        (TVoid [], [TPtr(TVoid [], []); TInt(ISChar, [])], false);
+        (TVoid [], [TPtr(C.Any, TVoid [], []); TInt(ISChar, [])], false);
     "__builtin_volatile_write_int16unsigned",
-        (TVoid [], [TPtr(TVoid [], []); TInt(IUShort, [])], false);
+        (TVoid [], [TPtr(C.Any, TVoid [], []); TInt(IUShort, [])], false);
     "__builtin_volatile_write_int16signed",
-        (TVoid [], [TPtr(TVoid [], []); TInt(IShort, [])], false);
+        (TVoid [], [TPtr(C.Any, TVoid [], []); TInt(IShort, [])], false);
     "__builtin_volatile_write_int32",
-        (TVoid [], [TPtr(TVoid [], []); TInt(IInt, [])], false);
+        (TVoid [], [TPtr(C.Any, TVoid [], []); TInt(IInt, [])], false);
     "__builtin_volatile_write_float32",
-        (TVoid [], [TPtr(TVoid [], []); TFloat(FFloat, [])], false);
+        (TVoid [], [TPtr(C.Any, TVoid [], []); TFloat(FFloat, [])], false);
     "__builtin_volatile_write_float64",
-         (TVoid [], [TPtr(TVoid [], []); TFloat(FDouble, [])], false);
+         (TVoid [], [TPtr(C.Any, TVoid [], []); TFloat(FDouble, [])], false);
     "__builtin_volatile_write_pointer",
-         (TVoid [], [TPtr(TVoid [], []); TPtr(TVoid [], [])], false)
+         (TVoid [], [TPtr(C.Any, TVoid [], []); TPtr(C.Any, TVoid [], [])], false)
   ]
 }
 

src/clight/clightInterpret.ml

@@ -29 +29 @@
   | Tfloat F32 -> 4
   | Tfloat F64 -> 8
   | Tpointer _ -> 4                     
-  | Tarray (_,_) -> 4                     
+  | Tarray _ -> 4                         
   | Tfunction (_,_) -> assert false
   | Tstruct (_,_) -> assert false 
   | Tunion (_,_) -> assert false
@@ -46 +46 @@
   | Tfloat F32 -> assert false 
   | Tfloat F64 -> Memory.MQ_float64
   | Tpointer _ -> Memory.MQ_int32                       
-  | Tarray (c,s) -> Memory.MQ_int32
+  | Tarray (_,c,s) -> Memory.MQ_int32
   | Tfunction (_,_) -> assert false 
   | Tstruct (_,_) -> assert false 
   | Tunion (_,_) -> assert false
@@ -207 +207 @@
   | (Value.Val_float f,_,Tfloat F64) -> Value.Val_float f
   (* Cast pointeur *)
   | (Value.Val_ptr (b,o),_,Tpointer _) -> Value.Val_ptr (b,o)
-  | (Value.Val_ptr (b,o),_,Tarray(_,_)) -> Value.Val_ptr (b,o)
+  | (Value.Val_ptr (b,o),_,Tarray _) -> Value.Val_ptr (b,o)
   (* no cast *)
   | (e,a,b) when a=b -> e
   (* error *)
@@ -232 +232 @@
       Value.Val_int (cast_int (i1+i2) t1)     
   | ((Value.Val_float i1,Tfloat F64) , (Value.Val_float i2,Tfloat F64)) ->
       Value.Val_float (i1+.i2)
-  | ((Value.Val_int i,_) , (Value.Val_ptr (b,o),Tarray(t,_))) ->
+  | ((Value.Val_int i,_) , (Value.Val_ptr (b,o),Tarray(_,t,_))) ->
       Value.Val_ptr (b,o+(i*(sizeof t)))
-  | ((Value.Val_ptr (b,o),Tarray(t,_)) , (Value.Val_int i,_)) ->
+  | ((Value.Val_ptr (b,o),Tarray(_,t,_)) , (Value.Val_int i,_)) ->
       Value.Val_ptr (b,o+(i*(sizeof t)))
-  | ((Value.Val_int i,_) , (Value.Val_ptr (b,o),Tpointer t)) ->
+  | ((Value.Val_int i,_) , (Value.Val_ptr (b,o),Tpointer (_,t))) ->
       Value.Val_ptr (b,o+(i*(sizeof t)))
-  | ((Value.Val_ptr (b,o),Tpointer t) , (Value.Val_int i,_)) ->
+  | ((Value.Val_ptr (b,o),Tpointer (_,t)) , (Value.Val_int i,_)) ->
       Value.Val_ptr (b,o+(i*(sizeof t)))
   | ((v1,_),(v2,_)) -> 
       print_string ("Debug: add "^(Value.string_of_value v1)^" with "
@@ -250 +250 @@
       Value.Val_int (cast_int (i1-i2) t1)    
   | ((Value.Val_float i1,Tfloat F64) , (Value.Val_float i2,Tfloat F64)) ->
       Value.Val_float (i1-.i2)
-  | ((Value.Val_int i,_) , (Value.Val_ptr (b,o),Tarray(t,_))) ->
+  | ((Value.Val_int i,_) , (Value.Val_ptr (b,o),Tarray(_,t,_))) ->
       Value.Val_ptr (b,o-(i*(sizeof t)))
-  | ((Value.Val_ptr (b,o),Tarray(t,_)) , (Value.Val_int i,_)) ->
+  | ((Value.Val_ptr (b,o),Tarray(_,t,_)) , (Value.Val_int i,_)) ->
       Value.Val_ptr (b,o-(i*(sizeof t)))
-  | ((Value.Val_int i,_) , (Value.Val_ptr (b,o),Tpointer t)) ->
+  | ((Value.Val_int i,_) , (Value.Val_ptr (b,o),Tpointer (_,t))) ->
       Value.Val_ptr (b,o-(i*(sizeof t)))
-  | ((Value.Val_ptr (b,o),Tpointer t) , (Value.Val_int i,_)) ->
+  | ((Value.Val_ptr (b,o),Tpointer (_,t)) , (Value.Val_int i,_)) ->
       Value.Val_ptr (b,o-(i*(sizeof t)))
   | _ -> assert false
 
@@ -475 +475 @@
     | _ -> assert false
   and treat_v (m,e) = function
     | [] -> (m,e)
-    | (id,Tarray(c,n))::l -> 
+    | (id,Tarray(s,c,n))::l -> 
         (match alloc m 0 (n*(sizeof c)) with
-           | Some(b,m') -> treat_v (bind m' e (id,Tarray(c,n)) (Value.Val_ptr(b,0)) ) l
+           | Some(b,m') -> treat_v (bind m' e (id,Tarray(s,c,n)) (Value.Val_ptr(b,0)) ) l
            | None -> assert false)
     | var::l -> treat_v (bind m e var Value.Val_undef) l
   in treat_v (treat_p (m,(Hashtbl.create 11)) (param_l,arg_l)) var_l

new file src/clight/clightPrintMatita.ml

@@ +1 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Pretty-printer for Csyntax *)
+
+open Format
+open AST
+open Clight
+
+(* If there's name hiding this might get us into trouble. *)
+let ident_map = Hashtbl.create 13;;
+let ident_next = ref 0;;
+let id_i n =
+  try Hashtbl.find ident_map n
+  with Not_found ->
+    let i = !ident_next in
+    Hashtbl.add ident_map n i;
+    ident_next := i+1;
+    i
+let id_s n = string_of_int (id_i n)
+
+let print_list f fmt l =
+  let rec aux fmt = function
+      | [] -> ()
+      | [x] -> f fmt x
+      | h::t -> f fmt h; fprintf fmt ";@ "; aux fmt t
+  in
+  fprintf fmt "@[[%a]@]" aux l
+
+let name_unop = function
+  | Onotbool -> "Onotbool"
+  | Onotint  -> "Onotint"
+  | Oneg     -> "Oneg"
+
+
+let name_binop = function
+  | Oadd -> "Oadd"
+  | Osub -> "Osub"
+  | Omul -> "Omul"
+  | Odiv -> "Odiv"
+  | Omod -> "Omod"
+  | Oand -> "Oand"
+  | Oor  -> "Oor"
+  | Oxor -> "Oxor"
+  | Oshl -> "Oshl"
+  | Oshr -> "Oshr"
+  | Oeq  -> "Oeq"
+  | One  -> "One"
+  | Olt  -> "Olt"
+  | Ogt  -> "Ogt"
+  | Ole  -> "Ole"
+  | Oge  -> "Oge"
+
+let name_inttype sz sg =
+  match sz, sg with
+  | I8, Signed    -> "I8 Signed   "
+  | I8, Unsigned  -> "I8 Unsigned "
+  | I16, Signed   -> "I16 Signed  "
+  | I16, Unsigned -> "I16 Unsigned"
+  | I32, Signed   -> "I32 Signed  "
+  | I32, Unsigned -> "I32 Unsigned"
+
+let name_floattype sz =
+  match sz with
+  | F32 -> "F32"
+  | F64 -> "F64"
+
+(* Collecting the names and fields of structs and unions *)
+
+module StructUnionSet = Set.Make(struct
+  type t = string * (ident*ctype) list
+  let compare (n1, _ : t) (n2, _ : t) = compare n1 n2
+end)
+
+let struct_unions = ref StructUnionSet.empty
+
+let register_struct_union id fld =
+  struct_unions := StructUnionSet.add (id, fld) !struct_unions
+
+(* Declarator (identifier + type) *)
+
+let name_optid id =
+  if id = "" then "" else " " ^ id
+
+let parenthesize_if_pointer id =
+  if String.length id > 0 && id.[0] = '*' then "(" ^ id ^ ")" else id
+
+let rec name_cdecl id ty =
+  match ty with
+  | Tvoid ->
+      "void" ^ name_optid id
+  | Tint(sz, sg) ->
+      name_inttype sz sg ^ name_optid id
+  | Tfloat sz ->
+      name_floattype sz ^ name_optid id
+  | Tpointer (s,t) -> (* XXX *)
+      name_cdecl ("*" ^ id) t
+  | Tarray(s, t, n) -> (* XXX *)
+      name_cdecl
+        (sprintf "%s[%d]" (parenthesize_if_pointer id) n)
+        t
+  | Tfunction(args, res) ->
+      let b = Buffer.create 20 in
+      if id = ""
+      then Buffer.add_string b "(*)"
+      else Buffer.add_string b (parenthesize_if_pointer id);
+      Buffer.add_char b '(';
+      begin match args with
+      | [] ->
+          Buffer.add_string b "void"
+      | _ ->
+          let rec add_args first = function
+          | [] -> ()
+          | t1::tl ->
+              if not first then Buffer.add_string b ", ";
+              Buffer.add_string b (name_cdecl "" t1);
+              add_args false tl in
+          add_args true args
+      end;
+      Buffer.add_char b ')';
+      name_cdecl (Buffer.contents b) res
+  | Tstruct(name, fld) ->
+      name ^ name_optid id
+  | Tunion(name, fld) ->
+      name ^ name_optid id
+  | Tcomp_ptr name ->
+      name ^ " *" ^ id
+
+(* Type *)
+
+let sspace = function
+| Any -> "Any"
+| Data -> "Data"
+| IData -> "IData"
+| PData -> "PData"
+| XData -> "XData"
+| Code -> "Code"
+
+let rec stype ty =
+  match ty with
+  | Tvoid -> "Tvoid"
+  | Tint(sz, sg) -> "(Tint " ^ name_inttype sz sg ^ ")"
+  | Tfloat sz -> "(Tfloat " ^ name_floattype sz ^ ")"
+  | Tpointer (sp, t) -> "(Tpointer " ^ sspace sp ^ " " ^ stype t ^ ")"
+  | Tarray(sp, t, n) -> "(Tarray " ^ sspace sp ^ " " ^ stype t ^ " " ^ (string_of_int n) ^ ")"
+  | Tfunction(args, res) -> "(Tfunction " ^ typelist args ^ " " ^ stype res ^ ")"
+  | Tstruct(name, fld) ->
+      fieldlist "(Tstruct (succ_pos_of_nat " name fld
+  | Tunion(name, fld) ->
+      fieldlist "(Tunion (succ_pos_of_nat " name fld
+  | Tcomp_ptr name ->
+      "(Tcomp_ptr (succ_pos_of_nat " ^ id_s name ^ "))"
+ and typelist l =
+    let b = Buffer.create 20 in
+      let rec add_types = function
+        | [] -> Buffer.add_string b "Tnil"
+        | t1::tl ->
+            Buffer.add_string b "(Tcons ";
+            Buffer.add_string b (stype t1);
+            Buffer.add_char b ' ';
+            add_types tl;
+            Buffer.add_char b ')'
+      in add_types l;
+        Buffer.contents b
+ and fieldlist s name l =
+    let b = Buffer.create 20 in
+      Buffer.add_string b s;
+      Buffer.add_string b (id_s name);
+      Buffer.add_string b ") ";
+      let rec add_fields = function
+        | [] -> Buffer.add_string b "Fnil"
+        | (id, ty)::tl ->
+            Buffer.add_string b "(Fcons (succ_pos_of_nat ";
+            Buffer.add_string b (id_s id);
+            Buffer.add_string b ") ";
+            Buffer.add_string b (stype ty);
+            Buffer.add_char b ' ';
+            add_fields tl;
+            Buffer.add_char b ')'
+      in add_fields l;
+        Buffer.add_char b ')';
+        Buffer.contents b
+
+let name_type ty = name_cdecl "" ty
+
+(* Expressions *)
+
+let rec print_expr p (Expr (eb, ty)) =
+  fprintf p "@[<hov 2>(Expr %a@ %s)@]" print_expr_descr eb (stype ty)
+and print_expr_descr p eb =
+  match eb with
+  | Ecost (_, Expr (e, _)) -> print_expr_descr p e
+  | Econst_int n ->
+      fprintf p "(Econst_int (repr %d))" n
+  | Econst_float f ->
+      fprintf p "(Econst_float %F)" f
+  | Evar id ->
+      fprintf p "(Evar (succ_pos_of_nat %d))" (id_i id)
+  | Eunop(op, e1) ->
+      fprintf p "(Eunop %s %a)" (name_unop op) print_expr e1
+  | Ederef e ->
+      fprintf p "(Ederef@ %a)" print_expr e
+  | Eaddrof e ->
+      fprintf p "(Eaddrof@ %a)" print_expr e
+  | Ebinop(op, e1, e2) ->
+      fprintf p "(Ebinop@ %s@ %a@ %a)"
+                (name_binop op)
+                print_expr e1
+                print_expr e2
+  | Ecast(ty, e1) ->
+      fprintf p "(Ecast %s@ %a)"
+                (stype ty)
+                print_expr e1
+  | Econdition(e1, e2, e3) ->
+      fprintf p "(Econdition %a@ %a@ %a)"
+                print_expr e1
+                print_expr e2
+                print_expr e3
+  | Eandbool(e1, e2) ->
+      fprintf p "(Eandbool %a@ %a)"
+                print_expr e1
+                print_expr e2
+  | Eorbool(e1, e2) ->
+      fprintf p "(Eorbool %a@ %a)"
+                print_expr e1
+                print_expr e2
+  | Esizeof ty ->
+      fprintf p "(Esizeof %s)" (stype ty)
+  | Efield(e1, id) ->
+      fprintf p "(Efield %a (succ_pos_of_nat %i))" print_expr e1 (id_i id)
+
+let rec print_expr_list p (first, el) =
+  match el with
+  | [] -> ()
+  | e1 :: et ->
+      if not first then fprintf p ",@ ";
+      print_expr p e1;
+      print_expr_list p (false, et)
+
+let rec print_stmt p s =
+  match s with
+  | Scost (_, s') -> print_stmt p s'
+  | Sskip ->
+      fprintf p "Sskip"
+  | Sassign(e1, e2) ->
+      fprintf p "@[<hv 2>(Sassign %a@ %a)@]" print_expr e1 print_expr e2
+  | Scall(None, e1, el) ->
+      fprintf p "@[<hv 2>(Scall (None ?) %a @[<hov 0>%a@])@]"
+                print_expr e1
+                (print_list print_expr) el
+  | Scall(Some lhs, e1, el) ->
+      fprintf p "@[<hv 2>(Scall (Some ? %a)@ %a@ @[<hov 0>%a@])@]"
+                print_expr lhs
+                print_expr e1
+                (print_list print_expr) el
+  | Ssequence(s1, s2) ->
+      fprintf p "(Ssequence@ %a@ %a)" print_stmt s1 print_stmt s2
+  | Sifthenelse(e, s1, s2) ->
+      fprintf p "@[<v 2>(Sifthenelse %a@ %a@ %a)@]"
+              print_expr e
+              print_stmt s1
+              print_stmt s2
+  | Swhile(e, s) ->
+      fprintf p "@[<v 2>(Swhile %a@ %a)@]"
+              print_expr e
+              print_stmt s
+  | Sdowhile(e, s) ->
+      fprintf p "@[<v 2>S(dowhile %a@ %a)@]"
+              print_expr e
+              print_stmt s
+  | Sfor(s_init, e, s_iter, s_body) ->
+      fprintf p "@[<v 2>(Sfor %a@ %a@ %a@\n%a@;<0 -2>)@]"
+              print_stmt s_init
+              print_expr e
+              print_stmt s_iter
+              print_stmt s_body
+  | Sbreak ->
+      fprintf p "Sbreak"
+  | Scontinue ->
+      fprintf p "Scontinue"
+  | Sswitch(e, cases) ->
+      fprintf p "@[<v 2>(Sswitch %a (@ %a@;<0 -2>))@]"
+              print_expr e
+              print_cases cases
+  | Sreturn None ->
+      fprintf p "(Sreturn (None ?))"
+  | Sreturn (Some e) ->
+      fprintf p "(Sreturn (Some ? %a))" print_expr e
+  | Slabel(lbl, s1) ->
+      fprintf p "(Slabel (succ_pos_of_nat %i)@ %a)" (id_i lbl) print_stmt s1
+  | Sgoto lbl ->
+      fprintf p "(Sgoto (succ_pos_of_nat %i))" (id_i lbl)
+
+and print_cases p cases =
+  match cases with
+  | LSdefault s ->
+      fprintf p "@[<v 2>(LSdefault@ %a)@]" print_stmt s
+  | LScase(lbl, s, rem) ->
+      fprintf p "@[<v 2>(LScase (repr %d)@ %a@ %a)@]"
+              lbl
+              print_stmt s
+              print_cases rem
+
+let name_function_parameters params =
+  let b = Buffer.create 20 in
+  Buffer.add_char b '[';
+    let rec add_params first = function
+      | [] -> ()
+      | (id, ty) :: rem ->
+          if not first then Buffer.add_string b "; ";
+          Buffer.add_string b "mk_pair ?? (succ_pos_of_nat ";
+          Buffer.add_string b (id_s id);
+          Buffer.add_string b ") ";
+          Buffer.add_string b (stype ty);
+          add_params false rem in
+      add_params true params;
+      Buffer.add_char b ']';
+      Buffer.contents b
+
+let print_function p f =
+  fprintf p "@[<v 2>mk_function %s %s %s@ " (stype f.fn_return)
+    (name_function_parameters f.fn_params)
+    (name_function_parameters f.fn_vars);
+  print_stmt p f.fn_body;
+  fprintf p "@;<0 -2>@]@ @ "
+
+let print_fundef p (id, fd) =
+  fprintf p "@[<v 2>mk_pair ?? (succ_pos_of_nat %i (* %s *)) " (id_i id) id;
+  match fd with
+  | External(id', args, res) ->
+      fprintf p "(External (succ_pos_of_nat %i) %s %s)@]" (id_i id) (typelist args) (stype res)
+  | Internal f ->
+      fprintf p "(Internal (@ %a@;<0 -2>))@]" print_function f
+
+let string_of_init id =
+  let b = Buffer.create (List.length id) in
+  let add_init = function
+  | Init_int8 c ->
+      if c >= 32 && c <= 126 && c <> Char.code '\"' && c <> Char.code '\\'
+      then Buffer.add_char b (Char.chr c)
+      else Buffer.add_string b (Printf.sprintf "\\%03o" c)
+  | _ ->
+      assert false
+  in List.iter add_init id; Buffer.contents b
+
+let chop_last_nul id =
+  match List.rev id with
+  | Init_int8 0 :: tl -> List.rev tl
+  | _ -> id
+
+let print_init p = function
+  | Init_int8 n -> fprintf p "(Init_int8 (repr %d))@ " n
+  | Init_int16 n -> fprintf p "(Init_int16 (repr %d))@ " n
+  | Init_int32 n -> fprintf p "(Init_int32 (repr %d))@ " n
+  | Init_float32 n -> fprintf p "(Init_float32 %F)@ " n
+  | Init_float64 n -> fprintf p "(Iinit_float64 %F)@ " n
+  | Init_space n -> fprintf p "(Init_space %d)@ " n
+  | Init_addrof(symb, ofs) -> fprintf p "(Init_addrof %d (repr %d))" (id_i symb) ofs
+
+let re_string_literal = Str.regexp "__stringlit_[0-9]+"
+
+let print_globvar p ((((id, init), sp), ty)) =
+  fprintf p "@[<hov 2>(mk_pair ?? (mk_pair ?? (mk_pair ?? (succ_pos_of_nat %i (* %s *))@ %a)@ %s)@ %s)@]"
+    (id_i id)
+    id
+    (print_list print_init) init
+    (sspace sp)
+    (stype ty)
+
+(* Collect struct and union types *)
+
+let rec collect_type = function
+  | Tvoid -> ()
+  | Tint(sz, sg) -> ()
+  | Tfloat sz -> ()
+  | Tpointer (_,t) -> collect_type t
+  | Tarray(_, t, n) -> collect_type t
+  | Tfunction(args, res) -> List.iter collect_type args; collect_type res
+  | Tstruct(id, fld) -> register_struct_union id fld; List.iter collect_field fld
+  | Tunion(id, fld) -> register_struct_union id fld; List.iter collect_field fld
+  | Tcomp_ptr _ -> ()
+
+and collect_field f = collect_type (snd f)
+
+let rec collect_expr (Expr(ed, ty)) =
+  match ed with
+  | Ecost (_, e) -> collect_expr e
+  | Econst_int n -> ()
+  | Econst_float f -> ()
+  | Evar id -> ()
+  | Eunop(op, e1) -> collect_expr e1
+  | Ederef e -> collect_expr e
+  | Eaddrof e -> collect_expr e
+  | Ebinop(op, e1, e2) -> collect_expr e1; collect_expr e2
+  | Ecast(ty, e1) -> collect_type ty; collect_expr e1
+  | Econdition(e1, e2, e3) -> collect_expr e1; collect_expr e2; collect_expr e3
+  | Eandbool(e1, e2) -> collect_expr e1; collect_expr e2
+  | Eorbool(e1, e2) -> collect_expr e1; collect_expr e2
+  | Esizeof ty -> collect_type ty
+  | Efield(e1, id) -> collect_expr e1
+
+let rec collect_expr_list = function
+  | [] -> ()
+  | hd :: tl -> collect_expr hd; collect_expr_list tl
+
+let rec collect_stmt = function
+  | Scost (_, s) -> collect_stmt s
+  | Sskip -> ()
+  | Sassign(e1, e2) -> collect_expr e1; collect_expr e2
+  | Scall(None, e1, el) -> collect_expr e1; collect_expr_list el
+  | Scall(Some lhs, e1, el) -> collect_expr lhs; collect_expr e1; collect_expr_list el
+  | Ssequence(s1, s2) -> collect_stmt s1; collect_stmt s2
+  | Sifthenelse(e, s1, s2) -> collect_expr e; collect_stmt s1; collect_stmt s2
+  | Swhile(e, s) -> collect_expr e; collect_stmt s
+  | Sdowhile(e, s) -> collect_stmt s; collect_expr e
+  | Sfor(s_init, e, s_iter, s_body) ->
+      collect_stmt s_init; collect_expr e;
+      collect_stmt s_iter; collect_stmt s_body
+  | Sbreak -> ()
+  | Scontinue -> ()
+  | Sswitch(e, cases) -> collect_expr e; collect_cases cases
+  | Sreturn None -> ()
+  | Sreturn (Some e) -> collect_expr e
+  | Slabel(lbl, s) -> collect_stmt s
+  | Sgoto lbl -> ()
+
+and collect_cases = function
+  | LSdefault s -> collect_stmt s
+  | LScase(lbl, s, rem) -> collect_stmt s; collect_cases rem
+
+let collect_function f =
+  collect_type f.fn_return;
+  List.iter (fun (id, ty) -> collect_type ty) f.fn_params;
+  List.iter (fun (id, ty) -> collect_type ty) f.fn_vars;
+  collect_stmt f.fn_body
+
+let collect_fundef (id, fd) =
+  match fd with
+  | External(_, args, res) -> List.iter collect_type args; collect_type res
+  | Internal f -> collect_function f
+
+let collect_globvar ((id, init), ty) =
+  collect_type ty
+
+let collect_program p =
+  List.iter collect_globvar p.prog_vars;
+  List.iter collect_fundef p.prog_funct
+
+let declare_struct_or_union p (name, fld) =
+  fprintf p "%s;@ @ " name
+
+let print_struct_or_union p (name, fld) =
+  fprintf p "@[<v 2>%s {" name;
+  let rec print_field (id, ty) =
+    fprintf p "@ %s;" (name_cdecl id ty) in
+  List.iter print_field fld;
+  fprintf p "@;<0 -2>};@]@ "
+
+let print_program p prog =
+  struct_unions := StructUnionSet.empty;
+  collect_program prog;
+  fprintf p "include \"Csyntax.ma\".@\n@\n";
+  fprintf p "@[<v 2>ndefinition myprog := mk_program fundef type@ ";
+(*  StructUnionSet.iter (declare_struct_or_union p) !struct_unions;
+  StructUnionSet.iter (print_struct_or_union p) !struct_unions;*)
+  print_list print_fundef p prog.prog_funct;
+  fprintf p "@\n(succ_pos_of_nat %i)@\n" (id_i "main");
+  print_list print_globvar p prog.prog_vars;
+  fprintf p "@;<0 -2>.@]@."
+
+

src/clight/clightPrinter.ml

@@ -19 +19 @@
 open AST
 open Clight
 
+let name_space = function
+  | Any -> ""
+  | Data -> "__data "
+  | IData -> "__idata "
+  | PData -> "__pdata "
+  | XData -> "__xdata "
+  | Code -> "__code "
+
+
 let name_unop = function
   | Onotbool -> "!"
   | Onotint  -> "~"
@@ -77 +86 @@
 let parenthesize_if_pointer id =
   if String.length id > 0 && id.[0] = '*' then "(" ^ id ^ ")" else id
 
-let rec name_cdecl id ty =
+(* Use Any for the space when nothing should appear. *)
+
+let rec name_cdecl sp id ty =
+  let ssp = name_space sp in
   match ty with
   | Tvoid ->
-      "void" ^ name_optid id
+      ssp ^ "void" ^ name_optid id
   | Tint(sz, sg) ->
-      name_inttype sz sg ^ name_optid id
+      ssp ^ name_inttype sz sg ^ name_optid id
   | Tfloat sz ->
-      name_floattype sz ^ name_optid id
-  | Tpointer t ->
-      name_cdecl ("*" ^ id) t
-  | Tarray(t, n) ->
+      ssp ^ name_floattype sz ^ name_optid id
+  | Tpointer (sp',t) ->
+      name_cdecl sp' ("* " ^ ssp ^ id) t
+  | Tarray(sp', t, n) ->
+      if sp <> sp' then eprintf "Array %s has wrong memory space.\n%!" id;
       name_cdecl
+        sp'
         (sprintf "%s[%ld]" (parenthesize_if_pointer id) (Int32.of_int n))
         t
   | Tfunction(args, res) ->
       let b = Buffer.create 20 in
+      Buffer.add_string b ssp;
       if id = ""
       then Buffer.add_string b "(*)"
       else Buffer.add_string b (parenthesize_if_pointer id);
@@ -105 +120 @@
           | [] -> ()
           | t1::tl ->
               if not first then Buffer.add_string b ", ";
-              Buffer.add_string b (name_cdecl "" t1);
+              Buffer.add_string b (name_cdecl Any "" t1);
               add_args false tl in
           add_args true args
       end;
       Buffer.add_char b ')';
-      name_cdecl (Buffer.contents b) res
+      name_cdecl Any (Buffer.contents b) res
   | Tstruct(name, fld) ->
-      name ^ name_optid id
+      ssp ^ name ^ name_optid id
   | Tunion(name, fld) ->
-      name ^ name_optid id
+      ssp ^ name ^ name_optid id
   | Tcomp_ptr name ->
-      name ^ " *" ^ id
+      ssp ^ name ^ " *" ^ id
 
 (* Type *)
 
-let name_type ty = name_cdecl "" ty
+let name_type ty = name_cdecl Any "" ty
 
 (* Expressions *)
 
@@ -318 +333 @@
       | [] -> ()
       | (id, ty) :: rem ->
           if not first then Buffer.add_string b ", ";
-          Buffer.add_string b (name_cdecl id ty);
+          Buffer.add_string b (name_cdecl Any id ty);
           add_params false rem in
       add_params true params
   end;
@@ -327 +342 @@
 
 let print_function p id f =
   fprintf p "%s@ "
-            (name_cdecl (name_function_parameters id f.fn_params)
+            (name_cdecl Any
+                        (name_function_parameters id f.fn_params)
                         f.fn_return);
   fprintf p "@[<v 2>{@ ";
   List.iter
     (fun ((id, ty)) ->
-      fprintf p "%s;@ " (name_cdecl id ty))
+      fprintf p "%s;@ " (name_cdecl Any id ty))
     f.fn_vars;
   print_stmt p f.fn_body;
   fprintf p "@;<0 -2>}@]@ @ "
@@ -341 +357 @@
   match fd with
   | External(_, args, res) ->
       fprintf p "extern %s;@ @ "
-                (name_cdecl id (Tfunction(args, res)))
+                (name_cdecl Any id (Tfunction(args, res)))
   | Internal f ->
       print_function p id f
 
@@ -376 +392 @@
 
 let re_string_literal = Str.regexp "__stringlit_[0-9]+"
 
-let print_globvar p (((id, init), ty)) =
+let print_globvar p ((((id, init), sp), ty)) =
   match init with
   | [] ->
       fprintf p "extern %s;@ @ "
-              (name_cdecl id ty)
+              (name_cdecl sp id ty)
   | [Init_space _] ->
       fprintf p "%s;@ @ "
-              (name_cdecl id ty)
+              (name_cdecl sp id ty)
   | _ ->
       fprintf p "@[<hov 2>%s = "
-              (name_cdecl id ty);
+              (name_cdecl sp id ty);
       if Str.string_match re_string_literal id 0
       && List.for_all (function Init_int8 _ -> true | _ -> false) init
       then
@@ -404 +420 @@
   | Tvoid -> ()
   | Tint(sz, sg) -> ()
   | Tfloat sz -> ()
-  | Tpointer t -> collect_type t
-  | Tarray(t, n) -> collect_type t
+  | Tpointer (_,t) -> collect_type t
+  | Tarray(_, t, n) -> collect_type t
   | Tfunction(args, res) -> collect_type_list args; collect_type res
   | Tstruct(id, fld) -> register_struct_union id fld; collect_fields fld
   | Tunion(id, fld) -> register_struct_union id fld; collect_fields fld
@@ -491 +507 @@
   let rec print_fields = function
   | [] -> ()
   | (id, ty)::rem ->
-      fprintf p "@ %s;" (name_cdecl id ty);
+      fprintf p "@ %s;" (name_cdecl Any id ty);
       print_fields rem in
   print_fields fld;
   fprintf p "@;<0 -2>};@]@ "

src/clight/clightToCminor.ml

@@ -7 +7 @@
   | Tint (_,_) -> Type_ret Sig_int
   | Tfloat _ -> Type_ret Sig_float
   | Tpointer _ -> Type_ret Sig_int
-  | Tarray (_,_) -> Type_ret Sig_int
+  | Tarray _ -> Type_ret Sig_int
   | Tfunction (_,_) | Tstruct (_,_)
   | Tunion (_,_) | Tcomp_ptr _ -> assert false
 
@@ -15 +15 @@
   | Tint (_,_) -> Sig_int
   | Tfloat _ -> Sig_float
   | Tpointer _ -> Sig_int
-  | Tarray (_,_) -> Sig_int
+  | Tarray _ -> Sig_int
   | Tvoid -> assert false
   | Tfunction (_,_) | Tstruct (_,_)| Tunion (_,_) | Tcomp_ptr _ ->
       assert false
@@ -31 +31 @@
   | Tfloat F32 -> assert false 
   | Tfloat F64 -> Memory.MQ_float64
   | Tpointer _ -> Memory.MQ_int32                       
-  | Tarray (c,s) -> Memory.MQ_int32
+  | Tarray _ -> Memory.MQ_int32
   | Tfunction (_,_) -> assert false
   | Tstruct (_,_) -> assert false 
   | Tunion (_,_) -> assert false
@@ -59 +59 @@
   | Tfloat F32 -> 8
   | Tfloat F64 -> 8
   | Tpointer _ -> 4                     
-  | Tarray (c,s) -> s*(size_of_ctype c)                   
+  | Tarray (_,c,s) -> s*(size_of_ctype c)                         
   | Tfunction (_,_) | Tstruct (_,_) | Tunion (_,_)  | Tcomp_ptr _ ->
       assert false
 
 let rec translate_vars v = 
-  let ((id,lst),cty) = v in
+  let (((id,lst),space),cty) = v in
     match cty with
       | Tint (_,_) | Tfloat _ | Tpointer _ -> (id,init_data_to_data_rec lst)
-      | Tarray(c,_) -> translate_vars ((id,lst),c) 
+      | Tarray(_,c,_) -> translate_vars (((id,lst),space),c) 
       | Tvoid | Tfunction (_,_) | Tstruct (_,_) | Tunion (_,_) | Tcomp_ptr _ ->
           assert false
 
@@ -95 +95 @@
       (match (t1,t2) with 
          | (Tint(_,_),Tint(_,_)) -> Op2 (Op_add,e1,e2)
          | (Tfloat _,Tfloat _) -> Op2 (Op_addf,e1,e2)
-         | (Tpointer t,Tint(_,_)) -> 
+         | (Tpointer (_,t),Tint(_,_)) -> 
              Op2 (Op_add,e1, Op2 (Op_mul,e2,Cst (Cst_int (size_of_ctype t))))
-         | (Tint(_,_),Tpointer t) -> 
+         | (Tint(_,_),Tpointer (_,t)) -> 
              Op2 (Op_add,Op2 (Op_mul,e1,Cst (Cst_int (size_of_ctype t))),e2)
-         | (Tarray (t,_),Tint(_,_)) -> 
+         | (Tarray (_,t,_),Tint(_,_)) -> 
              Op2 (Op_add,e1,Op2 (Op_mul,e2,(Cst (Cst_int (size_of_ctype t)))))
-         | (Tint(_,_),Tarray(t,_)) -> 
+         | (Tint(_,_),Tarray(_,t,_)) -> 
              Op2 (Op_add,e2,Op2 (Op_mul,e1,(Cst (Cst_int (size_of_ctype t)))))
          | _ -> assert false 
       )
@@ -109 +109 @@
       (match (t1,t2) with 
          | (Tint(_,_),Tint(_,_)) -> Op2 (Op_sub,e1,e2)
          | (Tfloat _,Tfloat _) -> Op2 (Op_subf,e1,e2)
-         | (Tpointer t,Tint(_,_)) -> 
+         | (Tpointer (_,t),Tint(_,_)) -> 
              Op2 (Op_sub,e1,Op2 (Op_mul,e2,(Cst (Cst_int (size_of_ctype t)))))
-         | (Tint(_,_),Tpointer t) ->
+         | (Tint(_,_),Tpointer (_,t)) ->
              Op2 (Op_sub,Op2 (Op_mul,e1,(Cst (Cst_int (size_of_ctype t)))),e2)
-         | (Tarray (t,_),Tint(_,_)) -> 
+         | (Tarray (_,t,_),Tint(_,_)) -> 
              Op2 (Op_sub,e1,Op2 (Op_mul,e2,(Cst (Cst_int (size_of_ctype t)))))
-         | (Tint(_,_),Tarray(t,_)) -> 
+         | (Tint(_,_),Tarray(_,t,_)) -> 
              Op2 (Op_sub,e2,Op2 (Op_mul,e1,(Cst (Cst_int (size_of_ctype t)))))
          | _ -> assert false
       )
@@ -310 +310 @@
   and stck = ref 0 in
   let treat_var v = match snd v with  
     | Tvoid | Tint (_,_) | Tfloat _ | Tpointer _ -> ()
-    | Tarray (_,_)  ->
+    | Tarray _  ->
         let size = size_of_ctype (snd v) in
           if size > 0 then (
             (Hashtbl.add addr_of_id (fst v) !stck);
@@ -400 +400 @@
   | (id,External (i,p,r)) -> (id, F_ext (translate_external i p r))
 
 let translate p = 
-  let globals = List.map (fun p -> fst (fst p)) p.prog_vars in 
+  let globals = List.map (fun p -> fst (fst (fst p))) p.prog_vars in 
     {Cminor.vars   = List.map translate_vars p.prog_vars;
      Cminor.functs = List.map (translate_funct globals) p.prog_funct;
      Cminor.main = p.prog_main }

src/common/cminorMemory.ml

@@ -204 +204 @@
   | Tfloat F32 -> 4
   | Tfloat F64 -> 8
   | Tpointer _ -> 4                     
-  | Tarray (_,_) -> 4                     
+  | Tarray _ -> 4                         
   | Tfunction (_,_) -> assert false
   | Tstruct (_,_) -> assert false 
   | Tunion (_,_) -> assert false
@@ -227 +227 @@
 let cast t v = v (*TODO*)
 
 let init m b lst = function
-  | Tarray (c,n) ->
+  | Tarray (_,c,n) ->
       (match alloc m 0 (n*(sizeof c)) with
          | Some(b',m') -> 
              (match store m' Memory.MQ_int32 b 0 (Val_ptr(b',0)) with 
@@ -253 +253 @@
   let b_of_id = Hashtbl.create 11
   and fd_of_b = Hashtbl.create 11
   and i = ref (-1) in
-  let update_mem m ((id,lst),cty) = 
+  let update_mem m (((id,lst),_),cty) = 
     (match alloc m 0 (sizeof cty) with
        | Some(b,m') -> 
            Hashtbl.add b_of_id id b;

src/languages.ml

@@ -230 +230 @@
   flush cout;
   close_out cout
 
+let rec find_clight = function
+| [] -> None
+| AstClight p :: t -> Some p
+| _::t -> find_clight t
+
+let save_matita filename asts =
+  match find_clight asts with
+  | None -> Error.warning "during matita output" "No Clight AST."
+  | Some prog -> begin
+    let output_filename = 
+      Misc.SysExt.alternative 
+        (Filename.chop_extension filename 
+         ^ ".ma")
+    in
+    let cout = open_out output_filename in
+    let fout = Format.formatter_of_out_channel cout in
+    ClightPrintMatita.print_program fout prog;
+    flush cout;
+    close_out cout
+  end
+
 let interpret = function
   | AstClight p ->
     ClightInterpret.interpret true p

src/languages.mli

@@ -75 +75 @@
     is deduced from the language of the AST. *)
 val save : string -> ast -> unit
 
+(** [save_matita filename asts] pretty prints the first Clight AST in
+    [asts] in a fresh file whose name is prefixed by [filename] and whose
+    extension is .ma. *)
+val save_matita : string -> ast list -> unit
+
 (** [from_string s] parses [s] as an intermediate language name. *)
 val from_string : string -> name
 

src/options.ml

@@ -39 +39 @@
 let set_debug                   = (:=) debug_flag
 let is_debug_enabled ()         = !debug_flag
 
+let matita_output_flag          = ref false
+let is_matita_output_enabled () = !matita_output_flag
+
 let options = OptionsParsing.register [
   "-s", Arg.String set_source_language,
   " Choose the source language between:";
@@ -58 +61 @@
 
   "-d", Arg.Set debug_flag,
   " Debugging mode.";
+
+  "-ma", Arg.Set matita_output_flag,
+  " Output matita formatted Clight program.";
 ]

src/options.mli

@@ -22 +22 @@
 
 (** {2 Verbose mode} *)
 val is_debug_enabled : unit -> bool
+
+(** {2 Matita output of Clight programs} *)
+val is_matita_output_enabled : unit -> bool