Changeset 2960 for extracted/rTL.ml


Ignore:
Timestamp:
Mar 26, 2013, 4:51:40 PM (7 years ago)
Author:
sacerdot
Message:

New extraction, it diverges in RTL execution now.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/rTL.ml

    r2951 r2960  
    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_18179, x_18178) -> h_rtl_stack_address x_18179 x_18178
     127| Rtl_stack_address (x_7, x_6) -> h_rtl_stack_address x_7 x_6
    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_18183, x_18182) -> h_rtl_stack_address x_18183 x_18182
     132| Rtl_stack_address (x_11, x_10) -> h_rtl_stack_address x_11 x_10
    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_18187, x_18186) -> h_rtl_stack_address x_18187 x_18186
     137| Rtl_stack_address (x_15, x_14) -> h_rtl_stack_address x_15 x_14
    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_18191, x_18190) -> h_rtl_stack_address x_18191 x_18190
     142| Rtl_stack_address (x_19, x_18) -> h_rtl_stack_address x_19 x_18
    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_18195, x_18194) -> h_rtl_stack_address x_18195 x_18194
     147| Rtl_stack_address (x_23, x_22) -> h_rtl_stack_address x_23 x_22
    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_18199, x_18198) -> h_rtl_stack_address x_18199 x_18198
     152| Rtl_stack_address (x_27, x_26) -> h_rtl_stack_address x_27 x_26
    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),
    315       (Obj.magic (List.map (fun x -> Joint.Reg x) rs)), (Obj.magic rs))),
    316       (Obj.magic l3))) res0
     314      p.Joint.joint_prog.AST.prog_main), (Obj.magic List.Nil),
     315      (Obj.magic List.Nil))), (Obj.magic l3))) res0
    317316  in
    318317  let res2 =
Note: See TracChangeset for help on using the changeset viewer.