Changeset 292


Ignore:
Timestamp:
Nov 25, 2010, 2:54:57 PM (9 years ago)
Author:
campbell
Message:

Update acc 8051 syntax extension patch.
Adds memory spaces to Clight pretty printing, and fixes the handling of
cost expressions in the matita output.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/acc-0.1.spaces.patch

    r160 r292  
    1 diff -N --exclude=myocamlbuild_config.ml --exclude=lib --exclude='*~' --exclude=_build -ur acc-0.1.orig/cparser/AddCasts.ml acc-0.1/cparser/AddCasts.ml
    2 --- acc-0.1.orig/cparser/AddCasts.ml    2010-09-28 16:14:19.000000000 +0100
    3 +++ acc-0.1/cparser/AddCasts.ml 2010-09-28 16:14:33.000000000 +0100
    4 @@ -39,7 +39,7 @@
     1diff --git a/cparser/AddCasts.ml b/cparser/AddCasts.ml
     2index 9ec128d..5f5184c 100644
     3--- a/cparser/AddCasts.ml
     4+++ b/cparser/AddCasts.ml
     5@@ -39,7 +39,7 @@ let widening_cast env tfrom tto =
    56       r1 < r2 || (r1 = r2 && is_signed_ikind k1 = is_signed_ikind k2)
    67   | TFloat(k1, _), TFloat(k2, _) ->
     
    1112   end
    1213 
    13 @@ -52,7 +52,7 @@
     14@@ -52,7 +52,7 @@ let cast_not_needed env tfrom tto =
    1415 let cast env e tto =
    1516   if cast_not_needed env e.etyp tto
     
    2021 (* Note: this pass applies only to simplified expressions
    2122    because casts cannot be materialized in op= expressions... *)
    22 @@ -73,7 +73,7 @@
     23@@ -73,7 +73,7 @@ let rec add_expr env e =
    2324             EUnop(op, e1')
    2425         | Opreincr | Opredecr | Opostincr | Opostdecr ->
     
    2930       let e1' = add_expr env e1 in
    3031       let e2' = add_expr env e2 in
    31 @@ -97,13 +97,14 @@
     32@@ -97,13 +97,14 @@ let rec add_expr env e =
    3233         | Oadd_assign|Osub_assign|Omul_assign|Odiv_assign|Omod_assign
    3334         | Oand_assign|Oor_assign|Oxor_assign|Oshl_assign|Oshr_assign ->
     
    4748       assert false (* not simplified *)
    4849 
    49 @@ -132,7 +133,7 @@
     50@@ -132,7 +133,7 @@ let add_arguments env ty_fun args =
    5051   let ty_args =
    5152     match unroll env ty_fun with
     
    5657         | TFun(res, args, vararg, a) -> args
    5758         | _ -> assert false
    58 @@ -146,10 +147,10 @@
     59@@ -146,10 +147,10 @@ let add_arguments env ty_fun args =
    5960 
    6061 let add_topexpr env loc e =
     
    6970         sassign loc (add_expr env lhs) ecall
    7071       else begin
    71 @@ -162,7 +163,7 @@
     72@@ -162,7 +163,7 @@ let add_topexpr env loc e =
    7273   | ECall(e1, el) ->
    7374       let ecall =
     
    7879   | _ ->
    7980       assert false
    80 @@ -175,7 +176,7 @@
     81@@ -175,7 +176,7 @@ let rec add_init env tto = function
    8182   | Init_array il ->
    8283       let ty_elt =
     
    8788   | Init_struct(id, fil) ->
    8889       Init_struct (id, List.map
    89 diff -N --exclude=myocamlbuild_config.ml --exclude=lib --exclude='*~' --exclude=_build -ur acc-0.1.orig/cparser/Bitfields.ml acc-0.1/cparser/Bitfields.ml
    90 --- acc-0.1.orig/cparser/Bitfields.ml   2010-09-28 16:14:19.000000000 +0100
    91 +++ acc-0.1/cparser/Bitfields.ml        2010-09-28 16:14:33.000000000 +0100
    92 @@ -118,7 +118,7 @@
     90diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml
     91index dea1862..c7dc25f 100644
     92--- a/cparser/Bitfields.ml
     93+++ b/cparser/Bitfields.ml
     94@@ -118,7 +118,7 @@ let insertion_mask bf =
    9395       (Int64.pred (Int64.shift_left 1L bf.bf_size))
    9496       bf.bf_pos in
     
    99101 (* Extract the value of a bitfield *)
    100102 
    101 @@ -140,12 +140,12 @@
     103@@ -140,12 +140,12 @@ signed int bitfield_signed_extract(unsigned int x, int ofs, int sz)
    102104 let bitfield_extract bf carrier =
    103105   let e1 =
     
    115117 (* Assign a bitfield within a carrier *)
    116118 
    117 @@ -161,19 +161,21 @@
     119@@ -161,19 +161,21 @@ unsigned int bitfield_insert(unsigned int x, int ofs, int sz, unsigned int y)
    118120 
    119121 let bitfield_assign bf carrier newval =
     
    142144 (* Expressions *)
    143145 
    144 @@ -188,7 +190,7 @@
     146@@ -188,7 +190,7 @@ let transf_expr env e =
    145147 
    146148   let is_bitfield_access_ptr ty fieldname =
     
    151153 
    152154   let rec texp e =
    153 @@ -201,27 +203,28 @@
     155@@ -201,27 +203,28 @@ let transf_expr env e =
    154156         let e1' = texp e1 in
    155157         begin match is_bitfield_access e1.etyp fieldname with
     
    185187     | EBinop(Oassign, e1, e2, ty) ->
    186188         begin match e1.edesc with
    187 @@ -231,17 +234,20 @@
     189@@ -231,17 +234,20 @@ let transf_expr env e =
    188190             | None ->
    189191                 {edesc = EBinop(Oassign,
     
    210212         | EUnop(Oarrow fieldname, e11) ->
    211213             let lhs = texp e11 in let rhs = texp e2 in
    212 @@ -249,31 +255,35 @@
     214@@ -249,31 +255,35 @@ let transf_expr env e =
    213215             | None ->
    214216                 {edesc = EBinop(Oassign,
     
    255257   in texp e
    256258 
    257 @@ -325,13 +335,16 @@
     259@@ -325,13 +335,16 @@ let bitfield_initializer bf i =
    258260       let m = Int64.pred (Int64.shift_left 1L bf.bf_size) in
    259261       let e_mask =
     
    275277 
    276278 let rec pack_bitfield_init id carrier fld_init_list =
    277 @@ -354,7 +367,8 @@
     279@@ -354,7 +367,8 @@ let rec or_expr_list = function
    278280   | [e] -> e
    279281   | e1 :: el ->
     
    285287 let rec transf_struct_init id fld_init_list =
    286288   match fld_init_list with
    287 @@ -367,7 +381,8 @@
     289@@ -367,7 +381,8 @@ let rec transf_struct_init id fld_init_list =
    288290         ({fld_name = bf.bf_carrier; fld_typ = bf.bf_carrier_typ;
    289291           fld_bitfield = None},
     
    295297       with Not_found ->
    296298         (fld, i) :: transf_struct_init id rem
    297 diff -N --exclude=myocamlbuild_config.ml --exclude=lib --exclude='*~' --exclude=_build -ur acc-0.1.orig/cparser/Builtins.ml acc-0.1/cparser/Builtins.ml
    298 --- acc-0.1.orig/cparser/Builtins.ml    2010-09-28 16:14:20.000000000 +0100
    299 +++ acc-0.1/cparser/Builtins.ml 2010-09-28 16:14:33.000000000 +0100
    300 @@ -37,10 +37,10 @@
     299diff --git a/cparser/Builtins.ml b/cparser/Builtins.ml
     300index 8eb1abf..aa243fd 100644
     301--- a/cparser/Builtins.ml
     302+++ b/cparser/Builtins.ml
     303@@ -37,10 +37,10 @@ let add_function (s, (res, args, va)) =
    301304     TFun(res,
    302305          Some (List.map (fun ty -> (Env.fresh_ident "", ty)) args),
     
    311314 type t = {
    312315   typedefs: (string * C.typ) list;
    313 diff -N --exclude=myocamlbuild_config.ml --exclude=lib --exclude='*~' --exclude=_build -ur acc-0.1.orig/cparser/Ceval.ml acc-0.1/cparser/Ceval.ml
    314 --- acc-0.1.orig/cparser/Ceval.ml       2010-09-28 16:14:20.000000000 +0100
    315 +++ acc-0.1/cparser/Ceval.ml    2010-09-28 16:14:33.000000000 +0100
    316 @@ -99,11 +99,11 @@
     316diff --git a/cparser/C.mli b/cparser/C.mli
     317index d477acd..90df378 100644
     318--- a/cparser/C.mli
     319+++ b/cparser/C.mli
     320@@ -124,12 +124,20 @@ type binary_operator =
     321 
     322 (** Types *)
     323 
     324+type memory_space =
     325+  | Any
     326+  | Data
     327+  | IData
     328+  | PData
     329+  | XData
     330+  | Code
     331+
     332 type typ =
     333   | TVoid of attributes
     334   | TInt of ikind * attributes
     335   | TFloat of fkind * attributes
     336-  | TPtr of typ * attributes
     337-  | TArray of typ * int64 option * attributes
     338+  | TPtr of memory_space * typ * attributes
     339+  | TArray of memory_space * typ * int64 option * attributes
     340   | TFun of typ * (ident * typ) list option * bool * attributes
     341   | TNamed of ident * attributes
     342   | TStruct of ident * attributes
     343@@ -137,7 +145,7 @@ type typ =
     344 
     345 (** Expressions *)
     346 
     347-type exp = { edesc: exp_desc; etyp: typ }
     348+type exp = { edesc: exp_desc; etyp: typ; espace: memory_space }
     349 
     350 and exp_desc =
     351   | EConst of constant
     352@@ -220,7 +228,7 @@ type globdecl =
     353   { gdesc: globdecl_desc; gloc: location }
     354 
     355 and globdecl_desc =
     356-  | Gdecl of decl           (* variable declaration, function prototype *)
     357+  | Gdecl of memory_space * decl  (* variable declaration, function prototype *)
     358   | Gfundef of fundef                   (* function definition *)
     359   | Gcompositedecl of struct_or_union * ident (* struct/union declaration *)
     360   | Gcompositedef of struct_or_union * ident * field list
     361diff --git a/cparser/Ceval.ml b/cparser/Ceval.ml
     362index 0e22852..acf84aa 100644
     363--- a/cparser/Ceval.ml
     364+++ b/cparser/Ceval.ml
     365@@ -99,11 +99,11 @@ let cast env ty_to ty_from v =
    317366       if is_signed env ty_from
    318367       then F(normalize_float (Int64.to_float n) fk)
     
    329378   | _, _ ->
    330379       raise Notconst
    331 @@ -270,8 +270,8 @@
     380@@ -270,8 +270,8 @@ let constant_expr env ty e =
    332381     match unroll env ty, cast env e.etyp ty (expr env e) with
    333382     | TInt(ik, _), I n -> Some(CInt(n, ik, ""))
     
    341390     | _   -> None
    342391   with Notconst -> None
    343 diff -N --exclude=myocamlbuild_config.ml --exclude=lib --exclude='*~' --exclude=_build -ur acc-0.1.orig/cparser/Cleanup.ml acc-0.1/cparser/Cleanup.ml
    344 --- acc-0.1.orig/cparser/Cleanup.ml     2010-09-28 16:14:20.000000000 +0100
    345 +++ acc-0.1/cparser/Cleanup.ml  2010-09-28 16:14:33.000000000 +0100
    346 @@ -40,8 +40,8 @@
     392diff --git a/cparser/Cleanup.ml b/cparser/Cleanup.ml
     393index be28989..9644654 100644
     394--- a/cparser/Cleanup.ml
     395+++ b/cparser/Cleanup.ml
     396@@ -40,8 +40,8 @@ let needed id =
    347397 (* Iterate [addref] on all syntactic categories. *)
    348398 
     
    355405   | TFun(res, Some params, _, _) -> add_typ res; add_vars params
    356406   | TNamed(id, _) -> addref id
    357 @@ -120,7 +120,7 @@
     407@@ -120,7 +120,7 @@ let rec add_init_globdecls accu = function
    358408   | [] -> accu
    359409   | g :: rem ->
     
    364414       | Gfundef({fd_storage = Storage_default} as f) ->
    365415           add_fundef f; add_init_globdecls accu rem
    366 @@ -135,7 +135,7 @@
     416@@ -135,7 +135,7 @@ let rec add_needed_globdecls accu = function
    367417   | [] -> accu
    368418   | g :: rem ->
     
    373423           then (add_decl decl; add_needed_globdecls accu rem)
    374424           else add_needed_globdecls (g :: accu) rem
    375 @@ -174,7 +174,7 @@
     425@@ -174,7 +174,7 @@ let rec simpl_globdecls accu = function
    376426   | g :: rem ->
    377427       let need =
     
    382432         | Gcompositedecl(_, id) -> needed id
    383433         | Gcompositedef(_, id, flds) -> needed id
    384 diff -N --exclude=myocamlbuild_config.ml --exclude=lib --exclude='*~' --exclude=_build -ur acc-0.1.orig/cparser/C.mli acc-0.1/cparser/C.mli
    385 --- acc-0.1.orig/cparser/C.mli  2010-09-28 16:14:19.000000000 +0100
    386 +++ acc-0.1/cparser/C.mli       2010-10-06 13:13:53.000000000 +0100
    387 @@ -124,12 +124,20 @@
    388  
    389  (** Types *)
    390  
    391 +type memory_space =
    392 +  | Any
    393 +  | Data
    394 +  | IData
    395 +  | PData
    396 +  | XData
    397 +  | Code
    398 +
    399  type typ =
    400    | TVoid of attributes
    401    | TInt of ikind * attributes
    402    | TFloat of fkind * attributes
    403 -  | TPtr of typ * attributes
    404 -  | TArray of typ * int64 option * attributes
    405 +  | TPtr of memory_space * typ * attributes
    406 +  | TArray of memory_space * typ * int64 option * attributes
    407    | TFun of typ * (ident * typ) list option * bool * attributes
    408    | TNamed of ident * attributes
    409    | TStruct of ident * attributes
    410 @@ -137,7 +145,7 @@
    411  
    412  (** Expressions *)
    413  
    414 -type exp = { edesc: exp_desc; etyp: typ }
    415 +type exp = { edesc: exp_desc; etyp: typ; espace: memory_space }
    416  
    417  and exp_desc =
    418    | EConst of constant
    419 @@ -220,7 +228,7 @@
    420    { gdesc: globdecl_desc; gloc: location }
    421  
    422  and globdecl_desc =
    423 -  | Gdecl of decl           (* variable declaration, function prototype *)
    424 +  | Gdecl of memory_space * decl  (* variable declaration, function prototype *)
    425    | Gfundef of fundef                   (* function definition *)
    426    | Gcompositedecl of struct_or_union * ident (* struct/union declaration *)
    427    | Gcompositedef of struct_or_union * ident * field list
    428 diff -N --exclude=myocamlbuild_config.ml --exclude=lib --exclude='*~' --exclude=_build -ur acc-0.1.orig/cparser/Cprint.ml acc-0.1/cparser/Cprint.ml
    429 --- acc-0.1.orig/cparser/Cprint.ml      2010-09-28 16:14:19.000000000 +0100
    430 +++ acc-0.1/cparser/Cprint.ml   2010-09-28 16:14:33.000000000 +0100
    431 @@ -67,13 +67,13 @@
     434diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml
     435index 7d8f2b3..70aba81 100644
     436--- a/cparser/Cprint.ml
     437+++ b/cparser/Cprint.ml
     438@@ -67,13 +67,13 @@ let rec dcl pp ty n =
    432439       fprintf pp "%s%a%t" (name_of_ikind k) attributes a n
    433440   | TFloat(k, a) ->
     
    445452         begin match a with
    446453         | [] -> n pp
    447 @@ -353,10 +353,12 @@
     454@@ -353,10 +353,12 @@ let rec exp_of_stmt s =
    448455   | Sdo e -> e
    449456   | Sseq(s1, s2) ->
     
    460467       raise Not_expr
    461468 
    462 @@ -373,7 +375,7 @@
     469@@ -373,7 +375,7 @@ let rec stmt pp s =
    463470       fprintf pp "@[<v 2>if (%a) {@ %a@;<0 -2>}@]"
    464471               exp (0, e) stmt_block s1
     
    469476               exp (0, not_e) stmt_block s2
    470477   | Sif(e, s1, s2) ->
    471 @@ -455,7 +457,7 @@
     478@@ -455,7 +457,7 @@ let field pp f =
    472479 let globdecl pp g =
    473480   location pp g.gloc;
     
    478485   | Gfundef f ->
    479486       fundef pp f
    480 diff -N --exclude=myocamlbuild_config.ml --exclude=lib --exclude='*~' --exclude=_build -ur acc-0.1.orig/cparser/Cutil.ml acc-0.1/cparser/Cutil.ml
    481 --- acc-0.1.orig/cparser/Cutil.ml       2010-09-28 16:14:19.000000000 +0100
    482 +++ acc-0.1/cparser/Cutil.ml    2010-09-28 16:14:33.000000000 +0100
    483 @@ -71,8 +71,8 @@
     487diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
     488index 49b25a2..4a43d09 100644
     489--- a/cparser/Cutil.ml
     490+++ b/cparser/Cutil.ml
     491@@ -71,8 +71,8 @@ let rec add_attributes_type attr t =
    484492   | TVoid a -> TVoid (add_attributes attr a)
    485493   | TInt(ik, a) -> TInt(ik, add_attributes attr a)
     
    492500 a)
    493501   | TNamed(s, a) -> TNamed(s, add_attributes attr a)
    494 @@ -95,8 +95,8 @@
     502@@ -95,8 +95,8 @@ let rec attributes_of_type env t =
    495503   | TVoid a -> a
    496504   | TInt(ik, a) -> a
     
    503511   | TNamed(s, a) -> attributes_of_type env (unroll env t)
    504512   | TStruct(s, a) -> a
    505 @@ -110,9 +110,9 @@
     513@@ -110,9 +110,9 @@ let rec change_attributes_type env (f: attributes -> attributes) t =
    506514   | TVoid a -> TVoid (f a)
    507515   | TInt(ik, a) -> TInt(ik, f a)
     
    516524   | TNamed(s, a) ->
    517525       let t1 = unroll env t in
    518 @@ -166,10 +166,10 @@
     526@@ -166,10 +166,10 @@ let combine_types ?(noattrs = false) env t1 t2 =
    519527         TInt(comp_base ik1 ik2, comp_attr a1 a2)
    520528     | TFloat(fk1, a1), TFloat(fk2, a2) ->
     
    531539         let (params, vararg) =
    532540           match params1, params2 with
    533 @@ -244,8 +244,8 @@
     541@@ -244,8 +244,8 @@ let rec alignof env t =
    534542   | TVoid _ -> !config.alignof_void
    535543   | TInt(ik, _) -> Some(alignof_ikind ik)
     
    542550   | TNamed(_, _) -> alignof env (unroll env t)
    543551   | TStruct(name, _) ->
    544 @@ -302,9 +302,9 @@
     552@@ -302,9 +302,9 @@ let rec sizeof env t =
    545553   | TVoid _ -> !config.sizeof_void
    546554   | TInt(ik, _) -> Some(sizeof_ikind ik)
     
    555563       | None -> None
    556564       | Some s ->
    557 @@ -343,7 +343,7 @@
     565@@ -343,7 +343,7 @@ let sizeof_union env members =
    558566 
    559567 let sizeof_struct env members =
     
    564572       begin match alignof_struct_union env members with
    565573       | None -> None                    (* should not happen? *)
    566 @@ -472,8 +472,8 @@
     574@@ -472,8 +472,8 @@ let float_rank = function
    567575 
    568576 let pointer_decay env t =
     
    575583 
    576584 (* The usual unary conversions (H&S 6.3.3) *)
    577 @@ -489,8 +489,8 @@
     585@@ -489,8 +489,8 @@ let unary_conversion env t =
    578586           TInt(kind, attr)
    579587       end
     
    586594   | t -> t
    587595 
    588 @@ -540,8 +540,8 @@
     596@@ -540,8 +540,8 @@ let argument_conversion env t =
    589597   (* Arrays and functions degrade automatically to pointers *)
    590598   (* Other types are not changed *)
     
    597605 
    598606 (* Conversion on function arguments (old-style unprototyped, or vararg *)
    599 @@ -584,8 +584,8 @@
     607@@ -584,8 +584,8 @@ let enum_ikind = IInt
    600608 let type_of_constant = function
    601609   | CInt(_, ik, _) -> TInt(ik, [])
     
    608616 
    609617 (* Check that a C expression is a lvalue *)
    610 @@ -612,12 +612,19 @@
     618@@ -612,12 +612,19 @@ let is_literal_0 e =
    611619 
    612620 (* Check that an assignment is allowed *)
     
    630638           || compatible_types env
    631639                (erase_attributes_type env ty)
    632 @@ -643,17 +650,17 @@
     640@@ -643,17 +650,17 @@ let valid_cast env tfrom tto =
    633641 (* Construct an integer constant *)
    634642 
     
    651659 (* Construct a sequence *)
    652660 
    653 @@ -667,7 +674,7 @@
     661@@ -667,7 +674,7 @@ let sseq loc s1 s2 =
    654662 (* Construct an assignment statement *)
    655663 
     
    660668 
    661669 (* Empty location *)
    662 diff -N --exclude=myocamlbuild_config.ml --exclude=lib --exclude='*~' --exclude=_build -ur acc-0.1.orig/cparser/Elab.ml acc-0.1/cparser/Elab.ml
    663 --- acc-0.1.orig/cparser/Elab.ml        2010-09-28 16:14:20.000000000 +0100
    664 +++ acc-0.1/cparser/Elab.ml     2010-10-06 13:12:56.000000000 +0100
    665 @@ -270,6 +270,28 @@
     670diff --git a/cparser/Elab.ml b/cparser/Elab.ml
     671index 7204508..1978b6b 100644
     672--- a/cparser/Elab.ml
     673+++ b/cparser/Elab.ml
     674@@ -270,6 +270,28 @@ let rec elab_attributes loc = function
    666675       | None -> elab_attributes loc al
    667676       | Some a -> add_attributes [a] (elab_attributes loc al)
     
    692701 
    693702 let typespec_rank = function (* Don't change this *)
    694 @@ -288,6 +310,7 @@
     703@@ -288,6 +310,7 @@ let typespec_rank = function (* Don't change this *)
    695704 
    696705 let typespec_order t1 t2 = compare (typespec_rank t1) (typespec_rank t2)
     
    700709      (storage class, "inline" flag, elaborated type, new env)
    701710    Optional argument "only" is true if this is a standalone
    702 @@ -302,7 +325,8 @@
     711@@ -302,7 +325,8 @@ let rec elab_specifier ?(only = false) loc env specifier =
    703712   let sto = ref Storage_default
    704713   and inline = ref false
     
    710719   let do_specifier = function
    711720   | SpecTypedef -> ()
    712 @@ -314,7 +338,13 @@
     721@@ -314,7 +338,13 @@ let rec elab_specifier ?(only = false) loc env specifier =
    713722         | CV_RESTRICT -> ARestrict in
    714723       attr := add_attributes [a] !attr
     
    725734       if !sto <> Storage_default then
    726735         error loc "multiple storage specifiers";
    727 @@ -330,7 +360,7 @@
     736@@ -330,7 +360,7 @@ let rec elab_specifier ?(only = false) loc env specifier =
    728737 
    729738   List.iter do_specifier specifier;
     
    734743   (* Now interpret the list of type specifiers.  Much of this code
    735744      is stolen from CIL. *)
    736 @@ -394,19 +424,19 @@
     745@@ -394,19 +424,19 @@ let rec elab_specifier ?(only = false) loc env specifier =
    737746         let (id', env') =
    738747           elab_struct_or_union only Struct loc id optmembers env in
     
    757766     | [Cabs.TtypeofE _] ->
    758767         fatal_error loc "GCC __typeof__ not supported"
    759 @@ -419,13 +449,14 @@
     768@@ -419,13 +449,14 @@ let rec elab_specifier ?(only = false) loc env specifier =
    760769 
    761770 (* Elaboration of a type declarator.  *)
     
    775784       let a = elab_attributes loc attr in
    776785       let sz' =
    777 @@ -440,10 +471,11 @@
     786@@ -440,10 +471,11 @@ and elab_type_declarator loc env ty = function
    778787             | None ->
    779788                 error loc "array size is not a compile-time constant";
     
    789798        begin match unroll env ty with
    790799        | TArray _ | TFun _ ->
    791 @@ -451,7 +483,7 @@
     800@@ -451,7 +483,7 @@ and elab_type_declarator loc env ty = function
    792801        | _ -> ()
    793802        end;
     
    798807 (* Elaboration of parameters in a prototype *)
    799808 
    800 @@ -476,25 +508,25 @@
     809@@ -476,25 +508,25 @@ and elab_parameter env (spec, name) =
    801810       "'extern' or 'static' storage not supported for function parameter";
    802811   (* replace array and function types by pointer types *)
     
    830839     ((id, sto, add_attributes_type a ty), env1) in
    831840   mmap elab_one_name env' namelist
    832 @@ -502,13 +534,13 @@
     841@@ -502,13 +534,13 @@ and elab_name_group env (spec, namelist) =
    833842 (* Elaboration of an init-name group *)
    834843 
     
    848857 
    849858 (* Elaboration of a field group *)
    850 @@ -558,7 +590,7 @@
     859@@ -558,7 +590,7 @@ and elab_struct_or_union_info kind loc env members =
    851860   (* Check for incomplete types *)
    852861   let rec check_incomplete = function
     
    857866   | fld :: rem ->
    858867       if incomplete_type env' fld.fld_typ then
    859 @@ -663,12 +695,16 @@
     868@@ -663,12 +695,16 @@ and elab_enum loc tag optmembers env =
    860869 (* Elaboration of a naked type, e.g. in a cast *)
    861870 
     
    877886 (* Elaboration of expressions *)
    878887 
    879 @@ -687,15 +723,15 @@
     888@@ -687,15 +723,15 @@ let elab_expr loc env a =
    880889 
    881890   | VARIABLE s ->
     
    897906   | PAREN e ->
    898907       elab e
    899 @@ -704,12 +740,12 @@
     908@@ -704,12 +740,12 @@ let elab_expr loc env a =
    900909 
    901910   | INDEX(a1, a2) ->            (* e1[e2] *)
     
    914923   | MEMBEROF(a1, fieldname) ->
    915924       let b1 = elab a1 in
    916 @@ -723,25 +759,27 @@
     925@@ -723,25 +759,27 @@ let elab_expr loc env a =
    917926             error "left-hand side of '.' is not a struct or union" in
    918927       (* A field of a const/volatile struct or union is itself const/volatile *)
     
    948957 (* Hack to treat vararg.h functions the GCC way.  Helps with testing.
    949958     va_start(ap,n)
    950 @@ -754,13 +792,15 @@
     959@@ -754,13 +792,15 @@ let elab_expr loc env a =
    951960   | CALL((VARIABLE "__builtin_va_start" as a1), [a2; a3]) ->
    952961       let b1 = elab a1 and b2 = elab a2 and b3 = elab a3 in
     
    967976   | CALL(a1, al) ->
    968977       let b1 =
    969 @@ -771,15 +811,15 @@
     978@@ -771,15 +811,15 @@ let elab_expr loc env a =
    970979             let ty = TFun(TInt(IInt, []), None, false, []) in
    971980             (* Emit an extern declaration for it *)
     
    986995             | TFun(res, args, vararg, a) -> (res, args, vararg)
    987996             | _ -> error "the function part of a call does not have a function type"
    988 @@ -791,7 +831,7 @@
     997@@ -791,7 +831,7 @@ let elab_expr loc env a =
    989998         match args with
    990999         | None -> bl
     
    9951004   | UNARY(POSINCR, a1) ->
    9961005       elab_pre_post_incr_decr Opostincr "postfix '++'" a1
    997 @@ -805,50 +845,50 @@
     1006@@ -805,50 +845,50 @@ let elab_expr loc env a =
    9981007       let b1 = elab a1 in
    9991008       if not (valid_cast env b1.etyp ty) then
     
    10541063   | UNARY(ADDROF, a1) ->
    10551064       let b1 = elab a1 in
    1056 @@ -857,15 +897,15 @@
     1065@@ -857,15 +897,15 @@ let elab_expr loc env a =
    10571066       | _ ->
    10581067         if not (is_lvalue env b1) then err "argument of '&' is not a l-value"
     
    10731082           error "argument of unary '*' is not a pointer"
    10741083       end
    1075 @@ -893,16 +933,16 @@
     1084@@ -893,16 +933,16 @@ let elab_expr loc env a =
    10761085         if is_arith_type env b1.etyp && is_arith_type env b2.etyp then
    10771086           binary_conversion env b1.etyp b2.etyp
     
    10951104   | BINARY(SUB, a1, a2) ->
    10961105       let b1 = elab a1 in
    1097 @@ -913,24 +953,25 @@
     1106@@ -913,24 +953,25 @@ let elab_expr loc env a =
    10981107           (tyres, tyres)
    10991108         end else begin
     
    11301139   | BINARY(SHL, a1, a2) ->
    11311140       elab_shift "<<" Oshl a1 a2
    1132 @@ -970,35 +1011,38 @@
     1141@@ -970,35 +1011,38 @@ let elab_expr loc env a =
    11331142       let b1 = elab a1 in
    11341143       let b2 = elab a2 in
     
    11801189 
    11811190 (* 7.9 Assignment expressions *)
    1182 @@ -1018,7 +1062,7 @@
     1191@@ -1018,7 +1062,7 @@ let elab_expr loc env a =
    11831192           err "assigning a value of type@ %a@ to a lvalue of type@ %a"
    11841193                   Cprint.typ b2.etyp Cprint.typ b1.etyp;
     
    11891198   | BINARY((ADD_ASSIGN | SUB_ASSIGN | MUL_ASSIGN | DIV_ASSIGN | MOD_ASSIGN
    11901199             | BAND_ASSIGN | BOR_ASSIGN | XOR_ASSIGN | SHL_ASSIGN | SHR_ASSIGN
    1191 @@ -1050,7 +1094,7 @@
     1200@@ -1050,7 +1094,7 @@ let elab_expr loc env a =
    11921201               err "assigning a value of type@ %a@ to a lvalue of type@ %a"
    11931202                       Cprint.typ ty Cprint.typ b1.etyp;
     
    11981207       end
    11991208 
    1200 @@ -1063,7 +1107,7 @@
     1209@@ -1063,7 +1107,7 @@ let elab_expr loc env a =
    12011210       | [] -> accu
    12021211       | a :: l ->
     
    12071216 
    12081217 (* Extensions that we do not handle *)
    1209 @@ -1099,7 +1143,7 @@
     1218@@ -1099,7 +1143,7 @@ let elab_expr loc env a =
    12101219         err "the argument of %s is not a l-value" msg;
    12111220       if not (is_scalar_type env b1.etyp) then
     
    12161225 (* Elaboration of binary operators over integers *)
    12171226   and elab_binary_integer msg op a1 a2 =
    1218 @@ -1110,7 +1154,7 @@
     1227@@ -1110,7 +1154,7 @@ let elab_expr loc env a =
    12191228       if not (is_integer_type env b2.etyp) then
    12201229         error "the second argument of '%s' is not an integer type" msg;
     
    12251234 (* Elaboration of binary operators over arithmetic types *)
    12261235   and elab_binary_arithmetic msg op a1 a2 =
    1227 @@ -1121,7 +1165,7 @@
     1236@@ -1121,7 +1165,7 @@ let elab_expr loc env a =
    12281237       if not (is_arith_type env b2.etyp) then
    12291238         error "the second argument of '%s' is not an arithmetic type" msg;
     
    12341243 (* Elaboration of shift operators *)
    12351244   and elab_shift msg op a1 a2 =
    1236 @@ -1132,7 +1176,7 @@
     1245@@ -1132,7 +1176,7 @@ let elab_expr loc env a =
    12371246       if not (is_integer_type env b2.etyp) then
    12381247         error "the second argument of '%s' is not an integer type" msg;
     
    12431252 (* Elaboration of comparisons *)
    12441253   and elab_comparison op a1 a2 =
    1245 @@ -1142,28 +1186,28 @@
     1254@@ -1142,28 +1186,28 @@ let elab_expr loc env a =
    12461255         match pointer_decay env b1.etyp, pointer_decay env b2.etyp with
    12471256         | (TInt _ | TFloat _), (TInt _ | TFloat _) ->
     
    12861295 (* Elaboration of && and || *)
    12871296   and elab_logical_operator msg op a1 a2 =
    1288 @@ -1173,7 +1217,7 @@
     1297@@ -1173,7 +1217,7 @@ let elab_expr loc env a =
    12891298       let b2 = elab a2 in
    12901299       if not (is_scalar_type env b2.etyp) then
     
    12951304 (* Type-checking of function arguments *)
    12961305   and elab_arguments argno args params vararg =
    1297 @@ -1271,7 +1315,7 @@
     1306@@ -1271,7 +1315,7 @@ let check_init_type loc env a ty =
    12981307 
    12991308 let rec elab_init loc env ty ile =
     
    13041313         match opt_sz, rem with
    13051314         | Some sz, _ when n >= sz ->
    1306 @@ -1390,8 +1434,8 @@
     1315@@ -1390,8 +1434,8 @@ let elab_initial loc env ty ie =
    13071316 
    13081317 let fixup_typ env ty init =
     
    13151324 
    13161325 (* Entry point *)
    1317 @@ -1416,9 +1460,9 @@
     1326@@ -1416,9 +1460,9 @@ let enter_typedef loc env (s, sto, ty) =
    13181327   emit_elab (elab_loc loc) (Gtypedef(id, ty));
    13191328   env'
     
    13271336         if local then begin
    13281337           error loc "redefinition of local variable '%s'" s;
    1329 @@ -1437,17 +1481,18 @@
     1338@@ -1437,17 +1481,18 @@ let enter_or_refine_ident local loc env s sto ty =
    13301339           warning loc "redefinition of '%s' with incompatible storage class" s;
    13311340           sto
     
    13501359       begin match sto with
    13511360       | Storage_extern ->
    1352 @@ -1462,11 +1507,11 @@
     1361@@ -1462,11 +1507,11 @@ let rec enter_decdefs local loc env = function
    13531362         match unroll env ty with TFun _ -> Storage_extern | _ -> sto in
    13541363       (* enter ident in environment with declared type, because
     
    13641373       if sto' <> Storage_extern && incomplete_type env ty' then
    13651374         warning loc "'%s' has incomplete type" s;
    1366 @@ -1476,7 +1521,7 @@
     1375@@ -1476,7 +1521,7 @@ let rec enter_decdefs local loc env = function
    13671376         ((sto', id, ty', init') :: decls, env3)
    13681377       end else begin
     
    13731382       end
    13741383 
    1375 @@ -1496,10 +1541,10 @@
     1384@@ -1496,10 +1541,10 @@ let elab_fundef env (spec, name) body loc1 loc2 =
    13761385     | TFun(ty_ret, Some params, vararg, attr) -> (ty_ret, params, vararg)
    13771386     | _ -> fatal_error loc1 "wrong type for function definition" in
     
    13861395   (* Elaborate function body *)
    13871396   let body' = !elab_block_f loc2 ty_ret env2 body in
    1388 @@ -1538,7 +1583,7 @@
     1397@@ -1538,7 +1583,7 @@ let rec elab_definition (local: bool) (env: Env.t) (def: Cabs.definition)
    13891398 
    13901399   (* "struct s { ...};" or "union u;" *)
     
    13951404         error loc "Non-default storage or 'inline' on 'struct' or 'union' declaration";
    13961405       ([], env')
    1397 diff -N --exclude=myocamlbuild_config.ml --exclude=lib --exclude='*~' --exclude=_build -ur acc-0.1.orig/cparser/Env.ml acc-0.1/cparser/Env.ml
    1398 --- acc-0.1.orig/cparser/Env.ml 2010-09-28 16:14:19.000000000 +0100
    1399 +++ acc-0.1/cparser/Env.ml      2010-09-28 16:14:33.000000000 +0100
    1400 @@ -70,7 +70,7 @@
     1406diff --git a/cparser/Env.ml b/cparser/Env.ml
     1407index 777b3e1..1f41c0c 100644
     1408--- a/cparser/Env.ml
     1409+++ b/cparser/Env.ml
     1410@@ -70,7 +70,7 @@ type composite_info = {
    14011411 (* Infos associated with an ordinary identifier *)
    14021412 
     
    14071417 
    14081418 (* Infos associated with a typedef *)
    1409 @@ -201,10 +201,10 @@
     1419@@ -201,10 +201,10 @@ let find_typedef env id =
    14101420 
    14111421 (* Inserting things by source name, with generation of a translated name *)
     
    14201430 let enter_composite env s ci =
    14211431   let id = fresh_ident s in
    1422 @@ -220,8 +220,8 @@
     1432@@ -220,8 +220,8 @@ let enter_typedef env s info =
    14231433 
    14241434 (* Inserting things by translated name *)
     
    14311441 let add_composite env id ci =
    14321442   { env with env_tag = IdentMap.add id ci env.env_tag }
    1433 diff -N --exclude=myocamlbuild_config.ml --exclude=lib --exclude='*~' --exclude=_build -ur acc-0.1.orig/cparser/Env.mli acc-0.1/cparser/Env.mli
    1434 --- acc-0.1.orig/cparser/Env.mli        2010-09-28 16:14:19.000000000 +0100
    1435 +++ acc-0.1/cparser/Env.mli     2010-09-28 16:14:33.000000000 +0100
    1436 @@ -31,7 +31,7 @@
     1443diff --git a/cparser/Env.mli b/cparser/Env.mli
     1444index e7a74af..a9daa21 100644
     1445--- a/cparser/Env.mli
     1446+++ b/cparser/Env.mli
     1447@@ -31,7 +31,7 @@ type composite_info = {
    14371448   ci_sizeof: int option;                (* size; None if incomplete *)
    14381449 }
     
    14431454 type typedef_info = C.typ
    14441455 
    1445 @@ -60,11 +60,11 @@
     1456@@ -60,11 +60,11 @@ val find_struct_member : t -> C.ident * string -> C.field
    14461457 val find_union_member : t -> C.ident * string -> C.field
    14471458 val find_typedef : t -> C.ident -> typedef_info
     
    14571468 val add_composite : t -> C.ident -> composite_info -> t
    14581469 val add_typedef : t -> C.ident -> typedef_info -> t
    1459 diff -N --exclude=myocamlbuild_config.ml --exclude=lib --exclude='*~' --exclude=_build -ur acc-0.1.orig/cparser/GCC.ml acc-0.1/cparser/GCC.ml
    1460 --- acc-0.1.orig/cparser/GCC.ml 2010-09-28 16:14:19.000000000 +0100
    1461 +++ acc-0.1/cparser/GCC.ml      2010-09-28 16:19:24.000000000 +0100
    1462 @@ -30,11 +30,11 @@
     1470diff --git a/cparser/GCC.ml b/cparser/GCC.ml
     1471index 9f864dc..17f3cfa 100644
     1472--- a/cparser/GCC.ml
     1473+++ b/cparser/GCC.ml
     1474@@ -30,11 +30,11 @@ let ulongLongType = TInt(IULongLong, [])
    14631475 let floatType = TFloat(FFloat, [])
    14641476 let doubleType = TFloat(FDouble, [])
     
    14771489 
    14781490 let builtins = {
    1479 @@ -150,9 +150,9 @@
     1491@@ -150,9 +150,9 @@ let builtins = {
    14801492   "__builtin_log10l",  (longDoubleType, [ longDoubleType ], false);
    14811493 
     
    14891501 
    14901502   "__builtin_nan",  (doubleType, [ charConstPtrType ], false);
    1491 diff -N --exclude=myocamlbuild_config.ml --exclude=lib --exclude='*~' --exclude=_build -ur acc-0.1.orig/cparser/Lexer.mll acc-0.1/cparser/Lexer.mll
    1492 --- acc-0.1.orig/cparser/Lexer.mll      2010-09-28 16:14:20.000000000 +0100
    1493 +++ acc-0.1/cparser/Lexer.mll   2010-10-06 13:12:24.000000000 +0100
    1494 @@ -181,7 +181,13 @@
     1503diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll
     1504index d4947ad..d3f3958 100644
     1505--- a/cparser/Lexer.mll
     1506+++ b/cparser/Lexer.mll
     1507@@ -181,7 +181,13 @@ let init_lexicon _ =
    14951508       ("__builtin_types_compatible_p", fun loc -> BUILTIN_TYPES_COMPAT loc);
    14961509       ("__builtin_offsetof", fun loc -> BUILTIN_OFFSETOF loc);
     
    15071520 
    15081521 (* Mark an identifier as a type name. The old mapping is preserved and will
    1509 diff -N --exclude=myocamlbuild_config.ml --exclude=lib --exclude='*~' --exclude=_build -ur acc-0.1.orig/cparser/Parser.mly acc-0.1/cparser/Parser.mly
    1510 --- acc-0.1.orig/cparser/Parser.mly     2010-09-28 16:14:20.000000000 +0100
    1511 +++ acc-0.1/cparser/Parser.mly  2010-10-06 13:11:57.000000000 +0100
    1512 @@ -221,6 +221,8 @@
     1522diff --git a/cparser/Parser.mly b/cparser/Parser.mly
     1523index 0eebb84..abec574 100644
     1524--- a/cparser/Parser.mly
     1525+++ b/cparser/Parser.mly
     1526@@ -221,6 +221,8 @@ let transformOffsetOf (speclist, dtype) member =
    15131527 %token<Cabs.cabsloc> VOLATILE EXTERN STATIC CONST RESTRICT AUTO REGISTER
    15141528 %token<Cabs.cabsloc> THREAD
     
    15191533 
    15201534 %token EQ PLUS_EQ MINUS_EQ STAR_EQ SLASH_EQ PERCENT_EQ
    1521 @@ -1249,6 +1251,12 @@
     1535@@ -1249,6 +1251,12 @@ attribute_nocv:
    15221536 |   MSATTR                              { (fst $1, []), snd $1 }
    15231537                                         /* ISO 6.7.3 */
     
    15321546 
    15331547 attribute_nocv_list:
    1534 diff -N --exclude=myocamlbuild_config.ml --exclude=lib --exclude='*~' --exclude=_build -ur acc-0.1.orig/cparser/Rename.ml acc-0.1/cparser/Rename.ml
    1535 --- acc-0.1.orig/cparser/Rename.ml      2010-09-28 16:14:19.000000000 +0100
    1536 +++ acc-0.1/cparser/Rename.ml   2010-09-28 16:14:33.000000000 +0100
    1537 @@ -75,8 +75,8 @@
     1548diff --git a/cparser/Rename.ml b/cparser/Rename.ml
     1549index 4b2f350..b6de8cd 100644
     1550--- a/cparser/Rename.ml
     1551+++ b/cparser/Rename.ml
     1552@@ -75,8 +75,8 @@ let ident env id =
    15381553                        id.name id.stamp
    15391554 
     
    15461561   | TFun(res, Some p, va, a) ->
    15471562       let (p', _) = mmap param env p in
    1548 @@ -97,7 +97,7 @@
     1563@@ -97,7 +97,7 @@ let constant env = function
    15491564   | cst -> cst
    15501565 
     
    15551570 and exp_desc env = function
    15561571   | EConst cst -> EConst(constant env cst)
    1557 @@ -191,9 +191,9 @@
     1572@@ -191,9 +191,9 @@ let rec globdecl env g =
    15581573   ( { gdesc = desc'; gloc = g.gloc }, env' )
    15591574 
     
    15671582       let (fd', env') = fundef env fd in
    15681583       (Gfundef fd', env')
    1569 @@ -230,7 +230,7 @@
     1584@@ -230,7 +230,7 @@ let rec reserve_public env = function
    15701585   | dcl :: rem ->
    15711586       let env' =
     
    15761591             | Storage_default | Storage_extern -> enter_global env id
    15771592             | Storage_static -> env
    1578 diff -N --exclude=myocamlbuild_config.ml --exclude=lib --exclude='*~' --exclude=_build -ur acc-0.1.orig/cparser/SimplExpr.ml acc-0.1/cparser/SimplExpr.ml
    1579 --- acc-0.1.orig/cparser/SimplExpr.ml   2010-09-28 16:14:19.000000000 +0100
    1580 +++ acc-0.1/cparser/SimplExpr.ml        2010-09-28 16:14:33.000000000 +0100
    1581 @@ -92,12 +92,13 @@
     1593diff --git a/cparser/SimplExpr.ml b/cparser/SimplExpr.ml
     1594index 330b184..8202cb2 100644
     1595--- a/cparser/SimplExpr.ml
     1596+++ b/cparser/SimplExpr.ml
     1597@@ -92,12 +92,13 @@ let simpl_expr loc env e act =
    15821598 
    15831599   let eboolvalof e =
     
    15951611 
    15961612   let sif e s1 s2 =
    1597 @@ -149,15 +150,15 @@
     1613@@ -149,15 +150,15 @@ let simpl_expr loc env e act =
    15981614 
    15991615         | Ominus | Oplus | Olognot | Onot | Oderef | Oarrow _ ->
     
    16141630         | Opreincr | Opredecr ->
    16151631             let (s1, e1') = simpl e1 LHS in
    1616 @@ -165,7 +166,7 @@
     1632@@ -165,7 +166,7 @@ let simpl_expr loc env e act =
    16171633             let op' = match op with Opreincr -> Oadd | _ -> Osub in
    16181634             let ty = unary_conversion env e.etyp in
     
    16231639             | Drop ->
    16241640                 (sseq s1 (sseq s2 (sassign e1' e3)), voidconst)
    1625 @@ -184,12 +185,12 @@
     1641@@ -184,12 +185,12 @@ let simpl_expr loc env e act =
    16261642             | Drop ->
    16271643                 let (s2, e2') = lhs_to_rhs e1' in
     
    16381654                        tmp
    16391655             end
    1640 @@ -205,7 +206,7 @@
     1656@@ -205,7 +206,7 @@ let simpl_expr loc env e act =
    16411657             let (s1, e1') = simpl e1 RHS in
    16421658             let (s2, e2') = simpl e2 RHS in
     
    16471663         | Oassign ->
    16481664             if act = Drop && is_simpl_expr e1 then
    1649 @@ -239,7 +240,7 @@
     1665@@ -239,7 +240,7 @@ let simpl_expr loc env e act =
    16501666               | Oshl_assign -> Oshl    | Oshr_assign -> Oshr
    16511667               | _ -> assert false in
     
    16561672             | Drop ->
    16571673                 (sseq s1 (sseq s11 (sseq s2 (sassign e1' e3))), voidconst)
    1658 @@ -259,7 +260,7 @@
     1674@@ -259,7 +260,7 @@ let simpl_expr loc env e act =
    16591675             let (s1, e1') = simpl e1 RHS in
    16601676             if is_simpl_expr e2 then begin
     
    16651681               match act with
    16661682               | Drop ->
    1667 @@ -284,7 +285,7 @@
     1683@@ -284,7 +285,7 @@ let simpl_expr loc env e act =
    16681684             let (s1, e1') = simpl e1 RHS in
    16691685             if is_simpl_expr e2 then begin
     
    16741690               match act with
    16751691               | Drop ->
    1676 @@ -310,7 +311,7 @@
     1692@@ -310,7 +311,7 @@ let simpl_expr loc env e act =
    16771693     | EConditional(e1, e2, e3) ->
    16781694         let (s1, e1') = simpl e1 RHS in
     
    16831699           match act with
    16841700           | Drop ->
    1685 @@ -336,13 +337,13 @@
     1701@@ -336,13 +337,13 @@ let simpl_expr loc env e act =
    16861702             simpl e1 act
    16871703         end else begin
     
    16991715         | Drop ->
    17001716             (sseq s1 (sseq s2 {sdesc = Sdo e2; sloc=loc}), voidconst)
    1701 @@ -481,7 +482,7 @@
     1717@@ -481,7 +482,7 @@ let simpl_statement env s =
    17021718         let (s', _) = simpl_expr s.sloc env e (Set tmp) in
    17031719         let s_init =
     
    17081724         {sdesc = Sfor(s_init, tmp, s', simpl_stmt s1); sloc = s.sloc}
    17091725       end
    1710 diff -N --exclude=myocamlbuild_config.ml --exclude=lib --exclude='*~' --exclude=_build -ur acc-0.1.orig/cparser/StructAssign.ml acc-0.1/cparser/StructAssign.ml
    1711 --- acc-0.1.orig/cparser/StructAssign.ml        2010-09-28 16:14:20.000000000 +0100
    1712 +++ acc-0.1/cparser/StructAssign.ml     2010-09-28 16:14:33.000000000 +0100
    1713 @@ -28,9 +28,9 @@
     1726diff --git a/cparser/StructAssign.ml b/cparser/StructAssign.ml
     1727index f5cecfc..5af7bed 100644
     1728--- a/cparser/StructAssign.ml
     1729+++ b/cparser/StructAssign.ml
     1730@@ -28,9 +28,9 @@ let maxsize = ref 8
    17141731 let need_memcpy = ref (None: ident option)
    17151732 
     
    17241741        false, [])
    17251742 
    1726 @@ -43,6 +43,11 @@
     1743@@ -43,6 +43,11 @@ let memcpy_ident () =
    17271744   | Some id ->
    17281745       id
     
    17361753 
    17371754   let num_assign = ref 0 in
    1738 @@ -62,9 +67,9 @@
     1755@@ -62,9 +67,9 @@ let transf_assign env loc lhs rhs =
    17391756         transf_struct l r ci.ci_members
    17401757     | TUnion(id, attr) ->
     
    17491766         sskip                           (* will be ignored later *)
    17501767     | _ ->
    1751 @@ -73,28 +78,29 @@
     1768@@ -73,28 +78,29 @@ let transf_assign env loc lhs rhs =
    17521769   and transf_struct l r = function
    17531770     | [] -> sskip
     
    17901807 
    17911808 let rec transf_stmt env s =
    1792 @@ -136,7 +142,7 @@
     1809@@ -136,7 +142,7 @@ let program p =
    17931810   match !need_memcpy with
    17941811   | None -> p'
     
    17991816 
    18001817 (* Horrible hack *)
    1801 diff -N --exclude=myocamlbuild_config.ml --exclude=lib --exclude='*~' --exclude=_build -ur acc-0.1.orig/cparser/StructByValue.ml acc-0.1/cparser/StructByValue.ml
    1802 --- acc-0.1.orig/cparser/StructByValue.ml       2010-09-28 16:14:19.000000000 +0100
    1803 +++ acc-0.1/cparser/StructByValue.ml    2010-09-28 16:14:33.000000000 +0100
    1804 @@ -38,21 +38,21 @@
     1818diff --git a/cparser/StructByValue.ml b/cparser/StructByValue.ml
     1819index de79737..60e088b 100644
     1820--- a/cparser/StructByValue.ml
     1821+++ b/cparser/StructByValue.ml
     1822@@ -38,21 +38,21 @@ let rec transf_type env t =
    18051823       let tres' = transf_type env tres in
    18061824       if is_composite_type env tres then begin
     
    18301848 
    18311849 (* Simple exprs: no change in structure, since calls cannot occur within,
    1832 @@ -60,6 +60,7 @@
     1850@@ -60,6 +60,7 @@ and transf_funarg env (id, t) =
    18331851 
    18341852 let rec transf_expr env e =
     
    18381856       | EConst c -> EConst c
    18391857       | ESizeof ty -> ESizeof (transf_type env ty)
    1840 @@ -104,7 +105,7 @@
     1858@@ -104,7 +105,7 @@ and transf_expr e = transf_expr env e in
    18411859 let transf_arg e =
    18421860   let e' = transf_expr e in
     
    18471865 in
    18481866 
    1849 @@ -118,25 +119,25 @@
     1867@@ -118,25 +119,25 @@ in
    18501868 let rec transf_stmt s =
    18511869   match s.sdesc with
     
    18811899       {s with sdesc = Sdo(transf_expr e)}
    18821900   | Sseq(s1, s2) ->
    1883 @@ -184,14 +185,15 @@
     1901@@ -184,14 +185,15 @@ let transf_params loc env params =
    18841902       let ty = transf_type env ty in
    18851903       if is_composite_type env ty then begin
     
    19011919       end else begin
    19021920         let (params', decls, init) = transf_prm params in
    1903 @@ -206,9 +208,9 @@
     1921@@ -206,9 +208,9 @@ let transf_fundef env f =
    19041922   let (ret1, params1, body1) =
    19051923     if is_composite_type env ret then begin
     
    19141932        (vres, tres) :: params,
    19151933        transf_funbody env f.fd_body (Some eeres))
    1916 diff -N --exclude=myocamlbuild_config.ml --exclude=lib --exclude='*~' --exclude=_build -ur acc-0.1.orig/cparser/Transform.ml acc-0.1/cparser/Transform.ml
    1917 --- acc-0.1.orig/cparser/Transform.ml   2010-09-28 16:14:20.000000000 +0100
    1918 +++ acc-0.1/cparser/Transform.ml        2010-09-28 16:14:33.000000000 +0100
    1919 @@ -33,7 +33,7 @@
     1934diff --git a/cparser/Transform.ml b/cparser/Transform.ml
     1935index b7f57f3..1a9dd20 100644
     1936--- a/cparser/Transform.ml
     1937+++ b/cparser/Transform.ml
     1938@@ -33,7 +33,7 @@ let new_temp_var ?(name = "t") ty =
    19201939 
    19211940 let new_temp ?(name = "t") ty =
     
    19261945 let get_temps () =
    19271946   let temps = !temporaries in
    1928 @@ -58,11 +58,11 @@
     1947@@ -58,11 +58,11 @@ let program
    19291948   | g :: gl ->
    19301949       let (desc', env') =
     
    19411960             (Gcompositedecl(su, id),
    19421961              Env.add_composite env id (composite_info_decl env su))
    1943 diff -N --exclude=myocamlbuild_config.ml --exclude=lib --exclude='*~' --exclude=_build -ur acc-0.1.orig/cparser/Unblock.ml acc-0.1/cparser/Unblock.ml
    1944 --- acc-0.1.orig/cparser/Unblock.ml     2010-09-28 16:14:19.000000000 +0100
    1945 +++ acc-0.1/cparser/Unblock.ml  2010-09-28 16:14:33.000000000 +0100
    1946 @@ -32,32 +32,33 @@
     1962diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml
     1963index fa304b7..d19940a 100644
     1964--- a/cparser/Unblock.ml
     1965+++ b/cparser/Unblock.ml
     1966@@ -32,32 +32,33 @@ let rec local_initializer loc env path init k =
    19471967   match init with
    19481968   | Init_single e ->
     
    19852005 
    19862006 (* Record new variables to be locally defined *)
    1987 @@ -82,7 +83,7 @@
     2007@@ -82,7 +83,7 @@ let process_decl loc env (sto, id, ty, optinit) k =
    19882008   match optinit with
    19892009   | None -> k
     
    19942014 (* Simplification of blocks within a statement *)
    19952015 
    1996 diff -N --exclude=myocamlbuild_config.ml --exclude=lib --exclude='*~' --exclude=_build -ur acc-0.1.orig/src/acc.ml acc-0.1/src/acc.ml
    1997 --- acc-0.1.orig/src/acc.ml     2010-09-28 16:14:22.000000000 +0100
    1998 +++ acc-0.1/src/acc.ml  2010-10-05 16:08:56.000000000 +0100
    1999 @@ -33,11 +33,15 @@
     2016diff --git a/src/acc.ml b/src/acc.ml
     2017index c8f6592..e2f782c 100644
     2018--- a/src/acc.ml
     2019+++ b/src/acc.ml
     2020@@ -33,11 +33,15 @@ let process filename =
    20002021       src_language tgt_language input_ast
    20012022   in
     
    20152036     let asts = input_ast :: target_asts in
    20162037     let label_traces = List.map Languages.interpret asts in
    2017 Binary files acc-0.1.orig/src/.acc.ml.swp and acc-0.1/src/.acc.ml.swp differ
    2018 diff -N --exclude=myocamlbuild_config.ml --exclude=lib --exclude='*~' --exclude=_build -ur acc-0.1.orig/src/clight/clightFromC.ml acc-0.1/src/clight/clightFromC.ml
    2019 --- acc-0.1.orig/src/clight/clightFromC.ml      2010-09-28 16:14:22.000000000 +0100
    2020 +++ acc-0.1/src/clight/clightFromC.ml   2010-10-06 13:13:44.000000000 +0100
    2021 @@ -19,7 +19,7 @@
     2038diff --git a/src/clight/clight.mli b/src/clight/clight.mli
     2039index 4c9d638..b831ef0 100644
     2040--- a/src/clight/clight.mli
     2041+++ b/src/clight/clight.mli
     2042@@ -7,6 +7,8 @@ open AST
     2043 
     2044 (** ** Types *)
     2045 
     2046+type memory_space = Any | Data | IData | PData | XData | Code
     2047+
     2048 (** Clight types are similar to those of C.  They include numeric types,
     2049   pointers, arrays, function types, and composite types (struct and
     2050   union).  Numeric types (integers and floats) fully specify the
     2051@@ -61,8 +63,8 @@ type ctype =
     2052   | Tvoid                                      (**r the [void] type *)
     2053   | Tint of intsize*signedness                 (**r integer types *)
     2054   | Tfloat of floatsize                                (**r floating-point types *)
     2055-  | Tpointer of ctype                          (**r pointer types ([*ty]) *)
     2056-  | Tarray of ctype*int                                (**r array types ([ty[len]]) *)
     2057+  | Tpointer of memory_space * ctype           (**r pointer types ([*ty]) *)
     2058+  | Tarray of memory_space * ctype*int         (**r array types ([ty[len]]) *)
     2059   | Tfunction of ctype list*ctype              (**r function types *)
     2060   | Tstruct of ident*(ident*ctype) list
     2061   (**r struct types *)
     2062@@ -199,5 +201,5 @@ type init_data =
     2063 type program = {
     2064   prog_funct: (ident * fundef) list ;
     2065   prog_main: ident;
     2066-  prog_vars: ((ident * init_data list) * ctype) list
     2067+  prog_vars: (((ident * init_data list) * memory_space) * ctype) list
     2068 }
     2069diff --git a/src/clight/clightFromC.ml b/src/clight/clightFromC.ml
     2070index 0aacbce..0a4b947 100644
     2071--- a/src/clight/clightFromC.ml
     2072+++ b/src/clight/clightFromC.ml
     2073@@ -19,7 +19,7 @@ let rec alignof = function
    20222074   | Tfloat F32 -> 4
    20232075   | Tfloat F64 -> 8
     
    20282080   | Tstruct (_,fld) -> alignof_fields fld
    20292081   | Tunion (_,fld) -> alignof_fields fld
    2030 @@ -42,7 +42,7 @@
     2082@@ -42,7 +42,7 @@ let rec sizeof t =
    20312083     | Tfloat F32 -> 4
    20322084     | Tfloat F64 -> 8
     
    20372089     | Tstruct (_,fld) -> align (max 1 (sizeof_struct fld 0)) (alignof t)
    20382090     | Tunion (_,fld) -> align (max 1 (sizeof_union fld)) (alignof t)
    2039 @@ -102,14 +102,14 @@
     2091@@ -102,14 +102,14 @@ let name_for_string_literal env s =
    20402092     Hashtbl.add decl_atom id
    20412093       (env, (C.Storage_static,
     
    20542106 let global_for_string s id =
    20552107   let init = ref [] in
    2056 @@ -119,7 +119,7 @@
     2108@@ -119,7 +119,7 @@ let global_for_string s id =
    20572109        :: !init in
    20582110   add_char '\000';
     
    20632115 let globals_for_strings globs =
    20642116   Hashtbl.fold
    2065 @@ -143,7 +143,7 @@
     2117@@ -143,7 +143,7 @@ let register_stub_function name tres targs =
    20662118     let rec types_of_types = function
    20672119       | [] -> []
     
    20722124     Hashtbl.add stub_function_table stub_name stub_type;
    20732125     (stub_name, stub_type)
    2074 @@ -193,6 +193,14 @@
     2126@@ -193,6 +193,14 @@ let convertFkind = function
    20752127       if not !ClightFlags.option_flonglong then unsupported "'long double' type";
    20762128       F64
     
    20872139 
    20882140   let rec convertTyp seen t =
    2089 @@ -202,19 +210,19 @@
     2141@@ -202,19 +210,19 @@ let convertTyp env t =
    20902142         let (sg, sz) = convertIkind ik in Tint(sz, sg)
    20912143     | C.TFloat(fk, a) ->
     
    21152167         if va then unsupported "variadic function type";
    21162168         if Cutil.is_composite_type env tres then
    2117 @@ -298,7 +306,7 @@
     2169@@ -298,7 +306,7 @@ let rec convertExpr env e =
    21182170       let e1' = convertExpr env e1 in
    21192171       let ty1 =
     
    21242176       Expr(Efield(Expr(Ederef(convertExpr env e1), ty1),
    21252177                    id), ty)
    2126 @@ -315,7 +323,7 @@
     2178@@ -315,7 +323,7 @@ let rec convertExpr env e =
    21272179 
    21282180   | C.EBinop(C.Oindex, e1, e2, _) ->
     
    21332185       Expr(Eandbool(convertExpr env e1, convertExpr env e2), ty)
    21342186   | C.EBinop(C.Ologor, e1, e2, _) ->
    2135 @@ -354,7 +362,7 @@
     2187@@ -354,7 +362,7 @@ let rec convertExpr env e =
    21362188 let rec projFunType env ty =
    21372189   match Cutil.unroll env ty with
     
    21422194 
    21432195 let convertFuncall env lhs fn args =
    2144 @@ -400,19 +408,19 @@
     2196@@ -400,19 +408,19 @@ let volatile_fun_suffix_type ty =
    21452197   | Tfloat F32 -> ("float32", ty)
    21462198   | Tfloat F64 -> ("float64", ty)
     
    21652217 (* Toplevel expression, argument of an Sdo *)
    21662218 
    2167 @@ -432,11 +440,11 @@
     2219@@ -432,11 +440,11 @@ let convertTopExpr env e =
    21682220       | false, true ->                  (* volatile read *)
    21692221           Scall(Some lhs',
     
    21792231           Sassign(convertExpr env lhs, convertExpr env rhs)
    21802232       end
    2181 @@ -663,7 +671,7 @@
     2233@@ -663,7 +671,7 @@ let convertInit env ty init =
    21822234   | Init_array il ->
    21832235       let ty_elt =
     
    21882240       List.iter (cvtInit ty_elt) il
    21892241   | Init_struct(_, flds) ->
    2190 @@ -690,7 +698,7 @@
     2242@@ -690,7 +698,7 @@ let convertInit env ty init =
    21912243 
    21922244 (** Global variable *)
     
    21972249   let ty' = convertTyp env ty in
    21982250   let init' =
    2199 @@ -701,7 +709,7 @@
     2251@@ -701,7 +709,7 @@ let convertGlobvar env (sto, id, ty, optinit as decl) =
    22002252         convertInit env ty i in
    22012253   Hashtbl.add decl_atom id' (env, decl);
     
    22062258 (** Convert a list of global declarations.
    22072259   Result is a pair [(funs, vars)] where [funs] are
    2208 @@ -714,7 +722,7 @@
     2260@@ -714,7 +722,7 @@ let rec convertGlobdecls env funs vars gl =
    22092261   | g :: gl' ->
    22102262       updateLoc g.gloc;
     
    22152267              Variadic functions are skipped.
    22162268              Other types become variable declarations. *)
    2217 @@ -727,7 +735,7 @@
     2269@@ -727,7 +735,7 @@ let rec convertGlobdecls env funs vars gl =
    22182270           | TFun(_, _, true, _) ->
    22192271               convertGlobdecls env funs vars gl'
     
    22242276       | C.Gfundef fd ->
    22252277           convertGlobdecls env (convertFundef env fd :: funs) vars gl'
    2226 @@ -769,11 +777,11 @@
     2278@@ -769,11 +777,11 @@ let cleanupGlobals p =
    22272279     | g :: gl ->
    22282280         updateLoc g.gloc;
     
    22382290               error ("multiple definitions of " ^ id.name);
    22392291             clean (IdentSet.add id defs) (g :: accu) gl
    2240 @@ -815,7 +823,7 @@
     2292@@ -815,7 +823,7 @@ let rec type_is_readonly env t =
    22412293   if List.mem C.AVolatile a then false else
    22422294   if List.mem C.AConst a then true else
     
    22472299 
    22482300 let atom_is_static a =
    2249 @@ -853,42 +861,42 @@
     2301@@ -853,42 +861,42 @@ open Builtins
    22502302 let builtins_generic = {
    22512303   typedefs = [
     
    23072359 }
    23082360 
    2309 diff -N --exclude=myocamlbuild_config.ml --exclude=lib --exclude='*~' --exclude=_build -ur acc-0.1.orig/src/clight/clightInterpret.ml acc-0.1/src/clight/clightInterpret.ml
    2310 --- acc-0.1.orig/src/clight/clightInterpret.ml  2010-09-28 16:14:22.000000000 +0100
    2311 +++ acc-0.1/src/clight/clightInterpret.ml       2010-09-28 16:47:52.000000000 +0100
    2312 @@ -29,7 +29,7 @@
     2361diff --git a/src/clight/clightInterpret.ml b/src/clight/clightInterpret.ml
     2362index 32b9884..b744932 100644
     2363--- a/src/clight/clightInterpret.ml
     2364+++ b/src/clight/clightInterpret.ml
     2365@@ -29,7 +29,7 @@ let rec sizeof = function
    23132366   | Tfloat F32 -> 4
    23142367   | Tfloat F64 -> 8
     
    23192372   | Tstruct (_,_) -> assert false
    23202373   | Tunion (_,_) -> assert false
    2321 @@ -46,7 +46,7 @@
     2374@@ -46,7 +46,7 @@ let rec mq_of_ty = function
    23222375   | Tfloat F32 -> assert false
    23232376   | Tfloat F64 -> Memory.MQ_float64
     
    23282381   | Tstruct (_,_) -> assert false
    23292382   | Tunion (_,_) -> assert false
    2330 @@ -207,7 +207,7 @@
     2383@@ -207,7 +207,7 @@ let eval_cast = function
    23312384   | (Value.Val_float f,_,Tfloat F64) -> Value.Val_float f
    23322385   (* Cast pointeur *)
     
    23372390   | (e,a,b) when a=b -> e
    23382391   (* error *)
    2339 @@ -232,13 +232,13 @@
     2392@@ -232,13 +232,13 @@ let eval_add = function
    23402393       Value.Val_int (cast_int (i1+i2) t1)     
    23412394   | ((Value.Val_float i1,Tfloat F64) , (Value.Val_float i2,Tfloat F64)) ->
     
    23552408   | ((v1,_),(v2,_)) ->
    23562409       print_string ("Debug: add "^(Value.string_of_value v1)^" with "
    2357 @@ -250,13 +250,13 @@
     2410@@ -250,13 +250,13 @@ let eval_sub = function
    23582411       Value.Val_int (cast_int (i1-i2) t1)   
    23592412   | ((Value.Val_float i1,Tfloat F64) , (Value.Val_float i2,Tfloat F64)) ->
     
    23732426   | _ -> assert false
    23742427 
    2375 @@ -475,9 +475,9 @@
     2428@@ -475,9 +475,9 @@ let bind_parameters m (param_l:(ident*ctype) list) (arg_l:Value.t list) (var_l:(
    23762429     | _ -> assert false
    23772430   and treat_v (m,e) = function
     
    23852438     | var::l -> treat_v (bind m e var Value.Val_undef) l
    23862439   in treat_v (treat_p (m,(Hashtbl.create 11)) (param_l,arg_l)) var_l
    2387 diff -N --exclude=myocamlbuild_config.ml --exclude=lib --exclude='*~' --exclude=_build -ur acc-0.1.orig/src/clight/clight.mli acc-0.1/src/clight/clight.mli
    2388 --- acc-0.1.orig/src/clight/clight.mli  2010-09-28 16:14:22.000000000 +0100
    2389 +++ acc-0.1/src/clight/clight.mli       2010-10-06 13:13:21.000000000 +0100
    2390 @@ -7,6 +7,8 @@
    2391  
    2392  (** ** Types *)
    2393  
    2394 +type memory_space = Any | Data | IData | PData | XData | Code
    2395 +
    2396  (** Clight types are similar to those of C.  They include numeric types,
    2397    pointers, arrays, function types, and composite types (struct and
    2398    union).  Numeric types (integers and floats) fully specify the
    2399 @@ -61,8 +63,8 @@
    2400    | Tvoid                                      (**r the [void] type *)
    2401    | Tint of intsize*signedness                 (**r integer types *)
    2402    | Tfloat of floatsize                                (**r floating-point types *)
    2403 -  | Tpointer of ctype                          (**r pointer types ([*ty]) *)
    2404 -  | Tarray of ctype*int                                (**r array types ([ty[len]]) *)
    2405 +  | Tpointer of memory_space * ctype           (**r pointer types ([*ty]) *)
    2406 +  | Tarray of memory_space * ctype*int         (**r array types ([ty[len]]) *)
    2407    | Tfunction of ctype list*ctype              (**r function types *)
    2408    | Tstruct of ident*(ident*ctype) list
    2409    (**r struct types *)
    2410 @@ -199,5 +201,5 @@
    2411  type program = {
    2412    prog_funct: (ident * fundef) list ;
    2413    prog_main: ident;
    2414 -  prog_vars: ((ident * init_data list) * ctype) list
    2415 +  prog_vars: (((ident * init_data list) * memory_space) * ctype) list
    2416  }
    2417 diff -N --exclude=myocamlbuild_config.ml --exclude=lib --exclude='*~' --exclude=_build -ur acc-0.1.orig/src/clight/clightPrinter.ml acc-0.1/src/clight/clightPrinter.ml
    2418 --- acc-0.1.orig/src/clight/clightPrinter.ml    2010-09-28 16:14:22.000000000 +0100
    2419 +++ acc-0.1/src/clight/clightPrinter.ml 2010-09-28 16:48:51.000000000 +0100
    2420 @@ -85,9 +85,9 @@
    2421        name_inttype sz sg ^ name_optid id
    2422    | Tfloat sz ->
    2423        name_floattype sz ^ name_optid id
    2424 -  | Tpointer t ->
    2425 +  | Tpointer (_,t) ->
    2426        name_cdecl ("*" ^ id) t
    2427 -  | Tarray(t, n) ->
    2428 +  | Tarray(_, t, n) ->
    2429        name_cdecl
    2430          (sprintf "%s[%ld]" (parenthesize_if_pointer id) (Int32.of_int n))
    2431          t
    2432 @@ -376,7 +376,7 @@
    2433  
    2434  let re_string_literal = Str.regexp "__stringlit_[0-9]+"
    2435  
    2436 -let print_globvar p (((id, init), ty)) =
    2437 +let print_globvar p ((((id, init), _), ty)) =
    2438    match init with
    2439    | [] ->
    2440        fprintf p "extern %s;@ @ "
    2441 @@ -404,8 +404,8 @@
    2442    | Tvoid -> ()
    2443    | Tint(sz, sg) -> ()
    2444    | Tfloat sz -> ()
    2445 -  | Tpointer t -> collect_type t
    2446 -  | Tarray(t, n) -> collect_type t
    2447 +  | Tpointer (_,t) -> collect_type t
    2448 +  | Tarray(_, t, n) -> collect_type t
    2449    | Tfunction(args, res) -> collect_type_list args; collect_type res
    2450    | Tstruct(id, fld) -> register_struct_union id fld; collect_fields fld
    2451    | Tunion(id, fld) -> register_struct_union id fld; collect_fields fld
    2452 diff -N --exclude=myocamlbuild_config.ml --exclude=lib --exclude='*~' --exclude=_build -ur acc-0.1.orig/src/clight/clightPrintMatita.ml acc-0.1/src/clight/clightPrintMatita.ml
    2453 --- acc-0.1.orig/src/clight/clightPrintMatita.ml        1970-01-01 01:00:00.000000000 +0100
    2454 +++ acc-0.1/src/clight/clightPrintMatita.ml     2010-10-06 13:14:39.000000000 +0100
    2455 @@ -0,0 +1,485 @@
     2440diff --git a/src/clight/clightPrintMatita.ml b/src/clight/clightPrintMatita.ml
     2441new file mode 100644
     2442index 0000000..a5e50b8
     2443--- /dev/null
     2444+++ b/src/clight/clightPrintMatita.ml
     2445@@ -0,0 +1,483 @@
    24562446+(* *********************************************************************)
    24572447+(*                                                                     *)
     
    26542644+
    26552645+let rec print_expr p (Expr (eb, ty)) =
    2656 +  fprintf p "@[<hov 2>(Expr ";
    2657 +  begin
     2646+  fprintf p "@[<hov 2>(Expr %a@ %s)@]" print_expr_descr eb (stype ty)
     2647+and print_expr_descr p eb =
    26582648+  match eb with
    2659 +  | Ecost (_, e) -> print_expr p e
     2649+  | Ecost (_, Expr (e, _)) -> print_expr_descr p e
    26602650+  | Econst_int n ->
    26612651+      fprintf p "(Econst_int (repr %d))" n
     
    26962686+  | Efield(e1, id) ->
    26972687+      fprintf p "(Efield %a (succ_pos_of_nat %i))" print_expr e1 (id_i id)
    2698 +  end;
    2699 +  fprintf p " %s)@]" (stype ty)
    27002688+
    27012689+let rec print_expr_list p (first, el) =
     
    29392927+
    29402928+
    2941 diff -N --exclude=myocamlbuild_config.ml --exclude=lib --exclude='*~' --exclude=_build -ur acc-0.1.orig/src/clight/clightToCminor.ml acc-0.1/src/clight/clightToCminor.ml
    2942 --- acc-0.1.orig/src/clight/clightToCminor.ml   2010-09-28 16:14:22.000000000 +0100
    2943 +++ acc-0.1/src/clight/clightToCminor.ml        2010-09-28 16:52:37.000000000 +0100
    2944 @@ -7,7 +7,7 @@
     2929diff --git a/src/clight/clightPrinter.ml b/src/clight/clightPrinter.ml
     2930index c458e36..b1efd87 100644
     2931--- a/src/clight/clightPrinter.ml
     2932+++ b/src/clight/clightPrinter.ml
     2933@@ -19,6 +19,15 @@ open Format
     2934 open AST
     2935 open Clight
     2936 
     2937+let name_space = function
     2938+  | Any -> ""
     2939+  | Data -> "__data "
     2940+  | IData -> "__idata "
     2941+  | PData -> "__pdata "
     2942+  | XData -> "__xdata "
     2943+  | Code -> "__code "
     2944+
     2945+
     2946 let name_unop = function
     2947   | Onotbool -> "!"
     2948   | Onotint  -> "~"
     2949@@ -77,22 +86,28 @@ let name_optid id =
     2950 let parenthesize_if_pointer id =
     2951   if String.length id > 0 && id.[0] = '*' then "(" ^ id ^ ")" else id
     2952 
     2953-let rec name_cdecl id ty =
     2954+(* Use Any for the space when nothing should appear. *)
     2955+
     2956+let rec name_cdecl sp id ty =
     2957+  let ssp = name_space sp in
     2958   match ty with
     2959   | Tvoid ->
     2960-      "void" ^ name_optid id
     2961+      ssp ^ "void" ^ name_optid id
     2962   | Tint(sz, sg) ->
     2963-      name_inttype sz sg ^ name_optid id
     2964+      ssp ^ name_inttype sz sg ^ name_optid id
     2965   | Tfloat sz ->
     2966-      name_floattype sz ^ name_optid id
     2967-  | Tpointer t ->
     2968-      name_cdecl ("*" ^ id) t
     2969-  | Tarray(t, n) ->
     2970+      ssp ^ name_floattype sz ^ name_optid id
     2971+  | Tpointer (sp',t) ->
     2972+      name_cdecl sp' ("* " ^ ssp ^ id) t
     2973+  | Tarray(sp', t, n) ->
     2974+      if sp <> sp' then eprintf "Array %s has wrong memory space.\n%!" id;
     2975       name_cdecl
     2976+        sp'
     2977         (sprintf "%s[%ld]" (parenthesize_if_pointer id) (Int32.of_int n))
     2978         t
     2979   | Tfunction(args, res) ->
     2980       let b = Buffer.create 20 in
     2981+      Buffer.add_string b ssp;
     2982       if id = ""
     2983       then Buffer.add_string b "(*)"
     2984       else Buffer.add_string b (parenthesize_if_pointer id);
     2985@@ -105,22 +120,22 @@ let rec name_cdecl id ty =
     2986           | [] -> ()
     2987           | t1::tl ->
     2988               if not first then Buffer.add_string b ", ";
     2989-              Buffer.add_string b (name_cdecl "" t1);
     2990+              Buffer.add_string b (name_cdecl Any "" t1);
     2991               add_args false tl in
     2992           add_args true args
     2993       end;
     2994       Buffer.add_char b ')';
     2995-      name_cdecl (Buffer.contents b) res
     2996+      name_cdecl Any (Buffer.contents b) res
     2997   | Tstruct(name, fld) ->
     2998-      name ^ name_optid id
     2999+      ssp ^ name ^ name_optid id
     3000   | Tunion(name, fld) ->
     3001-      name ^ name_optid id
     3002+      ssp ^ name ^ name_optid id
     3003   | Tcomp_ptr name ->
     3004-      name ^ " *" ^ id
     3005+      ssp ^ name ^ " *" ^ id
     3006 
     3007 (* Type *)
     3008 
     3009-let name_type ty = name_cdecl "" ty
     3010+let name_type ty = name_cdecl Any "" ty
     3011 
     3012 (* Expressions *)
     3013 
     3014@@ -318,7 +333,7 @@ let name_function_parameters fun_name params =
     3015       | [] -> ()
     3016       | (id, ty) :: rem ->
     3017           if not first then Buffer.add_string b ", ";
     3018-          Buffer.add_string b (name_cdecl id ty);
     3019+          Buffer.add_string b (name_cdecl Any id ty);
     3020           add_params false rem in
     3021       add_params true params
     3022   end;
     3023@@ -327,12 +342,13 @@ let name_function_parameters fun_name params =
     3024 
     3025 let print_function p id f =
     3026   fprintf p "%s@ "
     3027-            (name_cdecl (name_function_parameters id f.fn_params)
     3028+            (name_cdecl Any
     3029+                        (name_function_parameters id f.fn_params)
     3030                         f.fn_return);
     3031   fprintf p "@[<v 2>{@ ";
     3032   List.iter
     3033     (fun ((id, ty)) ->
     3034-      fprintf p "%s;@ " (name_cdecl id ty))
     3035+      fprintf p "%s;@ " (name_cdecl Any id ty))
     3036     f.fn_vars;
     3037   print_stmt p f.fn_body;
     3038   fprintf p "@;<0 -2>}@]@ @ "
     3039@@ -341,7 +357,7 @@ let print_fundef p (id, fd) =
     3040   match fd with
     3041   | External(_, args, res) ->
     3042       fprintf p "extern %s;@ @ "
     3043-                (name_cdecl id (Tfunction(args, res)))
     3044+                (name_cdecl Any id (Tfunction(args, res)))
     3045   | Internal f ->
     3046       print_function p id f
     3047 
     3048@@ -376,17 +392,17 @@ let print_init p = function
     3049 
     3050 let re_string_literal = Str.regexp "__stringlit_[0-9]+"
     3051 
     3052-let print_globvar p (((id, init), ty)) =
     3053+let print_globvar p ((((id, init), sp), ty)) =
     3054   match init with
     3055   | [] ->
     3056       fprintf p "extern %s;@ @ "
     3057-              (name_cdecl id ty)
     3058+              (name_cdecl sp id ty)
     3059   | [Init_space _] ->
     3060       fprintf p "%s;@ @ "
     3061-              (name_cdecl id ty)
     3062+              (name_cdecl sp id ty)
     3063   | _ ->
     3064       fprintf p "@[<hov 2>%s = "
     3065-              (name_cdecl id ty);
     3066+              (name_cdecl sp id ty);
     3067       if Str.string_match re_string_literal id 0
     3068       && List.for_all (function Init_int8 _ -> true | _ -> false) init
     3069       then
     3070@@ -404,8 +420,8 @@ let rec collect_type = function
     3071   | Tvoid -> ()
     3072   | Tint(sz, sg) -> ()
     3073   | Tfloat sz -> ()
     3074-  | Tpointer t -> collect_type t
     3075-  | Tarray(t, n) -> collect_type t
     3076+  | Tpointer (_,t) -> collect_type t
     3077+  | Tarray(_, t, n) -> collect_type t
     3078   | Tfunction(args, res) -> collect_type_list args; collect_type res
     3079   | Tstruct(id, fld) -> register_struct_union id fld; collect_fields fld
     3080   | Tunion(id, fld) -> register_struct_union id fld; collect_fields fld
     3081@@ -491,7 +507,7 @@ let print_struct_or_union p (name, fld) =
     3082   let rec print_fields = function
     3083   | [] -> ()
     3084   | (id, ty)::rem ->
     3085-      fprintf p "@ %s;" (name_cdecl id ty);
     3086+      fprintf p "@ %s;" (name_cdecl Any id ty);
     3087       print_fields rem in
     3088   print_fields fld;
     3089   fprintf p "@;<0 -2>};@]@ "
     3090diff --git a/src/clight/clightToCminor.ml b/src/clight/clightToCminor.ml
     3091index 956239e..8b76ff8 100644
     3092--- a/src/clight/clightToCminor.ml
     3093+++ b/src/clight/clightToCminor.ml
     3094@@ -7,7 +7,7 @@ let rec ctype_to_type_return t = match t with
    29453095   | Tint (_,_) -> Type_ret Sig_int
    29463096   | Tfloat _ -> Type_ret Sig_float
     
    29513101   | Tunion (_,_) | Tcomp_ptr _ -> assert false
    29523102 
    2953 @@ -15,7 +15,7 @@
     3103@@ -15,7 +15,7 @@ let rec ctype_to_sig_type t = match t with
    29543104   | Tint (_,_) -> Sig_int
    29553105   | Tfloat _ -> Sig_float
     
    29603110   | Tfunction (_,_) | Tstruct (_,_)| Tunion (_,_) | Tcomp_ptr _ ->
    29613111       assert false
    2962 @@ -31,7 +31,7 @@
     3112@@ -31,7 +31,7 @@ let rec mq_of_ty = function
    29633113   | Tfloat F32 -> assert false
    29643114   | Tfloat F64 -> Memory.MQ_float64
     
    29693119   | Tstruct (_,_) -> assert false
    29703120   | Tunion (_,_) -> assert false
    2971 @@ -59,15 +59,15 @@
     3121@@ -59,15 +59,15 @@ let rec size_of_ctype t = match t with
    29723122   | Tfloat F32 -> 8
    29733123   | Tfloat F64 -> 8
     
    29883138           assert false
    29893139 
    2990 @@ -95,13 +95,13 @@
     3140@@ -95,13 +95,13 @@ let translate_binop t1 e1 t2 e2 = function
    29913141       (match (t1,t2) with
    29923142          | (Tint(_,_),Tint(_,_)) -> Op2 (Op_add,e1,e2)
     
    30063156          | _ -> assert false
    30073157       )
    3008 @@ -109,13 +109,13 @@
     3158@@ -109,13 +109,13 @@ let translate_binop t1 e1 t2 e2 = function
    30093159       (match (t1,t2) with
    30103160          | (Tint(_,_),Tint(_,_)) -> Op2 (Op_sub,e1,e2)
     
    30243174          | _ -> assert false
    30253175       )
    3026 @@ -310,7 +310,7 @@
     3176@@ -310,7 +310,7 @@ let compute_stack f =
    30273177   and stck = ref 0 in
    30283178   let treat_var v = match snd v with 
     
    30333183           if size > 0 then (
    30343184             (Hashtbl.add addr_of_id (fst v) !stck);
    3035 @@ -400,7 +400,7 @@
     3185@@ -400,7 +400,7 @@ let translate_funct globals = function
    30363186   | (id,External (i,p,r)) -> (id, F_ext (translate_external i p r))
    30373187 
     
    30423192      Cminor.functs = List.map (translate_funct globals) p.prog_funct;
    30433193      Cminor.main = p.prog_main }
    3044 diff -N --exclude=myocamlbuild_config.ml --exclude=lib --exclude='*~' --exclude=_build -ur acc-0.1.orig/src/common/cminorMemory.ml acc-0.1/src/common/cminorMemory.ml
    3045 --- acc-0.1.orig/src/common/cminorMemory.ml     2010-09-28 16:14:22.000000000 +0100
    3046 +++ acc-0.1/src/common/cminorMemory.ml  2010-09-28 16:20:59.000000000 +0100
    3047 @@ -204,7 +204,7 @@
     3194diff --git a/src/common/cminorMemory.ml b/src/common/cminorMemory.ml
     3195index 1b3e509..813be71 100644
     3196--- a/src/common/cminorMemory.ml
     3197+++ b/src/common/cminorMemory.ml
     3198@@ -204,7 +204,7 @@ let rec sizeof = function
    30483199   | Tfloat F32 -> 4
    30493200   | Tfloat F64 -> 8
     
    30543205   | Tstruct (_,_) -> assert false
    30553206   | Tunion (_,_) -> assert false
    3056 @@ -227,7 +227,7 @@
     3207@@ -227,7 +227,7 @@ let vk_of_init_list = function (*FIXME*)
    30573208 let cast t v = v (*TODO*)
    30583209 
     
    30633214          | Some(b',m') ->
    30643215              (match store m' Memory.MQ_int32 b 0 (Val_ptr(b',0)) with
    3065 @@ -253,7 +253,7 @@
     3216@@ -253,7 +253,7 @@ let initmem_clight p =
    30663217   let b_of_id = Hashtbl.create 11
    30673218   and fd_of_b = Hashtbl.create 11
     
    30723223        | Some(b,m') ->
    30733224            Hashtbl.add b_of_id id b;
    3074 diff -N --exclude=myocamlbuild_config.ml --exclude=lib --exclude='*~' --exclude=_build -ur acc-0.1.orig/src/languages.ml acc-0.1/src/languages.ml
    3075 --- acc-0.1.orig/src/languages.ml       2010-09-28 16:14:22.000000000 +0100
    3076 +++ acc-0.1/src/languages.ml    2010-09-29 12:05:33.000000000 +0100
    3077 @@ -230,6 +230,27 @@
     3225diff --git a/src/languages.ml b/src/languages.ml
     3226index 4317d19..12ffdd2 100644
     3227--- a/src/languages.ml
     3228+++ b/src/languages.ml
     3229@@ -230,6 +230,27 @@ let save filename ast =
    30783230   flush cout;
    30793231   close_out cout
     
    31033255   | AstClight p ->
    31043256     ClightInterpret.interpret true p
    3105 diff -N --exclude=myocamlbuild_config.ml --exclude=lib --exclude='*~' --exclude=_build -ur acc-0.1.orig/src/languages.mli acc-0.1/src/languages.mli
    3106 --- acc-0.1.orig/src/languages.mli      2010-09-28 16:14:22.000000000 +0100
    3107 +++ acc-0.1/src/languages.mli   2010-09-29 12:07:22.000000000 +0100
    3108 @@ -75,6 +75,11 @@
     3257diff --git a/src/languages.mli b/src/languages.mli
     3258index 3dfc31a..f5d8e45 100644
     3259--- a/src/languages.mli
     3260+++ b/src/languages.mli
     3261@@ -75,6 +75,11 @@ val interpret : ast -> AST.label list
    31093262     is deduced from the language of the AST. *)
    31103263 val save : string -> ast -> unit
     
    31183271 val from_string : string -> name
    31193272 
    3120 diff -N --exclude=myocamlbuild_config.ml --exclude=lib --exclude='*~' --exclude=_build -ur acc-0.1.orig/src/options.ml acc-0.1/src/options.ml
    3121 --- acc-0.1.orig/src/options.ml 2010-09-28 16:14:22.000000000 +0100
    3122 +++ acc-0.1/src/options.ml      2010-09-29 10:27:10.000000000 +0100
    3123 @@ -39,6 +39,9 @@
     3273diff --git a/src/options.ml b/src/options.ml
     3274index 061f7d0..d47e558 100644
     3275--- a/src/options.ml
     3276+++ b/src/options.ml
     3277@@ -39,6 +39,9 @@ let debug_flag                        = ref false
    31243278 let set_debug                  = (:=) debug_flag
    31253279 let is_debug_enabled ()                = !debug_flag
     
    31313285   "-s", Arg.String set_source_language,
    31323286   " Choose the source language between:";
    3133 @@ -58,4 +61,7 @@
     3287@@ -58,4 +61,7 @@ let options = OptionsParsing.register [
    31343288 
    31353289   "-d", Arg.Set debug_flag,
     
    31393293+  " Output matita formatted Clight program.";
    31403294 ]
    3141 diff -N --exclude=myocamlbuild_config.ml --exclude=lib --exclude='*~' --exclude=_build -ur acc-0.1.orig/src/options.mli acc-0.1/src/options.mli
    3142 --- acc-0.1.orig/src/options.mli        2010-09-28 16:14:22.000000000 +0100
    3143 +++ acc-0.1/src/options.mli     2010-09-29 11:24:10.000000000 +0100
    3144 @@ -22,3 +22,6 @@
     3295diff --git a/src/options.mli b/src/options.mli
     3296index 4517400..ec6b020 100644
     3297--- a/src/options.mli
     3298+++ b/src/options.mli
     3299@@ -22,3 +22,6 @@ val input_files          : unit -> string list
    31453300 
    31463301 (** {2 Verbose mode} *)
Note: See TracChangeset for help on using the changeset viewer.