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

Fix up earlier front-end value conversion work.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.