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/CexecSound.ma

    r1516 r1545  
    44 exec_bool_of_val v ty = OK ? r → bool_of_val v ty (of_bool r).
    55#v #ty #r
    6 cases v; [ | #sz #i | #f | #r1 | #r' #b #pc #of ]
     6cases v; [ | #sz #i | #f | #r1 | #ptr ]
    77cases ty; [ 2,11,20,29,38: #sz' #sg | 3,12,21,30,39: #sz' | 4,13,22,31,40: #rg #ty | 5,14,23,32,41: #r #ty #n | 6,15,24,33,42: #args #rty | 7,8,16,17,25,26,34,35,43,44: #id #fs | 9,18,27,36,45: #r #id ]
    88whd in ⊢ (??%? → ?);
     
    100100    cases ty' in H2; normalize; try #a try #b try #c try #d destruct;
    101101    @cast_pp_z //;
    102 | #r #b #pc #of whd in ⊢ (??%? → ?); #e
     102| #ptr whd in ⊢ (??%? → ?); #e
    103103    elim (bind_inversion ????? e) #s * #es #e'
    104104    elim (bind_inversion ????? e') #u * #eu #e'' -e';
     
    112112            whd in e:(??%?); destruct; //;
    113113        | #Hty'
    114             cut (s = r). elim (eq_region_dec r s) in eu; //; normalize; #_ #e destruct.
     114            cut (s = ptype ptr). elim (eq_region_dec (ptype ptr) s) in eu; //; normalize; #_ #e destruct.
    115115            #e >e in Hty; #Hty
    116             cases (pointer_compat_dec b s') in e''';
     116            cases (pointer_compat_dec (pblock ptr) s') in e''';
    117117            #Hcompat #e''' whd in e''':(??%?); destruct (e'''); /2/
    118118        ]
     
    207207    ]
    208208| #ty #e #He whd in ⊢ (???%);
    209     @bind2_OK #v cases v // #r #l #pc #ofs #tr #Hv whd
     209    @bind2_OK #v cases v // * #r #l #pc #ofs #tr #Hv whd
    210210    >Hv in He; #He
    211211    @eval_Ederef [ 3: @He | *: skip ]
    212212| #ty #e'' #ty'' #He'' @bind2_OK * #loc #ofs #tr #H
    213   cases ty // * #pty
     213  cases ty try (try #a try #b try #c @I) * #pty
    214214  cases loc in H ⊢ %; * #loc' #H
    215215  whd try @I
     
    276276
    277277lemma addrof_eval_lvalue: ∀ge,en,m,e,r,loc,pc,off,tr,ty.
    278 eval_expr ge en m (Expr (Eaddrof e) ty) (Vptr r loc pc off) tr →
     278eval_expr ge en m (Expr (Eaddrof e) ty) (Vptr (mk_pointer r loc pc off)) tr →
    279279eval_lvalue ge en m e loc off tr.
    280280#ge #en #m #e #r #loc #pc #off #tr #ty #H inversion H;
     
    303303lemma addrof_exec_lvalue: ∀ge,en,m,e,r,loc,off,tr.
    304304exec_lvalue ge en m e = OK ? 〈〈mk_block r loc,off〉,tr〉 →
    305 exec_expr ge en m (Expr (Eaddrof e) (Tpointer r Tvoid)) = OK ? 〈Vptr r (mk_block r loc) (same_compat ??) off, tr〉.
     305exec_expr ge en m (Expr (Eaddrof e) (Tpointer r Tvoid)) = OK ? 〈Vptr (mk_pointer r (mk_block r loc) (same_compat ??) off), tr〉.
    306306#ge #en #m #e #r #loc #off #tr #H whd in ⊢ (??%?);
    307307>H whd in ⊢ (??%?); cases r @refl
Note: See TracChangeset for help on using the changeset viewer.