source: Deliverables/D2.2/8051/src/LTL/branch.mli @ 486

Last change on this file since 486 was 486, checked in by ayache, 8 years ago

Deliverable D2.2

File size: 621 bytes
2(** This module optimizes [LTL] code by suppressing all empty
3    statements. *)
5(* Pasted from Pottier's PP compiler *)
7(* This module optimizes [LTL] code by suppressing all [St_skip] statements. In
8   short, every statement whose successor is a [St_skip] statement is modified
9   so that its successor is the successor of the [St_skip] statement, and this
10   is repeated until no reachable [St_skip] statements remain. Unreachable
11   [St_skip] statements remain in the graph, but will be implicitly eliminated
12   in the translation of [LTL] to [LIN]. *)
14val compress: Label.t -> LTL.graph -> (Label.t * LTL.graph)
Note: See TracBrowser for help on using the repository browser.