Ignore:
Timestamp:
Apr 4, 2012, 6:48:23 PM (8 years ago)
Author:
campbell
Message:

Make binary operations in Cminor/RTLabs properly typed.
A few extra bits and pieces that help:
Separate out Clight operation classification to its own file.
Use dependently typed classification to refine the types.
Fix bug in cast simplification.
Remove memory_chunk in favour of the low-level typ, as this now contains
exactly the right amount of information (unlike in CompCert?).
Make Cminor/RTLabs comparisons produce an 8-bit result (and cast if
necessary).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/SimplifyCasts.ma

    r1224 r1872  
    114114            〈false, Expr (Ebinop op e1' e2') ty〉
    115115      else
    116         let 〈desired_type1, e1'〉 ≝ simplify_expr e1 ty in
    117         let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty in
     116        let 〈desired_type1, e1'〉 ≝ simplify_expr e1 (typeof e1) in
     117        let 〈desired_type2, e2'〉 ≝ simplify_expr e2 (typeof e2) in
    118118          〈type_eq ty ty', Expr (Ebinop op e1' e2') ty〉
    119119  | Ecast ty e1 ⇒
Note: See TracChangeset for help on using the changeset viewer.