Changeset 964 for src/Clight/Csem.ma
- Timestamp:
- Jun 15, 2011, 4:15:55 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/Csem.ma
r961 r964 417 417 resulting in value [v2]. *) 418 418 419 let rec cast_int_int (s rcsz: intsize) (sz: intsize) (sg: signedness) (i: BitVector (bitsize_of_intsize srcsz)) : BitVector (bitsize_of_intsizesz) ≝419 let rec cast_int_int (sz: intsize) (sg: signedness) (dstsz: intsize) (i: BitVector (bitsize_of_intsize sz)) : BitVector (bitsize_of_intsize dstsz) ≝ 420 420 match sg with [ Signed ⇒ sign_ext ?? i | Unsigned ⇒ zero_ext ?? i ]. 421 421 … … 447 447 | cast_ii: ∀m,sz2,sz1,si1,si2,i. (**r int to int *) 448 448 cast m (Vint sz1 i) (Tint sz1 si1) (Tint sz2 si2) 449 (Vint sz2 (cast_int_int ? sz2 si2 i))449 (Vint sz2 (cast_int_int sz1 si1 sz2 i)) 450 450 | cast_fi: ∀m,f,sz1,sz2,si2. (**r float to int *) 451 451 cast m (Vfloat f) (Tfloat sz1) (Tint sz2 si2)
Note: See TracChangeset
for help on using the changeset viewer.