Changeset 1873 for src/common


Ignore:
Timestamp:
Apr 4, 2012, 6:48:24 PM (8 years ago)
Author:
campbell
Message:

Fix up earlier front-end value conversion work.

Location:
src/common
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/common/AST.ma

    r1872 r1873  
    130130   (At the time of writing this is only used for bitsize_of_intsize.) *)
    131131
     132definition pred_size_intsize : intsize → nat ≝
     133λsz. match sz with [ I8 ⇒ 0 | I16 ⇒ 1 | I32 ⇒ 3].
     134
    132135definition size_intsize : intsize → nat ≝
    133 λsz. S match sz with [ I8 ⇒ 0 | I16 ⇒ 1 | I32 ⇒ 3].
     136λsz. S (pred_size_intsize sz).
    134137
    135138definition bitsize_of_intsize : intsize → nat ≝
    136 λsz. S match sz with [ I8 ⇒ 7 | I16 ⇒ 15 | I32 ⇒ 31].
     139λsz. size_intsize sz * 8.
    137140
    138141definition eq_intsize : intsize → intsize → bool ≝
  • src/common/FrontEndVal.ma

    r1551 r1873  
    2626] v.
    2727
    28 definition fe_to_be_values : memory_chunk → val → list beval ≝
    29 λc,v. match v with
    30 [ Vundef ⇒ make_list ? BVundef (size_chunk c)
     28definition fe_to_be_values : typ → val → list beval ≝
     29λt,v. match v with
     30[ Vundef ⇒ make_list ? BVundef (typesize t)
    3131| Vint sz i ⇒ map ?? (λb.BVByte b) (bytes_of_bitvector ? (i⌈bvint sz ↦ BitVector (size_intsize sz * 8)⌉))
    32 | Vfloat _ ⇒ make_list ? BVundef (size_chunk c) (* unsupported *)
     32| Vfloat _ ⇒ make_list ? BVundef (typesize t) (* unsupported *)
    3333| Vptr ptr ⇒ bevals_of_pointer ptr
    3434| Vnull r ⇒ make_be_null r
     
    7272].
    7373
    74 definition build_integer_val : memory_chunk → list beval → val ≝
    75 λc,l.
    76 match c with
    77 [ Mint8unsigned ⇒ option_map_def ?? (Vint I8) Vundef (build_integer 1 l)
    78 | Mint8signed ⇒ option_map_def ?? (Vint I8) Vundef (build_integer 1 l)
    79 | Mint16unsigned ⇒ option_map_def ?? (Vint I16) Vundef (build_integer 2 l)
    80 | Mint16signed ⇒ option_map_def ?? (Vint I16) Vundef (build_integer 2 l)
    81 | Mint32 ⇒ option_map_def ?? (Vint I32) Vundef (build_integer 4 l)
     74definition build_integer_val : typ → list beval → val ≝
     75λt,l.
     76match t with
     77[ ASTint sz sg ⇒ option_map_def ?? (Vint sz) Vundef (build_integer (size_intsize sz) l)
    8278| _ ⇒ Vundef
    8379].
    8480
    85 definition be_to_fe_value : memory_chunk → list beval → val ≝
    86 λc,l. match l with
     81definition be_to_fe_value : typ → list beval → val ≝
     82λty,l. match l with
    8783[ nil ⇒ Vundef
    8884| cons h t ⇒
    8985    match h with
    9086    [ BVundef ⇒ Vundef
    91     | BVByte b ⇒ build_integer_val c l
     87    | BVByte b ⇒ build_integer_val ty l
    9288    | BVptr ptr pt ⇒ if eqb (part_no ? pt) O ∧ check_be_ptr ptr (S O) t then Vptr ptr else Vundef
    9389    | BVnull r pt ⇒ if eqb (part_no ? pt) O ∧ check_be_null r (S O) t then Vnull r else Vundef
Note: See TracChangeset for help on using the changeset viewer.