Changeset 2649 for extracted/aSM.ml
 Timestamp:
 Feb 7, 2013, 10:43:49 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/aSM.ml
r2620 r2649 1 1 open Preamble 2 2 3 open Char 3 open Extranat 4 5 open Vector 6 7 open Div_and_mod 8 9 open Jmeq 10 11 open Russell 12 13 open Types 14 15 open List 16 17 open Util 18 19 open FoldStuff 20 21 open Bool 22 23 open Hints_declaration 24 25 open Core_notation 26 27 open Pts 28 29 open Logic 30 31 open Relations 32 33 open Nat 34 35 open BitVector 36 37 open Proper 38 39 open PositiveMap 40 41 open Deqsets 42 43 open ErrorMessages 44 45 open PreIdentifiers 46 47 open Errors 48 49 open Extralib 50 51 open Setoids 52 53 open Monad 54 55 open Option 56 57 open Lists 58 59 open Positive 60 61 open Identifiers 62 63 open Arithmetic 64 65 open Integers 66 67 open AST 68 69 open CostLabel 70 71 open LabelledObjects 4 72 5 73 open String 6 74 7 open Extranat8 9 open Vector10 11 open Div_and_mod12 13 open Jmeq14 15 open Russell16 17 open Types18 19 open List20 21 open Util22 23 open FoldStuff24 25 open Bool26 27 open Hints_declaration28 29 open Core_notation30 31 open Pts32 33 open Logic34 35 open Relations36 37 open Nat38 39 open BitVector40 41 open Proper42 43 open PositiveMap44 45 open Deqsets46 47 open PreIdentifiers48 49 open Errors50 51 open Extralib52 53 open Setoids54 55 open Monad56 57 open Option58 59 open Lists60 61 open Positive62 63 open Identifiers64 65 open Coqlib66 67 open Floats68 69 open Arithmetic70 71 open Integers72 73 open AST74 75 open CostLabel76 77 open LabelledObjects78 79 (** val aSMTag : String.string **)80 let aSMTag = "ASMTag"81 (* failwith "AXIOM TO BE REALIZED" *)82 83 75 type identifier0 = PreIdentifiers.identifier 84 76 85 77 (** val toASM_ident : 86 String.string > PreIdentifiers.identifier > identifier0 **)78 PreIdentifiers.identifierTag > PreIdentifiers.identifier > identifier0 **) 87 79 let toASM_ident t i = 88 80 let id = i in id … … 117 109 > 'a1) > addressing_mode > 'a1 **) 118 110 let rec addressing_mode_rect_Type4 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function 119  DIRECT x_ 14702 > h_DIRECT x_14702120  INDIRECT x_ 14703 > h_INDIRECT x_14703121  EXT_INDIRECT x_ 14704 > h_EXT_INDIRECT x_14704122  REGISTER x_ 14705 > h_REGISTER x_14705111  DIRECT x_59 > h_DIRECT x_59 112  INDIRECT x_60 > h_INDIRECT x_60 113  EXT_INDIRECT x_61 > h_EXT_INDIRECT x_61 114  REGISTER x_62 > h_REGISTER x_62 123 115  ACC_A > h_ACC_A 124 116  ACC_B > h_ACC_B 125 117  DPTR > h_DPTR 126  DATA x_ 14706 > h_DATA x_14706127  DATA16 x_ 14707 > h_DATA16 x_14707118  DATA x_63 > h_DATA x_63 119  DATA16 x_64 > h_DATA16 x_64 128 120  ACC_DPTR > h_ACC_DPTR 129 121  ACC_PC > h_ACC_PC … … 131 123  INDIRECT_DPTR > h_INDIRECT_DPTR 132 124  CARRY > h_CARRY 133  BIT_ADDR x_ 14708 > h_BIT_ADDR x_14708134  N_BIT_ADDR x_ 14709 > h_N_BIT_ADDR x_14709135  RELATIVE x_ 14710 > h_RELATIVE x_14710136  ADDR11 x_ 14711 > h_ADDR11 x_14711137  ADDR16 x_ 14712 > h_ADDR16 x_14712125  BIT_ADDR x_65 > h_BIT_ADDR x_65 126  N_BIT_ADDR x_66 > h_N_BIT_ADDR x_66 127  RELATIVE x_67 > h_RELATIVE x_67 128  ADDR11 x_68 > h_ADDR11 x_68 129  ADDR16 x_69 > h_ADDR16 x_69 138 130 139 131 (** val addressing_mode_rect_Type5 : … … 145 137 > 'a1) > addressing_mode > 'a1 **) 146 138 let rec addressing_mode_rect_Type5 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function 147  DIRECT x_ 14733 > h_DIRECT x_14733148  INDIRECT x_ 14734 > h_INDIRECT x_14734149  EXT_INDIRECT x_ 14735 > h_EXT_INDIRECT x_14735150  REGISTER x_ 14736 > h_REGISTER x_14736139  DIRECT x_90 > h_DIRECT x_90 140  INDIRECT x_91 > h_INDIRECT x_91 141  EXT_INDIRECT x_92 > h_EXT_INDIRECT x_92 142  REGISTER x_93 > h_REGISTER x_93 151 143  ACC_A > h_ACC_A 152 144  ACC_B > h_ACC_B 153 145  DPTR > h_DPTR 154  DATA x_ 14737 > h_DATA x_14737155  DATA16 x_ 14738 > h_DATA16 x_14738146  DATA x_94 > h_DATA x_94 147  DATA16 x_95 > h_DATA16 x_95 156 148  ACC_DPTR > h_ACC_DPTR 157 149  ACC_PC > h_ACC_PC … … 159 151  INDIRECT_DPTR > h_INDIRECT_DPTR 160 152  CARRY > h_CARRY 161  BIT_ADDR x_ 14739 > h_BIT_ADDR x_14739162  N_BIT_ADDR x_ 14740 > h_N_BIT_ADDR x_14740163  RELATIVE x_ 14741 > h_RELATIVE x_14741164  ADDR11 x_ 14742 > h_ADDR11 x_14742165  ADDR16 x_1 4743 > h_ADDR16 x_14743153  BIT_ADDR x_96 > h_BIT_ADDR x_96 154  N_BIT_ADDR x_97 > h_N_BIT_ADDR x_97 155  RELATIVE x_98 > h_RELATIVE x_98 156  ADDR11 x_99 > h_ADDR11 x_99 157  ADDR16 x_100 > h_ADDR16 x_100 166 158 167 159 (** val addressing_mode_rect_Type3 : … … 173 165 > 'a1) > addressing_mode > 'a1 **) 174 166 let rec addressing_mode_rect_Type3 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function 175  DIRECT x_1 4764 > h_DIRECT x_14764176  INDIRECT x_1 4765 > h_INDIRECT x_14765177  EXT_INDIRECT x_1 4766 > h_EXT_INDIRECT x_14766178  REGISTER x_1 4767 > h_REGISTER x_14767167  DIRECT x_121 > h_DIRECT x_121 168  INDIRECT x_122 > h_INDIRECT x_122 169  EXT_INDIRECT x_123 > h_EXT_INDIRECT x_123 170  REGISTER x_124 > h_REGISTER x_124 179 171  ACC_A > h_ACC_A 180 172  ACC_B > h_ACC_B 181 173  DPTR > h_DPTR 182  DATA x_1 4768 > h_DATA x_14768183  DATA16 x_1 4769 > h_DATA16 x_14769174  DATA x_125 > h_DATA x_125 175  DATA16 x_126 > h_DATA16 x_126 184 176  ACC_DPTR > h_ACC_DPTR 185 177  ACC_PC > h_ACC_PC … … 187 179  INDIRECT_DPTR > h_INDIRECT_DPTR 188 180  CARRY > h_CARRY 189  BIT_ADDR x_1 4770 > h_BIT_ADDR x_14770190  N_BIT_ADDR x_1 4771 > h_N_BIT_ADDR x_14771191  RELATIVE x_1 4772 > h_RELATIVE x_14772192  ADDR11 x_1 4773 > h_ADDR11 x_14773193  ADDR16 x_1 4774 > h_ADDR16 x_14774181  BIT_ADDR x_127 > h_BIT_ADDR x_127 182  N_BIT_ADDR x_128 > h_N_BIT_ADDR x_128 183  RELATIVE x_129 > h_RELATIVE x_129 184  ADDR11 x_130 > h_ADDR11 x_130 185  ADDR16 x_131 > h_ADDR16 x_131 194 186 195 187 (** val addressing_mode_rect_Type2 : … … 201 193 > 'a1) > addressing_mode > 'a1 **) 202 194 let rec addressing_mode_rect_Type2 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function 203  DIRECT x_1 4795 > h_DIRECT x_14795204  INDIRECT x_1 4796 > h_INDIRECT x_14796205  EXT_INDIRECT x_1 4797 > h_EXT_INDIRECT x_14797206  REGISTER x_1 4798 > h_REGISTER x_14798195  DIRECT x_152 > h_DIRECT x_152 196  INDIRECT x_153 > h_INDIRECT x_153 197  EXT_INDIRECT x_154 > h_EXT_INDIRECT x_154 198  REGISTER x_155 > h_REGISTER x_155 207 199  ACC_A > h_ACC_A 208 200  ACC_B > h_ACC_B 209 201  DPTR > h_DPTR 210  DATA x_1 4799 > h_DATA x_14799211  DATA16 x_1 4800 > h_DATA16 x_14800202  DATA x_156 > h_DATA x_156 203  DATA16 x_157 > h_DATA16 x_157 212 204  ACC_DPTR > h_ACC_DPTR 213 205  ACC_PC > h_ACC_PC … … 215 207  INDIRECT_DPTR > h_INDIRECT_DPTR 216 208  CARRY > h_CARRY 217  BIT_ADDR x_1 4801 > h_BIT_ADDR x_14801218  N_BIT_ADDR x_1 4802 > h_N_BIT_ADDR x_14802219  RELATIVE x_1 4803 > h_RELATIVE x_14803220  ADDR11 x_1 4804 > h_ADDR11 x_14804221  ADDR16 x_1 4805 > h_ADDR16 x_14805209  BIT_ADDR x_158 > h_BIT_ADDR x_158 210  N_BIT_ADDR x_159 > h_N_BIT_ADDR x_159 211  RELATIVE x_160 > h_RELATIVE x_160 212  ADDR11 x_161 > h_ADDR11 x_161 213  ADDR16 x_162 > h_ADDR16 x_162 222 214 223 215 (** val addressing_mode_rect_Type1 : … … 229 221 > 'a1) > addressing_mode > 'a1 **) 230 222 let rec addressing_mode_rect_Type1 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function 231  DIRECT x_1 4826 > h_DIRECT x_14826232  INDIRECT x_1 4827 > h_INDIRECT x_14827233  EXT_INDIRECT x_1 4828 > h_EXT_INDIRECT x_14828234  REGISTER x_1 4829 > h_REGISTER x_14829223  DIRECT x_183 > h_DIRECT x_183 224  INDIRECT x_184 > h_INDIRECT x_184 225  EXT_INDIRECT x_185 > h_EXT_INDIRECT x_185 226  REGISTER x_186 > h_REGISTER x_186 235 227  ACC_A > h_ACC_A 236 228  ACC_B > h_ACC_B 237 229  DPTR > h_DPTR 238  DATA x_1 4830 > h_DATA x_14830239  DATA16 x_1 4831 > h_DATA16 x_14831230  DATA x_187 > h_DATA x_187 231  DATA16 x_188 > h_DATA16 x_188 240 232  ACC_DPTR > h_ACC_DPTR 241 233  ACC_PC > h_ACC_PC … … 243 235  INDIRECT_DPTR > h_INDIRECT_DPTR 244 236  CARRY > h_CARRY 245  BIT_ADDR x_1 4832 > h_BIT_ADDR x_14832246  N_BIT_ADDR x_1 4833 > h_N_BIT_ADDR x_14833247  RELATIVE x_1 4834 > h_RELATIVE x_14834248  ADDR11 x_1 4835 > h_ADDR11 x_14835249  ADDR16 x_1 4836 > h_ADDR16 x_14836237  BIT_ADDR x_189 > h_BIT_ADDR x_189 238  N_BIT_ADDR x_190 > h_N_BIT_ADDR x_190 239  RELATIVE x_191 > h_RELATIVE x_191 240  ADDR11 x_192 > h_ADDR11 x_192 241  ADDR16 x_193 > h_ADDR16 x_193 250 242 251 243 (** val addressing_mode_rect_Type0 : … … 257 249 > 'a1) > addressing_mode > 'a1 **) 258 250 let rec addressing_mode_rect_Type0 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function 259  DIRECT x_ 14857 > h_DIRECT x_14857260  INDIRECT x_ 14858 > h_INDIRECT x_14858261  EXT_INDIRECT x_ 14859 > h_EXT_INDIRECT x_14859262  REGISTER x_ 14860 > h_REGISTER x_14860251  DIRECT x_214 > h_DIRECT x_214 252  INDIRECT x_215 > h_INDIRECT x_215 253  EXT_INDIRECT x_216 > h_EXT_INDIRECT x_216 254  REGISTER x_217 > h_REGISTER x_217 263 255  ACC_A > h_ACC_A 264 256  ACC_B > h_ACC_B 265 257  DPTR > h_DPTR 266  DATA x_ 14861 > h_DATA x_14861267  DATA16 x_ 14862 > h_DATA16 x_14862258  DATA x_218 > h_DATA x_218 259  DATA16 x_219 > h_DATA16 x_219 268 260  ACC_DPTR > h_ACC_DPTR 269 261  ACC_PC > h_ACC_PC … … 271 263  INDIRECT_DPTR > h_INDIRECT_DPTR 272 264  CARRY > h_CARRY 273  BIT_ADDR x_ 14863 > h_BIT_ADDR x_14863274  N_BIT_ADDR x_ 14864 > h_N_BIT_ADDR x_14864275  RELATIVE x_ 14865 > h_RELATIVE x_14865276  ADDR11 x_ 14866 > h_ADDR11 x_14866277  ADDR16 x_ 14867 > h_ADDR16 x_14867265  BIT_ADDR x_220 > h_BIT_ADDR x_220 266  N_BIT_ADDR x_221 > h_N_BIT_ADDR x_221 267  RELATIVE x_222 > h_RELATIVE x_222 268  ADDR11 x_223 > h_ADDR11 x_223 269  ADDR16 x_224 > h_ADDR16 x_224 278 270 279 271 (** val addressing_mode_inv_rect_Type4 : … … 1932 1924 Nat.nat > addressing_mode_tag Vector.vector > (addressing_mode > __ > 1933 1925 'a1) > subaddressing_mode > 'a1 **) 1934 let rec subaddressing_mode_rect_Type4 n l h_mk_subaddressing_mode x_ 15335=1935 let subaddressing_modeel = x_ 15335in1926 let rec subaddressing_mode_rect_Type4 n l h_mk_subaddressing_mode x_692 = 1927 let subaddressing_modeel = x_692 in 1936 1928 h_mk_subaddressing_mode subaddressing_modeel __ 1937 1929 … … 1939 1931 Nat.nat > addressing_mode_tag Vector.vector > (addressing_mode > __ > 1940 1932 'a1) > subaddressing_mode > 'a1 **) 1941 let rec subaddressing_mode_rect_Type5 n l h_mk_subaddressing_mode x_ 15337=1942 let subaddressing_modeel = x_ 15337in1933 let rec subaddressing_mode_rect_Type5 n l h_mk_subaddressing_mode x_694 = 1934 let subaddressing_modeel = x_694 in 1943 1935 h_mk_subaddressing_mode subaddressing_modeel __ 1944 1936 … … 1946 1938 Nat.nat > addressing_mode_tag Vector.vector > (addressing_mode > __ > 1947 1939 'a1) > subaddressing_mode > 'a1 **) 1948 let rec subaddressing_mode_rect_Type3 n l h_mk_subaddressing_mode x_ 15339=1949 let subaddressing_modeel = x_ 15339in1940 let rec subaddressing_mode_rect_Type3 n l h_mk_subaddressing_mode x_696 = 1941 let subaddressing_modeel = x_696 in 1950 1942 h_mk_subaddressing_mode subaddressing_modeel __ 1951 1943 … … 1953 1945 Nat.nat > addressing_mode_tag Vector.vector > (addressing_mode > __ > 1954 1946 'a1) > subaddressing_mode > 'a1 **) 1955 let rec subaddressing_mode_rect_Type2 n l h_mk_subaddressing_mode x_ 15341=1956 let subaddressing_modeel = x_ 15341in1947 let rec subaddressing_mode_rect_Type2 n l h_mk_subaddressing_mode x_698 = 1948 let subaddressing_modeel = x_698 in 1957 1949 h_mk_subaddressing_mode subaddressing_modeel __ 1958 1950 … … 1960 1952 Nat.nat > addressing_mode_tag Vector.vector > (addressing_mode > __ > 1961 1953 'a1) > subaddressing_mode > 'a1 **) 1962 let rec subaddressing_mode_rect_Type1 n l h_mk_subaddressing_mode x_ 15343=1963 let subaddressing_modeel = x_ 15343in1954 let rec subaddressing_mode_rect_Type1 n l h_mk_subaddressing_mode x_700 = 1955 let subaddressing_modeel = x_700 in 1964 1956 h_mk_subaddressing_mode subaddressing_modeel __ 1965 1957 … … 1967 1959 Nat.nat > addressing_mode_tag Vector.vector > (addressing_mode > __ > 1968 1960 'a1) > subaddressing_mode > 'a1 **) 1969 let rec subaddressing_mode_rect_Type0 n l h_mk_subaddressing_mode x_ 15345=1970 let subaddressing_modeel = x_ 15345in1961 let rec subaddressing_mode_rect_Type0 n l h_mk_subaddressing_mode x_702 = 1962 let subaddressing_modeel = x_702 in 1971 1963 h_mk_subaddressing_mode subaddressing_modeel __ 1972 1964 … … 2139 2131 'a2 > 'a2 > 'a1 preinstruction > 'a2 **) 2140 2132 let rec preinstruction_rect_Type4 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP = function 2141  ADD (x_ 15445, x_15444) > h_ADD x_15445 x_154442142  ADDC (x_ 15447, x_15446) > h_ADDC x_15447 x_154462143  SUBB (x_ 15449, x_15448) > h_SUBB x_15449 x_154482144  INC x_ 15450 > h_INC x_154502145  DEC x_ 15451 > h_DEC x_154512146  MUL (x_ 15453, x_15452) > h_MUL x_15453 x_154522147  DIV (x_ 15455, x_15454) > h_DIV x_15455 x_154542148  DA x_ 15456 > h_DA x_154562149  JC x_ 15457 > h_JC x_154572150  JNC x_ 15458 > h_JNC x_154582151  JB (x_ 15460, x_15459) > h_JB x_15460 x_154592152  JNB (x_ 15462, x_15461) > h_JNB x_15462 x_154612153  JBC (x_ 15464, x_15463) > h_JBC x_15464 x_154632154  JZ x_ 15465 > h_JZ x_154652155  JNZ x_ 15466 > h_JNZ x_154662156  CJNE (x_ 15468, x_15467) > h_CJNE x_15468 x_154672157  DJNZ (x_ 15470, x_15469) > h_DJNZ x_15470 x_154692158  ANL x_ 15471 > h_ANL x_154712159  ORL x_ 15472 > h_ORL x_154722160  XRL x_ 15473 > h_XRL x_154732161  CLR x_ 15474 > h_CLR x_154742162  CPL x_ 15475 > h_CPL x_154752163  RL x_ 15476 > h_RL x_154762164  RLC x_ 15477 > h_RLC x_154772165  RR x_ 15478 > h_RR x_154782166  RRC x_ 15479 > h_RRC x_154792167  SWAP x_ 15480 > h_SWAP x_154802168  MOV x_ 15481 > h_MOV x_154812169  MOVX x_ 15482 > h_MOVX x_154822170  SETB x_ 15483 > h_SETB x_154832171  PUSH x_ 15484 > h_PUSH x_154842172  POP x_ 15485 > h_POP x_154852173  XCH (x_ 15487, x_15486) > h_XCH x_15487 x_154862174  XCHD (x_ 15489, x_15488) > h_XCHD x_15489 x_154882133  ADD (x_802, x_801) > h_ADD x_802 x_801 2134  ADDC (x_804, x_803) > h_ADDC x_804 x_803 2135  SUBB (x_806, x_805) > h_SUBB x_806 x_805 2136  INC x_807 > h_INC x_807 2137  DEC x_808 > h_DEC x_808 2138  MUL (x_810, x_809) > h_MUL x_810 x_809 2139  DIV (x_812, x_811) > h_DIV x_812 x_811 2140  DA x_813 > h_DA x_813 2141  JC x_814 > h_JC x_814 2142  JNC x_815 > h_JNC x_815 2143  JB (x_817, x_816) > h_JB x_817 x_816 2144  JNB (x_819, x_818) > h_JNB x_819 x_818 2145  JBC (x_821, x_820) > h_JBC x_821 x_820 2146  JZ x_822 > h_JZ x_822 2147  JNZ x_823 > h_JNZ x_823 2148  CJNE (x_825, x_824) > h_CJNE x_825 x_824 2149  DJNZ (x_827, x_826) > h_DJNZ x_827 x_826 2150  ANL x_828 > h_ANL x_828 2151  ORL x_829 > h_ORL x_829 2152  XRL x_830 > h_XRL x_830 2153  CLR x_831 > h_CLR x_831 2154  CPL x_832 > h_CPL x_832 2155  RL x_833 > h_RL x_833 2156  RLC x_834 > h_RLC x_834 2157  RR x_835 > h_RR x_835 2158  RRC x_836 > h_RRC x_836 2159  SWAP x_837 > h_SWAP x_837 2160  MOV x_838 > h_MOV x_838 2161  MOVX x_839 > h_MOVX x_839 2162  SETB x_840 > h_SETB x_840 2163  PUSH x_841 > h_PUSH x_841 2164  POP x_842 > h_POP x_842 2165  XCH (x_844, x_843) > h_XCH x_844 x_843 2166  XCHD (x_846, x_845) > h_XCHD x_846 x_845 2175 2167  RET > h_RET 2176 2168  RETI > h_RETI … … 2213 2205 'a2 > 'a2 > 'a1 preinstruction > 'a2 **) 2214 2206 let rec preinstruction_rect_Type5 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP = function 2215  ADD (x_ 15529, x_15528) > h_ADD x_15529 x_155282216  ADDC (x_ 15531, x_15530) > h_ADDC x_15531 x_155302217  SUBB (x_ 15533, x_15532) > h_SUBB x_15533 x_155322218  INC x_ 15534 > h_INC x_155342219  DEC x_ 15535 > h_DEC x_155352220  MUL (x_ 15537, x_15536) > h_MUL x_15537 x_155362221  DIV (x_ 15539, x_15538) > h_DIV x_15539 x_155382222  DA x_ 15540 > h_DA x_155402223  JC x_ 15541 > h_JC x_155412224  JNC x_ 15542 > h_JNC x_155422225  JB (x_ 15544, x_15543) > h_JB x_15544 x_155432226  JNB (x_ 15546, x_15545) > h_JNB x_15546 x_155452227  JBC (x_ 15548, x_15547) > h_JBC x_15548 x_155472228  JZ x_ 15549 > h_JZ x_155492229  JNZ x_ 15550 > h_JNZ x_155502230  CJNE (x_ 15552, x_15551) > h_CJNE x_15552 x_155512231  DJNZ (x_ 15554, x_15553) > h_DJNZ x_15554 x_155532232  ANL x_ 15555 > h_ANL x_155552233  ORL x_ 15556 > h_ORL x_155562234  XRL x_ 15557 > h_XRL x_155572235  CLR x_ 15558 > h_CLR x_155582236  CPL x_ 15559 > h_CPL x_155592237  RL x_ 15560 > h_RL x_155602238  RLC x_ 15561 > h_RLC x_155612239  RR x_ 15562 > h_RR x_155622240  RRC x_ 15563 > h_RRC x_155632241  SWAP x_ 15564 > h_SWAP x_155642242  MOV x_ 15565 > h_MOV x_155652243  MOVX x_ 15566 > h_MOVX x_155662244  SETB x_ 15567 > h_SETB x_155672245  PUSH x_ 15568 > h_PUSH x_155682246  POP x_ 15569 > h_POP x_155692247  XCH (x_ 15571, x_15570) > h_XCH x_15571 x_155702248  XCHD (x_ 15573, x_15572) > h_XCHD x_15573 x_155722207  ADD (x_886, x_885) > h_ADD x_886 x_885 2208  ADDC (x_888, x_887) > h_ADDC x_888 x_887 2209  SUBB (x_890, x_889) > h_SUBB x_890 x_889 2210  INC x_891 > h_INC x_891 2211  DEC x_892 > h_DEC x_892 2212  MUL (x_894, x_893) > h_MUL x_894 x_893 2213  DIV (x_896, x_895) > h_DIV x_896 x_895 2214  DA x_897 > h_DA x_897 2215  JC x_898 > h_JC x_898 2216  JNC x_899 > h_JNC x_899 2217  JB (x_901, x_900) > h_JB x_901 x_900 2218  JNB (x_903, x_902) > h_JNB x_903 x_902 2219  JBC (x_905, x_904) > h_JBC x_905 x_904 2220  JZ x_906 > h_JZ x_906 2221  JNZ x_907 > h_JNZ x_907 2222  CJNE (x_909, x_908) > h_CJNE x_909 x_908 2223  DJNZ (x_911, x_910) > h_DJNZ x_911 x_910 2224  ANL x_912 > h_ANL x_912 2225  ORL x_913 > h_ORL x_913 2226  XRL x_914 > h_XRL x_914 2227  CLR x_915 > h_CLR x_915 2228  CPL x_916 > h_CPL x_916 2229  RL x_917 > h_RL x_917 2230  RLC x_918 > h_RLC x_918 2231  RR x_919 > h_RR x_919 2232  RRC x_920 > h_RRC x_920 2233  SWAP x_921 > h_SWAP x_921 2234  MOV x_922 > h_MOV x_922 2235  MOVX x_923 > h_MOVX x_923 2236  SETB x_924 > h_SETB x_924 2237  PUSH x_925 > h_PUSH x_925 2238  POP x_926 > h_POP x_926 2239  XCH (x_928, x_927) > h_XCH x_928 x_927 2240  XCHD (x_930, x_929) > h_XCHD x_930 x_929 2249 2241  RET > h_RET 2250 2242  RETI > h_RETI … … 2287 2279 'a2 > 'a2 > 'a1 preinstruction > 'a2 **) 2288 2280 let rec preinstruction_rect_Type3 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP = function 2289  ADD (x_ 15613, x_15612) > h_ADD x_15613 x_156122290  ADDC (x_ 15615, x_15614) > h_ADDC x_15615 x_156142291  SUBB (x_ 15617, x_15616) > h_SUBB x_15617 x_156162292  INC x_ 15618 > h_INC x_156182293  DEC x_ 15619 > h_DEC x_156192294  MUL (x_ 15621, x_15620) > h_MUL x_15621 x_156202295  DIV (x_ 15623, x_15622) > h_DIV x_15623 x_156222296  DA x_ 15624 > h_DA x_156242297  JC x_ 15625 > h_JC x_156252298  JNC x_ 15626 > h_JNC x_156262299  JB (x_ 15628, x_15627) > h_JB x_15628 x_156272300  JNB (x_ 15630, x_15629) > h_JNB x_15630 x_156292301  JBC (x_ 15632, x_15631) > h_JBC x_15632 x_156312302  JZ x_ 15633 > h_JZ x_156332303  JNZ x_ 15634 > h_JNZ x_156342304  CJNE (x_ 15636, x_15635) > h_CJNE x_15636 x_156352305  DJNZ (x_ 15638, x_15637) > h_DJNZ x_15638 x_156372306  ANL x_ 15639 > h_ANL x_156392307  ORL x_ 15640 > h_ORL x_156402308  XRL x_ 15641 > h_XRL x_156412309  CLR x_ 15642 > h_CLR x_156422310  CPL x_1 5643 > h_CPL x_156432311  RL x_1 5644 > h_RL x_156442312  RLC x_1 5645 > h_RLC x_156452313  RR x_1 5646 > h_RR x_156462314  RRC x_1 5647 > h_RRC x_156472315  SWAP x_1 5648 > h_SWAP x_156482316  MOV x_1 5649 > h_MOV x_156492317  MOVX x_1 5650 > h_MOVX x_156502318  SETB x_1 5651 > h_SETB x_156512319  PUSH x_1 5652 > h_PUSH x_156522320  POP x_1 5653 > h_POP x_156532321  XCH (x_1 5655, x_15654) > h_XCH x_15655 x_156542322  XCHD (x_1 5657, x_15656) > h_XCHD x_15657 x_156562281  ADD (x_970, x_969) > h_ADD x_970 x_969 2282  ADDC (x_972, x_971) > h_ADDC x_972 x_971 2283  SUBB (x_974, x_973) > h_SUBB x_974 x_973 2284  INC x_975 > h_INC x_975 2285  DEC x_976 > h_DEC x_976 2286  MUL (x_978, x_977) > h_MUL x_978 x_977 2287  DIV (x_980, x_979) > h_DIV x_980 x_979 2288  DA x_981 > h_DA x_981 2289  JC x_982 > h_JC x_982 2290  JNC x_983 > h_JNC x_983 2291  JB (x_985, x_984) > h_JB x_985 x_984 2292  JNB (x_987, x_986) > h_JNB x_987 x_986 2293  JBC (x_989, x_988) > h_JBC x_989 x_988 2294  JZ x_990 > h_JZ x_990 2295  JNZ x_991 > h_JNZ x_991 2296  CJNE (x_993, x_992) > h_CJNE x_993 x_992 2297  DJNZ (x_995, x_994) > h_DJNZ x_995 x_994 2298  ANL x_996 > h_ANL x_996 2299  ORL x_997 > h_ORL x_997 2300  XRL x_998 > h_XRL x_998 2301  CLR x_999 > h_CLR x_999 2302  CPL x_1000 > h_CPL x_1000 2303  RL x_1001 > h_RL x_1001 2304  RLC x_1002 > h_RLC x_1002 2305  RR x_1003 > h_RR x_1003 2306  RRC x_1004 > h_RRC x_1004 2307  SWAP x_1005 > h_SWAP x_1005 2308  MOV x_1006 > h_MOV x_1006 2309  MOVX x_1007 > h_MOVX x_1007 2310  SETB x_1008 > h_SETB x_1008 2311  PUSH x_1009 > h_PUSH x_1009 2312  POP x_1010 > h_POP x_1010 2313  XCH (x_1012, x_1011) > h_XCH x_1012 x_1011 2314  XCHD (x_1014, x_1013) > h_XCHD x_1014 x_1013 2323 2315  RET > h_RET 2324 2316  RETI > h_RETI … … 2361 2353 'a2 > 'a2 > 'a1 preinstruction > 'a2 **) 2362 2354 let rec preinstruction_rect_Type2 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP = function 2363  ADD (x_1 5697, x_15696) > h_ADD x_15697 x_156962364  ADDC (x_1 5699, x_15698) > h_ADDC x_15699 x_156982365  SUBB (x_1 5701, x_15700) > h_SUBB x_15701 x_157002366  INC x_1 5702 > h_INC x_157022367  DEC x_1 5703 > h_DEC x_157032368  MUL (x_1 5705, x_15704) > h_MUL x_15705 x_157042369  DIV (x_1 5707, x_15706) > h_DIV x_15707 x_157062370  DA x_1 5708 > h_DA x_157082371  JC x_1 5709 > h_JC x_157092372  JNC x_1 5710 > h_JNC x_157102373  JB (x_1 5712, x_15711) > h_JB x_15712 x_157112374  JNB (x_1 5714, x_15713) > h_JNB x_15714 x_157132375  JBC (x_1 5716, x_15715) > h_JBC x_15716 x_157152376  JZ x_1 5717 > h_JZ x_157172377  JNZ x_1 5718 > h_JNZ x_157182378  CJNE (x_1 5720, x_15719) > h_CJNE x_15720 x_157192379  DJNZ (x_1 5722, x_15721) > h_DJNZ x_15722 x_157212380  ANL x_1 5723 > h_ANL x_157232381  ORL x_1 5724 > h_ORL x_157242382  XRL x_1 5725 > h_XRL x_157252383  CLR x_1 5726 > h_CLR x_157262384  CPL x_1 5727 > h_CPL x_157272385  RL x_1 5728 > h_RL x_157282386  RLC x_1 5729 > h_RLC x_157292387  RR x_1 5730 > h_RR x_157302388  RRC x_1 5731 > h_RRC x_157312389  SWAP x_1 5732 > h_SWAP x_157322390  MOV x_1 5733 > h_MOV x_157332391  MOVX x_1 5734 > h_MOVX x_157342392  SETB x_1 5735 > h_SETB x_157352393  PUSH x_1 5736 > h_PUSH x_157362394  POP x_1 5737 > h_POP x_157372395  XCH (x_1 5739, x_15738) > h_XCH x_15739 x_157382396  XCHD (x_1 5741, x_15740) > h_XCHD x_15741 x_157402355  ADD (x_1054, x_1053) > h_ADD x_1054 x_1053 2356  ADDC (x_1056, x_1055) > h_ADDC x_1056 x_1055 2357  SUBB (x_1058, x_1057) > h_SUBB x_1058 x_1057 2358  INC x_1059 > h_INC x_1059 2359  DEC x_1060 > h_DEC x_1060 2360  MUL (x_1062, x_1061) > h_MUL x_1062 x_1061 2361  DIV (x_1064, x_1063) > h_DIV x_1064 x_1063 2362  DA x_1065 > h_DA x_1065 2363  JC x_1066 > h_JC x_1066 2364  JNC x_1067 > h_JNC x_1067 2365  JB (x_1069, x_1068) > h_JB x_1069 x_1068 2366  JNB (x_1071, x_1070) > h_JNB x_1071 x_1070 2367  JBC (x_1073, x_1072) > h_JBC x_1073 x_1072 2368  JZ x_1074 > h_JZ x_1074 2369  JNZ x_1075 > h_JNZ x_1075 2370  CJNE (x_1077, x_1076) > h_CJNE x_1077 x_1076 2371  DJNZ (x_1079, x_1078) > h_DJNZ x_1079 x_1078 2372  ANL x_1080 > h_ANL x_1080 2373  ORL x_1081 > h_ORL x_1081 2374  XRL x_1082 > h_XRL x_1082 2375  CLR x_1083 > h_CLR x_1083 2376  CPL x_1084 > h_CPL x_1084 2377  RL x_1085 > h_RL x_1085 2378  RLC x_1086 > h_RLC x_1086 2379  RR x_1087 > h_RR x_1087 2380  RRC x_1088 > h_RRC x_1088 2381  SWAP x_1089 > h_SWAP x_1089 2382  MOV x_1090 > h_MOV x_1090 2383  MOVX x_1091 > h_MOVX x_1091 2384  SETB x_1092 > h_SETB x_1092 2385  PUSH x_1093 > h_PUSH x_1093 2386  POP x_1094 > h_POP x_1094 2387  XCH (x_1096, x_1095) > h_XCH x_1096 x_1095 2388  XCHD (x_1098, x_1097) > h_XCHD x_1098 x_1097 2397 2389  RET > h_RET 2398 2390  RETI > h_RETI … … 2435 2427 'a2 > 'a2 > 'a1 preinstruction > 'a2 **) 2436 2428 let rec preinstruction_rect_Type1 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP = function 2437  ADD (x_1 5781, x_15780) > h_ADD x_15781 x_157802438  ADDC (x_1 5783, x_15782) > h_ADDC x_15783 x_157822439  SUBB (x_1 5785, x_15784) > h_SUBB x_15785 x_157842440  INC x_1 5786 > h_INC x_157862441  DEC x_1 5787 > h_DEC x_157872442  MUL (x_1 5789, x_15788) > h_MUL x_15789 x_157882443  DIV (x_1 5791, x_15790) > h_DIV x_15791 x_157902444  DA x_1 5792 > h_DA x_157922445  JC x_1 5793 > h_JC x_157932446  JNC x_1 5794 > h_JNC x_157942447  JB (x_1 5796, x_15795) > h_JB x_15796 x_157952448  JNB (x_1 5798, x_15797) > h_JNB x_15798 x_157972449  JBC (x_1 5800, x_15799) > h_JBC x_15800 x_157992450  JZ x_1 5801 > h_JZ x_158012451  JNZ x_1 5802 > h_JNZ x_158022452  CJNE (x_1 5804, x_15803) > h_CJNE x_15804 x_158032453  DJNZ (x_1 5806, x_15805) > h_DJNZ x_15806 x_158052454  ANL x_1 5807 > h_ANL x_158072455  ORL x_1 5808 > h_ORL x_158082456  XRL x_1 5809 > h_XRL x_158092457  CLR x_1 5810 > h_CLR x_158102458  CPL x_1 5811 > h_CPL x_158112459  RL x_1 5812 > h_RL x_158122460  RLC x_1 5813 > h_RLC x_158132461  RR x_1 5814 > h_RR x_158142462  RRC x_1 5815 > h_RRC x_158152463  SWAP x_1 5816 > h_SWAP x_158162464  MOV x_1 5817 > h_MOV x_158172465  MOVX x_1 5818 > h_MOVX x_158182466  SETB x_1 5819 > h_SETB x_158192467  PUSH x_1 5820 > h_PUSH x_158202468  POP x_1 5821 > h_POP x_158212469  XCH (x_1 5823, x_15822) > h_XCH x_15823 x_158222470  XCHD (x_1 5825, x_15824) > h_XCHD x_15825 x_158242429  ADD (x_1138, x_1137) > h_ADD x_1138 x_1137 2430  ADDC (x_1140, x_1139) > h_ADDC x_1140 x_1139 2431  SUBB (x_1142, x_1141) > h_SUBB x_1142 x_1141 2432  INC x_1143 > h_INC x_1143 2433  DEC x_1144 > h_DEC x_1144 2434  MUL (x_1146, x_1145) > h_MUL x_1146 x_1145 2435  DIV (x_1148, x_1147) > h_DIV x_1148 x_1147 2436  DA x_1149 > h_DA x_1149 2437  JC x_1150 > h_JC x_1150 2438  JNC x_1151 > h_JNC x_1151 2439  JB (x_1153, x_1152) > h_JB x_1153 x_1152 2440  JNB (x_1155, x_1154) > h_JNB x_1155 x_1154 2441  JBC (x_1157, x_1156) > h_JBC x_1157 x_1156 2442  JZ x_1158 > h_JZ x_1158 2443  JNZ x_1159 > h_JNZ x_1159 2444  CJNE (x_1161, x_1160) > h_CJNE x_1161 x_1160 2445  DJNZ (x_1163, x_1162) > h_DJNZ x_1163 x_1162 2446  ANL x_1164 > h_ANL x_1164 2447  ORL x_1165 > h_ORL x_1165 2448  XRL x_1166 > h_XRL x_1166 2449  CLR x_1167 > h_CLR x_1167 2450  CPL x_1168 > h_CPL x_1168 2451  RL x_1169 > h_RL x_1169 2452  RLC x_1170 > h_RLC x_1170 2453  RR x_1171 > h_RR x_1171 2454  RRC x_1172 > h_RRC x_1172 2455  SWAP x_1173 > h_SWAP x_1173 2456  MOV x_1174 > h_MOV x_1174 2457  MOVX x_1175 > h_MOVX x_1175 2458  SETB x_1176 > h_SETB x_1176 2459  PUSH x_1177 > h_PUSH x_1177 2460  POP x_1178 > h_POP x_1178 2461  XCH (x_1180, x_1179) > h_XCH x_1180 x_1179 2462  XCHD (x_1182, x_1181) > h_XCHD x_1182 x_1181 2471 2463  RET > h_RET 2472 2464  RETI > h_RETI … … 2509 2501 'a2 > 'a2 > 'a1 preinstruction > 'a2 **) 2510 2502 let rec preinstruction_rect_Type0 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP = function 2511  ADD (x_1 5865, x_15864) > h_ADD x_15865 x_158642512  ADDC (x_1 5867, x_15866) > h_ADDC x_15867 x_158662513  SUBB (x_1 5869, x_15868) > h_SUBB x_15869 x_158682514  INC x_1 5870 > h_INC x_158702515  DEC x_1 5871 > h_DEC x_158712516  MUL (x_1 5873, x_15872) > h_MUL x_15873 x_158722517  DIV (x_1 5875, x_15874) > h_DIV x_15875 x_158742518  DA x_1 5876 > h_DA x_158762519  JC x_1 5877 > h_JC x_158772520  JNC x_1 5878 > h_JNC x_158782521  JB (x_1 5880, x_15879) > h_JB x_15880 x_158792522  JNB (x_1 5882, x_15881) > h_JNB x_15882 x_158812523  JBC (x_1 5884, x_15883) > h_JBC x_15884 x_158832524  JZ x_1 5885 > h_JZ x_158852525  JNZ x_1 5886 > h_JNZ x_158862526  CJNE (x_1 5888, x_15887) > h_CJNE x_15888 x_158872527  DJNZ (x_1 5890, x_15889) > h_DJNZ x_15890 x_158892528  ANL x_1 5891 > h_ANL x_158912529  ORL x_1 5892 > h_ORL x_158922530  XRL x_1 5893 > h_XRL x_158932531  CLR x_1 5894 > h_CLR x_158942532  CPL x_1 5895 > h_CPL x_158952533  RL x_1 5896 > h_RL x_158962534  RLC x_1 5897 > h_RLC x_158972535  RR x_1 5898 > h_RR x_158982536  RRC x_1 5899 > h_RRC x_158992537  SWAP x_1 5900 > h_SWAP x_159002538  MOV x_1 5901 > h_MOV x_159012539  MOVX x_1 5902 > h_MOVX x_159022540  SETB x_1 5903 > h_SETB x_159032541  PUSH x_1 5904 > h_PUSH x_159042542  POP x_1 5905 > h_POP x_159052543  XCH (x_1 5907, x_15906) > h_XCH x_15907 x_159062544  XCHD (x_1 5909, x_15908) > h_XCHD x_15909 x_159082503  ADD (x_1222, x_1221) > h_ADD x_1222 x_1221 2504  ADDC (x_1224, x_1223) > h_ADDC x_1224 x_1223 2505  SUBB (x_1226, x_1225) > h_SUBB x_1226 x_1225 2506  INC x_1227 > h_INC x_1227 2507  DEC x_1228 > h_DEC x_1228 2508  MUL (x_1230, x_1229) > h_MUL x_1230 x_1229 2509  DIV (x_1232, x_1231) > h_DIV x_1232 x_1231 2510  DA x_1233 > h_DA x_1233 2511  JC x_1234 > h_JC x_1234 2512  JNC x_1235 > h_JNC x_1235 2513  JB (x_1237, x_1236) > h_JB x_1237 x_1236 2514  JNB (x_1239, x_1238) > h_JNB x_1239 x_1238 2515  JBC (x_1241, x_1240) > h_JBC x_1241 x_1240 2516  JZ x_1242 > h_JZ x_1242 2517  JNZ x_1243 > h_JNZ x_1243 2518  CJNE (x_1245, x_1244) > h_CJNE x_1245 x_1244 2519  DJNZ (x_1247, x_1246) > h_DJNZ x_1247 x_1246 2520  ANL x_1248 > h_ANL x_1248 2521  ORL x_1249 > h_ORL x_1249 2522  XRL x_1250 > h_XRL x_1250 2523  CLR x_1251 > h_CLR x_1251 2524  CPL x_1252 > h_CPL x_1252 2525  RL x_1253 > h_RL x_1253 2526  RLC x_1254 > h_RLC x_1254 2527  RR x_1255 > h_RR x_1255 2528  RRC x_1256 > h_RRC x_1256 2529  SWAP x_1257 > h_SWAP x_1257 2530  MOV x_1258 > h_MOV x_1258 2531  MOVX x_1259 > h_MOVX x_1259 2532  SETB x_1260 > h_SETB x_1260 2533  PUSH x_1261 > h_PUSH x_1261 2534  POP x_1262 > h_POP x_1262 2535  XCH (x_1264, x_1263) > h_XCH x_1264 x_1263 2536  XCHD (x_1266, x_1265) > h_XCHD x_1266 x_1265 2545 2537  RET > h_RET 2546 2538  RETI > h_RETI … … 4866 4858 preinstruction > 'a1) > instruction > 'a1 **) 4867 4859 let rec instruction_rect_Type4 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_JMP h_MOVC h_RealInstruction = function 4868  ACALL x_1 6470 > h_ACALL x_164704869  LCALL x_1 6471 > h_LCALL x_164714870  AJMP x_1 6472 > h_AJMP x_164724871  LJMP x_1 6473 > h_LJMP x_164734872  SJMP x_1 6474 > h_SJMP x_164744873  JMP x_1 6475 > h_JMP x_164754874  MOVC (x_1 6477, x_16476) > h_MOVC x_16477 x_164764875  RealInstruction x_1 6478 > h_RealInstruction x_164784860  ACALL x_1827 > h_ACALL x_1827 4861  LCALL x_1828 > h_LCALL x_1828 4862  AJMP x_1829 > h_AJMP x_1829 4863  LJMP x_1830 > h_LJMP x_1830 4864  SJMP x_1831 > h_SJMP x_1831 4865  JMP x_1832 > h_JMP x_1832 4866  MOVC (x_1834, x_1833) > h_MOVC x_1834 x_1833 4867  RealInstruction x_1835 > h_RealInstruction x_1835 4876 4868 4877 4869 (** val instruction_rect_Type5 : … … 4882 4874 preinstruction > 'a1) > instruction > 'a1 **) 4883 4875 let rec instruction_rect_Type5 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_JMP h_MOVC h_RealInstruction = function 4884  ACALL x_1 6488 > h_ACALL x_164884885  LCALL x_1 6489 > h_LCALL x_164894886  AJMP x_1 6490 > h_AJMP x_164904887  LJMP x_1 6491 > h_LJMP x_164914888  SJMP x_1 6492 > h_SJMP x_164924889  JMP x_1 6493 > h_JMP x_164934890  MOVC (x_1 6495, x_16494) > h_MOVC x_16495 x_164944891  RealInstruction x_1 6496 > h_RealInstruction x_164964876  ACALL x_1845 > h_ACALL x_1845 4877  LCALL x_1846 > h_LCALL x_1846 4878  AJMP x_1847 > h_AJMP x_1847 4879  LJMP x_1848 > h_LJMP x_1848 4880  SJMP x_1849 > h_SJMP x_1849 4881  JMP x_1850 > h_JMP x_1850 4882  MOVC (x_1852, x_1851) > h_MOVC x_1852 x_1851 4883  RealInstruction x_1853 > h_RealInstruction x_1853 4892 4884 4893 4885 (** val instruction_rect_Type3 : … … 4898 4890 preinstruction > 'a1) > instruction > 'a1 **) 4899 4891 let rec instruction_rect_Type3 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_JMP h_MOVC h_RealInstruction = function 4900  ACALL x_1 6506 > h_ACALL x_165064901  LCALL x_1 6507 > h_LCALL x_165074902  AJMP x_1 6508 > h_AJMP x_165084903  LJMP x_1 6509 > h_LJMP x_165094904  SJMP x_1 6510 > h_SJMP x_165104905  JMP x_1 6511 > h_JMP x_165114906  MOVC (x_1 6513, x_16512) > h_MOVC x_16513 x_165124907  RealInstruction x_1 6514 > h_RealInstruction x_165144892  ACALL x_1863 > h_ACALL x_1863 4893  LCALL x_1864 > h_LCALL x_1864 4894  AJMP x_1865 > h_AJMP x_1865 4895  LJMP x_1866 > h_LJMP x_1866 4896  SJMP x_1867 > h_SJMP x_1867 4897  JMP x_1868 > h_JMP x_1868 4898  MOVC (x_1870, x_1869) > h_MOVC x_1870 x_1869 4899  RealInstruction x_1871 > h_RealInstruction x_1871 4908 4900 4909 4901 (** val instruction_rect_Type2 : … … 4914 4906 preinstruction > 'a1) > instruction > 'a1 **) 4915 4907 let rec instruction_rect_Type2 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_JMP h_MOVC h_RealInstruction = function 4916  ACALL x_1 6524 > h_ACALL x_165244917  LCALL x_1 6525 > h_LCALL x_165254918  AJMP x_1 6526 > h_AJMP x_165264919  LJMP x_1 6527 > h_LJMP x_165274920  SJMP x_1 6528 > h_SJMP x_165284921  JMP x_1 6529 > h_JMP x_165294922  MOVC (x_1 6531, x_16530) > h_MOVC x_16531 x_165304923  RealInstruction x_1 6532 > h_RealInstruction x_165324908  ACALL x_1881 > h_ACALL x_1881 4909  LCALL x_1882 > h_LCALL x_1882 4910  AJMP x_1883 > h_AJMP x_1883 4911  LJMP x_1884 > h_LJMP x_1884 4912  SJMP x_1885 > h_SJMP x_1885 4913  JMP x_1886 > h_JMP x_1886 4914  MOVC (x_1888, x_1887) > h_MOVC x_1888 x_1887 4915  RealInstruction x_1889 > h_RealInstruction x_1889 4924 4916 4925 4917 (** val instruction_rect_Type1 : … … 4930 4922 preinstruction > 'a1) > instruction > 'a1 **) 4931 4923 let rec instruction_rect_Type1 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_JMP h_MOVC h_RealInstruction = function 4932  ACALL x_1 6542 > h_ACALL x_165424933  LCALL x_1 6543 > h_LCALL x_165434934  AJMP x_1 6544 > h_AJMP x_165444935  LJMP x_1 6545 > h_LJMP x_165454936  SJMP x_1 6546 > h_SJMP x_165464937  JMP x_1 6547 > h_JMP x_165474938  MOVC (x_1 6549, x_16548) > h_MOVC x_16549 x_165484939  RealInstruction x_1 6550 > h_RealInstruction x_165504924  ACALL x_1899 > h_ACALL x_1899 4925  LCALL x_1900 > h_LCALL x_1900 4926  AJMP x_1901 > h_AJMP x_1901 4927  LJMP x_1902 > h_LJMP x_1902 4928  SJMP x_1903 > h_SJMP x_1903 4929  JMP x_1904 > h_JMP x_1904 4930  MOVC (x_1906, x_1905) > h_MOVC x_1906 x_1905 4931  RealInstruction x_1907 > h_RealInstruction x_1907 4940 4932 4941 4933 (** val instruction_rect_Type0 : … … 4946 4938 preinstruction > 'a1) > instruction > 'a1 **) 4947 4939 let rec instruction_rect_Type0 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_JMP h_MOVC h_RealInstruction = function 4948  ACALL x_1 6560 > h_ACALL x_165604949  LCALL x_1 6561 > h_LCALL x_165614950  AJMP x_1 6562 > h_AJMP x_165624951  LJMP x_1 6563 > h_LJMP x_165634952  SJMP x_1 6564 > h_SJMP x_165644953  JMP x_1 6565 > h_JMP x_165654954  MOVC (x_1 6567, x_16566) > h_MOVC x_16567 x_165664955  RealInstruction x_1 6568 > h_RealInstruction x_165684940  ACALL x_1917 > h_ACALL x_1917 4941  LCALL x_1918 > h_LCALL x_1918 4942  AJMP x_1919 > h_AJMP x_1919 4943  LJMP x_1920 > h_LJMP x_1920 4944  SJMP x_1921 > h_SJMP x_1921 4945  JMP x_1922 > h_JMP x_1922 4946  MOVC (x_1924, x_1923) > h_MOVC x_1924 x_1923 4947  RealInstruction x_1925 > h_RealInstruction x_1925 4956 4948 4957 4949 (** val instruction_inv_rect_Type4 : … … 5165 5157 > 'a1 **) 5166 5158 let rec pseudo_instruction_rect_Type4 h_Instruction h_Comment h_Cost h_Jmp h_Call h_Mov = function 5167  Instruction x_ 16700 > h_Instruction x_167005168  Comment x_ 16701 > h_Comment x_167015169  Cost x_ 16702 > h_Cost x_167025170  Jmp x_ 16703 > h_Jmp x_167035171  Call x_ 16704 > h_Call x_167045172  Mov (x_ 16706, x_16705) > h_Mov x_16706 x_167055159  Instruction x_2057 > h_Instruction x_2057 5160  Comment x_2058 > h_Comment x_2058 5161  Cost x_2059 > h_Cost x_2059 5162  Jmp x_2060 > h_Jmp x_2060 5163  Call x_2061 > h_Call x_2061 5164  Mov (x_2063, x_2062) > h_Mov x_2063 x_2062 5173 5165 5174 5166 (** val pseudo_instruction_rect_Type5 : … … 5178 5170 > 'a1 **) 5179 5171 let rec pseudo_instruction_rect_Type5 h_Instruction h_Comment h_Cost h_Jmp h_Call h_Mov = function 5180  Instruction x_ 16714 > h_Instruction x_167145181  Comment x_ 16715 > h_Comment x_167155182  Cost x_ 16716 > h_Cost x_167165183  Jmp x_ 16717 > h_Jmp x_167175184  Call x_ 16718 > h_Call x_167185185  Mov (x_ 16720, x_16719) > h_Mov x_16720 x_167195172  Instruction x_2071 > h_Instruction x_2071 5173  Comment x_2072 > h_Comment x_2072 5174  Cost x_2073 > h_Cost x_2073 5175  Jmp x_2074 > h_Jmp x_2074 5176  Call x_2075 > h_Call x_2075 5177  Mov (x_2077, x_2076) > h_Mov x_2077 x_2076 5186 5178 5187 5179 (** val pseudo_instruction_rect_Type3 : … … 5191 5183 > 'a1 **) 5192 5184 let rec pseudo_instruction_rect_Type3 h_Instruction h_Comment h_Cost h_Jmp h_Call h_Mov = function 5193  Instruction x_ 16728 > h_Instruction x_167285194  Comment x_ 16729 > h_Comment x_167295195  Cost x_ 16730 > h_Cost x_167305196  Jmp x_ 16731 > h_Jmp x_167315197  Call x_ 16732 > h_Call x_167325198  Mov (x_ 16734, x_16733) > h_Mov x_16734 x_167335185  Instruction x_2085 > h_Instruction x_2085 5186  Comment x_2086 > h_Comment x_2086 5187  Cost x_2087 > h_Cost x_2087 5188  Jmp x_2088 > h_Jmp x_2088 5189  Call x_2089 > h_Call x_2089 5190  Mov (x_2091, x_2090) > h_Mov x_2091 x_2090 5199 5191 5200 5192 (** val pseudo_instruction_rect_Type2 : … … 5204 5196 > 'a1 **) 5205 5197 let rec pseudo_instruction_rect_Type2 h_Instruction h_Comment h_Cost h_Jmp h_Call h_Mov = function 5206  Instruction x_ 16742 > h_Instruction x_167425207  Comment x_ 16743 > h_Comment x_167435208  Cost x_ 16744 > h_Cost x_167445209  Jmp x_ 16745 > h_Jmp x_167455210  Call x_ 16746 > h_Call x_167465211  Mov (x_ 16748, x_16747) > h_Mov x_16748 x_167475198  Instruction x_2099 > h_Instruction x_2099 5199  Comment x_2100 > h_Comment x_2100 5200  Cost x_2101 > h_Cost x_2101 5201  Jmp x_2102 > h_Jmp x_2102 5202  Call x_2103 > h_Call x_2103 5203  Mov (x_2105, x_2104) > h_Mov x_2105 x_2104 5212 5204 5213 5205 (** val pseudo_instruction_rect_Type1 : … … 5217 5209 > 'a1 **) 5218 5210 let rec pseudo_instruction_rect_Type1 h_Instruction h_Comment h_Cost h_Jmp h_Call h_Mov = function 5219  Instruction x_ 16756 > h_Instruction x_167565220  Comment x_ 16757 > h_Comment x_167575221  Cost x_ 16758 > h_Cost x_167585222  Jmp x_ 16759 > h_Jmp x_167595223  Call x_ 16760 > h_Call x_167605224  Mov (x_ 16762, x_16761) > h_Mov x_16762 x_167615211  Instruction x_2113 > h_Instruction x_2113 5212  Comment x_2114 > h_Comment x_2114 5213  Cost x_2115 > h_Cost x_2115 5214  Jmp x_2116 > h_Jmp x_2116 5215  Call x_2117 > h_Call x_2117 5216  Mov (x_2119, x_2118) > h_Mov x_2119 x_2118 5225 5217 5226 5218 (** val pseudo_instruction_rect_Type0 : … … 5230 5222 > 'a1 **) 5231 5223 let rec pseudo_instruction_rect_Type0 h_Instruction h_Comment h_Cost h_Jmp h_Call h_Mov = function 5232  Instruction x_ 16770 > h_Instruction x_167705233  Comment x_ 16771 > h_Comment x_167715234  Cost x_ 16772 > h_Cost x_167725235  Jmp x_ 16773 > h_Jmp x_167735236  Call x_ 16774 > h_Call x_167745237  Mov (x_ 16776, x_16775) > h_Mov x_16776 x_167755224  Instruction x_2127 > h_Instruction x_2127 5225  Comment x_2128 > h_Comment x_2128 5226  Cost x_2129 > h_Cost x_2129 5227  Jmp x_2130 > h_Jmp x_2130 5228  Call x_2131 > h_Call x_2131 5229  Mov (x_2133, x_2132) > h_Mov x_2133 x_2132 5238 5230 5239 5231 (** val pseudo_instruction_inv_rect_Type4 :
Note: See TracChangeset
for help on using the changeset viewer.