Ignore:
Timestamp:
Jan 9, 2013, 1:23:29 PM (7 years ago)
Author:
garnier
Message:

Progress on toCminorCorrectness.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r2568 r2572  
    405405[ aop_case_ii sz sg ⇒
    406406    match sg return λsg. CMexpr (ASTint sz sg) → CMexpr (ASTint sz sg) → res (CMexpr (typ_of_type ty')) with
    407     [ Unsigned ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omodu …) e1 e2)
    408     | Signed ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omod …) e1 e2)
     407    [ Unsigned ⇒ λe1,e2.  typ_should_eq ??? (Op2 ??? (Oshru …) e1 e2)
     408    | Signed ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Oshr …) e1 e2)
    409409    ]
    410410(* no float case *)
     
    417417[ Tint sz sg ⇒ OK ? (Op1 ?? (Ocastint I8 Unsigned sz sg) e)
    418418| _ ⇒ Error ? (msg TypeMismatch)
    419 ].
    420 
     419]. 
     420 
    421421definition translate_cmp ≝
    422422λc,ty1,ty2,ty'.
     
    457457| Oxor ⇒ translate_misc_aop ty1 ty2 ty Oxor e1 e2
    458458| Oshl ⇒ translate_misc_aop ty1 ty2 ty Oshl e1 e2
    459 | Oshr ⇒ translate_shr ty1 ty2 ty e1 e2
     459(*| Oshr ⇒ translate_misc_aop ty1 ty2 ty Oshr e1 e2 *)
     460| Oshr ⇒ translate_shr ty1 ty2 ty e1 e2  (* split on signed/unsigned *)
    460461| Oeq ⇒ translate_cmp Ceq ty1 ty2 ty e1 e2
    461462| One ⇒ translate_cmp Cne ty1 ty2 ty e1 e2
Note: See TracChangeset for help on using the changeset viewer.