Changeset 961 for src/Clight/label.ma

Timestamp:

Jun 15, 2011, 4:15:52 PM (10 years ago)

Author:

campbell

Message:

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

File:

• src/Clight/label.ma (modified) (2 diffs)

src/Clight/label.ma

@@ -54 +54 @@
     do 〈e2,costgen〉 ← label_expr e2 costgen; 
     do 〈e2,costgen〉 ← add_cost_expr e2 costgen; 
-    do 〈ef,costgen〉 ← add_cost_expr (Expr (Econst_int zero) (Tint I32 Signed)) costgen;
+    do 〈ef,costgen〉 ← add_cost_expr (Expr (Econst_int I32 (zero ?)) (Tint I32 Signed)) costgen;
     OK ? 〈Econdition e1 e2 ef, costgen〉
 | Eorbool e1 e2 ⇒
     do 〈e1,costgen〉 ← label_expr e1 costgen; 
-    do 〈et,costgen〉 ← add_cost_expr (Expr (Econst_int one) (Tint I32 Signed)) costgen;
+    do 〈et,costgen〉 ← add_cost_expr (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed)) costgen;
     do 〈e2,costgen〉 ← label_expr e2 costgen; 
     do 〈e2,costgen〉 ← add_cost_expr e2 costgen; 
@@ -165 +165 @@
     do 〈s,costgen〉 ← add_cost_before s costgen;
     OK ? 〈LSdefault s, costgen〉
-| LScase i s ls' ⇒
+| LScase sz i s ls' ⇒
     do 〈s,costgen〉 ← label_statement s costgen;
     do 〈s,costgen〉 ← add_cost_before s costgen;
     do 〈ls',costgen〉 ← label_lstatements ls' costgen;
-    OK ? 〈LScase i s ls', costgen〉
+    OK ? 〈LScase sz i s ls', costgen〉
 ].