Changeset 964 for src/Clight/Csem.ma


Ignore:
Timestamp:
Jun 15, 2011, 4:15:55 PM (8 years ago)
Author:
campbell
Message:

Rest of cast fix.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Csem.ma

    r961 r964  
    417417  resulting in value [v2].  *)
    418418
    419 let rec cast_int_int (srcsz: intsize) (sz: intsize) (sg: signedness) (i: BitVector (bitsize_of_intsize srcsz)) : BitVector (bitsize_of_intsize sz) ≝
     419let rec cast_int_int (sz: intsize) (sg: signedness) (dstsz: intsize)  (i: BitVector (bitsize_of_intsize sz)) : BitVector (bitsize_of_intsize dstsz) ≝
    420420  match sg with [ Signed ⇒ sign_ext ?? i | Unsigned ⇒ zero_ext ?? i ].
    421421
     
    447447  | cast_ii:   ∀m,sz2,sz1,si1,si2,i.            (**r int to int  *)
    448448      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))
    450450  | cast_fi:   ∀m,f,sz1,sz2,si2.                (**r float to int *)
    451451      cast m (Vfloat f) (Tfloat sz1) (Tint sz2 si2)
Note: See TracChangeset for help on using the changeset viewer.