Changeset 964 for src/Clight/Csem.ma

Timestamp:

Jun 15, 2011, 4:15:55 PM (9 years ago)

Author:

campbell

Message:

Rest of cast fix.

File:

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

src/Clight/Csem.ma

@@ -417 +417 @@
   resulting in value [v2].  *)
 
-let rec cast_int_int (srcsz: intsize) (sz: intsize) (sg: signedness) (i: BitVector (bitsize_of_intsize srcsz)) : BitVector (bitsize_of_intsize sz) ≝
+let rec cast_int_int (sz: intsize) (sg: signedness) (dstsz: intsize)  (i: BitVector (bitsize_of_intsize sz)) : BitVector (bitsize_of_intsize dstsz) ≝
   match sg with [ Signed ⇒ sign_ext ?? i | Unsigned ⇒ zero_ext ?? i ].
 
@@ -447 +447 @@
   | cast_ii:   ∀m,sz2,sz1,si1,si2,i.            (**r int to int  *)
       cast m (Vint sz1 i) (Tint sz1 si1) (Tint sz2 si2)
-           (Vint sz2 (cast_int_int ? sz2 si2 i))
+           (Vint sz2 (cast_int_int sz1 si1 sz2 i))
   | cast_fi:   ∀m,f,sz1,sz2,si2.                (**r float to int *)
       cast m (Vfloat f) (Tfloat sz1) (Tint sz2 si2)