Changeset 3014 for src/ERTL/uses.ma


Ignore:
Timestamp:
Mar 28, 2013, 4:58:26 PM (7 years ago)
Author:
tranquil
Message:

ERTL to ERTLptr pass suppressed (it introduced a bug in the later ERTLptr to LTL), and integrated in a single ERTToLTL pass like before

File:
1 moved

Legend:

Unmodified
Added
Removed
  • src/ERTL/uses.ma

    r3012 r3014  
    1313(**************************************************************************)
    1414
    15 include "ERTLptr/ERTLptr.ma".
     15include "ERTL/ERTL.ma".
    1616
    1717(* This file is used only by untrusted code. We write it in Matita to
     
    1919
    2020definition examine_internal:
    21  ∀globals. joint_internal_function ERTLptr globals →
     21 ∀globals. joint_internal_function ERTL globals →
    2222  identifier_map RegisterTag Pos ≝
    2323λglobals,fun.
     
    7070         | extension_seq s ⇒
    7171            match s with
    72             [ ertlptr_ertl s ⇒
    73                match s with
    74                [ ertl_new_frame ⇒ map
    75                | ertl_del_frame ⇒ map
    76                | ertl_frame_size r ⇒ incr r map ]
    77             | LOW_ADDRESS r _ ⇒ incr r map
    78             | HIGH_ADDRESS r _ ⇒ incr r map ]]]
     72             [ ertl_new_frame ⇒ map
     73             | ertl_del_frame ⇒ map
     74             | ertl_frame_size r ⇒ incr r map ]]]
    7975   | final _ ⇒ map
    80    | FCOND (abs : has_fcond ERTLptr) _ _ _ ⇒ Ⓧabs ]
     76   | FCOND (abs : has_fcond ERTL) _ _ _ ⇒ Ⓧabs ]
    8177 in
    8278 foldi … f (joint_if_code … fun) (empty_map …).
Note: See TracChangeset for help on using the changeset viewer.