Changeset 3024


Ignore:
Timestamp:
Mar 28, 2013, 10:53:54 PM (4 years ago)
Author:
sacerdot
Message:

Bug fixed: set_flags was ignoring the cy and ov flags.

Files:
2 edited

Legend:

Unmodified
Added
Removed
  • extracted/status.ml

    r2999 r3024  
    8989    serialBufferType -> 'a1 **)
    9090let rec serialBufferType_rect_Type4 h_Eight h_Nine = function
    91 | Eight x_2400 -> h_Eight x_2400
    92 | Nine (x_2402, x_2401) -> h_Nine x_2402 x_2401
     91| Eight x_8 -> h_Eight x_8
     92| Nine (x_10, x_9) -> h_Nine x_10 x_9
    9393
    9494(** val serialBufferType_rect_Type5 :
     
    9696    serialBufferType -> 'a1 **)
    9797let rec serialBufferType_rect_Type5 h_Eight h_Nine = function
    98 | Eight x_2406 -> h_Eight x_2406
    99 | Nine (x_2408, x_2407) -> h_Nine x_2408 x_2407
     98| Eight x_14 -> h_Eight x_14
     99| Nine (x_16, x_15) -> h_Nine x_16 x_15
    100100
    101101(** val serialBufferType_rect_Type3 :
     
    103103    serialBufferType -> 'a1 **)
    104104let rec serialBufferType_rect_Type3 h_Eight h_Nine = function
    105 | Eight x_2412 -> h_Eight x_2412
    106 | Nine (x_2414, x_2413) -> h_Nine x_2414 x_2413
     105| Eight x_20 -> h_Eight x_20
     106| Nine (x_22, x_21) -> h_Nine x_22 x_21
    107107
    108108(** val serialBufferType_rect_Type2 :
     
    110110    serialBufferType -> 'a1 **)
    111111let rec serialBufferType_rect_Type2 h_Eight h_Nine = function
    112 | Eight x_2418 -> h_Eight x_2418
    113 | Nine (x_2420, x_2419) -> h_Nine x_2420 x_2419
     112| Eight x_26 -> h_Eight x_26
     113| Nine (x_28, x_27) -> h_Nine x_28 x_27
    114114
    115115(** val serialBufferType_rect_Type1 :
     
    117117    serialBufferType -> 'a1 **)
    118118let rec serialBufferType_rect_Type1 h_Eight h_Nine = function
    119 | Eight x_2424 -> h_Eight x_2424
    120 | Nine (x_2426, x_2425) -> h_Nine x_2426 x_2425
     119| Eight x_32 -> h_Eight x_32
     120| Nine (x_34, x_33) -> h_Nine x_34 x_33
    121121
    122122(** val serialBufferType_rect_Type0 :
     
    124124    serialBufferType -> 'a1 **)
    125125let rec serialBufferType_rect_Type0 h_Eight h_Nine = function
    126 | Eight x_2430 -> h_Eight x_2430
    127 | Nine (x_2432, x_2431) -> h_Nine x_2432 x_2431
     126| Eight x_38 -> h_Eight x_38
     127| Nine (x_40, x_39) -> h_Nine x_40 x_39
    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_2479 -> h_P1 x_2479
    185 | P3 x_2480 -> h_P3 x_2480
    186 | SerialBuffer x_2481 -> h_SerialBuffer x_2481
     184| P1 x_87 -> h_P1 x_87
     185| P3 x_88 -> h_P3 x_88
     186| SerialBuffer x_89 -> h_SerialBuffer x_89
    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_2486 -> h_P1 x_2486
    193 | P3 x_2487 -> h_P3 x_2487
    194 | SerialBuffer x_2488 -> h_SerialBuffer x_2488
     192| P1 x_94 -> h_P1 x_94
     193| P3 x_95 -> h_P3 x_95
     194| SerialBuffer x_96 -> h_SerialBuffer x_96
    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_2493 -> h_P1 x_2493
    201 | P3 x_2494 -> h_P3 x_2494
    202 | SerialBuffer x_2495 -> h_SerialBuffer x_2495
     200| P1 x_101 -> h_P1 x_101
     201| P3 x_102 -> h_P3 x_102
     202| SerialBuffer x_103 -> h_SerialBuffer x_103
    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_2500 -> h_P1 x_2500
    209 | P3 x_2501 -> h_P3 x_2501
    210 | SerialBuffer x_2502 -> h_SerialBuffer x_2502
     208| P1 x_108 -> h_P1 x_108
     209| P3 x_109 -> h_P3 x_109
     210| SerialBuffer x_110 -> h_SerialBuffer x_110
    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_2507 -> h_P1 x_2507
    217 | P3 x_2508 -> h_P3 x_2508
    218 | SerialBuffer x_2509 -> h_SerialBuffer x_2509
     216| P1 x_115 -> h_P1 x_115
     217| P3 x_116 -> h_P3 x_116
     218| SerialBuffer x_117 -> h_SerialBuffer x_117
    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_2514 -> h_P1 x_2514
    225 | P3 x_2515 -> h_P3 x_2515
    226 | SerialBuffer x_2516 -> h_SerialBuffer x_2516
     224| P1 x_122 -> h_P1 x_122
     225| P3 x_123 -> h_P3 x_123
     226| SerialBuffer x_124 -> h_SerialBuffer x_124
    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_2902 =
     733let rec preStatus_rect_Type4 code_memory h_mk_PreStatus x_510 =
    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_2902
     739    p3_latch0; clock = clock0 } = x_510
    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_2904 =
     751let rec preStatus_rect_Type5 code_memory h_mk_PreStatus x_512 =
    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_2904
     757    p3_latch0; clock = clock0 } = x_512
    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_2906 =
     769let rec preStatus_rect_Type3 code_memory h_mk_PreStatus x_514 =
    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_2906
     775    p3_latch0; clock = clock0 } = x_514
    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_2908 =
     787let rec preStatus_rect_Type2 code_memory h_mk_PreStatus x_516 =
    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_2908
     793    p3_latch0; clock = clock0 } = x_516
    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_2910 =
     805let rec preStatus_rect_Type1 code_memory h_mk_PreStatus x_518 =
    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_2910
     811    p3_latch0; clock = clock0 } = x_518
    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_2912 =
     823let rec preStatus_rect_Type0 code_memory h_mk_PreStatus x_520 =
    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_2912
     829    p3_latch0; clock = clock0 } = x_520
    830830  in
    831831  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     
    12961296  in
    12971297  set_8051_sfr code_memory s SFR_PSW (Vector.VCons ((Nat.S (Nat.S (Nat.S
    1298     (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), old_cy, (Vector.VCons ((Nat.S
     1298    (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), cy, (Vector.VCons ((Nat.S
    12991299    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), new_ac, (Vector.VCons
    13001300    ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), old_fo, (Vector.VCons
    13011301    ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), old_rs1, (Vector.VCons ((Nat.S
    13021302    (Nat.S (Nat.S Nat.O))), old_rs0, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
    1303     old_ov, (Vector.VCons ((Nat.S Nat.O), old_ud, (Vector.VCons (Nat.O,
    1304     old_p, Vector.VEmpty))))))))))))))))
     1303    ov, (Vector.VCons ((Nat.S Nat.O), old_ud, (Vector.VCons (Nat.O, old_p,
     1304    Vector.VEmpty))))))))))))))))
    13051305
    13061306(** val initialise_status : 'a1 -> 'a1 preStatus **)
  • src/ASM/Status.ma

    r2907 r3024  
    521521    let new_ac ≝ match ac with [ None ⇒ old_ac | Some j ⇒ j ] in
    522522      set_8051_sfr ?? s SFR_PSW
    523       [[ old_cy ; new_ac ; old_fo ; old_rs1 ;
    524          old_rs0 ; old_ov ; old_ud ; old_p ]].
     523      [[ cy ; new_ac ; old_fo ; old_rs1 ;
     524         old_rs0 ; ov ; old_ud ; old_p ]].
    525525    [1,2,3,4,5,6,7,8:
    526526       normalize
Note: See TracChangeset for help on using the changeset viewer.