Changeset 2960 for extracted/eRTL.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/eRTL.ml

    r2951 r2960  
    126126    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    127127let rec move_dst_rect_Type4 h_PSD h_HDW = function
    128 | PSD x_18520 -> h_PSD x_18520
    129 | HDW x_18521 -> h_HDW x_18521
     128| PSD x_7 -> h_PSD x_7
     129| HDW x_8 -> h_HDW x_8
    130130
    131131(** val move_dst_rect_Type5 :
    132132    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    133133let rec move_dst_rect_Type5 h_PSD h_HDW = function
    134 | PSD x_18525 -> h_PSD x_18525
    135 | HDW x_18526 -> h_HDW x_18526
     134| PSD x_12 -> h_PSD x_12
     135| HDW x_13 -> h_HDW x_13
    136136
    137137(** val move_dst_rect_Type3 :
    138138    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    139139let rec move_dst_rect_Type3 h_PSD h_HDW = function
    140 | PSD x_18530 -> h_PSD x_18530
    141 | HDW x_18531 -> h_HDW x_18531
     140| PSD x_17 -> h_PSD x_17
     141| HDW x_18 -> h_HDW x_18
    142142
    143143(** val move_dst_rect_Type2 :
    144144    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    145145let rec move_dst_rect_Type2 h_PSD h_HDW = function
    146 | PSD x_18535 -> h_PSD x_18535
    147 | HDW x_18536 -> h_HDW x_18536
     146| PSD x_22 -> h_PSD x_22
     147| HDW x_23 -> h_HDW x_23
    148148
    149149(** val move_dst_rect_Type1 :
    150150    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    151151let rec move_dst_rect_Type1 h_PSD h_HDW = function
    152 | PSD x_18540 -> h_PSD x_18540
    153 | HDW x_18541 -> h_HDW x_18541
     152| PSD x_27 -> h_PSD x_27
     153| HDW x_28 -> h_HDW x_28
    154154
    155155(** val move_dst_rect_Type0 :
    156156    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    157157let rec move_dst_rect_Type0 h_PSD h_HDW = function
    158 | PSD x_18545 -> h_PSD x_18545
    159 | HDW x_18546 -> h_HDW x_18546
     158| PSD x_32 -> h_PSD x_32
     159| HDW x_33 -> h_HDW x_33
    160160
    161161(** val move_dst_inv_rect_Type4 :
     
    352352| Ertl_new_frame -> h_ertl_new_frame
    353353| Ertl_del_frame -> h_ertl_del_frame
    354 | Ertl_frame_size x_18585 -> h_ertl_frame_size x_18585
     354| Ertl_frame_size x_72 -> h_ertl_frame_size x_72
    355355
    356356(** val ertl_seq_rect_Type5 :
     
    359359| Ertl_new_frame -> h_ertl_new_frame
    360360| Ertl_del_frame -> h_ertl_del_frame
    361 | Ertl_frame_size x_18590 -> h_ertl_frame_size x_18590
     361| Ertl_frame_size x_77 -> h_ertl_frame_size x_77
    362362
    363363(** val ertl_seq_rect_Type3 :
     
    366366| Ertl_new_frame -> h_ertl_new_frame
    367367| Ertl_del_frame -> h_ertl_del_frame
    368 | Ertl_frame_size x_18595 -> h_ertl_frame_size x_18595
     368| Ertl_frame_size x_82 -> h_ertl_frame_size x_82
    369369
    370370(** val ertl_seq_rect_Type2 :
     
    373373| Ertl_new_frame -> h_ertl_new_frame
    374374| Ertl_del_frame -> h_ertl_del_frame
    375 | Ertl_frame_size x_18600 -> h_ertl_frame_size x_18600
     375| Ertl_frame_size x_87 -> h_ertl_frame_size x_87
    376376
    377377(** val ertl_seq_rect_Type1 :
     
    380380| Ertl_new_frame -> h_ertl_new_frame
    381381| Ertl_del_frame -> h_ertl_del_frame
    382 | Ertl_frame_size x_18605 -> h_ertl_frame_size x_18605
     382| Ertl_frame_size x_92 -> h_ertl_frame_size x_92
    383383
    384384(** val ertl_seq_rect_Type0 :
     
    387387| Ertl_new_frame -> h_ertl_new_frame
    388388| Ertl_del_frame -> h_ertl_del_frame
    389 | Ertl_frame_size x_18610 -> h_ertl_frame_size x_18610
     389| Ertl_frame_size x_97 -> h_ertl_frame_size x_97
    390390
    391391(** val ertl_seq_inv_rect_Type4 :
     
    697697    Joint.add_graph eRTL (AST.prog_var_names p.Joint.joint_prog) l2
    698698      (Joint.Sequential ((Joint.CALL ((Types.Inl
    699       p.Joint.joint_prog.AST.prog_main),
    700       (Obj.magic (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
     699      p.Joint.joint_prog.AST.prog_main), (Obj.magic Nat.O),
    701700      (Obj.magic Types.It))), (Obj.magic l3))) res0
    702701  in
Note: See TracChangeset for help on using the changeset viewer.