Ignore:
Timestamp:
Jun 15, 2011, 4:15:52 PM (8 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/Clight/CexecComplete.ma

    r891 r961  
    100100#m #v #ty #ty' #v' #H
    101101elim H;
    102 [ #m #i #sz1 #sz2 #sg1 #sg2 @refl
     102[ #m #sz1 #sz2 #sg1 #sg2 #i whd in ⊢ (??%?) >intsize_eq_elim_true @refl
    103103| #m #f #sz #szi #sg @refl
    104 | #m #i #sz #sz' #sg @refl
     104| #m #sz #sz' #sg #i whd in ⊢ (??%?) >intsize_eq_elim_true @refl
    105105| #m #f #sz #sz' @refl
    106106| #m #r #r' #ty #ty' #b #pc #ofs #H1 #H2 #pc'
     
    111111    #pc' whd in ⊢ (??%?)
    112112    @(dec_true ? (pointer_compat_dec b sp2) pc') //
    113 | #m #sz #si #ty'' #r #H cases H; //;
     113| #m #sz #si #ty'' #r #H cases H; [ #s #t | #s #t #n | #tys #ty0 ] whd in ⊢ (??%?)
     114  >intsize_eq_elim_true whd in ⊢ (??%?) cases sz //;
    114115| #m #t #t' #r #r' #H #H' cases H; try #a try #b try #c cases H'; try #d try #e try #f
    115116    whd in ⊢ (??%?); try @refl @(dec_true ? (eq_region_dec a a) (refl ??)) #H0 @refl
     
    131132lemma bool_of_val_3_complete : ∀v,ty,r. bool_of_val v ty r → ∃b. r = of_bool b ∧ yields ? (exec_bool_of_val v ty) b.
    132133#v #ty #r #H elim H; #v #t #H' elim H';
    133   [ #i #is #s #ne %{ true} % //; whd; >(eq_false … ne) //;
     134  [ #sz #sg #i #ne %{ true} % //; whd in ⊢ (??%?) >intsize_eq_elim_true
     135    >(eq_bv_false … ne) //
    134136  | #r #b #pc #i #i0 #s %{ true} % //
    135137  | #f #s #ne %{ true} % //; whd; >(Feq_zero_false … ne) //;
    136   | #i #s %{ false} % //;
     138  | #sz #sg %{ false} % // whd in ⊢ (??%?) >intsize_eq_elim_true >eq_bv_true //
    137139  | #r #r' #t %{ false} % //;
    138140  | #s %{ false} % //; whd; >(Feq_zero_true …) //;
     
    142144lemma bool_of_true: ∀v,ty. is_true v ty → yields ? (exec_bool_of_val v ty) true.
    143145#v #ty #H elim H;
    144   [ #i #is #s #ne whd; >(eq_false … ne) //;
     146  [ #i #is #s #ne whd in ⊢ (??%?) >intsize_eq_elim_true >(eq_bv_false … ne) //;
    145147  | #p #b #i #i0 #s //
    146148  | #f #s #ne whd; >(Feq_zero_false … ne) //;
     
    150152lemma bool_of_false: ∀v,ty. is_false v ty → yields ? (exec_bool_of_val v ty) false.
    151153#v #ty #H elim H;
    152   [ #i #s //;
     154  [ #sz #sg whd in ⊢ (??%?) >intsize_eq_elim_true >eq_bv_true //;
    153155  | #r #r' #t //;
    154156  | #s whd; >(Feq_zero_true …) //;
     
    163165  (λe,v,tr,H. yields ? (exec_expr ge env m e) (〈v,tr〉))
    164166  (λe,l,off,tr,H. yields ? (exec_lvalue ge env m e) (〈〈l,off〉,tr〉)));
    165 [ #i #ty @refl
     167[ #sz #sg #i whd in ⊢ (??%?) >eq_intsize_true @refl
    166168| #f #ty @refl
    167169| #e #ty #l #off #v #tr #H1 #H2 @(lvalue_expr … H1)
     
    179181    @(dec_true ? (pointer_compat_dec l r) pc) #pc' whd
    180182    @refl
    181 | #ty' #ty @refl
     183| #ty' #sz #sg @refl
    182184| #op #e #ty #v1 #v #tr #H1 #H2 #H3 whd in ⊢ (??%?);
    183185    >(yields_eq ??? H3)
     
    342344lemma eventval_match_complete': ∀ev,ty,v.
    343345  eventval_match ev ty v → yields ? (check_eventval' v ty) ev.
    344 #ev #ty #v #H elim H; //; qed.
     346#ev #ty #v #H elim H; // #sz #sg #i whd in ⊢ (??%?) >eq_intsize_true @refl qed.
    345347
    346348lemma eventval_list_match_complete: ∀vs,tys,evs.
     
    431433    | #r #f' #env' #k' #H1 #H2 whd in ⊢ (??%?); >H2 @refl
    432434    ]
    433 | #f #e #s #k #env #m #i #tr #H1 whd in ⊢ (??%?);
     435| #f #e #s #k #env #m #sz #i #tr #H1 whd in ⊢ (??%?);
    434436    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
    435437    @refl
     
    446448    #H1 #H2
    447449    >(yields_eq ??? (eventval_list_match_complete … H1)) whd in ⊢ (??%?);
    448     whd; inversion H2; #x #sz [ #sg ] #e5 #e6 #e7 %{ x} whd in ⊢ (??%?);
     450    whd; inversion H2; [ #sz #sg #x | #x #sz ] #e5 #e6 #e7 %{ x} whd in ⊢ (??%?);
    449451    @refl
    450452| #v #f #env #k #m @refl
Note: See TracChangeset for help on using the changeset viewer.