Changeset 3263 for src/joint/Joint.ma
 Timestamp:
 May 10, 2013, 1:40:31 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/Joint.ma
r3145 r3263 481 481 joint_if_result : call_dest p; 482 482 joint_if_params : paramsT p; 483 joint_if_stacksize: nat;484 483 joint_if_local_stacksize: nat; (* size of the stack devoted to "forced" stack positions 485 484 (that are already on stack in the front end) *) 485 joint_if_params_stacksize: nat; (* size of the stack devoted to parameters *) 486 joint_if_spilled_stacksize: nat; (* size of the stack devoted to spilled registers *) 486 487 joint_if_code : codeT p globals ; 487 488 joint_if_entry : code_point p (* Paolo: condition entry ∈ code is ensured by good_if ; 488 489 joint_if_exit : Σpt.bool_to_Prop (code_has_point … joint_if_code pt) *) 489 490 }. 491 492 definition joint_if_stacksize ≝ λp,globals,fn. 493 joint_if_spilled_stacksize p globals fn + joint_if_params_stacksize … fn + 494 joint_if_local_stacksize … fn. 490 495 491 496 definition regs_in_universe : ∀p,globals. … … 560 565 (joint_if_params … int_fun) (joint_if_stacksize … int_fun) 561 566 (joint_if_local_stacksize … int_fun) 567 (joint_if_params_stacksize … int_fun) 562 568 graph entry (*exit*). 563 569 … … 569 575 luniverse (joint_if_runiverse … p) (joint_if_result … p) 570 576 (joint_if_params … p) (joint_if_stacksize … p) (joint_if_local_stacksize … p) 577 (joint_if_params_stacksize … p) 571 578 (joint_if_code … p) (joint_if_entry … p) (*(joint_if_exit … p)*). 572 579 … … 578 585 (joint_if_luniverse … p) runiverse (joint_if_result … p) 579 586 (joint_if_params … p) (joint_if_stacksize … p) (joint_if_local_stacksize … p) 587 (joint_if_params_stacksize … p) 580 588 (joint_if_code … p) (joint_if_entry … p) (*(joint_if_exit … p)*). 581 589 … … 588 596 (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p) 589 597 (joint_if_params … p) (joint_if_stacksize … p) (joint_if_local_stacksize … p) 598 (joint_if_params_stacksize … p) 590 599 code 591 600 (joint_if_entry … p)
Note: See TracChangeset
for help on using the changeset viewer.