Changeset 2867 for extracted/eRTLptr.ml


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/eRTLptr.ml

    r2854 r2867  
    116116    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    117117let rec ertlptr_seq_rect_Type4 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    118 | Ertlptr_ertl x_1386 -> h_ertlptr_ertl x_1386
    119 | LOW_ADDRESS (x_1388, x_1387) -> h_LOW_ADDRESS x_1388 x_1387
    120 | HIGH_ADDRESS (x_1390, x_1389) -> h_HIGH_ADDRESS x_1390 x_1389
     118| Ertlptr_ertl x_21381 -> h_ertlptr_ertl x_21381
     119| LOW_ADDRESS (x_21383, x_21382) -> h_LOW_ADDRESS x_21383 x_21382
     120| HIGH_ADDRESS (x_21385, x_21384) -> h_HIGH_ADDRESS x_21385 x_21384
    121121
    122122(** val ertlptr_seq_rect_Type5 :
     
    124124    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    125125let rec ertlptr_seq_rect_Type5 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    126 | Ertlptr_ertl x_1395 -> h_ertlptr_ertl x_1395
    127 | LOW_ADDRESS (x_1397, x_1396) -> h_LOW_ADDRESS x_1397 x_1396
    128 | HIGH_ADDRESS (x_1399, x_1398) -> h_HIGH_ADDRESS x_1399 x_1398
     126| Ertlptr_ertl x_21390 -> h_ertlptr_ertl x_21390
     127| LOW_ADDRESS (x_21392, x_21391) -> h_LOW_ADDRESS x_21392 x_21391
     128| HIGH_ADDRESS (x_21394, x_21393) -> h_HIGH_ADDRESS x_21394 x_21393
    129129
    130130(** val ertlptr_seq_rect_Type3 :
     
    132132    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    133133let rec ertlptr_seq_rect_Type3 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    134 | Ertlptr_ertl x_1404 -> h_ertlptr_ertl x_1404
    135 | LOW_ADDRESS (x_1406, x_1405) -> h_LOW_ADDRESS x_1406 x_1405
    136 | HIGH_ADDRESS (x_1408, x_1407) -> h_HIGH_ADDRESS x_1408 x_1407
     134| Ertlptr_ertl x_21399 -> h_ertlptr_ertl x_21399
     135| LOW_ADDRESS (x_21401, x_21400) -> h_LOW_ADDRESS x_21401 x_21400
     136| HIGH_ADDRESS (x_21403, x_21402) -> h_HIGH_ADDRESS x_21403 x_21402
    137137
    138138(** val ertlptr_seq_rect_Type2 :
     
    140140    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    141141let rec ertlptr_seq_rect_Type2 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    142 | Ertlptr_ertl x_1413 -> h_ertlptr_ertl x_1413
    143 | LOW_ADDRESS (x_1415, x_1414) -> h_LOW_ADDRESS x_1415 x_1414
    144 | HIGH_ADDRESS (x_1417, x_1416) -> h_HIGH_ADDRESS x_1417 x_1416
     142| Ertlptr_ertl x_21408 -> h_ertlptr_ertl x_21408
     143| LOW_ADDRESS (x_21410, x_21409) -> h_LOW_ADDRESS x_21410 x_21409
     144| HIGH_ADDRESS (x_21412, x_21411) -> h_HIGH_ADDRESS x_21412 x_21411
    145145
    146146(** val ertlptr_seq_rect_Type1 :
     
    148148    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    149149let rec ertlptr_seq_rect_Type1 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    150 | Ertlptr_ertl x_1422 -> h_ertlptr_ertl x_1422
    151 | LOW_ADDRESS (x_1424, x_1423) -> h_LOW_ADDRESS x_1424 x_1423
    152 | HIGH_ADDRESS (x_1426, x_1425) -> h_HIGH_ADDRESS x_1426 x_1425
     150| Ertlptr_ertl x_21417 -> h_ertlptr_ertl x_21417
     151| LOW_ADDRESS (x_21419, x_21418) -> h_LOW_ADDRESS x_21419 x_21418
     152| HIGH_ADDRESS (x_21421, x_21420) -> h_HIGH_ADDRESS x_21421 x_21420
    153153
    154154(** val ertlptr_seq_rect_Type0 :
     
    156156    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    157157let rec ertlptr_seq_rect_Type0 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    158 | Ertlptr_ertl x_1431 -> h_ertlptr_ertl x_1431
    159 | LOW_ADDRESS (x_1433, x_1432) -> h_LOW_ADDRESS x_1433 x_1432
    160 | HIGH_ADDRESS (x_1435, x_1434) -> h_HIGH_ADDRESS x_1435 x_1434
     158| Ertlptr_ertl x_21426 -> h_ertlptr_ertl x_21426
     159| LOW_ADDRESS (x_21428, x_21427) -> h_LOW_ADDRESS x_21428 x_21427
     160| HIGH_ADDRESS (x_21430, x_21429) -> h_HIGH_ADDRESS x_21430 x_21429
    161161
    162162(** val ertlptr_seq_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.