Changeset 2812
 Timestamp:
 Mar 7, 2013, 9:23:23 PM (7 years ago)
 Location:
 extracted
 Files:

 1 added
 2 edited
Legend:
 Unmodified
 Added
 Removed

extracted/rTLabs_abstract.ml
r2797 r2812 150 150 RTLabs_semantics.genv > (RTLabs_semantics.state > Pointers.block 151 151 List.list > __ > 'a1) > rTLabs_ext_state > 'a1 **) 152 let rec rTLabs_ext_state_rect_Type4 ge h_mk_RTLabs_ext_state x_ 17319=153 let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_ 17319in152 let rec rTLabs_ext_state_rect_Type4 ge h_mk_RTLabs_ext_state x_341 = 153 let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_341 in 154 154 h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __ 155 155 … … 157 157 RTLabs_semantics.genv > (RTLabs_semantics.state > Pointers.block 158 158 List.list > __ > 'a1) > rTLabs_ext_state > 'a1 **) 159 let rec rTLabs_ext_state_rect_Type5 ge h_mk_RTLabs_ext_state x_ 17321=160 let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_ 17321in159 let rec rTLabs_ext_state_rect_Type5 ge h_mk_RTLabs_ext_state x_343 = 160 let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_343 in 161 161 h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __ 162 162 … … 164 164 RTLabs_semantics.genv > (RTLabs_semantics.state > Pointers.block 165 165 List.list > __ > 'a1) > rTLabs_ext_state > 'a1 **) 166 let rec rTLabs_ext_state_rect_Type3 ge h_mk_RTLabs_ext_state x_ 17323=167 let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_ 17323in166 let rec rTLabs_ext_state_rect_Type3 ge h_mk_RTLabs_ext_state x_345 = 167 let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_345 in 168 168 h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __ 169 169 … … 171 171 RTLabs_semantics.genv > (RTLabs_semantics.state > Pointers.block 172 172 List.list > __ > 'a1) > rTLabs_ext_state > 'a1 **) 173 let rec rTLabs_ext_state_rect_Type2 ge h_mk_RTLabs_ext_state x_ 17325=174 let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_ 17325in173 let rec rTLabs_ext_state_rect_Type2 ge h_mk_RTLabs_ext_state x_347 = 174 let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_347 in 175 175 h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __ 176 176 … … 178 178 RTLabs_semantics.genv > (RTLabs_semantics.state > Pointers.block 179 179 List.list > __ > 'a1) > rTLabs_ext_state > 'a1 **) 180 let rec rTLabs_ext_state_rect_Type1 ge h_mk_RTLabs_ext_state x_ 17327=181 let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_ 17327in180 let rec rTLabs_ext_state_rect_Type1 ge h_mk_RTLabs_ext_state x_349 = 181 let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_349 in 182 182 h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __ 183 183 … … 185 185 RTLabs_semantics.genv > (RTLabs_semantics.state > Pointers.block 186 186 List.list > __ > 'a1) > rTLabs_ext_state > 'a1 **) 187 let rec rTLabs_ext_state_rect_Type0 ge h_mk_RTLabs_ext_state x_ 17329=188 let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_ 17329in187 let rec rTLabs_ext_state_rect_Type0 ge h_mk_RTLabs_ext_state x_351 = 188 let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_351 in 189 189 h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __ 190 190 … … 340 340 rTLabs_pc > 'a1 **) 341 341 let rec rTLabs_pc_rect_Type4 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function 342  Rapc_state (x_ 17355, x_17354) > h_rapc_state x_17355 x_17354343  Rapc_call (x_ 17357, x_17356) > h_rapc_call x_17357 x_17356344  Rapc_ret x_ 17358 > h_rapc_ret x_17358342  Rapc_state (x_377, x_376) > h_rapc_state x_377 x_376 343  Rapc_call (x_379, x_378) > h_rapc_call x_379 x_378 344  Rapc_ret x_380 > h_rapc_ret x_380 345 345  Rapc_fin > h_rapc_fin 346 346 … … 350 350 rTLabs_pc > 'a1 **) 351 351 let rec rTLabs_pc_rect_Type5 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function 352  Rapc_state (x_ 17365, x_17364) > h_rapc_state x_17365 x_17364353  Rapc_call (x_ 17367, x_17366) > h_rapc_call x_17367 x_17366354  Rapc_ret x_ 17368 > h_rapc_ret x_17368352  Rapc_state (x_387, x_386) > h_rapc_state x_387 x_386 353  Rapc_call (x_389, x_388) > h_rapc_call x_389 x_388 354  Rapc_ret x_390 > h_rapc_ret x_390 355 355  Rapc_fin > h_rapc_fin 356 356 … … 360 360 rTLabs_pc > 'a1 **) 361 361 let rec rTLabs_pc_rect_Type3 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function 362  Rapc_state (x_ 17375, x_17374) > h_rapc_state x_17375 x_17374363  Rapc_call (x_ 17377, x_17376) > h_rapc_call x_17377 x_17376364  Rapc_ret x_ 17378 > h_rapc_ret x_17378362  Rapc_state (x_397, x_396) > h_rapc_state x_397 x_396 363  Rapc_call (x_399, x_398) > h_rapc_call x_399 x_398 364  Rapc_ret x_400 > h_rapc_ret x_400 365 365  Rapc_fin > h_rapc_fin 366 366 … … 370 370 rTLabs_pc > 'a1 **) 371 371 let rec rTLabs_pc_rect_Type2 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function 372  Rapc_state (x_ 17385, x_17384) > h_rapc_state x_17385 x_17384373  Rapc_call (x_ 17387, x_17386) > h_rapc_call x_17387 x_17386374  Rapc_ret x_ 17388 > h_rapc_ret x_17388372  Rapc_state (x_407, x_406) > h_rapc_state x_407 x_406 373  Rapc_call (x_409, x_408) > h_rapc_call x_409 x_408 374  Rapc_ret x_410 > h_rapc_ret x_410 375 375  Rapc_fin > h_rapc_fin 376 376 … … 380 380 rTLabs_pc > 'a1 **) 381 381 let rec rTLabs_pc_rect_Type1 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function 382  Rapc_state (x_ 17395, x_17394) > h_rapc_state x_17395 x_17394383  Rapc_call (x_ 17397, x_17396) > h_rapc_call x_17397 x_17396384  Rapc_ret x_ 17398 > h_rapc_ret x_17398382  Rapc_state (x_417, x_416) > h_rapc_state x_417 x_416 383  Rapc_call (x_419, x_418) > h_rapc_call x_419 x_418 384  Rapc_ret x_420 > h_rapc_ret x_420 385 385  Rapc_fin > h_rapc_fin 386 386 … … 390 390 rTLabs_pc > 'a1 **) 391 391 let rec rTLabs_pc_rect_Type0 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function 392  Rapc_state (x_ 17405, x_17404) > h_rapc_state x_17405 x_17404393  Rapc_call (x_ 17407, x_17406) > h_rapc_call x_17407 x_17406394  Rapc_ret x_ 17408 > h_rapc_ret x_17408392  Rapc_state (x_427, x_426) > h_rapc_state x_427 x_426 393  Rapc_call (x_429, x_428) > h_rapc_call x_429 x_428 394  Rapc_ret x_430 > h_rapc_ret x_430 395 395  Rapc_fin > h_rapc_fin 396 396 
extracted/rTLabs_semantics.ml
r2797 r2812 128 128 Graphs.label > __ > Pointers.block > Registers.register Types.option 129 129 > 'a1) > frame > 'a1 **) 130 let rec frame_rect_Type4 h_mk_frame x_ 16011=130 let rec frame_rect_Type4 h_mk_frame x_3 = 131 131 let { func = func0; locals = locals0; next = next0; sp = sp0; retdst = 132 retdst0 } = x_ 16011132 retdst0 } = x_3 133 133 in 134 134 h_mk_frame func0 locals0 next0 __ sp0 retdst0 … … 138 138 Graphs.label > __ > Pointers.block > Registers.register Types.option 139 139 > 'a1) > frame > 'a1 **) 140 let rec frame_rect_Type5 h_mk_frame x_ 16013=140 let rec frame_rect_Type5 h_mk_frame x_5 = 141 141 let { func = func0; locals = locals0; next = next0; sp = sp0; retdst = 142 retdst0 } = x_ 16013142 retdst0 } = x_5 143 143 in 144 144 h_mk_frame func0 locals0 next0 __ sp0 retdst0 … … 148 148 Graphs.label > __ > Pointers.block > Registers.register Types.option 149 149 > 'a1) > frame > 'a1 **) 150 let rec frame_rect_Type3 h_mk_frame x_ 16015=150 let rec frame_rect_Type3 h_mk_frame x_7 = 151 151 let { func = func0; locals = locals0; next = next0; sp = sp0; retdst = 152 retdst0 } = x_ 16015152 retdst0 } = x_7 153 153 in 154 154 h_mk_frame func0 locals0 next0 __ sp0 retdst0 … … 158 158 Graphs.label > __ > Pointers.block > Registers.register Types.option 159 159 > 'a1) > frame > 'a1 **) 160 let rec frame_rect_Type2 h_mk_frame x_ 16017=160 let rec frame_rect_Type2 h_mk_frame x_9 = 161 161 let { func = func0; locals = locals0; next = next0; sp = sp0; retdst = 162 retdst0 } = x_ 16017162 retdst0 } = x_9 163 163 in 164 164 h_mk_frame func0 locals0 next0 __ sp0 retdst0 … … 168 168 Graphs.label > __ > Pointers.block > Registers.register Types.option 169 169 > 'a1) > frame > 'a1 **) 170 let rec frame_rect_Type1 h_mk_frame x_1 6019=170 let rec frame_rect_Type1 h_mk_frame x_11 = 171 171 let { func = func0; locals = locals0; next = next0; sp = sp0; retdst = 172 retdst0 } = x_1 6019172 retdst0 } = x_11 173 173 in 174 174 h_mk_frame func0 locals0 next0 __ sp0 retdst0 … … 178 178 Graphs.label > __ > Pointers.block > Registers.register Types.option 179 179 > 'a1) > frame > 'a1 **) 180 let rec frame_rect_Type0 h_mk_frame x_1 6021=180 let rec frame_rect_Type0 h_mk_frame x_13 = 181 181 let { func = func0; locals = locals0; next = next0; sp = sp0; retdst = 182 retdst0 } = x_1 6021182 retdst0 } = x_13 183 183 in 184 184 h_mk_frame func0 locals0 next0 __ sp0 retdst0 … … 632 632 (Obj.magic 633 633 (IOMonad.err_to_io 634 (IO.check_eventval_list params fn.AST.ef_sig.AST.sig_args)))634 (IO.check_eventval_list params (AST.sig_args (AST.ef_sig fn))))) 635 635 (fun evargs > 636 636 Monad.m_bind0 (Monad.max_def IOMonad.iOMonad) 637 637 (Obj.magic 638 (IO.do_io fn.AST.ef_id evargs (AST.proj_sig_res fn.AST.ef_sig)))639 (fun evres >638 (IO.do_io (AST.ef_id fn) evargs 639 (AST.proj_sig_res (AST.ef_sig fn)))) (fun evres > 640 640 Monad.m_return0 (Monad.max_def IOMonad.iOMonad) { Types.fst = 641 (Events.eextcall fn.AST.ef_idevargs642 (IO.mk_eventval (AST.proj_sig_res fn.AST.ef_sig) evres));641 (Events.eextcall (AST.ef_id fn) evargs 642 (IO.mk_eventval (AST.proj_sig_res (AST.ef_sig fn)) evres)); 643 643 Types.snd = (Returnstate ((Types.Some 644 (IO.mk_val (AST.proj_sig_res fn.AST.ef_sig) evres)), dst, fs,644 (IO.mk_val (AST.proj_sig_res (AST.ef_sig fn)) evres)), dst, fs, 645 645 m)) })))) 646 646  Returnstate (v, dst, fs, m) > … … 735 735 (Globalenvs.init_mem (fun x > List.Cons ((AST.Init_space x), 736 736 List.Nil)) p)) (fun m > 737 let main = p.AST.prog_mainin737 let main = AST.prog_main p in 738 738 Monad.m_bind0 (Monad.max_def Errors.res0) 739 739 (Obj.magic … … 1562 1562 IOMonad.bindIO_value 1563 1563 (IOMonad.err_to_io 1564 (IO.check_eventval_list args0 fn.AST.ef_sig.AST.sig_args))1564 (IO.check_eventval_list args0 (AST.sig_args (AST.ef_sig fn)))) 1565 1565 (fun evargs > 1566 1566 Obj.magic 1567 1567 (Monad.m_bind0 (Monad.max_def IOMonad.iOMonad) 1568 1568 (Obj.magic 1569 (IO.do_io fn.AST.ef_idevargs1570 (AST.proj_sig_res fn.AST.ef_sig))) (fun evres >1569 (IO.do_io (AST.ef_id fn) evargs 1570 (AST.proj_sig_res (AST.ef_sig fn)))) (fun evres > 1571 1571 Monad.m_return0 (Monad.max_def IOMonad.iOMonad) { Types.fst = 1572 (Events.eextcall fn.AST.ef_idevargs1573 (IO.mk_eventval (AST.proj_sig_res fn.AST.ef_sig) evres));1572 (Events.eextcall (AST.ef_id fn) evargs 1573 (IO.mk_eventval (AST.proj_sig_res (AST.ef_sig fn)) evres)); 1574 1574 Types.snd = (Returnstate ((Types.Some 1575 (IO.mk_val (AST.proj_sig_res fn.AST.ef_sig) evres)),1575 (IO.mk_val (AST.proj_sig_res (AST.ef_sig fn)) evres)), 1576 1576 retdst0, stk, m0)) }))) { Types.fst = tr; Types.snd = 1577 1577 (Callstate (vf', fd', args', dst', fs', m')) } (fun evargs _ _ > 1578 1578 Obj.magic IOMonad.iO_discr (IOMonad.Interact ({ IO.io_function = 1579 fn.AST.ef_id; IO.io_args = evargs; IO.io_in_typ =1580 (AST.proj_sig_res fn.AST.ef_sig) }, (fun res >1579 (AST.ef_id fn); IO.io_args = evargs; IO.io_in_typ = 1580 (AST.proj_sig_res (AST.ef_sig fn)) }, (fun res > 1581 1581 IOMonad.bindIO (IOMonad.Value res) (fun evres > 1582 1582 Obj.magic 1583 1583 (Monad.m_return0 (Monad.max_def IOMonad.iOMonad) 1584 1584 { Types.fst = 1585 (Events.eextcall fn.AST.ef_idevargs1586 (IO.mk_eventval (AST.proj_sig_res fn.AST.ef_sig) evres));1587 Types.snd = (Returnstate ((Types.Some1588 (IO.mk_val (AST.proj_sig_res fn.AST.ef_sig) evres)),1585 (Events.eextcall (AST.ef_id fn) evargs 1586 (IO.mk_eventval (AST.proj_sig_res (AST.ef_sig fn)) 1587 evres)); Types.snd = (Returnstate ((Types.Some 1588 (IO.mk_val (AST.proj_sig_res (AST.ef_sig fn)) evres)), 1589 1589 retdst0, stk, m0)) }))))) (IOMonad.Value { Types.fst = 1590 1590 tr; Types.snd = (Callstate (vf', fd', args', dst', fs', m')) })
Note: See TracChangeset
for help on using the changeset viewer.