Ignore:
Timestamp:
Nov 15, 2012, 6:12:57 PM (8 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/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
Note: See TracChangeset for help on using the changeset viewer.