Changeset 2624


Ignore:
Timestamp:
Feb 6, 2013, 6:39:21 PM (6 years ago)
Author:
campbell
Message:

Properly evict unused and axiomatised Floats.

Location:
src
Files:
1 deleted
3 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/initialisation.ma

    r2601 r2624  
    1212| Init_int16 i         ⇒ Some ? (mk_DPair ?? (ASTint I16 Unsigned) (Cst ? (Ointconst I16 Unsigned i)))
    1313| Init_int32 i         ⇒ Some ? (mk_DPair ?? (ASTint I32 Unsigned) (Cst ? (Ointconst I32 Unsigned i)))
    14 | Init_float32 f       ⇒ None ? (*Some ? (mk_DPair ?? (ASTfloat F32) (Cst ? (Ofloatconst F32 f)))*)
    15 | Init_float64 f       ⇒ None ? (*Some ? (mk_DPair ?? (ASTfloat F64) (Cst ? (Ofloatconst F64 f)))*)
     14(*| Init_float32 f       ⇒ None ? (*Some ? (mk_DPair ?? (ASTfloat F32) (Cst ? (Ofloatconst F32 f)))*)
     15| Init_float64 f       ⇒ None ? (*Some ? (mk_DPair ?? (ASTfloat F64) (Cst ? (Ofloatconst F64 f)))*)*)
    1616| Init_space n         ⇒ None ?
    1717| Init_null            ⇒ Some ? (mk_DPair ?? ASTptr (Op1 (ASTint I8 Unsigned) ? (Optrofint ??) (Cst ? (Ointconst I8 Unsigned (zero ?)))))
     
    3939].
    4040% /3/
    41 cases init in p; [ 7: | 8: #a #b | *: #a ] #p normalize in p;
     41cases init in p; [ 5: | 6: #a #b | *: #a ] #p normalize in p;
    4242destruct;/4 by stmt_labels_mp, conj/
    4343qed.
  • src/common/AST.ma

    r2468 r2624  
    1919include "basics/types.ma".
    2020include "common/Integers.ma".
    21 include "common/Floats.ma".
    2221include "ASM/Arithmetic.ma".
    2322include "common/Identifiers.ma".
     
    292291  | Init_int16: bvint I16 → init_data
    293292  | Init_int32: bvint I32 → init_data
    294   | Init_float32: float → init_data
    295   | Init_float64: float → init_data
     293(*  | Init_float32: float → init_data
     294  | Init_float64: float → init_data*)
    296295  | Init_space: nat → init_data
    297296  | Init_null: (*region →*) init_data
  • src/common/Globalenvs.ma

    r2608 r2624  
    208208  | Init_int16 n ⇒ store (ASTint I16 Unsigned) m ptr (Vint I16 n)
    209209  | Init_int32 n ⇒ store (ASTint I32 Unsigned) m ptr (Vint I32 n)
    210   | Init_float32 n ⇒ None ? (*store (ASTfloat F32) m ptr (Vfloat n)*)
    211   | Init_float64 n ⇒ None ? (*store (ASTfloat F64) m ptr (Vfloat n) *)
     210  (*| Init_float32 n ⇒ None ? (*store (ASTfloat F32) m ptr (Vfloat n)*)
     211  | Init_float64 n ⇒ None ? (*store (ASTfloat F64) m ptr (Vfloat n) *)*)
    212212  | Init_addrof (*r'*) symb ofs ⇒
    213213      match find_symbol … ge symb with
     
    230230  | Init_int16 _ ⇒ 2
    231231  | Init_int32 _ ⇒ 4
    232   | Init_float32 _ ⇒ 4
    233   | Init_float64 _ ⇒ 8
     232  (*| Init_float32 _ ⇒ 4
     233  | Init_float64 _ ⇒ 8*)
    234234  | Init_space n ⇒ max n 0
    235235  | Init_null (*r*) ⇒ size_pointer (*r*)
Note: See TracChangeset for help on using the changeset viewer.