Changeset 961 for src/RTLabs


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

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/semantics.ma

    r888 r961  
    148148      ! v ← reg_retrieve (locals f) r;
    149149      match v with
    150       [ Vint i ⇒
     150      [ Vint _ i ⇒
    151151          ! l ← opt_to_io … (msg BadJumpTable) (nth_opt ? (nat_of_bitvector ? i) ls);
    152152          ret ? 〈E0, build_state f fs m l〉
     
    193193| Callstate _ _ _ _ _ ⇒ None ?
    194194| Returnstate v _ fs _ ⇒
    195     match fs with [ nil ⇒ match v with [ Some v' ⇒ match v' with [ Vint i ⇒ Some ? i | _ ⇒ None ? ] | None ⇒ None ? ] | cons _ _ ⇒ None ? ]
     195    match fs with [ nil ⇒
     196      match v with [ Some v' ⇒
     197        match v' with
     198        [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. Some ? i) (None ?)
     199        | _ ⇒ None ? ]
     200      | None ⇒ None ? ]
     201    | cons _ _ ⇒ None ? ]
    196202].
    197203
Note: See TracChangeset for help on using the changeset viewer.