src/ERTL/ERTLToLTL.mli

   1
   2 (** This module is the external part of the translation of [ERTL]
   3     programs into [LTL] programs. *)
   4
   5 (** The translation consists in the following operations:
   6     - Build an interference graph and color it. This process relies an a
   7       liveness analysis and allows to associate a physical location to each
   8       pseudo-register.
   9     - Do the actual translation by removing the statements whose written
  10       register is dead (using the results of the liveness analysis). *)
  11
  12 val translate : ERTL.program -> LTL.program