Ignore:
Timestamp:
Mar 28, 2013, 5:27:46 PM (7 years ago)
Author:
sacerdot
Message:

New extraction after ERTLptr abortion.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/joint_LTL_LIN.ml

    r3001 r3019  
    130130    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    131131let rec registers_move_rect_Type4 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    132 | From_acc (x_5280, x_5279) -> h_from_acc x_5280 x_5279
    133 | To_acc (x_5282, x_5281) -> h_to_acc x_5282 x_5281
    134 | Int_to_reg (x_5284, x_5283) -> h_int_to_reg x_5284 x_5283
    135 | Int_to_acc (x_5286, x_5285) -> h_int_to_acc x_5286 x_5285
     132| From_acc (x_16, x_15) -> h_from_acc x_16 x_15
     133| To_acc (x_18, x_17) -> h_to_acc x_18 x_17
     134| Int_to_reg (x_20, x_19) -> h_int_to_reg x_20 x_19
     135| Int_to_acc (x_22, x_21) -> h_int_to_acc x_22 x_21
    136136
    137137(** val registers_move_rect_Type5 :
     
    140140    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    141141let rec registers_move_rect_Type5 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    142 | From_acc (x_5293, x_5292) -> h_from_acc x_5293 x_5292
    143 | To_acc (x_5295, x_5294) -> h_to_acc x_5295 x_5294
    144 | Int_to_reg (x_5297, x_5296) -> h_int_to_reg x_5297 x_5296
    145 | Int_to_acc (x_5299, x_5298) -> h_int_to_acc x_5299 x_5298
     142| From_acc (x_29, x_28) -> h_from_acc x_29 x_28
     143| To_acc (x_31, x_30) -> h_to_acc x_31 x_30
     144| Int_to_reg (x_33, x_32) -> h_int_to_reg x_33 x_32
     145| Int_to_acc (x_35, x_34) -> h_int_to_acc x_35 x_34
    146146
    147147(** val registers_move_rect_Type3 :
     
    150150    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    151151let rec registers_move_rect_Type3 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    152 | From_acc (x_5306, x_5305) -> h_from_acc x_5306 x_5305
    153 | To_acc (x_5308, x_5307) -> h_to_acc x_5308 x_5307
    154 | Int_to_reg (x_5310, x_5309) -> h_int_to_reg x_5310 x_5309
    155 | Int_to_acc (x_5312, x_5311) -> h_int_to_acc x_5312 x_5311
     152| From_acc (x_42, x_41) -> h_from_acc x_42 x_41
     153| To_acc (x_44, x_43) -> h_to_acc x_44 x_43
     154| Int_to_reg (x_46, x_45) -> h_int_to_reg x_46 x_45
     155| Int_to_acc (x_48, x_47) -> h_int_to_acc x_48 x_47
    156156
    157157(** val registers_move_rect_Type2 :
     
    160160    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    161161let rec registers_move_rect_Type2 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    162 | From_acc (x_5319, x_5318) -> h_from_acc x_5319 x_5318
    163 | To_acc (x_5321, x_5320) -> h_to_acc x_5321 x_5320
    164 | Int_to_reg (x_5323, x_5322) -> h_int_to_reg x_5323 x_5322
    165 | Int_to_acc (x_5325, x_5324) -> h_int_to_acc x_5325 x_5324
     162| From_acc (x_55, x_54) -> h_from_acc x_55 x_54
     163| To_acc (x_57, x_56) -> h_to_acc x_57 x_56
     164| Int_to_reg (x_59, x_58) -> h_int_to_reg x_59 x_58
     165| Int_to_acc (x_61, x_60) -> h_int_to_acc x_61 x_60
    166166
    167167(** val registers_move_rect_Type1 :
     
    170170    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    171171let rec registers_move_rect_Type1 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    172 | From_acc (x_5332, x_5331) -> h_from_acc x_5332 x_5331
    173 | To_acc (x_5334, x_5333) -> h_to_acc x_5334 x_5333
    174 | Int_to_reg (x_5336, x_5335) -> h_int_to_reg x_5336 x_5335
    175 | Int_to_acc (x_5338, x_5337) -> h_int_to_acc x_5338 x_5337
     172| From_acc (x_68, x_67) -> h_from_acc x_68 x_67
     173| To_acc (x_70, x_69) -> h_to_acc x_70 x_69
     174| Int_to_reg (x_72, x_71) -> h_int_to_reg x_72 x_71
     175| Int_to_acc (x_74, x_73) -> h_int_to_acc x_74 x_73
    176176
    177177(** val registers_move_rect_Type0 :
     
    180180    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    181181let rec registers_move_rect_Type0 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    182 | From_acc (x_5345, x_5344) -> h_from_acc x_5345 x_5344
    183 | To_acc (x_5347, x_5346) -> h_to_acc x_5347 x_5346
    184 | Int_to_reg (x_5349, x_5348) -> h_int_to_reg x_5349 x_5348
    185 | Int_to_acc (x_5351, x_5350) -> h_int_to_acc x_5351 x_5350
     182| From_acc (x_81, x_80) -> h_from_acc x_81 x_80
     183| To_acc (x_83, x_82) -> h_to_acc x_83 x_82
     184| Int_to_reg (x_85, x_84) -> h_int_to_reg x_85 x_84
     185| Int_to_acc (x_87, x_86) -> h_int_to_acc x_87 x_86
    186186
    187187(** val registers_move_inv_rect_Type4 :
     
    246246| SAVE_CARRY
    247247| RESTORE_CARRY
    248 | LOW_ADDRESS of I8051.register * Graphs.label
    249 | HIGH_ADDRESS of I8051.register * Graphs.label
     248| LOW_ADDRESS of Graphs.label
     249| HIGH_ADDRESS of Graphs.label
    250250
    251251(** val ltl_lin_seq_rect_Type4 :
    252     'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register
    253     -> Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1 **)
     252    'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) ->
     253    ltl_lin_seq -> 'a1 **)
    254254let rec ltl_lin_seq_rect_Type4 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
    255255| SAVE_CARRY -> h_SAVE_CARRY
    256256| RESTORE_CARRY -> h_RESTORE_CARRY
    257 | LOW_ADDRESS (x_5445, x_5444) -> h_LOW_ADDRESS x_5445 x_5444
    258 | HIGH_ADDRESS (x_5447, x_5446) -> h_HIGH_ADDRESS x_5447 x_5446
     257| LOW_ADDRESS x_178 -> h_LOW_ADDRESS x_178
     258| HIGH_ADDRESS x_179 -> h_HIGH_ADDRESS x_179
    259259
    260260(** val ltl_lin_seq_rect_Type5 :
    261     'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register
    262     -> Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1 **)
     261    'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) ->
     262    ltl_lin_seq -> 'a1 **)
    263263let rec ltl_lin_seq_rect_Type5 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
    264264| SAVE_CARRY -> h_SAVE_CARRY
    265265| RESTORE_CARRY -> h_RESTORE_CARRY
    266 | LOW_ADDRESS (x_5454, x_5453) -> h_LOW_ADDRESS x_5454 x_5453
    267 | HIGH_ADDRESS (x_5456, x_5455) -> h_HIGH_ADDRESS x_5456 x_5455
     266| LOW_ADDRESS x_185 -> h_LOW_ADDRESS x_185
     267| HIGH_ADDRESS x_186 -> h_HIGH_ADDRESS x_186
    268268
    269269(** val ltl_lin_seq_rect_Type3 :
    270     'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register
    271     -> Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1 **)
     270    'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) ->
     271    ltl_lin_seq -> 'a1 **)
    272272let rec ltl_lin_seq_rect_Type3 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
    273273| SAVE_CARRY -> h_SAVE_CARRY
    274274| RESTORE_CARRY -> h_RESTORE_CARRY
    275 | LOW_ADDRESS (x_5463, x_5462) -> h_LOW_ADDRESS x_5463 x_5462
    276 | HIGH_ADDRESS (x_5465, x_5464) -> h_HIGH_ADDRESS x_5465 x_5464
     275| LOW_ADDRESS x_192 -> h_LOW_ADDRESS x_192
     276| HIGH_ADDRESS x_193 -> h_HIGH_ADDRESS x_193
    277277
    278278(** val ltl_lin_seq_rect_Type2 :
    279     'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register
    280     -> Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1 **)
     279    'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) ->
     280    ltl_lin_seq -> 'a1 **)
    281281let rec ltl_lin_seq_rect_Type2 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
    282282| SAVE_CARRY -> h_SAVE_CARRY
    283283| RESTORE_CARRY -> h_RESTORE_CARRY
    284 | LOW_ADDRESS (x_5472, x_5471) -> h_LOW_ADDRESS x_5472 x_5471
    285 | HIGH_ADDRESS (x_5474, x_5473) -> h_HIGH_ADDRESS x_5474 x_5473
     284| LOW_ADDRESS x_199 -> h_LOW_ADDRESS x_199
     285| HIGH_ADDRESS x_200 -> h_HIGH_ADDRESS x_200
    286286
    287287(** val ltl_lin_seq_rect_Type1 :
    288     'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register
    289     -> Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1 **)
     288    'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) ->
     289    ltl_lin_seq -> 'a1 **)
    290290let rec ltl_lin_seq_rect_Type1 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
    291291| SAVE_CARRY -> h_SAVE_CARRY
    292292| RESTORE_CARRY -> h_RESTORE_CARRY
    293 | LOW_ADDRESS (x_5481, x_5480) -> h_LOW_ADDRESS x_5481 x_5480
    294 | HIGH_ADDRESS (x_5483, x_5482) -> h_HIGH_ADDRESS x_5483 x_5482
     293| LOW_ADDRESS x_206 -> h_LOW_ADDRESS x_206
     294| HIGH_ADDRESS x_207 -> h_HIGH_ADDRESS x_207
    295295
    296296(** val ltl_lin_seq_rect_Type0 :
    297     'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register
    298     -> Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1 **)
     297    'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) ->
     298    ltl_lin_seq -> 'a1 **)
    299299let rec ltl_lin_seq_rect_Type0 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
    300300| SAVE_CARRY -> h_SAVE_CARRY
    301301| RESTORE_CARRY -> h_RESTORE_CARRY
    302 | LOW_ADDRESS (x_5490, x_5489) -> h_LOW_ADDRESS x_5490 x_5489
    303 | HIGH_ADDRESS (x_5492, x_5491) -> h_HIGH_ADDRESS x_5492 x_5491
     302| LOW_ADDRESS x_213 -> h_LOW_ADDRESS x_213
     303| HIGH_ADDRESS x_214 -> h_HIGH_ADDRESS x_214
    304304
    305305(** val ltl_lin_seq_inv_rect_Type4 :
    306     ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (I8051.register ->
    307     Graphs.label -> __ -> 'a1) -> (I8051.register -> Graphs.label -> __ ->
    308     'a1) -> 'a1 **)
     306    ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1)
     307    -> (Graphs.label -> __ -> 'a1) -> 'a1 **)
    309308let ltl_lin_seq_inv_rect_Type4 hterm h1 h2 h3 h4 =
    310309  let hcut = ltl_lin_seq_rect_Type4 h1 h2 h3 h4 hterm in hcut __
    311310
    312311(** val ltl_lin_seq_inv_rect_Type3 :
    313     ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (I8051.register ->
    314     Graphs.label -> __ -> 'a1) -> (I8051.register -> Graphs.label -> __ ->
    315     'a1) -> 'a1 **)
     312    ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1)
     313    -> (Graphs.label -> __ -> 'a1) -> 'a1 **)
    316314let ltl_lin_seq_inv_rect_Type3 hterm h1 h2 h3 h4 =
    317315  let hcut = ltl_lin_seq_rect_Type3 h1 h2 h3 h4 hterm in hcut __
    318316
    319317(** val ltl_lin_seq_inv_rect_Type2 :
    320     ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (I8051.register ->
    321     Graphs.label -> __ -> 'a1) -> (I8051.register -> Graphs.label -> __ ->
    322     'a1) -> 'a1 **)
     318    ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1)
     319    -> (Graphs.label -> __ -> 'a1) -> 'a1 **)
    323320let ltl_lin_seq_inv_rect_Type2 hterm h1 h2 h3 h4 =
    324321  let hcut = ltl_lin_seq_rect_Type2 h1 h2 h3 h4 hterm in hcut __
    325322
    326323(** val ltl_lin_seq_inv_rect_Type1 :
    327     ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (I8051.register ->
    328     Graphs.label -> __ -> 'a1) -> (I8051.register -> Graphs.label -> __ ->
    329     'a1) -> 'a1 **)
     324    ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1)
     325    -> (Graphs.label -> __ -> 'a1) -> 'a1 **)
    330326let ltl_lin_seq_inv_rect_Type1 hterm h1 h2 h3 h4 =
    331327  let hcut = ltl_lin_seq_rect_Type1 h1 h2 h3 h4 hterm in hcut __
    332328
    333329(** val ltl_lin_seq_inv_rect_Type0 :
    334     ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (I8051.register ->
    335     Graphs.label -> __ -> 'a1) -> (I8051.register -> Graphs.label -> __ ->
    336     'a1) -> 'a1 **)
     330    ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1)
     331    -> (Graphs.label -> __ -> 'a1) -> 'a1 **)
    337332let ltl_lin_seq_inv_rect_Type0 hterm h1 h2 h3 h4 =
    338333  let hcut = ltl_lin_seq_rect_Type0 h1 h2 h3 h4 hterm in hcut __
     
    344339     | SAVE_CARRY -> Obj.magic (fun _ dH -> dH)
    345340     | RESTORE_CARRY -> Obj.magic (fun _ dH -> dH)
    346      | LOW_ADDRESS (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
    347      | HIGH_ADDRESS (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
     341     | LOW_ADDRESS a0 -> Obj.magic (fun _ dH -> dH __)
     342     | HIGH_ADDRESS a0 -> Obj.magic (fun _ dH -> dH __)) y
    348343
    349344(** val ltl_lin_seq_jmdiscr : ltl_lin_seq -> ltl_lin_seq -> __ **)
     
    353348     | SAVE_CARRY -> Obj.magic (fun _ dH -> dH)
    354349     | RESTORE_CARRY -> Obj.magic (fun _ dH -> dH)
    355      | LOW_ADDRESS (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
    356      | HIGH_ADDRESS (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
     350     | LOW_ADDRESS a0 -> Obj.magic (fun _ dH -> dH __)
     351     | HIGH_ADDRESS a0 -> Obj.magic (fun _ dH -> dH __)) y
    357352
    358353(** val ltl_lin_seq_labels : ltl_lin_seq -> Graphs.label List.list **)
     
    360355| SAVE_CARRY -> List.Nil
    361356| RESTORE_CARRY -> List.Nil
    362 | LOW_ADDRESS (x, lbl) -> List.Cons (lbl, List.Nil)
    363 | HIGH_ADDRESS (x, lbl) -> List.Cons (lbl, List.Nil)
     357| LOW_ADDRESS lbl -> List.Cons (lbl, List.Nil)
     358| HIGH_ADDRESS lbl -> List.Cons (lbl, List.Nil)
    364359
    365360(** val lTL_LIN_uns : Joint.unserialized_params **)
Note: See TracChangeset for help on using the changeset viewer.