Changeset 2797 for extracted/status.ml


Ignore:
Timestamp:
Mar 7, 2013, 12:55:34 PM (7 years ago)
Author:
sacerdot
Message:

Extracted again after James's cleanup and the implementation of the
new testing function to be used in the untrusted code.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/status.ml

    r2775 r2797  
    8989    serialBufferType -> 'a1 **)
    9090let rec serialBufferType_rect_Type4 h_Eight h_Nine = function
    91 | Eight x_24240 -> h_Eight x_24240
    92 | Nine (x_24242, x_24241) -> h_Nine x_24242 x_24241
     91| Eight x_24319 -> h_Eight x_24319
     92| Nine (x_24321, x_24320) -> h_Nine x_24321 x_24320
    9393
    9494(** val serialBufferType_rect_Type5 :
     
    9696    serialBufferType -> 'a1 **)
    9797let rec serialBufferType_rect_Type5 h_Eight h_Nine = function
    98 | Eight x_24246 -> h_Eight x_24246
    99 | Nine (x_24248, x_24247) -> h_Nine x_24248 x_24247
     98| Eight x_24325 -> h_Eight x_24325
     99| Nine (x_24327, x_24326) -> h_Nine x_24327 x_24326
    100100
    101101(** val serialBufferType_rect_Type3 :
     
    103103    serialBufferType -> 'a1 **)
    104104let rec serialBufferType_rect_Type3 h_Eight h_Nine = function
    105 | Eight x_24252 -> h_Eight x_24252
    106 | Nine (x_24254, x_24253) -> h_Nine x_24254 x_24253
     105| Eight x_24331 -> h_Eight x_24331
     106| Nine (x_24333, x_24332) -> h_Nine x_24333 x_24332
    107107
    108108(** val serialBufferType_rect_Type2 :
     
    110110    serialBufferType -> 'a1 **)
    111111let rec serialBufferType_rect_Type2 h_Eight h_Nine = function
    112 | Eight x_24258 -> h_Eight x_24258
    113 | Nine (x_24260, x_24259) -> h_Nine x_24260 x_24259
     112| Eight x_24337 -> h_Eight x_24337
     113| Nine (x_24339, x_24338) -> h_Nine x_24339 x_24338
    114114
    115115(** val serialBufferType_rect_Type1 :
     
    117117    serialBufferType -> 'a1 **)
    118118let rec serialBufferType_rect_Type1 h_Eight h_Nine = function
    119 | Eight x_24264 -> h_Eight x_24264
    120 | Nine (x_24266, x_24265) -> h_Nine x_24266 x_24265
     119| Eight x_24343 -> h_Eight x_24343
     120| Nine (x_24345, x_24344) -> h_Nine x_24345 x_24344
    121121
    122122(** val serialBufferType_rect_Type0 :
     
    124124    serialBufferType -> 'a1 **)
    125125let rec serialBufferType_rect_Type0 h_Eight h_Nine = function
    126 | Eight x_24270 -> h_Eight x_24270
    127 | Nine (x_24272, x_24271) -> h_Nine x_24272 x_24271
     126| Eight x_24349 -> h_Eight x_24349
     127| Nine (x_24351, x_24350) -> h_Nine x_24351 x_24350
    128128
    129129(** val serialBufferType_inv_rect_Type4 :
     
    182182    -> 'a1) -> lineType -> 'a1 **)
    183183let rec lineType_rect_Type4 h_P1 h_P3 h_SerialBuffer = function
    184 | P1 x_24319 -> h_P1 x_24319
    185 | P3 x_24320 -> h_P3 x_24320
    186 | SerialBuffer x_24321 -> h_SerialBuffer x_24321
     184| P1 x_24398 -> h_P1 x_24398
     185| P3 x_24399 -> h_P3 x_24399
     186| SerialBuffer x_24400 -> h_SerialBuffer x_24400
    187187
    188188(** val lineType_rect_Type5 :
     
    190190    -> 'a1) -> lineType -> 'a1 **)
    191191let rec lineType_rect_Type5 h_P1 h_P3 h_SerialBuffer = function
    192 | P1 x_24326 -> h_P1 x_24326
    193 | P3 x_24327 -> h_P3 x_24327
    194 | SerialBuffer x_24328 -> h_SerialBuffer x_24328
     192| P1 x_24405 -> h_P1 x_24405
     193| P3 x_24406 -> h_P3 x_24406
     194| SerialBuffer x_24407 -> h_SerialBuffer x_24407
    195195
    196196(** val lineType_rect_Type3 :
     
    198198    -> 'a1) -> lineType -> 'a1 **)
    199199let rec lineType_rect_Type3 h_P1 h_P3 h_SerialBuffer = function
    200 | P1 x_24333 -> h_P1 x_24333
    201 | P3 x_24334 -> h_P3 x_24334
    202 | SerialBuffer x_24335 -> h_SerialBuffer x_24335
     200| P1 x_24412 -> h_P1 x_24412
     201| P3 x_24413 -> h_P3 x_24413
     202| SerialBuffer x_24414 -> h_SerialBuffer x_24414
    203203
    204204(** val lineType_rect_Type2 :
     
    206206    -> 'a1) -> lineType -> 'a1 **)
    207207let rec lineType_rect_Type2 h_P1 h_P3 h_SerialBuffer = function
    208 | P1 x_24340 -> h_P1 x_24340
    209 | P3 x_24341 -> h_P3 x_24341
    210 | SerialBuffer x_24342 -> h_SerialBuffer x_24342
     208| P1 x_24419 -> h_P1 x_24419
     209| P3 x_24420 -> h_P3 x_24420
     210| SerialBuffer x_24421 -> h_SerialBuffer x_24421
    211211
    212212(** val lineType_rect_Type1 :
     
    214214    -> 'a1) -> lineType -> 'a1 **)
    215215let rec lineType_rect_Type1 h_P1 h_P3 h_SerialBuffer = function
    216 | P1 x_24347 -> h_P1 x_24347
    217 | P3 x_24348 -> h_P3 x_24348
    218 | SerialBuffer x_24349 -> h_SerialBuffer x_24349
     216| P1 x_24426 -> h_P1 x_24426
     217| P3 x_24427 -> h_P3 x_24427
     218| SerialBuffer x_24428 -> h_SerialBuffer x_24428
    219219
    220220(** val lineType_rect_Type0 :
     
    222222    -> 'a1) -> lineType -> 'a1 **)
    223223let rec lineType_rect_Type0 h_P1 h_P3 h_SerialBuffer = function
    224 | P1 x_24354 -> h_P1 x_24354
    225 | P3 x_24355 -> h_P3 x_24355
    226 | SerialBuffer x_24356 -> h_SerialBuffer x_24356
     224| P1 x_24433 -> h_P1 x_24433
     225| P3 x_24434 -> h_P3 x_24434
     226| SerialBuffer x_24435 -> h_SerialBuffer x_24435
    227227
    228228(** val lineType_inv_rect_Type4 :
     
    731731    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    732732    preStatus -> 'a2 **)
    733 let rec preStatus_rect_Type4 code_memory h_mk_PreStatus x_24742 =
     733let rec preStatus_rect_Type4 code_memory h_mk_PreStatus x_24821 =
    734734  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    735735    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    737737    special_function_registers_8053; special_function_registers_8052 =
    738738    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    739     p3_latch0; clock = clock0 } = x_24742
     739    p3_latch0; clock = clock0 } = x_24821
    740740  in
    741741  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     
    749749    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    750750    preStatus -> 'a2 **)
    751 let rec preStatus_rect_Type5 code_memory h_mk_PreStatus x_24744 =
     751let rec preStatus_rect_Type5 code_memory h_mk_PreStatus x_24823 =
    752752  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    753753    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    755755    special_function_registers_8053; special_function_registers_8052 =
    756756    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    757     p3_latch0; clock = clock0 } = x_24744
     757    p3_latch0; clock = clock0 } = x_24823
    758758  in
    759759  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     
    767767    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    768768    preStatus -> 'a2 **)
    769 let rec preStatus_rect_Type3 code_memory h_mk_PreStatus x_24746 =
     769let rec preStatus_rect_Type3 code_memory h_mk_PreStatus x_24825 =
    770770  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    771771    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    773773    special_function_registers_8053; special_function_registers_8052 =
    774774    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    775     p3_latch0; clock = clock0 } = x_24746
     775    p3_latch0; clock = clock0 } = x_24825
    776776  in
    777777  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     
    785785    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    786786    preStatus -> 'a2 **)
    787 let rec preStatus_rect_Type2 code_memory h_mk_PreStatus x_24748 =
     787let rec preStatus_rect_Type2 code_memory h_mk_PreStatus x_24827 =
    788788  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    789789    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    791791    special_function_registers_8053; special_function_registers_8052 =
    792792    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    793     p3_latch0; clock = clock0 } = x_24748
     793    p3_latch0; clock = clock0 } = x_24827
    794794  in
    795795  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     
    803803    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    804804    preStatus -> 'a2 **)
    805 let rec preStatus_rect_Type1 code_memory h_mk_PreStatus x_24750 =
     805let rec preStatus_rect_Type1 code_memory h_mk_PreStatus x_24829 =
    806806  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    807807    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    809809    special_function_registers_8053; special_function_registers_8052 =
    810810    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    811     p3_latch0; clock = clock0 } = x_24750
     811    p3_latch0; clock = clock0 } = x_24829
    812812  in
    813813  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     
    821821    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    822822    preStatus -> 'a2 **)
    823 let rec preStatus_rect_Type0 code_memory h_mk_PreStatus x_24752 =
     823let rec preStatus_rect_Type0 code_memory h_mk_PreStatus x_24831 =
    824824  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    825825    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    827827    special_function_registers_8053; special_function_registers_8052 =
    828828    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    829     p3_latch0; clock = clock0 } = x_24752
     829    p3_latch0; clock = clock0 } = x_24831
    830830  in
    831831  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
Note: See TracChangeset for help on using the changeset viewer.