Changeset 1545 for src/Clight/Cexec.ma


Ignore:
Timestamp:
Nov 23, 2011, 6:03:07 PM (8 years ago)
Author:
campbell
Message:

Use pointer record in front-end.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r1516 r1545  
    2323    | _ ⇒ Error ? (msg TypeMismatch)
    2424    ]
    25   | Vptr _ _ _ _ ⇒ match ty with
     25  | Vptr _ ⇒ match ty with
    2626    [ Tpointer _ _ ⇒ OK ? true
    2727    | _ ⇒ Error ? (msg TypeMismatch)
     
    3737#v #ty #r #H elim H; #v #t #H' elim H';
    3838  [ * #sg #i #ne %{ true} % // whd in ⊢ (??%?); >(eq_bv_false … ne) //
    39   | #r #b #pc #i #i0 #s %{ true} % //
     39  | #ptr #r #ty %{ true} % //
    4040  | #f #s #ne %{ true} % //; whd in ⊢ (??%?); >(Feq_zero_false … ne) //;
    4141  | * #sg %{ false} % //
     
    124124  | _ ⇒ Error ? (msg TypeMismatch)
    125125  ]
    126 | Vptr r b _ ofs
     126| Vptr ptr
    127127    do s ← match ty with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? (msg TypeMismatch) ];
    128     do u ← match eq_region_dec r s with [ inl _ ⇒ OK ? it | inr _ ⇒ Error ? (msg BadCast) ];
     128    do u ← match eq_region_dec (ptype ptr) s with [ inl _ ⇒ OK ? it | inr _ ⇒ Error ? (msg BadCast) ];
    129129    do s' ← match ty' with
    130130         [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code
    131131         | _ ⇒ Error ? (msg BadCast)];
    132     match pointer_compat_dec b s' with
    133     [ inl p' ⇒ OK ? (Vptr s' b p' ofs)
     132    match pointer_compat_dec (pblock ptr) s' with
     133    [ inl p' ⇒ OK ? (Vptr (mk_pointer s' (pblock ptr) p' (poff ptr)))
    134134    | inr _ ⇒ Error ? (msg BadCast)
    135135    ]
     
    187187        match lo with [ pair loc ofs ⇒
    188188          match pointer_compat_dec loc r with
    189           [ inl pc ⇒ OK ? 〈Vptr r loc pc ofs, tr〉
     189          [ inl pc ⇒ OK ? 〈Vptr (mk_pointer r loc pc ofs), tr〉
    190190          | inr _ ⇒ Error ? (msg TypeMismatch)
    191191          ]
     
    249249      do 〈v,tr〉 ← exec_expr ge en m a;
    250250      match v with
    251       [ Vptr _ l _ ofs ⇒ OK ? 〈〈l,ofs〉,tr〉
     251      [ Vptr ptr ⇒ OK ? 〈〈pblock ptr, poff ptr〉,tr〉
    252252      | _ ⇒ Error ? (msg TypeMismatch)
    253253      ]
     
    535535    | #f %2 ; % *;   #r #H inversion H; #i #m #e destruct;
    536536    | #r %2 ; % *;   #r #H inversion H; #i #m #e destruct;
    537     | #r #b #pc #of %2 ; % *;   #r #H inversion H; #i #m #e destruct;
     537    | #ptr %2 ; % *;   #r #H inversion H; #i #m #e destruct;
    538538    ]
    539539  | #a #b %2 ; % *; #r #H inversion H; #i #m #e destruct;
Note: See TracChangeset for help on using the changeset viewer.