Changeset 2862
- Timestamp:
- Mar 13, 2013, 2:07:20 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTL/RTLToERTL.ma
r2861 r2862 301 301 (* init_stack_size ≝ *) new_stacksize 302 302 (* added_prologue ≝ *) prologue 303 (* new_regs ≝ *) ( addr2 :: addr1 :: tmpr :: rah :: ral :: map … (λx.\fst x) to_save)303 (* new_regs ≝ *) (reverse … (addr2 :: addr1 :: tmpr :: rah :: ral :: map … (λx.\fst x) to_save)) 304 304 (* f_step ≝ *) (translate_step globals) 305 305 (* f_fin ≝ *) (translate_fin_step globals (joint_if_result … def) ral rah to_save) … … 313 313 try #a try #b try #c try #d try #e try #f destruct 314 314 cases a in b; #a1 #a2 normalize nodelta #EQ destruct 315 | #r1 #r2 #r3 #r4 #r5 #r6 #r7 #r8 #ral #rah #tmpr #addr1 #addr2 316 change with (? = ?) 315 | #r1 #r2 #r3 #r4 #r5 #r6 #r7 #r8 #ral #rah #tmpr #addr1 #addr2 317 316 % (* XXX: FAILS, unintentional list reversal??? *) 318 317 ]
Note: See TracChangeset
for help on using the changeset viewer.