Changeset 2174


Ignore:
Timestamp:
Jul 10, 2012, 5:37:10 PM (5 years ago)
Author:
tranquil
Message:
  • factored out script for (axiomatised) fixpoint computation
  • ERTL → LTL pass
Location:
src
Files:
6 added
2 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL_paolo.ma

    r2162 r2174  
    4646  (mk_local_params
    4747    (mk_funct_params
    48       (* resultT ≝ *) (list register)
     48      (* resultT ≝ *) unit
    4949      (* paramsT ≝ *) ℕ)
    5050      (* localsT ≝ *) register).
  • 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.