Ignore:
Timestamp:
Nov 15, 2012, 6:12:57 PM (8 years ago)
Author:
garnier
Message:

Floats are gone from the front-end. Some trace amount might remain in RTL/RTLabs, but this should be easily fixable.
Also, work-in-progress in Clight/memoryInjections.ma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecComplete.ma

    r2428 r2468  
    9090elim H;
    9191[ #m #sz1 #sz2 #sg1 #sg2 #i whd in ⊢ (??%?); >intsize_eq_elim_true @refl
    92 | #m #f #sz #szi #sg @refl
     92(*| #m #f #sz #szi #sg @refl
    9393| #m #sz #sz' #sg #i whd in ⊢ (??%?); >intsize_eq_elim_true @refl
    94 | #m #f #sz #sz' @refl
     94| #m #f #sz #sz' @refl*)
    9595| #m #ty0 #ty0' #ptr #H1 #H2 cases H1 cases H2 //
    9696| #m #sz #sg #ty' #H' cases H' [ #ty'' | #ty'' #n | #tys #ty'' ] whd in ⊢ (??%?);
     
    130130    >(eq_bv_false … ne) //
    131131  | *  #b #i #i0  %{ true} % //
    132   | #f #s #ne %{ true} % //; whd; >(Feq_zero_false … ne) //;
     132(*  | #f #s #ne %{ true} % //; whd; >(Feq_zero_false … ne) //;*)
    133133  | #sz #sg %{ false} % // whd in ⊢ (??%?); >intsize_eq_elim_true >eq_bv_true //
    134134  |  #t %{ false} % //;
    135   | #s %{ false} % //; whd; >(Feq_zero_true …) //;
     135(*  | #s %{ false} % //; whd; >(Feq_zero_true …) //;*)
    136136  ]
    137137qed.
     
    140140#v #ty #H elim H;
    141141  [ #i #is #s #ne whd in ⊢ (??%?); >intsize_eq_elim_true >(eq_bv_false … ne) //;
    142   | #s //
    143   | #f #s #ne whd; >(Feq_zero_false … ne) //;
     142  | #s // 
     143(*  | #f #s #ne whd; >(Feq_zero_false … ne) //;*)
    144144  ]
    145145qed.
     
    149149  [ #sz #sg whd in ⊢ (??%?); >intsize_eq_elim_true >eq_bv_true //;
    150150  | #t //;
    151   | #s whd; >(Feq_zero_true …) //;
     151(*  | #s whd; >(Feq_zero_true …) //;*)
    152152  ]
    153153qed.
     
    161161  (λe,l,off,tr,H. yields ? (exec_lvalue ge env m e) (〈〈l,off〉,tr〉)));
    162162[ #sz #sg #i whd in ⊢ (??%?); >eq_intsize_true @refl
    163 | #f #ty @refl
     163(*| #f #ty @refl*)
    164164| #e #ty #l #off #v #tr #H1 #H2 @(lvalue_expr … H1)
    165165    [ #id | #e' | #e' #id ] #H3
     
    268268  (vo:P Tvoid)
    269269  (it:∀i,s. P (Tint i s))
    270   (fl:∀f. P (Tfloat f))
     270(*  (fl:∀f. P (Tfloat f))*)
    271271  (pt:∀t. P t → P (Tpointer t))
    272272  (ar:∀t,n. P t → P (Tarray t n))
     
    281281  [ Tvoid ⇒ vo
    282282  | Tint i s ⇒ it i s
    283   | Tfloat s ⇒ fl s
    284   | Tpointer t' ⇒ pt t' (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t')
    285   | Tarray t' n ⇒ ar t' n (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t')
    286   | Tfunction tl t' ⇒ fn tl t' (typelist_ind2l P Q vo it fl pt ar fn st un cp nl cs tl) (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t')
     283(*  | Tfloat s ⇒ fl s*)
     284  | Tpointer t' ⇒ pt t' (type_ind2l P Q vo it pt ar fn st un cp nl cs t')
     285  | Tarray t' n ⇒ ar t' n (type_ind2l P Q vo it pt ar fn st un cp nl cs t')
     286  | Tfunction tl t' ⇒ fn tl t' (typelist_ind2l P Q vo it pt ar fn st un cp nl cs tl) (type_ind2l P Q vo it pt ar fn st un cp nl cs t')
    287287  | Tstruct i fs ⇒ st i fs
    288288  | Tunion i fs ⇒ un i fs
     
    293293  (vo:P Tvoid)
    294294  (it:∀i,s. P (Tint i s))
    295   (fl:∀f. P (Tfloat f))
     295(*  (fl:∀f. P (Tfloat f))*)
    296296  (pt:∀t. P t → P (Tpointer t))
    297297  (ar:∀t,n. P t → P (Tarray t n))
     
    305305  match ts return λts'.Q ts' with
    306306  [ Tnil ⇒ nl
    307   | Tcons t tl ⇒ cs t tl (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t)
    308                      (typelist_ind2l P Q vo it fl pt ar fn st un cp nl cs tl)
     307  | Tcons t tl ⇒ cs t tl (type_ind2l P Q vo it pt ar fn st un cp nl cs t)
     308                     (typelist_ind2l P Q vo it pt ar fn st un cp nl cs tl)
    309309  ].
    310310
     
    340340lemma eventval_match_complete': ∀ev,ty,v.
    341341  eventval_match ev ty v → yields ? (check_eventval' v ty) ev.
    342 #ev #ty #v #H elim H; // #sz #sg #i whd in ⊢ (??%?); >eq_intsize_true @refl qed.
     342#ev #ty #v #H elim H #sz #sg #i whd in ⊢ (??%?); >eq_intsize_true @refl qed.
    343343
    344344lemma eventval_list_match_complete: ∀vs,tys,evs.
     
    446446    #H1 #H2
    447447    >(yields_eq ??? (eventval_list_match_complete … H1)) whd in ⊢ (??%?);
    448     whd; inversion H2; [ #sz #sg #x | #x #sz ] #e5 #e6 #e7 #e8 %{ x} whd in ⊢ (??%?);
     448    whd; inversion H2; #sz #sg #x (*| #x #sz ]*) #e5 #e6 #e7 #e8 %{ x} whd in ⊢ (??%?);
    449449    @refl
    450450| #v #f #env #k #m @refl
Note: See TracChangeset for help on using the changeset viewer.