Changeset 2468 for src/common


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

Location:
src/common
Files:
7 edited

Legend:

Unmodified
Added
Removed
  • src/common/AST.ma

    r2439 r2468  
    128128inductive typ : Type[0] ≝
    129129  | ASTint : intsize → signedness → typ
    130   | ASTptr : (*region →*) typ
    131   | ASTfloat : floatsize → typ.
     130  | ASTptr : (*region →*) typ.
     131(*  | ASTfloat : floatsize → typ. *)
    132132
    133133(* XXX aliases *)
     
    246246  match ty with
    247247  [ ASTint sz _ ⇒ size_intsize sz
    248   | ASTptr  ⇒ size_pointer
    249   | ASTfloat sz ⇒ size_floatsize sz ].
     248  | ASTptr  ⇒ size_pointer ].
     249(*  | ASTfloat sz ⇒ size_floatsize sz ].*)
    250250
    251251lemma typesize_pos: ∀ty. typesize ty > 0.
  • src/common/Events.ma

    r1599 r2468  
    3838
    3939inductive eventval: Type[0] ≝
    40   | EVint: ∀sz. bvint sz → eventval
    41   | EVfloat: float → eventval.
     40  | EVint: ∀sz. bvint sz → eventval.
     41(*  | EVfloat: float → eventval.*)
    4242
    4343inductive event : Type[0] ≝
     
    194194  | ev_match_int:
    195195      ∀sz,sg,i. eventval_match (EVint sz i) (ASTint sz sg) (Vint sz i)
    196   | ev_match_float:
    197       ∀f,sz. eventval_match (EVfloat f) (ASTfloat sz) (Vfloat f).
     196(*  | ev_match_float:
     197      ∀f,sz. eventval_match (EVfloat f) (ASTfloat sz) (Vfloat f) *).
    198198
    199199inductive eventval_list_match: list eventval -> list typ -> list val -> Prop :=
  • src/common/FrontEndOps.ma

    r2432 r2468  
    2323inductive constant : typ → Type[0] ≝
    2424  | Ointconst: ∀sz,sg. bvint sz → constant (ASTint sz sg)
    25   | Ofloatconst: ∀sz. float → constant (ASTfloat sz)
     25(*  | Ofloatconst: ∀sz. float → constant (ASTfloat sz) *)
    2626  | Oaddrsymbol: ident → nat → constant ASTptr (**r address of the symbol plus the offset *)
    2727  | Oaddrstack: nat → constant ASTptr.         (**r stack pointer plus the given offset *)
     
    3434  | Onotbool: ∀t,sz,sg. boolsrc t → unary_operation t (ASTint sz sg)           (**r boolean negation  *)
    3535  | Onotint:  ∀sz,sg. unary_operation (ASTint sz sg) (ASTint sz sg)            (**r bitwise complement  *)
    36   | Onegf: ∀sz. unary_operation (ASTfloat sz) (ASTfloat sz)                    (**r float opposite *)
    37   | Oabsf: ∀sz. unary_operation (ASTfloat sz) (ASTfloat sz)                    (**r float absolute value *)
    38   | Osingleoffloat: unary_operation (ASTfloat F64) (ASTfloat F32)              (**r float truncation *)
    39   | Ointoffloat:  ∀fsz,sz. unary_operation (ASTfloat fsz) (ASTint sz Signed)  (**r signed integer to float *)
    40   | Ointuoffloat: ∀fsz,sz. unary_operation (ASTfloat fsz) (ASTint sz Unsigned) (**r unsigned integer to float *)
    41   | Ofloatofint:  ∀fsz,sz. unary_operation (ASTint sz Signed) (ASTfloat fsz)   (**r float to signed integer *)
    42   | Ofloatofintu: ∀fsz,sz. unary_operation (ASTint sz Unsigned) (ASTfloat fsz) (**r float to unsigned integer *)
     36(*| Onegf: ∀sz. unary_operation (ASTfloat sz) (ASTfloat sz)*)                  (**r float opposite *)
     37(*| Oabsf: ∀sz. unary_operation (ASTfloat sz) (ASTfloat sz)*)                  (**r float absolute value *)
     38(*| Osingleoffloat: unary_operation (ASTfloat F64) (ASTfloat F32)*)            (**r float truncation *)
     39(*| Ointoffloat:  ∀fsz,sz. unary_operation (ASTfloat fsz) (ASTint sz Signed)*) (**r signed integer to float *)
     40(*| Ointuoffloat: ∀fsz,sz. unary_operation (ASTfloat fsz) (ASTint sz Unsigned)*) (**r unsigned integer to float *)
     41(*| Ofloatofint:  ∀fsz,sz. unary_operation (ASTint sz Signed) (ASTfloat fsz)*)   (**r float to signed integer *)
     42(*| Ofloatofintu: ∀fsz,sz. unary_operation (ASTint sz Unsigned) (ASTfloat fsz)*) (**r float to unsigned integer *)
    4343  | Oid: ∀t. unary_operation t t                                               (**r identity (used to move between registers *)
    4444  | Optrofint: ∀sz,sg. unary_operation (ASTint sz sg) ASTptr                   (**r int to pointer with given representation *)
     
    5959  | Oshr:  ∀sz,sg. binary_operation (ASTint sz sg)       (ASTint sz sg)       (ASTint sz sg)       (**r right signed shift *)
    6060  | Oshru: ∀sz,sg. binary_operation (ASTint sz Unsigned) (ASTint sz sg)       (ASTint sz sg)       (**r right unsigned shift *)
    61   | Oaddf: ∀sz.    binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTfloat sz)        (**r float addition *)
    62   | Osubf: ∀sz.    binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTfloat sz)        (**r float subtraction *)
    63   | Omulf: ∀sz.    binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTfloat sz)        (**r float multiplication *)
    64   | Odivf: ∀sz.    binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTfloat sz)        (**r float division *)
     61(*  | Oaddf: ∀sz.    binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTfloat sz)*)        (**r float addition *)
     62(*  | Osubf: ∀sz.    binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTfloat sz)*)        (**r float subtraction *)
     63(*  | Omulf: ∀sz.    binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTfloat sz)*)        (**r float multiplication *)
     64(*  | Odivf: ∀sz.    binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTfloat sz)*)        (**r float division *)
    6565  | Ocmp: ∀sz,sg,sg'. comparison -> binary_operation (ASTint sz sg)       (ASTint sz sg)       (ASTint I8 sg') (**r integer signed comparison *)
    6666  | Ocmpu: ∀sz,sg'.   comparison -> binary_operation (ASTint sz Unsigned) (ASTint sz Unsigned) (ASTint I8 sg') (**r integer unsigned comparison *)
    67   | Ocmpf: ∀sz,sg'.   comparison -> binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTint I8 sg') (**r float comparison *)
     67(*  | Ocmpf: ∀sz,sg'.   comparison -> binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTint I8 sg') *) (**r float comparison *)
    6868  | Oaddp: ∀sz.    binary_operation  ASTptr              (ASTint sz Signed)    ASTptr              (**r add an integer to a pointer *)
    6969  | Osubpi: ∀sz.   binary_operation  ASTptr              (ASTint sz Signed)    ASTptr              (**r subtract int from a pointers *)
     
    7676match t with
    7777[ ASTint sz sg ⇒ ∀i.P (Vint sz i)
    78 | ASTfloat sz ⇒ ∀f.P (Vfloat f)
     78(*| ASTfloat sz ⇒ ∀f.P (Vfloat f) *)
    7979| ASTptr ⇒ P Vnull ∧ ∀b,o. P (Vptr (mk_pointer b o))
    8080] →
    8181P v.
    8282#v #t #P *
    83 [ 1,2: //
     83[ 1: //
    8484| * //
    8585| #b #o * //
     
    9595  match cst with
    9696  [ Ointconst sz sg n ⇒ Some ? (Vint sz n)
    97   | Ofloatconst sz n ⇒ Some ? (Vfloat n)
     97(*  | Ofloatconst sz n ⇒ Some ? (Vfloat n)*)
    9898  | Oaddrsymbol s ofs ⇒
    9999      match find_symbol s with
     
    113113#t #f #sp *
    114114[ #sz #sg #i #v #E normalize in E; destruct //
    115 | #sz #f #v #E normalize in E; destruct //
     115(*| #sz #f #v #E normalize in E; destruct //*)
    116116| #id #n #v whd in ⊢ (??%? → ?); cases (f id) [2:#b] #E whd in E:(??%?); destruct
    117117(*  cases (pointer_compat_dec b r) in E; #pc #E whd in E:(??%?); destruct *)
     
    137137      ]
    138138  | Onotint sz sg ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vint sz1 (exclusive_disjunction_bv ? n1 (mone ?))) | _ ⇒ None ? ]
    139   | Onegf _ ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vfloat (Fneg f1)) | _ ⇒ None ? ]
    140   | Oabsf _ ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vfloat (Fabs f1)) | _ ⇒ None ? ]
     139(*  | Onegf _ ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vfloat (Fneg f1)) | _ ⇒ None ? ]
     140  | Oabsf _ ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vfloat (Fabs f1)) | _ ⇒ None ? ] 
    141141  | Osingleoffloat ⇒ Some ? (singleoffloat arg)
    142142  | Ointoffloat _ sz ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint sz (intoffloat ? f1)) | _ ⇒ None ? ]
    143143  | Ointuoffloat _ sz ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint sz (intuoffloat ? f1)) | _ ⇒ None ? ]
    144144  | Ofloatofint _ _ ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vfloat (floatofint ? n1)) | _ ⇒ None ? ]
    145   | Ofloatofintu _ _ ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vfloat (floatofintu ? n1)) | _ ⇒ None ? ]
     145  | Ofloatofintu _ _ ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vfloat (floatofintu ? n1)) | _ ⇒ None ? ] *)
    146146  | Oid t ⇒ Some ? arg (* XXX should we restricted the values allowed? *)
    147147  (* Only conversion of null pointers is specified. *)
     
    164164    | #b #o whd in ⊢ (??%? → ?); #E' destruct %
    165165    ]
    166   | #f *
     166(*  | #f * *)
    167167  ]
    168168| #sz #sg #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); #E destruct %
     169(*
    169170| #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?); #E destruct %2
    170171| #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?); #E destruct %2
     
    174175| #fsz #sz #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); #E destruct %2
    175176| #fsz #sz #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); #E destruct %2
     177*)
    176178| #t'' #v #v' #H whd in ⊢ (??%? → ?); #E destruct @H
    177179| #sz #sg #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); cases (eq_bv ???)
     
    349351  | _ ⇒ None ? ].
    350352
     353(*
    351354definition ev_addf ≝ λv1,v2: val.
    352355  match v1 with
     
    375378    [ Vfloat f2 ⇒ Some ? (Vfloat (Fdiv f1 f2))
    376379    | _ ⇒ None ? ]
    377   | _ ⇒ None ? ].
     380  | _ ⇒ None ? ]. *)
    378381
    379382definition FEtrue : val ≝ Vint I8 (repr I8 1).
     
    434437  | _ ⇒ None ? ].
    435438
     439(*
    436440definition ev_cmpf ≝ λc: comparison. λv1,v2: val.
    437441  match v1 with
     
    439443    [ Vfloat f2 ⇒ Some ? (FE_of_bool (Fcmp c f1 f2))
    440444    | _ ⇒ None ? ]
    441   | _ ⇒ None ? ].
     445  | _ ⇒ None ? ]. *)
    442446
    443447definition eval_binop : mem → ∀t1,t2,t'. binary_operation t1 t2 t' → val → val → option val ≝
     
    457461  | Oshr _ _ ⇒ ev_shr
    458462  | Oshru _ _ ⇒ ev_shru
    459   | Oaddf _ ⇒ ev_addf
     463(*  | Oaddf _ ⇒ ev_addf
    460464  | Osubf _ ⇒ ev_subf
    461465  | Omulf _ ⇒ ev_mulf
    462   | Odivf _ ⇒ ev_divf
     466  | Odivf _ ⇒ ev_divf *)
    463467  | Ocmp _ _ _ c ⇒ ev_cmp c
    464468  | Ocmpu _ _ c ⇒ ev_cmpu c
    465   | Ocmpf _ _ c ⇒ ev_cmpf c
     469(*  | Ocmpf _ _ c ⇒ ev_cmpf c *)
    466470  | Oaddp _ ⇒ ev_addp
    467471  | Osubpi _ ⇒ ev_subpi
     
    490494  whd in ⊢ (??%? → ?); cases (lt_u ???) whd in ⊢ (??%? → ?); #E destruct //
    491495(* floats *)
    492 | 14,15,16,17: #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #f1 @(elim_val_typ … V2) #f2
    493   whd in ⊢ (??%? → ?); #E destruct //
     496(*| 14,15,16,17: #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #f1 @(elim_val_typ … V2) #f2
     497  whd in ⊢ (??%? → ?); #E destruct // *)
    494498(* comparisons *)
    495499| #sz #sg #sg' #c #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) #i2
     
    497501| #sz #sg' #c #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) #i2
    498502  whd in ⊢ (??%? → ?); >intsize_eq_elim_true cases (cmpu_int ????) #E destruct //
    499 | #sz #sg' #c #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #f1 @(elim_val_typ … V2) #f2
    500   whd in ⊢ (??%? → ?); cases (Fcmp ???) #E destruct //
     503(*| #sz #sg' #c #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #f1 @(elim_val_typ … V2) #f2
     504  whd in ⊢ (??%? → ?); cases (Fcmp ???) #E destruct // *)
    501505(* pointers *)
    502 | 21,22: #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ 2,4: #b #o ] @(elim_val_typ … V2) #i2
     506| 16,17: #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ 2,4: #b #o ] @(elim_val_typ … V2) #i2
    503507  whd in ⊢ (??%? → ?); [ 3,4: cases (eq_bv ???) whd in ⊢ (??%? → ?); | ] #E destruct //
    504508| #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ | #b1 #o1 ] @(elim_val_typ … V2) % [ 2,4: #b2 #o2 ]
  • src/common/FrontEndVal.ma

    r2435 r2468  
    2222[ Vundef ⇒ make_list ? BVundef (typesize t)
    2323| Vint sz i ⇒ map ?? (λb.BVByte b) (bytes_of_bitvector ? (i⌈bvint sz ↦ BitVector (size_intsize sz * 8)⌉))
    24 | Vfloat _ ⇒ make_list ? BVundef (typesize t) (* unsupported *)
     24(*| Vfloat _ ⇒ make_list ? BVundef (typesize t) *) (* unsupported *)
    2525| Vptr ptr ⇒ bevals_of_pointer ptr
    2626| Vnull  ⇒ make_be_null
  • src/common/Globalenvs.ma

    r2439 r2468  
    181181  | Init_int16 n ⇒ store (ASTint I16 Unsigned) m ptr (Vint I16 n)
    182182  | Init_int32 n ⇒ store (ASTint I32 Unsigned) m ptr (Vint I32 n)
    183   | Init_float32 n ⇒ store (ASTfloat F32) m ptr (Vfloat n)
    184   | Init_float64 n ⇒ store (ASTfloat F64) m ptr (Vfloat n)
     183  | Init_float32 n ⇒ None ? (*store (ASTfloat F32) m ptr (Vfloat n)*)
     184  | Init_float64 n ⇒ None ? (*store (ASTfloat F64) m ptr (Vfloat n) *)
    185185  | Init_addrof (*r'*) symb ofs ⇒
    186186      match find_symbol … ge symb with
     
    334334[ #f #E normalize in E; destruct
    335335| #sz #i #f #E normalize in E; destruct
    336 | #f #fn #E normalize in E; destruct
     336(*| #f #fn #E normalize in E; destruct*)
    337337| (*#r*) #f #E normalize in E; destruct
    338338| * (*#pty*) #b (*#c*) * #off #f whd in ⊢ (??%? → ?);
     
    10671067  | skip
    10681068  ]
    1069 | * [5: #ptr #fn whd in match (find_funct ???);
     1069| * [ 4: #ptr #fn whd in match (find_funct ???);
    10701070     @if_elim #Eoff #FFP
    10711071     [ cases (find_funct_ptr_match … (transform_program_gen_match … tf p) … FFP)
  • src/common/IO.ma

    r2176 r2468  
    66
    77definition eventval_type : ∀ty:typ. Type[0] ≝
    8 λty. match ty with [ ASTint sz _ ⇒ bvint sz | ASTptr ⇒ False | ASTfloat _ ⇒ float ].
     8λty. match ty return λ_. Type[0] with [ ASTptr ⇒ False | ASTint sz _ ⇒ bvint sz ].
    99
    1010definition mk_eventval: ∀ty:typ. eventval_type ty → eventval ≝
    11 λty:typ. match ty return λty'.eventval_type ty' → eventval with [ ASTint sz sg ⇒ λv.EVint sz v | ASTptr ⇒ ? | ASTfloat _ ⇒ λv.EVfloat v ].
     11λty:typ. match ty return λty'.eventval_type ty' → eventval with [ ASTint sz sg ⇒ λv.EVint sz v | ASTptr ⇒ ?  (*| ASTfloat _ ⇒ λv.EVfloat v*) ].
    1212*; qed.
    1313
    1414definition mk_val: ∀ty:typ. eventval_type ty → val ≝
    15 λty:typ. match ty return λty'.eventval_type ty' → val with [ ASTint sz _ ⇒ λv.Vint sz v | ASTptr ⇒ ? | ASTfloat _ ⇒ λv.Vfloat v ].
     15λty:typ. match ty return λty'.eventval_type ty' → val with [ ASTint sz _ ⇒ λv.Vint sz v | ASTptr ⇒ ? (*| ASTfloat _ ⇒ λv.Vfloat v*) ].
    1616*; qed.
    1717
     
    2828  [ EVint sz' i ⇒ if eq_intsize sz sz' then OK ? (Vint sz' i) else Error ? (msg IllTypedEvent)
    2929  | _ ⇒ Error ? (msg IllTypedEvent)]
    30 | ASTfloat _ ⇒ match ev with [ EVfloat f ⇒ OK ? (Vfloat f) | _ ⇒ Error ? (msg IllTypedEvent)]
     30(*| ASTfloat _ ⇒ match ev with [ EVfloat f ⇒ OK ? (Vfloat f) | _ ⇒ Error ? (msg IllTypedEvent)] *)
    3131| _ ⇒ Error ? (msg IllTypedEvent)
    3232].
     
    3838  [ Vint sz' i ⇒ if eq_intsize sz sz' then OK ? (EVint sz' i) else Error ? (msg IllTypedEvent)
    3939  | _ ⇒ Error ? (msg IllTypedEvent) ]
    40 | ASTfloat _ ⇒ match v with [ Vfloat f ⇒ OK ? (EVfloat f) | _ ⇒ Error ? (msg IllTypedEvent) ]
     40(*| ASTfloat _ ⇒ match v with [ Vfloat f ⇒ OK ? (EVfloat f) | _ ⇒ Error ? (msg IllTypedEvent) ]*)
    4141| _ ⇒ Error ? (msg IllTypedEvent)
    4242].
  • src/common/Values.ma

    r2176 r2468  
    1818
    1919include "utilities/Coqlib.ma".
    20 include "common/Floats.ma".
     20(*include "common/Floats.ma".*)
    2121include "common/Errors.ma".
    2222include "common/Pointers.ma".
     
    2525(* * A value is either:
    2626- a machine integer;
    27 - a floating-point number;
     27- /* a floating-point number; */ No more
    2828- a pointer: a triple giving the representation of the pointer (in terms of the
    2929             memory regions such a pointer could address), a memory address and
     
    3737  | Vundef: val
    3838  | Vint: ∀sz:intsize. bvint sz → val
    39   | Vfloat: float → val
     39(*  | Vfloat: float → val*)
    4040  | Vnull: (*region →*) val
    4141  | Vptr: pointer → val.
     
    5252inductive val_typ : val → typ → Prop ≝
    5353  | VTint: ∀sz,sg,i. val_typ (Vint sz i) (ASTint sz sg)
    54   | VTfloat: ∀sz,f. val_typ (Vfloat f) (ASTfloat sz)
     54(*  | VTfloat: ∀sz,f. val_typ (Vfloat f) (ASTfloat sz)*)
    5555  | VTnull: val_typ Vnull ASTptr
    5656  | VTptr: ∀b,o. val_typ (Vptr (mk_pointer b o)) ASTptr.
     
    109109  ].
    110110
     111(*
    111112definition negf : val → val ≝ λv.
    112113  match v with
     
    115116  ].
    116117
     118
    117119definition absf : val → val ≝ λv.
    118120  match v with
     
    121123  ].
    122124
     125
    123126definition intoffloat : intsize → val → val ≝ λsz,v.
    124127  match v with
     
    143146  [ Vint sz n ⇒ Vfloat (floatofintu ? n)
    144147  | _ ⇒ Vundef
    145   ].
     148  ]. *)
    146149
    147150definition notint : val → val ≝ λv.
     
    171174  ].
    172175
     176(*
    173177definition singleoffloat : val → val ≝ λv.
    174178  match v with
    175179  [ Vfloat f ⇒ Vfloat (singleoffloat f)
    176180  | _ ⇒ Vundef
    177   ].
     181  ]. *)
    178182
    179183(* TODO: add zero to null? *)
     
    334338  end.
    335339*)
     340
     341(*
    336342definition addf ≝ λv1,v2: val.
    337343  match v1 with
     
    360366    [ Vfloat f2 ⇒ Vfloat (Fdiv f1 f2)
    361367    | _ ⇒ Vundef ]
    362   | _ ⇒ Vundef ].
     368  | _ ⇒ Vundef ]. *)
    363369
    364370definition cmp_match : comparison → val ≝ λc.
     
    451457  | _ ⇒ Vundef ].
    452458
     459
     460(*
    453461definition cmpf ≝ λc: comparison. λsz:intsize. λv1,v2: val.
    454462  match v1 with
     
    456464    [ Vfloat f2 ⇒ of_bool (Fcmp c f1 f2)
    457465    | _ ⇒ Vundef ]
    458   | _ ⇒ Vundef ].
     466  | _ ⇒ Vundef ]. *)
    459467
    460468(* * [load_result] is used in the memory model (library [Mem])
     
    487495    | _ ⇒ Vundef
    488496    ]
    489   | Vfloat f ⇒
     497(*  | Vfloat f ⇒
    490498    match chunk with
    491499    [ ASTfloat sz ⇒ match sz with [ F32 ⇒ Vfloat(singleoffloat f) | F64 ⇒ Vfloat f ]
    492500    | _ ⇒ Vundef
    493     ]
     501    ] *)
    494502  | _ ⇒ Vundef
    495503  ].
     
    10801088  Val_lessdef v1 v2 → Val_lessdef (load_result chunk v1) (load_result chunk v2).
    10811089#chunk #v1 #v2 #H inversion H; //; #v #e1 #e2 #e3 cases chunk
    1082 [ #sz #sg | | #sz ] whd in ⊢ (?%?); //;
     1090[ #sz #sg | ] whd in ⊢ (?%?); //;
    10831091qed.
    10841092
Note: See TracChangeset for help on using the changeset viewer.