Ignore:
Timestamp:
Mar 14, 2013, 10:37:39 PM (8 years ago)
Author:
sacerdot
Message:

Extracted again.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/joint_LTL_LIN.ml

    r2867 r2873  
    116116    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    117117let rec registers_move_rect_Type4 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    118 | From_acc (x_21503, x_21502) -> h_from_acc x_21503 x_21502
    119 | To_acc (x_21505, x_21504) -> h_to_acc x_21505 x_21504
    120 | Int_to_reg (x_21507, x_21506) -> h_int_to_reg x_21507 x_21506
    121 | Int_to_acc (x_21509, x_21508) -> h_int_to_acc x_21509 x_21508
     118| From_acc (x_21672, x_21671) -> h_from_acc x_21672 x_21671
     119| To_acc (x_21674, x_21673) -> h_to_acc x_21674 x_21673
     120| Int_to_reg (x_21676, x_21675) -> h_int_to_reg x_21676 x_21675
     121| Int_to_acc (x_21678, x_21677) -> h_int_to_acc x_21678 x_21677
    122122
    123123(** val registers_move_rect_Type5 :
     
    126126    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    127127let rec registers_move_rect_Type5 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    128 | From_acc (x_21516, x_21515) -> h_from_acc x_21516 x_21515
    129 | To_acc (x_21518, x_21517) -> h_to_acc x_21518 x_21517
    130 | Int_to_reg (x_21520, x_21519) -> h_int_to_reg x_21520 x_21519
    131 | Int_to_acc (x_21522, x_21521) -> h_int_to_acc x_21522 x_21521
     128| From_acc (x_21685, x_21684) -> h_from_acc x_21685 x_21684
     129| To_acc (x_21687, x_21686) -> h_to_acc x_21687 x_21686
     130| Int_to_reg (x_21689, x_21688) -> h_int_to_reg x_21689 x_21688
     131| Int_to_acc (x_21691, x_21690) -> h_int_to_acc x_21691 x_21690
    132132
    133133(** val registers_move_rect_Type3 :
     
    136136    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    137137let rec registers_move_rect_Type3 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    138 | From_acc (x_21529, x_21528) -> h_from_acc x_21529 x_21528
    139 | To_acc (x_21531, x_21530) -> h_to_acc x_21531 x_21530
    140 | Int_to_reg (x_21533, x_21532) -> h_int_to_reg x_21533 x_21532
    141 | Int_to_acc (x_21535, x_21534) -> h_int_to_acc x_21535 x_21534
     138| From_acc (x_21698, x_21697) -> h_from_acc x_21698 x_21697
     139| To_acc (x_21700, x_21699) -> h_to_acc x_21700 x_21699
     140| Int_to_reg (x_21702, x_21701) -> h_int_to_reg x_21702 x_21701
     141| Int_to_acc (x_21704, x_21703) -> h_int_to_acc x_21704 x_21703
    142142
    143143(** val registers_move_rect_Type2 :
     
    146146    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    147147let rec registers_move_rect_Type2 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    148 | From_acc (x_21542, x_21541) -> h_from_acc x_21542 x_21541
    149 | To_acc (x_21544, x_21543) -> h_to_acc x_21544 x_21543
    150 | Int_to_reg (x_21546, x_21545) -> h_int_to_reg x_21546 x_21545
    151 | Int_to_acc (x_21548, x_21547) -> h_int_to_acc x_21548 x_21547
     148| From_acc (x_21711, x_21710) -> h_from_acc x_21711 x_21710
     149| To_acc (x_21713, x_21712) -> h_to_acc x_21713 x_21712
     150| Int_to_reg (x_21715, x_21714) -> h_int_to_reg x_21715 x_21714
     151| Int_to_acc (x_21717, x_21716) -> h_int_to_acc x_21717 x_21716
    152152
    153153(** val registers_move_rect_Type1 :
     
    156156    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    157157let rec registers_move_rect_Type1 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    158 | From_acc (x_21555, x_21554) -> h_from_acc x_21555 x_21554
    159 | To_acc (x_21557, x_21556) -> h_to_acc x_21557 x_21556
    160 | Int_to_reg (x_21559, x_21558) -> h_int_to_reg x_21559 x_21558
    161 | Int_to_acc (x_21561, x_21560) -> h_int_to_acc x_21561 x_21560
     158| From_acc (x_21724, x_21723) -> h_from_acc x_21724 x_21723
     159| To_acc (x_21726, x_21725) -> h_to_acc x_21726 x_21725
     160| Int_to_reg (x_21728, x_21727) -> h_int_to_reg x_21728 x_21727
     161| Int_to_acc (x_21730, x_21729) -> h_int_to_acc x_21730 x_21729
    162162
    163163(** val registers_move_rect_Type0 :
     
    166166    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    167167let rec registers_move_rect_Type0 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    168 | From_acc (x_21568, x_21567) -> h_from_acc x_21568 x_21567
    169 | To_acc (x_21570, x_21569) -> h_to_acc x_21570 x_21569
    170 | Int_to_reg (x_21572, x_21571) -> h_int_to_reg x_21572 x_21571
    171 | Int_to_acc (x_21574, x_21573) -> h_int_to_acc x_21574 x_21573
     168| From_acc (x_21737, x_21736) -> h_from_acc x_21737 x_21736
     169| To_acc (x_21739, x_21738) -> h_to_acc x_21739 x_21738
     170| Int_to_reg (x_21741, x_21740) -> h_int_to_reg x_21741 x_21740
     171| Int_to_acc (x_21743, x_21742) -> h_int_to_acc x_21743 x_21742
    172172
    173173(** val registers_move_inv_rect_Type4 :
     
    241241| SAVE_CARRY -> h_SAVE_CARRY
    242242| RESTORE_CARRY -> h_RESTORE_CARRY
    243 | LOW_ADDRESS (x_21668, x_21667) -> h_LOW_ADDRESS x_21668 x_21667
    244 | HIGH_ADDRESS (x_21670, x_21669) -> h_HIGH_ADDRESS x_21670 x_21669
     243| LOW_ADDRESS (x_21837, x_21836) -> h_LOW_ADDRESS x_21837 x_21836
     244| HIGH_ADDRESS (x_21839, x_21838) -> h_HIGH_ADDRESS x_21839 x_21838
    245245
    246246(** val ltl_lin_seq_rect_Type5 :
     
    250250| SAVE_CARRY -> h_SAVE_CARRY
    251251| RESTORE_CARRY -> h_RESTORE_CARRY
    252 | LOW_ADDRESS (x_21677, x_21676) -> h_LOW_ADDRESS x_21677 x_21676
    253 | HIGH_ADDRESS (x_21679, x_21678) -> h_HIGH_ADDRESS x_21679 x_21678
     252| LOW_ADDRESS (x_21846, x_21845) -> h_LOW_ADDRESS x_21846 x_21845
     253| HIGH_ADDRESS (x_21848, x_21847) -> h_HIGH_ADDRESS x_21848 x_21847
    254254
    255255(** val ltl_lin_seq_rect_Type3 :
     
    259259| SAVE_CARRY -> h_SAVE_CARRY
    260260| RESTORE_CARRY -> h_RESTORE_CARRY
    261 | LOW_ADDRESS (x_21686, x_21685) -> h_LOW_ADDRESS x_21686 x_21685
    262 | HIGH_ADDRESS (x_21688, x_21687) -> h_HIGH_ADDRESS x_21688 x_21687
     261| LOW_ADDRESS (x_21855, x_21854) -> h_LOW_ADDRESS x_21855 x_21854
     262| HIGH_ADDRESS (x_21857, x_21856) -> h_HIGH_ADDRESS x_21857 x_21856
    263263
    264264(** val ltl_lin_seq_rect_Type2 :
     
    268268| SAVE_CARRY -> h_SAVE_CARRY
    269269| RESTORE_CARRY -> h_RESTORE_CARRY
    270 | LOW_ADDRESS (x_21695, x_21694) -> h_LOW_ADDRESS x_21695 x_21694
    271 | HIGH_ADDRESS (x_21697, x_21696) -> h_HIGH_ADDRESS x_21697 x_21696
     270| LOW_ADDRESS (x_21864, x_21863) -> h_LOW_ADDRESS x_21864 x_21863
     271| HIGH_ADDRESS (x_21866, x_21865) -> h_HIGH_ADDRESS x_21866 x_21865
    272272
    273273(** val ltl_lin_seq_rect_Type1 :
     
    277277| SAVE_CARRY -> h_SAVE_CARRY
    278278| RESTORE_CARRY -> h_RESTORE_CARRY
    279 | LOW_ADDRESS (x_21704, x_21703) -> h_LOW_ADDRESS x_21704 x_21703
    280 | HIGH_ADDRESS (x_21706, x_21705) -> h_HIGH_ADDRESS x_21706 x_21705
     279| LOW_ADDRESS (x_21873, x_21872) -> h_LOW_ADDRESS x_21873 x_21872
     280| HIGH_ADDRESS (x_21875, x_21874) -> h_HIGH_ADDRESS x_21875 x_21874
    281281
    282282(** val ltl_lin_seq_rect_Type0 :
     
    286286| SAVE_CARRY -> h_SAVE_CARRY
    287287| RESTORE_CARRY -> h_RESTORE_CARRY
    288 | LOW_ADDRESS (x_21713, x_21712) -> h_LOW_ADDRESS x_21713 x_21712
    289 | HIGH_ADDRESS (x_21715, x_21714) -> h_HIGH_ADDRESS x_21715 x_21714
     288| LOW_ADDRESS (x_21882, x_21881) -> h_LOW_ADDRESS x_21882 x_21881
     289| HIGH_ADDRESS (x_21884, x_21883) -> h_HIGH_ADDRESS x_21884 x_21883
    290290
    291291(** val ltl_lin_seq_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.