Changeset 3001 for extracted/rTL.ml


Ignore:
Timestamp:
Mar 28, 2013, 1:02:48 PM (7 years ago)
Author:
sacerdot
Message:

New extraction.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/rTL.ml

    r2977 r3001  
    125125    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    126126let rec rtl_seq_rect_Type4 h_rtl_stack_address = function
    127 | Rtl_stack_address (x_1495, x_1494) -> h_rtl_stack_address x_1495 x_1494
     127| Rtl_stack_address (x_5953, x_5952) -> h_rtl_stack_address x_5953 x_5952
    128128
    129129(** val rtl_seq_rect_Type5 :
    130130    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    131131let rec rtl_seq_rect_Type5 h_rtl_stack_address = function
    132 | Rtl_stack_address (x_1499, x_1498) -> h_rtl_stack_address x_1499 x_1498
     132| Rtl_stack_address (x_5957, x_5956) -> h_rtl_stack_address x_5957 x_5956
    133133
    134134(** val rtl_seq_rect_Type3 :
    135135    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    136136let rec rtl_seq_rect_Type3 h_rtl_stack_address = function
    137 | Rtl_stack_address (x_1503, x_1502) -> h_rtl_stack_address x_1503 x_1502
     137| Rtl_stack_address (x_5961, x_5960) -> h_rtl_stack_address x_5961 x_5960
    138138
    139139(** val rtl_seq_rect_Type2 :
    140140    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    141141let rec rtl_seq_rect_Type2 h_rtl_stack_address = function
    142 | Rtl_stack_address (x_1507, x_1506) -> h_rtl_stack_address x_1507 x_1506
     142| Rtl_stack_address (x_5965, x_5964) -> h_rtl_stack_address x_5965 x_5964
    143143
    144144(** val rtl_seq_rect_Type1 :
    145145    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    146146let rec rtl_seq_rect_Type1 h_rtl_stack_address = function
    147 | Rtl_stack_address (x_1511, x_1510) -> h_rtl_stack_address x_1511 x_1510
     147| Rtl_stack_address (x_5969, x_5968) -> h_rtl_stack_address x_5969 x_5968
    148148
    149149(** val rtl_seq_rect_Type0 :
    150150    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    151151let rec rtl_seq_rect_Type0 h_rtl_stack_address = function
    152 | Rtl_stack_address (x_1515, x_1514) -> h_rtl_stack_address x_1515 x_1514
     152| Rtl_stack_address (x_5973, x_5972) -> h_rtl_stack_address x_5973 x_5972
    153153
    154154(** val rtl_seq_inv_rect_Type4 :
     
    312312    Joint.add_graph rTL (AST.prog_var_names p.Joint.joint_prog) l2
    313313      (Joint.Sequential ((Joint.CALL ((Types.Inl
    314       p.Joint.joint_prog.AST.prog_main), (Obj.magic List.Nil),
     314      (AST.prog_main p.Joint.joint_prog)), (Obj.magic List.Nil),
    315315      (Obj.magic rs))), (Obj.magic l3))) res0
    316316  in
Note: See TracChangeset for help on using the changeset viewer.