Ignore:
Timestamp:
Mar 5, 2013, 9:52:39 PM (7 years ago)
Author:
sacerdot
Message:

The compiler now computes also the stack cost model.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/joint_LTL_LIN.ml

    r2773 r2775  
    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_16467, x_16466) -> h_from_acc x_16467 x_16466
    119 | To_acc (x_16469, x_16468) -> h_to_acc x_16469 x_16468
    120 | Int_to_reg (x_16471, x_16470) -> h_int_to_reg x_16471 x_16470
    121 | Int_to_acc (x_16473, x_16472) -> h_int_to_acc x_16473 x_16472
     118| From_acc (x_21298, x_21297) -> h_from_acc x_21298 x_21297
     119| To_acc (x_21300, x_21299) -> h_to_acc x_21300 x_21299
     120| Int_to_reg (x_21302, x_21301) -> h_int_to_reg x_21302 x_21301
     121| Int_to_acc (x_21304, x_21303) -> h_int_to_acc x_21304 x_21303
    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_16480, x_16479) -> h_from_acc x_16480 x_16479
    129 | To_acc (x_16482, x_16481) -> h_to_acc x_16482 x_16481
    130 | Int_to_reg (x_16484, x_16483) -> h_int_to_reg x_16484 x_16483
    131 | Int_to_acc (x_16486, x_16485) -> h_int_to_acc x_16486 x_16485
     128| From_acc (x_21311, x_21310) -> h_from_acc x_21311 x_21310
     129| To_acc (x_21313, x_21312) -> h_to_acc x_21313 x_21312
     130| Int_to_reg (x_21315, x_21314) -> h_int_to_reg x_21315 x_21314
     131| Int_to_acc (x_21317, x_21316) -> h_int_to_acc x_21317 x_21316
    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_16493, x_16492) -> h_from_acc x_16493 x_16492
    139 | To_acc (x_16495, x_16494) -> h_to_acc x_16495 x_16494
    140 | Int_to_reg (x_16497, x_16496) -> h_int_to_reg x_16497 x_16496
    141 | Int_to_acc (x_16499, x_16498) -> h_int_to_acc x_16499 x_16498
     138| From_acc (x_21324, x_21323) -> h_from_acc x_21324 x_21323
     139| To_acc (x_21326, x_21325) -> h_to_acc x_21326 x_21325
     140| Int_to_reg (x_21328, x_21327) -> h_int_to_reg x_21328 x_21327
     141| Int_to_acc (x_21330, x_21329) -> h_int_to_acc x_21330 x_21329
    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_16506, x_16505) -> h_from_acc x_16506 x_16505
    149 | To_acc (x_16508, x_16507) -> h_to_acc x_16508 x_16507
    150 | Int_to_reg (x_16510, x_16509) -> h_int_to_reg x_16510 x_16509
    151 | Int_to_acc (x_16512, x_16511) -> h_int_to_acc x_16512 x_16511
     148| From_acc (x_21337, x_21336) -> h_from_acc x_21337 x_21336
     149| To_acc (x_21339, x_21338) -> h_to_acc x_21339 x_21338
     150| Int_to_reg (x_21341, x_21340) -> h_int_to_reg x_21341 x_21340
     151| Int_to_acc (x_21343, x_21342) -> h_int_to_acc x_21343 x_21342
    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_16519, x_16518) -> h_from_acc x_16519 x_16518
    159 | To_acc (x_16521, x_16520) -> h_to_acc x_16521 x_16520
    160 | Int_to_reg (x_16523, x_16522) -> h_int_to_reg x_16523 x_16522
    161 | Int_to_acc (x_16525, x_16524) -> h_int_to_acc x_16525 x_16524
     158| From_acc (x_21350, x_21349) -> h_from_acc x_21350 x_21349
     159| To_acc (x_21352, x_21351) -> h_to_acc x_21352 x_21351
     160| Int_to_reg (x_21354, x_21353) -> h_int_to_reg x_21354 x_21353
     161| Int_to_acc (x_21356, x_21355) -> h_int_to_acc x_21356 x_21355
    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_16532, x_16531) -> h_from_acc x_16532 x_16531
    169 | To_acc (x_16534, x_16533) -> h_to_acc x_16534 x_16533
    170 | Int_to_reg (x_16536, x_16535) -> h_int_to_reg x_16536 x_16535
    171 | Int_to_acc (x_16538, x_16537) -> h_int_to_acc x_16538 x_16537
     168| From_acc (x_21363, x_21362) -> h_from_acc x_21363 x_21362
     169| To_acc (x_21365, x_21364) -> h_to_acc x_21365 x_21364
     170| Int_to_reg (x_21367, x_21366) -> h_int_to_reg x_21367 x_21366
     171| Int_to_acc (x_21369, x_21368) -> h_int_to_acc x_21369 x_21368
    172172
    173173(** val registers_move_inv_rect_Type4 :
     
    241241| SAVE_CARRY -> h_SAVE_CARRY
    242242| RESTORE_CARRY -> h_RESTORE_CARRY
    243 | LOW_ADDRESS (x_16632, x_16631) -> h_LOW_ADDRESS x_16632 x_16631
    244 | HIGH_ADDRESS (x_16634, x_16633) -> h_HIGH_ADDRESS x_16634 x_16633
     243| LOW_ADDRESS (x_21463, x_21462) -> h_LOW_ADDRESS x_21463 x_21462
     244| HIGH_ADDRESS (x_21465, x_21464) -> h_HIGH_ADDRESS x_21465 x_21464
    245245
    246246(** val ltl_lin_seq_rect_Type5 :
     
    250250| SAVE_CARRY -> h_SAVE_CARRY
    251251| RESTORE_CARRY -> h_RESTORE_CARRY
    252 | LOW_ADDRESS (x_16641, x_16640) -> h_LOW_ADDRESS x_16641 x_16640
    253 | HIGH_ADDRESS (x_16643, x_16642) -> h_HIGH_ADDRESS x_16643 x_16642
     252| LOW_ADDRESS (x_21472, x_21471) -> h_LOW_ADDRESS x_21472 x_21471
     253| HIGH_ADDRESS (x_21474, x_21473) -> h_HIGH_ADDRESS x_21474 x_21473
    254254
    255255(** val ltl_lin_seq_rect_Type3 :
     
    259259| SAVE_CARRY -> h_SAVE_CARRY
    260260| RESTORE_CARRY -> h_RESTORE_CARRY
    261 | LOW_ADDRESS (x_16650, x_16649) -> h_LOW_ADDRESS x_16650 x_16649
    262 | HIGH_ADDRESS (x_16652, x_16651) -> h_HIGH_ADDRESS x_16652 x_16651
     261| LOW_ADDRESS (x_21481, x_21480) -> h_LOW_ADDRESS x_21481 x_21480
     262| HIGH_ADDRESS (x_21483, x_21482) -> h_HIGH_ADDRESS x_21483 x_21482
    263263
    264264(** val ltl_lin_seq_rect_Type2 :
     
    268268| SAVE_CARRY -> h_SAVE_CARRY
    269269| RESTORE_CARRY -> h_RESTORE_CARRY
    270 | LOW_ADDRESS (x_16659, x_16658) -> h_LOW_ADDRESS x_16659 x_16658
    271 | HIGH_ADDRESS (x_16661, x_16660) -> h_HIGH_ADDRESS x_16661 x_16660
     270| LOW_ADDRESS (x_21490, x_21489) -> h_LOW_ADDRESS x_21490 x_21489
     271| HIGH_ADDRESS (x_21492, x_21491) -> h_HIGH_ADDRESS x_21492 x_21491
    272272
    273273(** val ltl_lin_seq_rect_Type1 :
     
    277277| SAVE_CARRY -> h_SAVE_CARRY
    278278| RESTORE_CARRY -> h_RESTORE_CARRY
    279 | LOW_ADDRESS (x_16668, x_16667) -> h_LOW_ADDRESS x_16668 x_16667
    280 | HIGH_ADDRESS (x_16670, x_16669) -> h_HIGH_ADDRESS x_16670 x_16669
     279| LOW_ADDRESS (x_21499, x_21498) -> h_LOW_ADDRESS x_21499 x_21498
     280| HIGH_ADDRESS (x_21501, x_21500) -> h_HIGH_ADDRESS x_21501 x_21500
    281281
    282282(** val ltl_lin_seq_rect_Type0 :
     
    286286| SAVE_CARRY -> h_SAVE_CARRY
    287287| RESTORE_CARRY -> h_RESTORE_CARRY
    288 | LOW_ADDRESS (x_16677, x_16676) -> h_LOW_ADDRESS x_16677 x_16676
    289 | HIGH_ADDRESS (x_16679, x_16678) -> h_HIGH_ADDRESS x_16679 x_16678
     288| LOW_ADDRESS (x_21508, x_21507) -> h_LOW_ADDRESS x_21508 x_21507
     289| HIGH_ADDRESS (x_21510, x_21509) -> h_HIGH_ADDRESS x_21510 x_21509
    290290
    291291(** val ltl_lin_seq_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.