Ignore:
Timestamp:
Jun 3, 2011, 5:35:31 PM (9 years ago)
Author:
campbell
Message:

Sort out regions in Cminor to fix Clight to Cminor translation of Ederef.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/initialisation.ma

    r880 r881  
    2222   away. *)
    2323
    24 definition init_datum : ident → init_data → int (*offset?*) → stmt ≝
    25 λid,init,off.
     24definition init_datum : ident → region → init_data → int (*offset?*) → stmt ≝
     25λid,r,init,off.
    2626match init_expr init with
    2727[ None ⇒ St_skip
    2828| Some x ⇒
    2929    match x with [ dp chunk e ⇒
    30       St_store ? chunk (Cst ? (Oaddrsymbol id off)) e
     30      St_store ? r chunk (Cst ? (Oaddrsymbol id off)) e
    3131    ]
    3232].
    3333
    34 definition init_var : ident → list init_data → stmt ≝
    35 λid,init.
     34definition init_var : ident → region → list init_data → stmt ≝
     35λid,r,init.
    3636\snd (foldr ??
    3737  (λdatum,os.
    3838   let 〈off,s〉 ≝ os in
    39      〈addition_n ? off (repr (size_init_data datum)), St_seq (init_datum id datum off) s〉)
     39     〈addition_n ? off (repr (size_init_data datum)), St_seq (init_datum id r datum off) s〉)
    4040  〈zero, St_skip〉 init).
    4141
    4242definition init_vars : list (ident × (list init_data) × region × unit) → stmt ≝
    4343λvars. foldr ??
    44   (λvar,s. St_seq s (init_var (\fst (\fst (\fst var))) (\snd (\fst (\fst var))))) St_skip vars.
     44  (λvar,s. St_seq s (init_var (\fst (\fst (\fst var))) (\snd (\fst var)) (\snd (\fst (\fst var))))) St_skip vars.
    4545
    4646definition add_statement : ident → stmt →
Note: See TracChangeset for help on using the changeset viewer.