Changeset 3019 for extracted/liveness.ml


Ignore:
Timestamp:
Mar 28, 2013, 5:27:46 PM (7 years ago)
Author:
sacerdot
Message:

New extraction after ERTLptr abortion.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/liveness.ml

    r3009 r3019  
    120120
    121121open ERTL
    122 
    123 open ERTLptr
    124122
    125123open Set_adt
     
    226224      | Joint.Extension_seq ext ->
    227225        (match Obj.magic ext with
    228          | ERTLptr.Ertlptr_ertl ext' ->
    229            (match ext' with
    230             | ERTL.Ertl_new_frame ->
    231               rl_join (rl_hsingleton I8051.registerSPL)
    232                 (rl_hsingleton I8051.registerSPH)
    233             | ERTL.Ertl_del_frame ->
    234               rl_join (rl_hsingleton I8051.registerSPL)
    235                 (rl_hsingleton I8051.registerSPH)
    236             | ERTL.Ertl_frame_size r -> rl_psingleton r)
    237          | ERTLptr.LOW_ADDRESS (r1, l0) -> rl_psingleton r1
    238          | ERTLptr.HIGH_ADDRESS (r1, l0) -> rl_psingleton r1)))
     226         | ERTL.Ertl_new_frame ->
     227           rl_join (rl_hsingleton I8051.registerSPL)
     228             (rl_hsingleton I8051.registerSPH)
     229         | ERTL.Ertl_del_frame ->
     230           rl_join (rl_hsingleton I8051.registerSPL)
     231             (rl_hsingleton I8051.registerSPH)
     232         | ERTL.Ertl_frame_size r -> rl_psingleton r)))
    239233| Joint.Final x -> rl_bottom
    240234| Joint.FCOND (x, x0, x1) -> assert false (* absurd case *)
     
    306300      | Joint.Extension_seq ext ->
    307301        (match Obj.magic ext with
    308          | ERTLptr.Ertlptr_ertl ext' ->
    309            (match ext' with
    310             | ERTL.Ertl_new_frame ->
    311               Obj.magic
    312                 (rl_join (rl_hsingleton I8051.registerSPL)
    313                   (rl_hsingleton I8051.registerSPH))
    314             | ERTL.Ertl_del_frame ->
    315               Obj.magic
    316                 (rl_join (rl_hsingleton I8051.registerSPL)
    317                   (rl_hsingleton I8051.registerSPH))
    318             | ERTL.Ertl_frame_size r -> Obj.magic rl_bottom)
    319          | ERTLptr.LOW_ADDRESS (r1, l0) -> Obj.magic rl_bottom
    320          | ERTLptr.HIGH_ADDRESS (r1, l0) -> Obj.magic rl_bottom)))
     302         | ERTL.Ertl_new_frame ->
     303           Obj.magic
     304             (rl_join (rl_hsingleton I8051.registerSPL)
     305               (rl_hsingleton I8051.registerSPH))
     306         | ERTL.Ertl_del_frame ->
     307           Obj.magic
     308             (rl_join (rl_hsingleton I8051.registerSPL)
     309               (rl_hsingleton I8051.registerSPH))
     310         | ERTL.Ertl_frame_size r -> Obj.magic rl_bottom)))
    321311| Joint.Final fin ->
    322312  (match fin with
     
    407397      | Joint.Extension_seq ext ->
    408398        (match Obj.magic ext with
    409          | ERTLptr.Ertlptr_ertl ext' ->
    410            (match ext' with
    411             | ERTL.Ertl_new_frame -> Bool.False
    412             | ERTL.Ertl_del_frame -> Bool.False
    413             | ERTL.Ertl_frame_size r ->
    414               Bool.notb
    415                 (Set_adt.set_member
    416                   (Identifiers.eq_identifier PreIdentifiers.RegisterTag) r
    417                   pliveafter))
    418          | ERTLptr.LOW_ADDRESS (r1, l') ->
     399         | ERTL.Ertl_new_frame -> Bool.False
     400         | ERTL.Ertl_del_frame -> Bool.False
     401         | ERTL.Ertl_frame_size r ->
    419402           Bool.notb
    420403             (Set_adt.set_member
    421                (Identifiers.eq_identifier PreIdentifiers.RegisterTag) r1
    422                pliveafter)
    423          | ERTLptr.HIGH_ADDRESS (r1, l') ->
    424            Bool.notb
    425              (Set_adt.set_member
    426                (Identifiers.eq_identifier PreIdentifiers.RegisterTag) r1
     404               (Identifiers.eq_identifier PreIdentifiers.RegisterTag) r
    427405               pliveafter))))
    428406
     
    465443    List.fold rl_join rl_bottom (fun successor -> Bool.True)
    466444      (fun successor -> livebefore globals int_fun liveafter0 successor)
    467       (Joint.stmt_labels { Joint.uns_pars = (Joint.g_u_pars ERTLptr.eRTLptr);
     445      (Joint.stmt_labels { Joint.uns_pars = (Joint.g_u_pars ERTL.eRTL);
    468446        Joint.succ_label = (Obj.magic (fun x -> Types.Some x));
    469447        Joint.has_fcond = Bool.False } globals stmt)
Note: See TracChangeset for help on using the changeset viewer.