Changeset 2468 for src/Clight/Csem.ma


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

    r2433 r2468  
    4040      is_false (Vint sz (zero ?)) (Tint sz sg)
    4141  | is_false_pointer: ∀t.
    42       is_false Vnull (Tpointer t)
    43  | is_false_float: ∀sz.
    44       is_false (Vfloat Fzero) (Tfloat sz).
     42      is_false Vnull (Tpointer t).
    4543
    4644inductive is_true: val → type → Prop ≝
     
    4947      is_true (Vint sz n) (Tint sz sg)
    5048  | is_true_pointer_pointer: ∀ptr,t.
    51       is_true (Vptr ptr) (Tpointer t)
    52   | is_true_float: ∀f,sz.
    53       f ≠ Fzero →
    54       is_true (Vfloat f) (Tfloat sz).
     49      is_true (Vptr ptr) (Tpointer t).
    5550
    5651inductive bool_of_val : val → type → val → Prop ≝
     
    7772                     then Some ? (Vint ? (two_complement_negation ? n))
    7873                     else None ?
    79       | _ ⇒ None ?
    80       ]
    81   | Tfloat _ ⇒
    82       match v with
    83       [ Vfloat f ⇒ Some ? (Vfloat (Fneg f))
    8474      | _ ⇒ None ?
    8575      ]
     
    10898      | _ ⇒ None ?
    10999      ]
    110   | Tfloat _ ⇒
    111       match v with
    112       [ Vfloat f ⇒ Some ? (of_bool (Fcmp Ceq f Fzero))
    113       | _ ⇒ None ?
    114       ]
    115100  | _ ⇒ None ?
    116101  ].
     
    123108        [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
    124109                        (λn1. Some ? (Vint ? (addition_n ? n1 n2))) (None ?)
    125         | _ ⇒ None ? ]
    126       | _ ⇒ None ? ]
    127   | add_case_ff _ ⇒                       (**r float addition *)
    128       match v1 with
    129       [ Vfloat n1 ⇒ match v2 with
    130         [ Vfloat n2 ⇒ Some ? (Vfloat (Fadd n1 n2))
    131110        | _ ⇒ None ? ]
    132111      | _ ⇒ None ? ]
     
    157136        [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
    158137                        (λn1.Some ? (Vint sz2 (subtraction ? n1 n2))) (None ?)
    159         | _ ⇒ None ? ]
    160       | _ ⇒ None ? ]
    161   | sub_case_ff _ ⇒                (**r float subtraction *)
    162       match v1 with
    163       [ Vfloat f1 ⇒ match v2 with
    164         [ Vfloat f2 ⇒ Some ? (Vfloat (Fsub f1 f2))
    165138        | _ ⇒ None ? ]
    166139      | _ ⇒ None ? ]
     
    200173        | _ ⇒ None ? ]
    201174      | _ ⇒ None ? ]
    202   | aop_case_ff _ ⇒
    203       match v1 with
    204       [ Vfloat f1 ⇒ match v2 with
    205         [ Vfloat f2 ⇒ Some ? (Vfloat (Fmul f1 f2))
    206         | _ ⇒ None ? ]
    207       | _ ⇒ None ? ]
    208175  | aop_default _ _ ⇒
    209176      None ?
     
    223190           ]
    224191         | _ ⇒ None ? ]
    225       | _ ⇒ None ? ]
    226   | aop_case_ff _ ⇒
    227       match v1 with
    228       [ Vfloat f1 ⇒ match v2 with
    229         [ Vfloat f2 ⇒ Some ? (Vfloat(Fdiv f1 f2))
    230         | _ ⇒ None ? ]
    231192      | _ ⇒ None ? ]
    232193  | aop_default _ _ ⇒
     
    363324        ]
    364325      | _ ⇒ None ? ]
    365   | cmp_case_ff _ ⇒
    366       match v1 with
    367       [ Vfloat f1 ⇒
    368         match v2 with
    369         [ Vfloat f2 ⇒ Some ? (of_bool (Fcmp c f1 f2))
    370         | _ ⇒ None ? ]
    371       | _ ⇒ None ? ]
    372326  | cmp_default _ _ ⇒ None ?
    373327  ].
     
    412366  match sg with [ Signed ⇒ sign_ext ?? i | Unsigned ⇒ zero_ext ?? i ].
    413367
    414 let rec cast_int_float (si : signedness) (n:nat) (i: BitVector n) : float ≝
    415   match si with
    416   [ Signed ⇒ floatofint ? i
    417   | Unsigned ⇒ floatofintu ? i
    418   ].
    419 
    420 let rec cast_float_int (sz : intsize) (si : signedness) (f: float) : BitVector (bitsize_of_intsize sz) ≝
    421   match si with
    422   [ Signed ⇒ intoffloat ? f
    423   | Unsigned ⇒ intuoffloat ? f
    424   ].
    425 
    426 let rec cast_float_float (sz: floatsize) (f: float) : float ≝
    427   match sz with
    428   [ F32 ⇒ singleoffloat f
    429   | F64 ⇒ f
    430   ].
    431 
    432368(* Only for full 8051 memory spaces
    433369inductive type_region : type → region → Prop ≝
     
    447383      cast m (Vint sz1 i) (Tint sz1 si1) (Tint sz2 si2)
    448384           (Vint sz2 (cast_int_int sz1 si1 sz2 i))
    449   | cast_fi:   ∀m,f,sz1,sz2,si2.                (**r float to int *)
    450       cast m (Vfloat f) (Tfloat sz1) (Tint sz2 si2)
    451            (Vint sz2 (cast_float_int sz2 si2 f))
    452   | cast_if:   ∀m,sz1,sz2,si1,i.                (**r int to float  *)
    453       cast m (Vint sz1 i) (Tint sz1 si1) (Tfloat sz2)
    454           (Vfloat (cast_float_float sz2 (cast_int_float si1 ? i)))
    455   | cast_ff:   ∀m,f,sz1,sz2.                    (**r float to float *)
    456       cast m (Vfloat f) (Tfloat sz1) (Tfloat sz2)
    457            (Vfloat (cast_float_float sz2 f))
    458385  | cast_pp: ∀m,ty,ty',ptr.
    459386(*      type_region ty (ptype ptr) →
     
    607534  | eval_Econst_int:   ∀sz,sg,i.
    608535      eval_expr ge e m (Expr (Econst_int sz i) (Tint sz sg)) (Vint sz i) E0
     536(*
    609537  | eval_Econst_float:   ∀f,ty.
    610       eval_expr ge e m (Expr (Econst_float f) ty) (Vfloat f) E0
     538      eval_expr ge e m (Expr (Econst_float f) ty) (Vfloat f) E0 *)
    611539  | eval_Elvalue: ∀a,ty,loc,ofs,v,tr.
    612540      eval_lvalue ge e m (Expr a ty) loc ofs tr →
     
    698626  (P:∀a,v,tr. eval_expr ge e m a v tr → Prop)
    699627  (eci:∀sz,sg,i. P ??? (eval_Econst_int ge e m sz sg i))
    700   (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty))
     628(*  (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty)) *)
    701629  (elv:∀a,ty,loc,ofs,v,tr,H1,H2. P ??? (eval_Elvalue ge e m a ty loc ofs v tr H1 H2))
    702630  (ead:∀a,ty,loc,ofs,tr,H. P ??? (eval_Eaddrof ge e m a ty loc ofs tr H))
     
    715643  match ev with
    716644  [ eval_Econst_int sz sg i ⇒ eci sz sg i
    717   | eval_Econst_float f ty ⇒ ecF f ty
     645(*  | eval_Econst_float f ty ⇒ ecF f ty *)
    718646  | eval_Elvalue a ty loc ofs v tr H1 H2 ⇒ elv a ty loc ofs v tr H1 H2
    719647  | eval_Eaddrof a ty loc ofs tr H ⇒ ead a ty loc ofs tr H
    720648  | eval_Esizeof ty' sz sg ⇒ esz ty' sz sg
    721   | eval_Eunop op a ty v1 v tr H1 H2 ⇒ eun op a ty v1 v tr H1 H2 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a v1 tr H1)
    722   | eval_Ebinop op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 ⇒ ebi op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr1 H1) (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a2 v2 tr2 H2)
    723   | eval_Econdition_true a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3 ⇒ ect a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr1 H1) (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a2 v2 tr2 H3)
    724   | eval_Econdition_false a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3 ⇒ ecf a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr1 H1) (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a3 v3 tr2 H3)
    725   | eval_Eorbool_1 a1 a2 ty v1 tr H1 H2 ⇒ eo1 a1 a2 ty v1 tr H1 H2 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr H1)
    726   | eval_Eorbool_2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 ⇒ eo2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr1 H1) (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a2 v2 tr2 H3)
    727   | eval_Eandbool_1 a1 a2 ty v1 tr H1 H2 ⇒ ea1 a1 a2 ty v1 tr H1 H2 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr H1)
    728   | eval_Eandbool_2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 ⇒ ea2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr1 H1) (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a2 v2 tr2 H3)
    729   | eval_Ecast a ty ty' v1 v tr H1 H2 ⇒ ecs a ty ty' v1 v tr H1 H2 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a v1 tr H1)
    730   | eval_Ecost a ty v l tr H ⇒ eco a ty v l tr H (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a v tr H)
     649  | eval_Eunop op a ty v1 v tr H1 H2 ⇒ eun op a ty v1 v tr H1 H2 (eval_expr_ind ge e m P eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a v1 tr H1)
     650  | eval_Ebinop op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 ⇒ ebi op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 (eval_expr_ind ge e m P eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr1 H1) (eval_expr_ind ge e m P eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a2 v2 tr2 H2)
     651  | eval_Econdition_true a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3 ⇒ ect a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3 (eval_expr_ind ge e m P eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr1 H1) (eval_expr_ind ge e m P eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a2 v2 tr2 H3)
     652  | eval_Econdition_false a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3 ⇒ ecf a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3 (eval_expr_ind ge e m P eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr1 H1) (eval_expr_ind ge e m P eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a3 v3 tr2 H3)
     653  | eval_Eorbool_1 a1 a2 ty v1 tr H1 H2 ⇒ eo1 a1 a2 ty v1 tr H1 H2 (eval_expr_ind ge e m P eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr H1)
     654  | eval_Eorbool_2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 ⇒ eo2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 (eval_expr_ind ge e m P eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr1 H1) (eval_expr_ind ge e m P eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a2 v2 tr2 H3)
     655  | eval_Eandbool_1 a1 a2 ty v1 tr H1 H2 ⇒ ea1 a1 a2 ty v1 tr H1 H2 (eval_expr_ind ge e m P eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr H1)
     656  | eval_Eandbool_2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 ⇒ ea2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 (eval_expr_ind ge e m P eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr1 H1) (eval_expr_ind ge e m P eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a2 v2 tr2 H3)
     657  | eval_Ecast a ty ty' v1 v tr H1 H2 ⇒ ecs a ty ty' v1 v tr H1 H2 (eval_expr_ind ge e m P eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a v1 tr H1)
     658  | eval_Ecost a ty v l tr H ⇒ eco a ty v l tr H (eval_expr_ind ge e m P eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a v tr H)
    731659  ].
    732660(*
     
    806734  (Q:∀a,loc,ofs,tr. eval_lvalue ge e m a loc ofs tr → Prop)
    807735  (eci:∀sz,sg,i. P ??? (eval_Econst_int ge e m sz sg i))
    808   (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty))
    809736  (elv:∀a,ty,loc,ofs,v,tr,H1,H2. Q (Expr a ty) loc ofs tr H1 → P ??? (eval_Elvalue ge e m a ty loc ofs v tr H1 H2))
    810737  (ead:∀a,ty,loc,ofs,tr,H. Q a loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty loc ofs tr H))
     
    829756  match ev with
    830757  [ eval_Econst_int sz sg i ⇒ eci sz sg i
    831   | eval_Econst_float f ty ⇒ ecF f ty
    832   | eval_Elvalue a ty loc ofs v tr H1 H2 ⇒ elv a ty loc ofs v tr H1 H2 (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu (Expr a ty) loc ofs tr H1)
    833   | eval_Eaddrof a ty loc ofs tr H ⇒ ead a ty loc ofs tr H (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a loc ofs tr H)
     758  | eval_Elvalue a ty loc ofs v tr H1 H2 ⇒ elv a ty loc ofs v tr H1 H2 (eval_lvalue_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu (Expr a ty) loc ofs tr H1)
     759  | eval_Eaddrof a ty loc ofs tr H ⇒ ead a ty loc ofs tr H (eval_lvalue_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a loc ofs tr H)
    834760  | eval_Esizeof ty' sz sg ⇒ esz ty' sz sg
    835   | eval_Eunop op a ty v1 v tr H1 H2 ⇒ eun op a ty v1 v tr H1 H2 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a v1 tr H1)
    836   | eval_Ebinop op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 ⇒ ebi op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr1 H1) (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a2 v2 tr2 H2)
    837   | eval_Econdition_true a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3 ⇒ ect a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr1 H1) (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a2 v2 tr2 H3)
    838   | eval_Econdition_false a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3 ⇒ ecf a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr1 H1) (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a3 v3 tr2 H3)
    839   | eval_Eorbool_1 a1 a2 ty v1 tr H1 H2 ⇒ eo1 a1 a2 ty v1 tr H1 H2 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr H1)
    840   | eval_Eorbool_2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 ⇒ eo2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr1 H1) (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a2 v2 tr2 H3)
    841   | eval_Eandbool_1 a1 a2 ty v1 tr H1 H2 ⇒ ea1 a1 a2 ty v1 tr H1 H2 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr H1)
    842   | eval_Eandbool_2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 ⇒ ea2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr1 H1) (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a2 v2 tr2 H3)
    843   | eval_Ecast a ty ty' v1 v tr H1 H2 ⇒ ecs a ty ty' v1 v tr H1 H2 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a v1 tr H1)
    844   | eval_Ecost a ty v l tr H ⇒ eco a ty v l tr H (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a v tr H)
     761  | eval_Eunop op a ty v1 v tr H1 H2 ⇒ eun op a ty v1 v tr H1 H2 (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a v1 tr H1)
     762  | eval_Ebinop op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 ⇒ ebi op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr1 H1) (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a2 v2 tr2 H2)
     763  | eval_Econdition_true a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3 ⇒ ect a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3 (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr1 H1) (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a2 v2 tr2 H3)
     764  | eval_Econdition_false a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3 ⇒ ecf a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3 (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr1 H1) (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a3 v3 tr2 H3)
     765  | eval_Eorbool_1 a1 a2 ty v1 tr H1 H2 ⇒ eo1 a1 a2 ty v1 tr H1 H2 (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr H1)
     766  | eval_Eorbool_2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 ⇒ eo2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr1 H1) (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a2 v2 tr2 H3)
     767  | eval_Eandbool_1 a1 a2 ty v1 tr H1 H2 ⇒ ea1 a1 a2 ty v1 tr H1 H2 (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr H1)
     768  | eval_Eandbool_2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 ⇒ ea2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr1 H1) (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a2 v2 tr2 H3)
     769  | eval_Ecast a ty ty' v1 v tr H1 H2 ⇒ ecs a ty ty' v1 v tr H1 H2 (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a v1 tr H1)
     770  | eval_Ecost a ty v l tr H ⇒ eco a ty v l tr H (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a v tr H)
    845771  ]
    846772and eval_lvalue_ind2 (ge:genv) (e:env) (m:mem)
     
    848774  (Q:∀a,loc,ofs,tr. eval_lvalue ge e m a loc ofs tr → Prop)
    849775  (eci:∀sz,sg,i. P ??? (eval_Econst_int ge e m sz sg i))
    850   (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty))
    851776  (elv:∀a,ty,loc,ofs,v,tr,H1,H2. Q (Expr a ty) loc ofs tr H1 → P ??? (eval_Elvalue ge e m a ty loc ofs v tr H1 H2))
    852777  (ead:∀a,ty,loc,ofs,tr,H. Q a loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty loc ofs tr H))
     
    871796  [ eval_Evar_local id l ty H ⇒ lvl id l ty H
    872797  | eval_Evar_global id l ty H1 H2 ⇒ lvg id l ty H1 H2
    873   | eval_Ederef a ty l ofs tr H ⇒ lde a ty l ofs tr H (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a (Vptr (mk_pointer l ofs)) tr H)
    874   | eval_Efield_struct a i ty l ofs id fList delta tr H1 H2 H3 ⇒ lfs a i ty l ofs id fList delta tr H1 H2 H3 (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a l ofs tr H1)
    875   | eval_Efield_union a i ty l ofs id fList tr H1 H2 ⇒ lfu a i ty l ofs id fList tr H1 H2 (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a l ofs tr H1)
     798  | eval_Ederef a ty l ofs tr H ⇒ lde a ty l ofs tr H (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a (Vptr (mk_pointer l ofs)) tr H)
     799  | eval_Efield_struct a i ty l ofs id fList delta tr H1 H2 H3 ⇒ lfs a i ty l ofs id fList delta tr H1 H2 H3 (eval_lvalue_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a l ofs tr H1)
     800  | eval_Efield_union a i ty l ofs id fList tr H1 H2 ⇒ lfu a i ty l ofs id fList tr H1 H2 (eval_lvalue_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a l ofs tr H1)
    876801  ].
    877802
    878803definition combined_expr_lvalue_ind ≝
    879 λge,e,m,P,Q,eci,ecF,elv,ead,esz,eun,ebi,ect,ecf,eo1,eo2,ea1,ea2,ecs,eco,lvl,lvg,lde,lfs,lfu. 
     804λge,e,m,P,Q,eci,elv,ead,esz,eun,ebi,ect,ecf,eo1,eo2,ea1,ea2,ecs,eco,lvl,lvg,lde,lfs,lfu. 
    880805conj ??
    881   (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu)
    882   (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu).
     806  (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu)
     807  (eval_lvalue_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu).
    883808
    884809(* * [eval_lvalue ge e m a b ofs] defines the evaluation of expression [a]
     
    1028953[ Tvoid ⇒ Tvoid
    1029954| Tint a b ⇒ Tint a b
    1030 | Tfloat a ⇒ Tfloat a
     955(*| Tfloat a ⇒ Tfloat a*)
    1031956| Tpointer ty ⇒ ty
    1032957| Tarray a b ⇒ Tarray a b
Note: See TracChangeset for help on using the changeset viewer.