Ignore:
Timestamp:
Mar 13, 2013, 11:12:29 PM (7 years ago)
Author:
sacerdot
Message:

New extraction after indianess bug fixes by Paolo.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/joint_LTL_LIN.ml

    r2854 r2867  
    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_1508, x_1507) -> h_from_acc x_1508 x_1507
    119 | To_acc (x_1510, x_1509) -> h_to_acc x_1510 x_1509
    120 | Int_to_reg (x_1512, x_1511) -> h_int_to_reg x_1512 x_1511
    121 | Int_to_acc (x_1514, x_1513) -> h_int_to_acc x_1514 x_1513
     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
    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_1521, x_1520) -> h_from_acc x_1521 x_1520
    129 | To_acc (x_1523, x_1522) -> h_to_acc x_1523 x_1522
    130 | Int_to_reg (x_1525, x_1524) -> h_int_to_reg x_1525 x_1524
    131 | Int_to_acc (x_1527, x_1526) -> h_int_to_acc x_1527 x_1526
     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
    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_1534, x_1533) -> h_from_acc x_1534 x_1533
    139 | To_acc (x_1536, x_1535) -> h_to_acc x_1536 x_1535
    140 | Int_to_reg (x_1538, x_1537) -> h_int_to_reg x_1538 x_1537
    141 | Int_to_acc (x_1540, x_1539) -> h_int_to_acc x_1540 x_1539
     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
    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_1547, x_1546) -> h_from_acc x_1547 x_1546
    149 | To_acc (x_1549, x_1548) -> h_to_acc x_1549 x_1548
    150 | Int_to_reg (x_1551, x_1550) -> h_int_to_reg x_1551 x_1550
    151 | Int_to_acc (x_1553, x_1552) -> h_int_to_acc x_1553 x_1552
     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
    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_1560, x_1559) -> h_from_acc x_1560 x_1559
    159 | To_acc (x_1562, x_1561) -> h_to_acc x_1562 x_1561
    160 | Int_to_reg (x_1564, x_1563) -> h_int_to_reg x_1564 x_1563
    161 | Int_to_acc (x_1566, x_1565) -> h_int_to_acc x_1566 x_1565
     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
    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_1573, x_1572) -> h_from_acc x_1573 x_1572
    169 | To_acc (x_1575, x_1574) -> h_to_acc x_1575 x_1574
    170 | Int_to_reg (x_1577, x_1576) -> h_int_to_reg x_1577 x_1576
    171 | Int_to_acc (x_1579, x_1578) -> h_int_to_acc x_1579 x_1578
     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
    172172
    173173(** val registers_move_inv_rect_Type4 :
     
    241241| SAVE_CARRY -> h_SAVE_CARRY
    242242| RESTORE_CARRY -> h_RESTORE_CARRY
    243 | LOW_ADDRESS (x_1673, x_1672) -> h_LOW_ADDRESS x_1673 x_1672
    244 | HIGH_ADDRESS (x_1675, x_1674) -> h_HIGH_ADDRESS x_1675 x_1674
     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
    245245
    246246(** val ltl_lin_seq_rect_Type5 :
     
    250250| SAVE_CARRY -> h_SAVE_CARRY
    251251| RESTORE_CARRY -> h_RESTORE_CARRY
    252 | LOW_ADDRESS (x_1682, x_1681) -> h_LOW_ADDRESS x_1682 x_1681
    253 | HIGH_ADDRESS (x_1684, x_1683) -> h_HIGH_ADDRESS x_1684 x_1683
     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
    254254
    255255(** val ltl_lin_seq_rect_Type3 :
     
    259259| SAVE_CARRY -> h_SAVE_CARRY
    260260| RESTORE_CARRY -> h_RESTORE_CARRY
    261 | LOW_ADDRESS (x_1691, x_1690) -> h_LOW_ADDRESS x_1691 x_1690
    262 | HIGH_ADDRESS (x_1693, x_1692) -> h_HIGH_ADDRESS x_1693 x_1692
     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
    263263
    264264(** val ltl_lin_seq_rect_Type2 :
     
    268268| SAVE_CARRY -> h_SAVE_CARRY
    269269| RESTORE_CARRY -> h_RESTORE_CARRY
    270 | LOW_ADDRESS (x_1700, x_1699) -> h_LOW_ADDRESS x_1700 x_1699
    271 | HIGH_ADDRESS (x_1702, x_1701) -> h_HIGH_ADDRESS x_1702 x_1701
     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
    272272
    273273(** val ltl_lin_seq_rect_Type1 :
     
    277277| SAVE_CARRY -> h_SAVE_CARRY
    278278| RESTORE_CARRY -> h_RESTORE_CARRY
    279 | LOW_ADDRESS (x_1709, x_1708) -> h_LOW_ADDRESS x_1709 x_1708
    280 | HIGH_ADDRESS (x_1711, x_1710) -> h_HIGH_ADDRESS x_1711 x_1710
     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
    281281
    282282(** val ltl_lin_seq_rect_Type0 :
     
    286286| SAVE_CARRY -> h_SAVE_CARRY
    287287| RESTORE_CARRY -> h_RESTORE_CARRY
    288 | LOW_ADDRESS (x_1718, x_1717) -> h_LOW_ADDRESS x_1718 x_1717
    289 | HIGH_ADDRESS (x_1720, x_1719) -> h_HIGH_ADDRESS x_1720 x_1719
     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
    290290
    291291(** val ltl_lin_seq_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.