Changeset 2174 for src/RTL


Ignore:
Timestamp:
Jul 10, 2012, 5:37:10 PM (8 years ago)
Author:
tranquil
Message:
  • factored out script for (axiomatised) fixpoint computation
  • ERTL → LTL pass
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLToERTL_paolo.ma

    r2162 r2174  
    3434  let int_offset : Byte ≝ \snd (half_add ? (bitvector_of_nat ? off) int_size) in
    3535  [ (ertl_frame_size addr1 : joint_seq ??) ;
    36     (* shouldn't we CLEAR_CARRY … ; ? *)
     36    CLEAR_CARRY … ;
    3737    addr1 ← addr1 .Sub. int_offset ; (* are we sure carry bit is unimportant? *)
    3838    PSD destr ← HDW RegisterSPL ;
     
    133133
    134134(* Paolo: The following can probably be done way more efficiently with INC DPTR *)
    135 (* why get_param_stack and set_param_stack are not symmetric? *)
    136135
    137136definition set_param_stack :
Note: See TracChangeset for help on using the changeset viewer.