Changeset 881 for src/Cminor/toRTLabs.ma


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/toRTLabs.ma

    r880 r881  
    8383    | _ ⇒ false
    8484    ]
    85 | Mem _ q e' ⇒
     85| Mem _ _ q e' ⇒
    8686    match q with
    8787    [ Mpointer _ ⇒ true
     
    133133    do f ← add_expr env ? e2 r2 ptrs f;
    134134    add_expr env ? e1 r1 ptrs f
    135 | Mem _ q e' ⇒
     135| Mem _ _ q e' ⇒
    136136    add_with_addressing_internal env ? e' (λm,rs. St_load q m rs dst) ptrs f (add_expr env ? e')
    137137| Cond _ _ _ e' e1 e2 ⇒
     
    248248    do dst ← opt_to_res … [MSG UnknownVariable; CTX ? x] (lookup ?? env x);
    249249    add_expr env ? e dst ptrs f
    250 | St_store _ q e1 e2 ⇒
     250| St_store _ _ q e1 e2 ⇒
    251251    do 〈val_reg, f〉 ← choose_reg env ? e2 ptrs f;
    252252    do f ← add_with_addressing env ? e1 (λm,rs. St_store q m rs val_reg) ptrs f;
Note: See TracChangeset for help on using the changeset viewer.