Ignore:
Timestamp:
Nov 15, 2012, 6:12:57 PM (7 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/CexecInd.ma

    r2019 r2468  
    1515  (Q:expr_descr → type → Prop)
    1616  (ci:∀sz,ty,i.P (Expr (Econst_int sz i) ty))
    17   (cf:∀ty,f.P (Expr (Econst_float f) ty))
     17(*  (cf:∀ty,f.P (Expr (Econst_float f) ty))*)
    1818  (lv:∀e,ty. Q e ty → Plvalue P e ty)
    1919  (vr:∀v,ty.Q (Evar v) ty)
     
    3535  match e' with
    3636  [ Econst_int sz i ⇒ ci sz ty i
    37   | Econst_float f ⇒ cf ty f
     37(*  | Econst_float f ⇒ cf ty f*)
    3838  | Evar v ⇒ lv (Evar v) ty (vr v ty)
    39   | Ederef e'' ⇒ lv (Ederef e'') ty (dr e'' ty (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e''))
    40   | Eaddrof e'' ⇒ match e'' with [ Expr e0 ty0 ⇒ ao ty e0 ty0 (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e0 ty0) ]
    41   | Eunop op e'' ⇒ uo ty op e'' (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e'')
    42   | Ebinop op e1 e2 ⇒ bo ty op e1 e2 (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e1) (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e2)
    43   | Ecast ty' e'' ⇒ ca ty ty' e'' (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e'')
    44   | Econdition e1 e2 e3 ⇒ cd ty e1 e2 e3 (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e1) (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e2) (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e3)
    45   | Eandbool e1 e2 ⇒ ab ty e1 e2 (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e1) (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e2)
    46   | Eorbool e1 e2 ⇒ ob ty e1 e2 (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e1) (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e2)
     39  | Ederef e'' ⇒ lv (Ederef e'') ty (dr e'' ty (expr_lvalue_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx e''))
     40  | Eaddrof e'' ⇒ match e'' with [ Expr e0 ty0 ⇒ ao ty e0 ty0 (lvalue_expr_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx e0 ty0) ]
     41  | Eunop op e'' ⇒ uo ty op e'' (expr_lvalue_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx e'')
     42  | Ebinop op e1 e2 ⇒ bo ty op e1 e2 (expr_lvalue_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx e1) (expr_lvalue_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx e2)
     43  | Ecast ty' e'' ⇒ ca ty ty' e'' (expr_lvalue_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx e'')
     44  | Econdition e1 e2 e3 ⇒ cd ty e1 e2 e3 (expr_lvalue_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx e1) (expr_lvalue_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx e2) (expr_lvalue_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx e3)
     45  | Eandbool e1 e2 ⇒ ab ty e1 e2 (expr_lvalue_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx e1) (expr_lvalue_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx e2)
     46  | Eorbool e1 e2 ⇒ ob ty e1 e2 (expr_lvalue_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx e1) (expr_lvalue_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx e2)
    4747  | Esizeof ty' ⇒ sz ty ty'
    48   | Efield e'' i ⇒ match e'' with [ Expr ef tyf ⇒ lv (Efield (Expr ef tyf) i) ty (fl ty ef tyf i (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx ef tyf)) ]
    49   | Ecost l e'' ⇒ co ty l e'' (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e'')
     48  | Efield e'' i ⇒ match e'' with [ Expr ef tyf ⇒ lv (Efield (Expr ef tyf) i) ty (fl ty ef tyf i (lvalue_expr_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx ef tyf)) ]
     49  | Ecost l e'' ⇒ co ty l e'' (expr_lvalue_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx e'')
    5050  ]
    5151]
     
    5454  (Q:expr_descr → type → Prop)
    5555  (ci:∀sz,ty,i.P (Expr (Econst_int sz i) ty))
    56   (cf:∀ty,f.P (Expr (Econst_float f) ty))
     56(*  (cf:∀ty,f.P (Expr (Econst_float f) ty))*)
    5757  (lv:∀e,ty. Q e ty → Plvalue P e ty)
    5858  (vr:∀v,ty.Q (Evar v) ty)
     
    7272  match e return λe0. Q e0 ty with
    7373  [ Evar v ⇒ vr v ty
    74   | Ederef e'' ⇒ dr e'' ty (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e'')
    75   | Efield e' i ⇒ match e' return λe1.Q (Efield e1 i) ty with [ Expr e'' ty'' ⇒ fl ty e'' ty'' i (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e'' ty'') ]
     74  | Ederef e'' ⇒ dr e'' ty (expr_lvalue_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx e'')
     75  | Efield e' i ⇒ match e' return λe1.Q (Efield e1 i) ty with [ Expr e'' ty'' ⇒ fl ty e'' ty'' i (lvalue_expr_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx e'' ty'') ]
    7676  | _ ⇒ xx ? ty ?
    7777  ]. whd; @I qed.
    7878
    7979definition expr_lvalue_ind_combined ≝
    80 λP,Q,ci,cf,lv,vr,dr,ao,uo,bo,ca,cd,ab,ob,sz,fl,co,xx.
     80λP,Q,ci,lv,vr,dr,ao,uo,bo,ca,cd,ab,ob,sz,fl,co,xx.
    8181conj ??
    82  (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx)
    83  (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx).
     82 (expr_lvalue_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx)
     83 (lvalue_expr_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx).
Note: See TracChangeset for help on using the changeset viewer.