Changeset 127 for C-semantics/CexecIO.ma


Ignore:
Timestamp:
Sep 24, 2010, 10:31:34 AM (10 years ago)
Author:
campbell
Message:

Allow the storage of pointers in suitably large integers.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIO.ma

    r125 r127  
    221221| Vptr p b ofs ⇒
    222222  Some ? (
    223     p ← match ty with [ Tpointer _ _ ⇒ OK ? something | Tarray _ _ _ ⇒ OK ? something | Tfunction _ _ ⇒ OK ? something | _ ⇒ Error ? ];:
    224     s' ← match ty' with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? ];:
     223    u ← match ty with [ Tpointer _ _ ⇒ OK ? something | Tarray _ _ _ ⇒ OK ? something | Tfunction _ _ ⇒ OK ? something | _ ⇒ Error ? ];:
     224    s' ← match ty' with
     225         [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code
     226         | Tint sz sg ⇒ match sg with [ Signed ⇒ Error ? | Unsigned ⇒
     227             if Zleb (sizeof_pointer p) (sizeof ty') then OK ? p else Error ? ]
     228         | _ ⇒ Error ? ];:
    225229    if is_pointer_compat (block_space m b) s'
    226230    then OK ? (Vptr s' b ofs)
     
    238242      ##[ ncases ty' in es' ⊢ %; ##[ #e; ##| ##3,9: #a e; ##| ##2,4,6,7,8: #a b e; ##| #a b c e; ##]
    239243          nwhd in e:(??%?); ndestruct; //;
     244          ncases b in e ⊢ %; #e; nwhd in e:(??%?); ndestruct;
     245          napply type_spc_int; napply Zleb_true_to_Zle;
     246          ncut (c0 = s'); ##[
     247            nelim (Zleb (sizeof_pointer c0) (sizeof (Tint a Unsigned))) in e;
     248            nnormalize; #e; ndestruct; //;
     249          ##| #e2; nrewrite > e2 in e;
     250              nelim (Zleb (sizeof_pointer s') (sizeof (Tint a Unsigned)));
     251              //; nnormalize; #e; ndestruct;
     252          ##]
    240253      ##| #Hty' Hty;
    241254          nwhd in match (is_pointer_compat ??) in ⊢ %;
Note: See TracChangeset for help on using the changeset viewer.