Changeset 2681 for src/ERTL/liveness.ma


Ignore:
Timestamp:
Feb 19, 2013, 6:48:32 PM (7 years ago)
Author:
tranquil
Message:
  • improvements to the graph translation function
  • fixed passes up to LTL
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/liveness.ma

    r2490 r2681  
    8383        ]
    8484      (* Potentially destroys all caller-save hardware registers. *)
    85       | CALL _ _ _ ⇒ 〈set_empty …, set_from_list … RegisterCallerSaved〉
    8685      ]
     86    | CALL _ _ _ ⇒ 〈set_empty …, set_from_list … RegisterCallerSaved〉
    8787    | COND r lbl_true ⇒ rl_bottom
    8888    ]
    8989  | final _ ⇒ rl_bottom
     90  | FCOND abs _ _ _ ⇒ Ⓧabs
    9091  ].
    9192
     
    138139        ]
    139140      (* Reads the hardware registers that are used to pass parameters. *)
    140       | CALL _ nparams _ ⇒ 〈set_empty …, set_from_list … (prefix ? nparams RegisterParams)〉
    141141      | _ ⇒ rl_bottom
    142142      ]
     143    | CALL _ nparams _ ⇒ 〈set_empty …, set_from_list … (prefix ? nparams RegisterParams)〉
    143144    | COND r lbl_true ⇒ rl_psingleton r
    144145    ]
     
    149150    | TAILCALL abs _ _ ⇒ match abs in False with [ ]
    150151    ]
     152  | FCOND abs _ _ _ ⇒ Ⓧabs
    151153  ].
    152154
     
    218220      | _ ⇒ None ?
    219221      ]
    220     | COND _ _ ⇒ None ?
     222    | _ ⇒ None ?
    221223    ]
    222224  | _ ⇒ None ?
Note: See TracChangeset for help on using the changeset viewer.