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/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)
Note: See TracChangeset for help on using the changeset viewer.