Changeset 1157 for src/RTLabs/test/search.RTLabs.ma
 Timestamp:
 Aug 31, 2011, 12:15:39 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/test/search.RTLabs.ma
r967 r1157 5 5 6 6 7 definition id_search := ident_of_nat 0. 8 definition search9 := 50. 9 definition search8 := 49. 10 definition search7 := 48. 11 definition search6 := 47. 12 definition search50 := 46. 13 definition search5 := 45. 14 definition search49 := 44. 15 definition search48 := 43. 16 definition search47 := 42. 17 definition search46 := 41. 18 definition search45 := 40. 19 definition search44 := 39. 20 definition search43 := 38. 21 definition search42 := 37. 22 definition search41 := 36. 23 definition search40 := 35. 24 definition search4 := 34. 25 definition search39 := 33. 26 definition search38 := 32. 27 definition search37 := 31. 28 definition search36 := 30. 29 definition search35 := 29. 30 definition search34 := 28. 31 definition search33 := 27. 32 definition search32 := 26. 33 definition search31 := 25. 34 definition search30 := 24. 35 definition search3 := 23. 36 definition search29 := 22. 37 definition search28 := 21. 38 definition search27 := 20. 39 definition search26 := 19. 40 definition search25 := 18. 41 definition search24 := 17. 42 definition search23 := 16. 43 definition search22 := 15. 44 definition search21 := 14. 45 definition search20 := 13. 46 definition search2 := 12. 47 definition search19 := 11. 48 definition search18 := 10. 49 definition search17 := 9. 50 definition search16 := 8. 51 definition search15 := 7. 52 definition search14 := 6. 53 definition search13 := 5. 54 definition search12 := 4. 55 definition search11 := 3. 56 definition search10 := 2. 57 definition search1 := 1. 58 definition search0 := 0. 59 definition C_cost1 := costlabel_of_nat 8. 60 definition C_cost8 := costlabel_of_nat 7. 61 definition C_cost6 := costlabel_of_nat 6. 62 definition C_cost7 := costlabel_of_nat 5. 63 definition C_cost4 := costlabel_of_nat 4. 64 definition C_cost5 := costlabel_of_nat 3. 65 definition C_cost2 := costlabel_of_nat 2. 66 definition C_cost3 := costlabel_of_nat 1. 67 definition C_cost0 := costlabel_of_nat 0. 68 69 70 definition pre_search := mk_pre_internal_function 71 (Some ? (pair ?? 6 (ASTint I8 Unsigned))) 72 [(pair ?? 0 (ASTptr Any)); (pair ?? 1 (ASTint I8 Unsigned)); (pair ?? 2 (ASTint I8 Unsigned))] 73 [(pair ?? 3 (ASTint I8 Unsigned)); (pair ?? 4 (ASTint I8 Unsigned)); (pair ?? 5 (ASTint I8 Unsigned)); (pair ?? 6 (ASTint I8 Unsigned)); (pair ?? 7 (ASTint I8 Signed)); (pair ?? 8 (ASTint I8 Signed)); (pair ?? 9 (ASTint I8 Unsigned)); (pair ?? 10 (ASTint I8 Unsigned)); (pair ?? 11 (ASTint I8 Unsigned)); (pair ?? 12 (ASTint I8 Unsigned)); (pair ?? 13 (ASTptr Any)); (pair ?? 14 (ASTint I8 Unsigned)); (pair ?? 15 (ASTint I8 Unsigned)); (pair ?? 16 (ASTint I8 Unsigned)); (pair ?? 17 (ASTint I8 Unsigned)); (pair ?? 18 (ASTint I8 Unsigned)); (pair ?? 19 (ASTint I8 Unsigned)); (pair ?? 20 (ASTptr Any)); (pair ?? 21 (ASTint I8 Unsigned)); (pair ?? 22 (ASTint I8 Unsigned)); (pair ?? 23 (ASTint I8 Unsigned)); (pair ?? 24 (ASTint I8 Unsigned)); (pair ?? 25 (ASTptr Any)); (pair ?? 26 (ASTint I8 Unsigned)); (pair ?? 27 (ASTint I8 Unsigned)); (pair ?? 28 (ASTint I8 Unsigned)); (pair ?? 29 (ASTint I8 Unsigned)); (pair ?? 30 (ASTint I8 Unsigned)); (pair ?? 31 (ASTint I8 Unsigned)); (pair ?? 32 (ASTint I8 Unsigned)); (pair ?? 33 (ASTint I8 Unsigned)); (pair ?? 34 (ASTint I8 Unsigned)); (pair ?? 35 (ASTint I8 Signed))] 7 definition id__div32u := ident_of_nat 0. 8 definition lbl__div32u9 := 15. 9 definition lbl__div32u8 := 14. 10 definition lbl__div32u7 := 13. 11 definition lbl__div32u6 := 12. 12 definition lbl__div32u5 := 11. 13 definition lbl__div32u4 := 10. 14 definition lbl__div32u3 := 9. 15 definition lbl__div32u2 := 8. 16 definition lbl__div32u15 := 7. 17 definition lbl__div32u14 := 6. 18 definition lbl__div32u13 := 5. 19 definition lbl__div32u12 := 4. 20 definition lbl__div32u11 := 3. 21 definition lbl__div32u10 := 2. 22 definition lbl__div32u1 := 1. 23 definition lbl__div32u0 := 0. 24 definition C_cost0 := costlabel_of_nat 2. 25 definition C_cost1 := costlabel_of_nat 1. 26 definition C_cost2 := costlabel_of_nat 0. 27 28 29 definition pre__div32u := mk_pre_internal_function 30 (Some ? (pair ?? 4 (ASTint I32 Unsigned))) 31 [(pair ?? 0 (ASTint I32 Unsigned)); (pair ?? 1 (ASTint I32 Unsigned))] 32 [(pair ?? 2 (ASTint I32 Unsigned)); (pair ?? 3 (ASTint I32 Unsigned)); (pair ?? 4 (ASTint I32 Unsigned)); (pair ?? 5 (ASTint I32 Unsigned)); (pair ?? 6 (ASTint I32 Signed)); (pair ?? 7 (ASTint I32 Signed)); (pair ?? 8 (ASTint I32 Signed)); (pair ?? 9 (ASTint I8 Signed))] 74 33 0 75 34 [ 76 (pair ?? search9 (make_St_const 10 (Ointconst I8 (repr ? 1)) search8)); 77 (pair ?? search8 (make_St_op2 Oadd 9 4 10 search7)); 78 (pair ?? search7 (make_St_op1 (Ocastint Unsigned I8) 5 9 search5)); 79 (pair ?? search6 (make_St_cost C_cost1 search5)); 80 (pair ?? search50 (make_St_cost C_cost8 search49)); 81 (pair ?? search5 (make_St_skip search44)); 82 (pair ?? search49 (make_St_const 35 (Ointconst I8 (repr ? 0)) search48)); 83 (pair ?? search48 (make_St_op1 (Ocastint Signed I8) 5 35 search47)); 84 (pair ?? search47 (make_St_const 34 (Ointconst I8 (repr ? 1)) search46)); 85 (pair ?? search46 (make_St_op2 Osub 33 1 34 search45)); 86 (pair ?? search45 (make_St_op1 (Ocastint Unsigned I8) 3 33 search5)); 87 (pair ?? search44 (make_St_op2 (Ocmpu Cge) 32 3 5 search43)); 88 (pair ?? search43 (make_St_op1 Onotbool 31 32 search42)); 89 (pair ?? search42 (make_St_cond 31 search4 search41)); 90 (pair ?? search41 (make_St_cost C_cost6 search40)); 91 (pair ?? search40 (make_St_op2 Oadd 29 3 5 search39)); 92 (pair ?? search4 (make_St_cost C_cost7 search3)); 93 (pair ?? search39 (make_St_const 30 (Ointconst I8 (repr ? 2)) search38)); 94 (pair ?? search38 (make_St_op2 Odivu 28 29 30 search37)); 95 (pair ?? search37 (make_St_op1 (Ocastint Unsigned I8) 4 28 search36)); 96 (pair ?? search36 (make_St_const 27 (Ointconst I8 (repr ? 1)) search35)); 97 (pair ?? search35 (make_St_op2 Omul 26 4 27 search34)); 98 (pair ?? search34 (make_St_op2 Oaddp 25 0 26 search33)); 99 (pair ?? search33 (make_St_load Mint8unsigned 25 24 search32)); 100 (pair ?? search32 (make_St_op2 (Ocmpu Ceq) 23 24 2 search31)); 101 (pair ?? search31 (make_St_cond 23 search30 search28)); 102 (pair ?? search30 (make_St_cost C_cost4 search29)); 103 (pair ?? search3 (make_St_const 8 (Ointconst I8 (repr ? 1)) search2)); 104 (pair ?? search29 (make_St_op1 Oid 6 4 search0)); 105 (pair ?? search28 (make_St_cost C_cost5 search27)); 106 (pair ?? search27 (make_St_const 22 (Ointconst I8 (repr ? 1)) search26)); 107 (pair ?? search26 (make_St_op2 Omul 21 4 22 search25)); 108 (pair ?? search25 (make_St_op2 Oaddp 20 0 21 search24)); 109 (pair ?? search24 (make_St_load Mint8unsigned 20 19 search23)); 110 (pair ?? search23 (make_St_op2 (Ocmpu Cgt) 18 19 2 search22)); 111 (pair ?? search22 (make_St_cond 18 search21 search17)); 112 (pair ?? search21 (make_St_cost C_cost2 search20)); 113 (pair ?? search20 (make_St_const 17 (Ointconst I8 (repr ? 1)) search19)); 114 (pair ?? search2 (make_St_op1 Onegint 7 8 search1)); 115 (pair ?? search19 (make_St_op2 Osub 16 4 17 search18)); 116 (pair ?? search18 (make_St_op1 (Ocastint Unsigned I8) 3 16 search16)); 117 (pair ?? search17 (make_St_cost C_cost3 search16)); 118 (pair ?? search16 (make_St_const 15 (Ointconst I8 (repr ? 1)) search15)); 119 (pair ?? search15 (make_St_op2 Omul 14 4 15 search14)); 120 (pair ?? search14 (make_St_op2 Oaddp 13 0 14 search13)); 121 (pair ?? search13 (make_St_load Mint8unsigned 13 12 search12)); 122 (pair ?? search12 (make_St_op2 (Ocmpu Clt) 11 12 2 search11)); 123 (pair ?? search11 (make_St_cond 11 search10 search6)); 124 (pair ?? search10 (make_St_cost C_cost0 search9)); 125 (pair ?? search1 (make_St_op1 (Ocastint Signed I8) 6 7 search0)); 126 (pair ?? search0 (make_St_return)) 35 (pair ?? lbl__div32u9 (make_St_cond 7 lbl__div32u2 lbl__div32u8)); 36 (pair ?? lbl__div32u8 (make_St_cost C_cost0 lbl__div32u7)); 37 (pair ?? lbl__div32u7 (make_St_op2 Osub 3 3 1 lbl__div32u6)); 38 (pair ?? lbl__div32u6 (make_St_const 6 (Ointconst I32 (repr ? 1)) lbl__div32u5)); 39 (pair ?? lbl__div32u5 (make_St_op1 (Ocastint Signed I32) 5 6 lbl__div32u4)); 40 (pair ?? lbl__div32u4 (make_St_op2 Oadd 2 2 5 lbl__div32u3)); 41 (pair ?? lbl__div32u3 (make_St_skip lbl__div32u11)); 42 (pair ?? lbl__div32u2 (make_St_cost C_cost1 lbl__div32u1)); 43 (pair ?? lbl__div32u15 (make_St_cost C_cost2 lbl__div32u14)); 44 (pair ?? lbl__div32u14 (make_St_const 9 (Ointconst I8 (repr ? 0)) lbl__div32u13)); 45 (pair ?? lbl__div32u13 (make_St_op1 (Ocastint Signed I32) 2 9 lbl__div32u12)); 46 (pair ?? lbl__div32u12 (make_St_op1 Oid 3 0 lbl__div32u3)); 47 (pair ?? lbl__div32u11 (make_St_op2 (Ocmpu Cge) 8 3 1 lbl__div32u10)); 48 (pair ?? lbl__div32u10 (make_St_op1 Onotbool 7 8 lbl__div32u9)); 49 (pair ?? lbl__div32u1 (make_St_op1 Oid 4 2 lbl__div32u0)); 50 (pair ?? lbl__div32u0 (make_St_return)) 127 51 ] 128 52 129 search50 130 search0. 131 132 definition id_main := ident_of_nat 1. 133 definition main9 := 61. 134 definition main8 := 60. 135 definition main7 := 59. 136 definition main61 := 58. 137 definition main60 := 57. 138 definition main6 := 56. 139 definition main59 := 55. 140 definition main58 := 54. 141 definition main57 := 53. 142 definition main56 := 52. 143 definition main55 := 51. 144 definition main54 := 50. 145 definition main53 := 49. 146 definition main52 := 48. 147 definition main51 := 47. 148 definition main50 := 46. 149 definition main5 := 45. 150 definition main49 := 44. 151 definition main48 := 43. 152 definition main47 := 42. 153 definition main46 := 41. 154 definition main45 := 40. 155 definition main44 := 39. 156 definition main43 := 38. 157 definition main42 := 37. 158 definition main41 := 36. 159 definition main40 := 35. 160 definition main4 := 34. 161 definition main39 := 33. 162 definition main38 := 32. 163 definition main37 := 31. 164 definition main36 := 30. 165 definition main35 := 29. 166 definition main34 := 28. 167 definition main33 := 27. 168 definition main32 := 26. 169 definition main31 := 25. 170 definition main30 := 24. 171 definition main3 := 23. 172 definition main29 := 22. 173 definition main28 := 21. 174 definition main27 := 20. 175 definition main26 := 19. 176 definition main25 := 18. 177 definition main24 := 17. 178 definition main23 := 16. 179 definition main22 := 15. 180 definition main21 := 14. 181 definition main20 := 13. 182 definition main2 := 12. 183 definition main19 := 11. 184 definition main18 := 10. 185 definition main17 := 9. 186 definition main16 := 8. 187 definition main15 := 7. 188 definition main14 := 6. 189 definition main13 := 5. 190 definition main12 := 4. 191 definition main11 := 3. 192 definition main10 := 2. 193 definition main1 := 1. 194 definition main0 := 0. 195 definition C_cost9 := costlabel_of_nat 0. 53 lbl__div32u15 54 lbl__div32u0. 55 56 definition id__div32s := ident_of_nat 1. 57 definition lbl__div32s9 := 25. 58 definition lbl__div32s8 := 24. 59 definition lbl__div32s7 := 23. 60 definition lbl__div32s6 := 22. 61 definition lbl__div32s5 := 21. 62 definition lbl__div32s4 := 20. 63 definition lbl__div32s3 := 19. 64 definition lbl__div32s25 := 18. 65 definition lbl__div32s24 := 17. 66 definition lbl__div32s23 := 16. 67 definition lbl__div32s22 := 15. 68 definition lbl__div32s21 := 14. 69 definition lbl__div32s20 := 13. 70 definition lbl__div32s2 := 12. 71 definition lbl__div32s19 := 11. 72 definition lbl__div32s18 := 10. 73 definition lbl__div32s17 := 9. 74 definition lbl__div32s16 := 8. 75 definition lbl__div32s15 := 7. 76 definition lbl__div32s14 := 6. 77 definition lbl__div32s13 := 5. 78 definition lbl__div32s12 := 4. 79 definition lbl__div32s11 := 3. 80 definition lbl__div32s10 := 2. 81 definition lbl__div32s1 := 1. 82 definition lbl__div32s0 := 0. 83 definition C_cost3 := costlabel_of_nat 4. 84 definition C_cost4 := costlabel_of_nat 3. 85 definition C_cost7 := costlabel_of_nat 2. 86 definition C_cost5 := costlabel_of_nat 1. 87 definition C_cost6 := costlabel_of_nat 0. 88 89 90 definition pre__div32s := mk_pre_internal_function 91 (Some ? (pair ?? 7 (ASTint I32 Signed))) 92 [(pair ?? 0 (ASTint I32 Signed)); (pair ?? 1 (ASTint I32 Signed))] 93 [(pair ?? 2 (ASTint I32 Unsigned)); (pair ?? 3 (ASTint I32 Signed)); (pair ?? 4 (ASTint I32 Unsigned)); (pair ?? 5 (ASTint I32 Unsigned)); (pair ?? 6 (ASTint I32 Unsigned)); (pair ?? 7 (ASTint I32 Signed)); (pair ?? 8 (ASTint I32 Signed)); (pair ?? 9 (ASTint I32 Signed)); (pair ?? 10 (ASTint I32 Signed)); (pair ?? 11 (ASTint I32 Signed)); (pair ?? 12 (ASTint I32 Signed)); (pair ?? 13 (ASTint I32 Signed)); (pair ?? 14 (ASTint I32 Signed)); (pair ?? 15 (ASTint I8 Signed))] 94 0 95 [ 96 (pair ?? lbl__div32s9 (make_St_cost C_cost3 lbl__div32s8)); 97 (pair ?? lbl__div32s8 (make_St_op1 Onegint 9 1 lbl__div32s7)); 98 (pair ?? lbl__div32s7 (make_St_op1 (Ocastint Signed I32) 5 9 lbl__div32s6)); 99 (pair ?? lbl__div32s6 (make_St_op1 Onegint 3 3 lbl__div32s4)); 100 (pair ?? lbl__div32s5 (make_St_cost C_cost4 lbl__div32s4)); 101 (pair ?? lbl__div32s4 (make_St_call_id id__div32u [4; 5] (Some ? 6) lbl__div32s3)); 102 (pair ?? lbl__div32s3 (make_St_op1 Oid 2 6 lbl__div32s2)); 103 (pair ?? lbl__div32s25 (make_St_cost C_cost7 lbl__div32s24)); 104 (pair ?? lbl__div32s24 (make_St_op1 (Ocastint Signed I32) 4 0 lbl__div32s23)); 105 (pair ?? lbl__div32s23 (make_St_op1 (Ocastint Signed I32) 5 1 lbl__div32s22)); 106 (pair ?? lbl__div32s22 (make_St_const 15 (Ointconst I8 (repr ? 1)) lbl__div32s21)); 107 (pair ?? lbl__div32s21 (make_St_op1 (Ocastint Signed I32) 3 15 lbl__div32s20)); 108 (pair ?? lbl__div32s20 (make_St_const 14 (Ointconst I32 (repr ? 0)) lbl__div32s19)); 109 (pair ?? lbl__div32s2 (make_St_op1 (Ocastint Unsigned I32) 8 2 lbl__div32s1)); 110 (pair ?? lbl__div32s19 (make_St_op2 (Ocmp Clt) 13 0 14 lbl__div32s18)); 111 (pair ?? lbl__div32s18 (make_St_cond 13 lbl__div32s17 lbl__div32s13)); 112 (pair ?? lbl__div32s17 (make_St_cost C_cost5 lbl__div32s16)); 113 (pair ?? lbl__div32s16 (make_St_op1 Onegint 12 0 lbl__div32s15)); 114 (pair ?? lbl__div32s15 (make_St_op1 (Ocastint Signed I32) 4 12 lbl__div32s14)); 115 (pair ?? lbl__div32s14 (make_St_op1 Onegint 3 3 lbl__div32s12)); 116 (pair ?? lbl__div32s13 (make_St_cost C_cost6 lbl__div32s12)); 117 (pair ?? lbl__div32s12 (make_St_const 11 (Ointconst I32 (repr ? 0)) lbl__div32s11)); 118 (pair ?? lbl__div32s11 (make_St_op2 (Ocmp Clt) 10 1 11 lbl__div32s10)); 119 (pair ?? lbl__div32s10 (make_St_cond 10 lbl__div32s9 lbl__div32s5)); 120 (pair ?? lbl__div32s1 (make_St_op2 Omul 7 3 8 lbl__div32s0)); 121 (pair ?? lbl__div32s0 (make_St_return)) 122 ] 123 124 lbl__div32s25 125 lbl__div32s0. 126 127 definition id_search := ident_of_nat 2. 128 definition lbl_search9 := 65. 129 definition lbl_search8 := 64. 130 definition lbl_search7 := 63. 131 definition lbl_search65 := 62. 132 definition lbl_search64 := 61. 133 definition lbl_search63 := 60. 134 definition lbl_search62 := 59. 135 definition lbl_search61 := 58. 136 definition lbl_search60 := 57. 137 definition lbl_search6 := 56. 138 definition lbl_search59 := 55. 139 definition lbl_search58 := 54. 140 definition lbl_search57 := 53. 141 definition lbl_search56 := 52. 142 definition lbl_search55 := 51. 143 definition lbl_search54 := 50. 144 definition lbl_search53 := 49. 145 definition lbl_search52 := 48. 146 definition lbl_search51 := 47. 147 definition lbl_search50 := 46. 148 definition lbl_search5 := 45. 149 definition lbl_search49 := 44. 150 definition lbl_search48 := 43. 151 definition lbl_search47 := 42. 152 definition lbl_search46 := 41. 153 definition lbl_search45 := 40. 154 definition lbl_search44 := 39. 155 definition lbl_search43 := 38. 156 definition lbl_search42 := 37. 157 definition lbl_search41 := 36. 158 definition lbl_search40 := 35. 159 definition lbl_search4 := 34. 160 definition lbl_search39 := 33. 161 definition lbl_search38 := 32. 162 definition lbl_search37 := 31. 163 definition lbl_search36 := 30. 164 definition lbl_search35 := 29. 165 definition lbl_search34 := 28. 166 definition lbl_search33 := 27. 167 definition lbl_search32 := 26. 168 definition lbl_search31 := 25. 169 definition lbl_search30 := 24. 170 definition lbl_search3 := 23. 171 definition lbl_search29 := 22. 172 definition lbl_search28 := 21. 173 definition lbl_search27 := 20. 174 definition lbl_search26 := 19. 175 definition lbl_search25 := 18. 176 definition lbl_search24 := 17. 177 definition lbl_search23 := 16. 178 definition lbl_search22 := 15. 179 definition lbl_search21 := 14. 180 definition lbl_search20 := 13. 181 definition lbl_search2 := 12. 182 definition lbl_search19 := 11. 183 definition lbl_search18 := 10. 184 definition lbl_search17 := 9. 185 definition lbl_search16 := 8. 186 definition lbl_search15 := 7. 187 definition lbl_search14 := 6. 188 definition lbl_search13 := 5. 189 definition lbl_search12 := 4. 190 definition lbl_search11 := 3. 191 definition lbl_search10 := 2. 192 definition lbl_search1 := 1. 193 definition lbl_search0 := 0. 194 definition C_cost16 := costlabel_of_nat 8. 195 definition C_cost9 := costlabel_of_nat 7. 196 definition C_cost14 := costlabel_of_nat 6. 197 definition C_cost15 := costlabel_of_nat 5. 198 definition C_cost12 := costlabel_of_nat 4. 199 definition C_cost13 := costlabel_of_nat 3. 200 definition C_cost10 := costlabel_of_nat 2. 201 definition C_cost11 := costlabel_of_nat 1. 202 definition C_cost8 := costlabel_of_nat 0. 203 204 205 definition pre_search := mk_pre_internal_function 206 (Some ? (pair ?? 8 (ASTint I8 Unsigned))) 207 [(pair ?? 0 (ASTptr Any)); (pair ?? 1 (ASTint I8 Unsigned)); (pair ?? 2 (ASTint I8 Unsigned))] 208 [(pair ?? 3 (ASTint I32 Signed)); (pair ?? 4 (ASTint I8 Unsigned)); (pair ?? 5 (ASTint I8 Unsigned)); (pair ?? 6 (ASTint I8 Unsigned)); (pair ?? 7 (ASTint I32 Signed)); (pair ?? 8 (ASTint I8 Unsigned)); (pair ?? 9 (ASTint I32 Signed)); (pair ?? 10 (ASTint I32 Signed)); (pair ?? 11 (ASTint I32 Signed)); (pair ?? 12 (ASTint I32 Signed)); (pair ?? 13 (ASTint I32 Signed)); (pair ?? 14 (ASTint I32 Signed)); (pair ?? 15 (ASTint I32 Signed)); (pair ?? 16 (ASTint I32 Signed)); (pair ?? 17 (ASTint I8 Unsigned)); (pair ?? 18 (ASTptr Any)); (pair ?? 19 (ASTint I8 Unsigned)); (pair ?? 20 (ASTint I8 Unsigned)); (pair ?? 21 (ASTint I32 Signed)); (pair ?? 22 (ASTint I32 Signed)); (pair ?? 23 (ASTint I32 Signed)); (pair ?? 24 (ASTint I32 Signed)); (pair ?? 25 (ASTint I32 Signed)); (pair ?? 26 (ASTint I32 Signed)); (pair ?? 27 (ASTint I8 Unsigned)); (pair ?? 28 (ASTptr Any)); (pair ?? 29 (ASTint I8 Unsigned)); (pair ?? 30 (ASTint I8 Unsigned)); (pair ?? 31 (ASTint I32 Signed)); (pair ?? 32 (ASTint I32 Signed)); (pair ?? 33 (ASTint I32 Signed)); (pair ?? 34 (ASTint I8 Unsigned)); (pair ?? 35 (ASTptr Any)); (pair ?? 36 (ASTint I8 Unsigned)); (pair ?? 37 (ASTint I8 Unsigned)); (pair ?? 38 (ASTint I32 Signed)); (pair ?? 39 (ASTint I32 Signed)); (pair ?? 40 (ASTint I8 Signed)); (pair ?? 41 (ASTint I32 Signed)); (pair ?? 42 (ASTint I32 Signed)); (pair ?? 43 (ASTint I32 Signed)); (pair ?? 44 (ASTint I32 Signed)); (pair ?? 45 (ASTint I32 Signed)); (pair ?? 46 (ASTint I32 Signed)); (pair ?? 47 (ASTint I32 Signed)); (pair ?? 48 (ASTint I32 Signed)); (pair ?? 49 (ASTint I32 Signed)); (pair ?? 50 (ASTint I8 Signed))] 209 0 210 [ 211 (pair ?? lbl_search9 (make_St_const 13 (Ointconst I32 (repr ? 1)) lbl_search8)); 212 (pair ?? lbl_search8 (make_St_op2 Oadd 11 12 13 lbl_search7)); 213 (pair ?? lbl_search7 (make_St_op1 (Ocastint Signed I8) 6 11 lbl_search5)); 214 (pair ?? lbl_search65 (make_St_cost C_cost16 lbl_search64)); 215 (pair ?? lbl_search64 (make_St_const 50 (Ointconst I8 (repr ? 0)) lbl_search63)); 216 (pair ?? lbl_search63 (make_St_op1 (Ocastint Signed I8) 6 50 lbl_search62)); 217 (pair ?? lbl_search62 (make_St_op1 (Ocastint Unsigned I32) 48 1 lbl_search61)); 218 (pair ?? lbl_search61 (make_St_const 49 (Ointconst I32 (repr ? 1)) lbl_search60)); 219 (pair ?? lbl_search60 (make_St_op2 Osub 47 48 49 lbl_search59)); 220 (pair ?? lbl_search6 (make_St_cost C_cost9 lbl_search5)); 221 (pair ?? lbl_search59 (make_St_op1 (Ocastint Signed I8) 4 47 lbl_search5)); 222 (pair ?? lbl_search58 (make_St_op1 (Ocastint Unsigned I32) 45 4 lbl_search57)); 223 (pair ?? lbl_search57 (make_St_op1 (Ocastint Unsigned I32) 46 6 lbl_search56)); 224 (pair ?? lbl_search56 (make_St_op2 (Ocmp Cge) 44 45 46 lbl_search55)); 225 (pair ?? lbl_search55 (make_St_op1 Onotbool 43 44 lbl_search54)); 226 (pair ?? lbl_search54 (make_St_cond 43 lbl_search4 lbl_search53)); 227 (pair ?? lbl_search53 (make_St_cost C_cost14 lbl_search52)); 228 (pair ?? lbl_search52 (make_St_op1 (Ocastint Unsigned I32) 41 4 lbl_search51)); 229 (pair ?? lbl_search51 (make_St_op1 (Ocastint Unsigned I32) 42 6 lbl_search50)); 230 (pair ?? lbl_search50 (make_St_op2 Oadd 38 41 42 lbl_search49)); 231 (pair ?? lbl_search5 (make_St_skip lbl_search58)); 232 (pair ?? lbl_search49 (make_St_const 40 (Ointconst I8 (repr ? 2)) lbl_search48)); 233 (pair ?? lbl_search48 (make_St_op1 (Ocastint Signed I32) 39 40 lbl_search47)); 234 (pair ?? lbl_search47 (make_St_call_id id__div32s [38; 39] (Some ? 7) lbl_search46)); 235 (pair ?? lbl_search46 (make_St_op1 Oid 3 7 lbl_search45)); 236 (pair ?? lbl_search45 (make_St_op1 (Ocastint Signed I8) 5 3 lbl_search44)); 237 (pair ?? lbl_search44 (make_St_const 37 (Ointconst I8 (repr ? 1)) lbl_search43)); 238 (pair ?? lbl_search43 (make_St_op2 Omul 36 5 37 lbl_search42)); 239 (pair ?? lbl_search42 (make_St_op2 Oaddp 35 0 36 lbl_search41)); 240 (pair ?? lbl_search41 (make_St_load Mint8unsigned 35 34 lbl_search40)); 241 (pair ?? lbl_search40 (make_St_op1 (Ocastint Unsigned I32) 32 34 lbl_search39)); 242 (pair ?? lbl_search4 (make_St_cost C_cost15 lbl_search3)); 243 (pair ?? lbl_search39 (make_St_op1 (Ocastint Unsigned I32) 33 2 lbl_search38)); 244 (pair ?? lbl_search38 (make_St_op2 (Ocmp Ceq) 31 32 33 lbl_search37)); 245 (pair ?? lbl_search37 (make_St_cond 31 lbl_search36 lbl_search34)); 246 (pair ?? lbl_search36 (make_St_cost C_cost12 lbl_search35)); 247 (pair ?? lbl_search35 (make_St_op1 Oid 8 5 lbl_search0)); 248 (pair ?? lbl_search34 (make_St_cost C_cost13 lbl_search33)); 249 (pair ?? lbl_search33 (make_St_const 30 (Ointconst I8 (repr ? 1)) lbl_search32)); 250 (pair ?? lbl_search32 (make_St_op2 Omul 29 5 30 lbl_search31)); 251 (pair ?? lbl_search31 (make_St_op2 Oaddp 28 0 29 lbl_search30)); 252 (pair ?? lbl_search30 (make_St_load Mint8unsigned 28 27 lbl_search29)); 253 (pair ?? lbl_search3 (make_St_const 10 (Ointconst I32 (repr ? 1)) lbl_search2)); 254 (pair ?? lbl_search29 (make_St_op1 (Ocastint Unsigned I32) 25 27 lbl_search28)); 255 (pair ?? lbl_search28 (make_St_op1 (Ocastint Unsigned I32) 26 2 lbl_search27)); 256 (pair ?? lbl_search27 (make_St_op2 (Ocmp Cgt) 24 25 26 lbl_search26)); 257 (pair ?? lbl_search26 (make_St_cond 24 lbl_search25 lbl_search20)); 258 (pair ?? lbl_search25 (make_St_cost C_cost10 lbl_search24)); 259 (pair ?? lbl_search24 (make_St_op1 (Ocastint Unsigned I32) 22 5 lbl_search23)); 260 (pair ?? lbl_search23 (make_St_const 23 (Ointconst I32 (repr ? 1)) lbl_search22)); 261 (pair ?? lbl_search22 (make_St_op2 Osub 21 22 23 lbl_search21)); 262 (pair ?? lbl_search21 (make_St_op1 (Ocastint Signed I8) 4 21 lbl_search19)); 263 (pair ?? lbl_search20 (make_St_cost C_cost11 lbl_search19)); 264 (pair ?? lbl_search2 (make_St_op1 Onegint 9 10 lbl_search1)); 265 (pair ?? lbl_search19 (make_St_const 20 (Ointconst I8 (repr ? 1)) lbl_search18)); 266 (pair ?? lbl_search18 (make_St_op2 Omul 19 5 20 lbl_search17)); 267 (pair ?? lbl_search17 (make_St_op2 Oaddp 18 0 19 lbl_search16)); 268 (pair ?? lbl_search16 (make_St_load Mint8unsigned 18 17 lbl_search15)); 269 (pair ?? lbl_search15 (make_St_op1 (Ocastint Unsigned I32) 15 17 lbl_search14)); 270 (pair ?? lbl_search14 (make_St_op1 (Ocastint Unsigned I32) 16 2 lbl_search13)); 271 (pair ?? lbl_search13 (make_St_op2 (Ocmp Clt) 14 15 16 lbl_search12)); 272 (pair ?? lbl_search12 (make_St_cond 14 lbl_search11 lbl_search6)); 273 (pair ?? lbl_search11 (make_St_cost C_cost8 lbl_search10)); 274 (pair ?? lbl_search10 (make_St_op1 (Ocastint Unsigned I32) 12 5 lbl_search9)); 275 (pair ?? lbl_search1 (make_St_op1 (Ocastint Signed I8) 8 9 lbl_search0)); 276 (pair ?? lbl_search0 (make_St_return)) 277 ] 278 279 lbl_search65 280 lbl_search0. 281 282 definition id_main := ident_of_nat 3. 283 definition lbl_main9 := 61. 284 definition lbl_main8 := 60. 285 definition lbl_main7 := 59. 286 definition lbl_main61 := 58. 287 definition lbl_main60 := 57. 288 definition lbl_main6 := 56. 289 definition lbl_main59 := 55. 290 definition lbl_main58 := 54. 291 definition lbl_main57 := 53. 292 definition lbl_main56 := 52. 293 definition lbl_main55 := 51. 294 definition lbl_main54 := 50. 295 definition lbl_main53 := 49. 296 definition lbl_main52 := 48. 297 definition lbl_main51 := 47. 298 definition lbl_main50 := 46. 299 definition lbl_main5 := 45. 300 definition lbl_main49 := 44. 301 definition lbl_main48 := 43. 302 definition lbl_main47 := 42. 303 definition lbl_main46 := 41. 304 definition lbl_main45 := 40. 305 definition lbl_main44 := 39. 306 definition lbl_main43 := 38. 307 definition lbl_main42 := 37. 308 definition lbl_main41 := 36. 309 definition lbl_main40 := 35. 310 definition lbl_main4 := 34. 311 definition lbl_main39 := 33. 312 definition lbl_main38 := 32. 313 definition lbl_main37 := 31. 314 definition lbl_main36 := 30. 315 definition lbl_main35 := 29. 316 definition lbl_main34 := 28. 317 definition lbl_main33 := 27. 318 definition lbl_main32 := 26. 319 definition lbl_main31 := 25. 320 definition lbl_main30 := 24. 321 definition lbl_main3 := 23. 322 definition lbl_main29 := 22. 323 definition lbl_main28 := 21. 324 definition lbl_main27 := 20. 325 definition lbl_main26 := 19. 326 definition lbl_main25 := 18. 327 definition lbl_main24 := 17. 328 definition lbl_main23 := 16. 329 definition lbl_main22 := 15. 330 definition lbl_main21 := 14. 331 definition lbl_main20 := 13. 332 definition lbl_main2 := 12. 333 definition lbl_main19 := 11. 334 definition lbl_main18 := 10. 335 definition lbl_main17 := 9. 336 definition lbl_main16 := 8. 337 definition lbl_main15 := 7. 338 definition lbl_main14 := 6. 339 definition lbl_main13 := 5. 340 definition lbl_main12 := 4. 341 definition lbl_main11 := 3. 342 definition lbl_main10 := 2. 343 definition lbl_main1 := 1. 344 definition lbl_main0 := 0. 345 definition C_cost17 := costlabel_of_nat 0. 196 346 197 347 … … 199 349 (Some ? (pair ?? 2 (ASTint I32 Signed))) 200 350 [] 201 [(pair ?? 0 (ASTint I8 Unsigned)); (pair ?? 1 (ASTint I8 Unsigned)); (pair ?? 2 (ASTint I32 Signed)); (pair ?? 3 (ASTptr Any)); (pair ?? 4 (ASTint I8 Unsigned)); (pair ?? 5 (ASTint I8 Unsigned)); (pair ?? 6 (ASTint I8 Signed)); (pair ?? 7 (ASTint I8 Signed)); (pair ?? 8 (ASTptr Any)); (pair ?? 9 (ASTint I32 Unsigned)); (pair ?? 10 (ASTptr Any)); (pair ?? 11 (ASTint I8 Unsigned)); (pair ?? 12 (ASTint I8 Signed)); (pair ?? 13 (ASTptr Any)); (pair ?? 14 (ASTint I 8 Signed)); (pair ?? 15 (ASTint I8 Signed)); (pair ?? 16 (ASTint I8 Signed)); (pair ?? 17 (ASTptr Any)); (pair ?? 18 (ASTint I32 Unsigned)); (pair ?? 19 (ASTptr Any)); (pair ?? 20 (ASTint I8 Unsigned)); (pair ?? 21 (ASTint I8 Signed)); (pair ?? 22 (ASTptr Any)); (pair ?? 23 (ASTint I8 Signed)); (pair ?? 24 (ASTint I8 Signed)); (pair ?? 25 (ASTint I8 Signed)); (pair ?? 26 (ASTptr Any)); (pair ?? 27 (ASTint I32 Unsigned)); (pair ?? 28 (ASTptr Any)); (pair ?? 29 (ASTint I8 Unsigned)); (pair ?? 30 (ASTint I8 Signed)); (pair ?? 31 (ASTptr Any)); (pair ?? 32 (ASTint I8 Signed)); (pair ?? 33 (ASTint I8 Signed)); (pair ?? 34 (ASTint I8 Signed)); (pair ?? 35 (ASTptr Any)); (pair ?? 36 (ASTint I32 Unsigned)); (pair ?? 37 (ASTptr Any)); (pair ?? 38 (ASTint I8 Unsigned)); (pair ?? 39 (ASTint I8 Signed)); (pair ?? 40 (ASTptr Any)); (pair ?? 41 (ASTint I8 Signed)); (pair ?? 42 (ASTint I8 Signed)); (pair ?? 43 (ASTint I8 Signed)); (pair ?? 44 (ASTptr Any)); (pair ?? 45 (ASTint I32 Unsigned)); (pair ?? 46 (ASTptr Any)); (pair ?? 47 (ASTint I8 Unsigned)); (pair ?? 48 (ASTint I8 Signed)); (pair ?? 49 (ASTptr Any)); (pair ?? 50 (ASTint I8 Signed)); (pair ?? 51 (ASTint I8 Signed)); (pair ?? 52 (ASTint I8Signed)); (pair ?? 53 (ASTptr Any)); (pair ?? 54 (ASTint I32 Unsigned))]351 [(pair ?? 0 (ASTint I8 Unsigned)); (pair ?? 1 (ASTint I8 Unsigned)); (pair ?? 2 (ASTint I32 Signed)); (pair ?? 3 (ASTptr Any)); (pair ?? 4 (ASTint I8 Unsigned)); (pair ?? 5 (ASTint I8 Unsigned)); (pair ?? 6 (ASTint I8 Signed)); (pair ?? 7 (ASTint I8 Signed)); (pair ?? 8 (ASTptr Any)); (pair ?? 9 (ASTint I32 Unsigned)); (pair ?? 10 (ASTptr Any)); (pair ?? 11 (ASTint I8 Unsigned)); (pair ?? 12 (ASTint I8 Signed)); (pair ?? 13 (ASTptr Any)); (pair ?? 14 (ASTint I32 Signed)); (pair ?? 15 (ASTint I32 Signed)); (pair ?? 16 (ASTint I32 Signed)); (pair ?? 17 (ASTptr Any)); (pair ?? 18 (ASTint I32 Unsigned)); (pair ?? 19 (ASTptr Any)); (pair ?? 20 (ASTint I8 Unsigned)); (pair ?? 21 (ASTint I8 Signed)); (pair ?? 22 (ASTptr Any)); (pair ?? 23 (ASTint I32 Signed)); (pair ?? 24 (ASTint I32 Signed)); (pair ?? 25 (ASTint I32 Signed)); (pair ?? 26 (ASTptr Any)); (pair ?? 27 (ASTint I32 Unsigned)); (pair ?? 28 (ASTptr Any)); (pair ?? 29 (ASTint I8 Unsigned)); (pair ?? 30 (ASTint I8 Signed)); (pair ?? 31 (ASTptr Any)); (pair ?? 32 (ASTint I32 Signed)); (pair ?? 33 (ASTint I32 Signed)); (pair ?? 34 (ASTint I32 Signed)); (pair ?? 35 (ASTptr Any)); (pair ?? 36 (ASTint I32 Unsigned)); (pair ?? 37 (ASTptr Any)); (pair ?? 38 (ASTint I8 Unsigned)); (pair ?? 39 (ASTint I8 Signed)); (pair ?? 40 (ASTptr Any)); (pair ?? 41 (ASTint I32 Signed)); (pair ?? 42 (ASTint I32 Signed)); (pair ?? 43 (ASTint I32 Signed)); (pair ?? 44 (ASTptr Any)); (pair ?? 45 (ASTint I32 Unsigned)); (pair ?? 46 (ASTptr Any)); (pair ?? 47 (ASTint I8 Unsigned)); (pair ?? 48 (ASTint I8 Signed)); (pair ?? 49 (ASTptr Any)); (pair ?? 50 (ASTint I32 Signed)); (pair ?? 51 (ASTint I32 Signed)); (pair ?? 52 (ASTint I32 Signed)); (pair ?? 53 (ASTptr Any)); (pair ?? 54 (ASTint I32 Unsigned))] 202 352 5 203 353 [ 204 (pair ?? main9 (make_St_const 9 (Ointconst I32 (repr ? 0))main8));205 (pair ?? main8 (make_St_op2 Oaddp 3 8 9main7));206 (pair ?? main7 (make_St_const 7 (Ointconst I8 (repr ? 5))main6));207 (pair ?? main61 (make_St_cost C_cost9main60));208 (pair ?? main60 (make_St_const 53 (Oaddrstack 0)main59));209 (pair ?? main6 (make_St_op1 (Ocastint Signed I8) 4 7main5));210 (pair ?? main59 (make_St_const 54 (Ointconst I32 (repr ? 0))main58));211 (pair ?? main58 (make_St_op2 Oaddp 49 53 54main57));212 (pair ?? main57 (make_St_const 51 (Ointconst I8 (repr ? 0))main56));213 (pair ?? main56 (make_St_const 52 (Ointconst I8 (repr ? 1))main55));214 (pair ?? main55 (make_St_op2 Omul 50 51 52main54));215 (pair ?? main54 (make_St_op2 Oaddp 46 49 50main53));216 (pair ?? main53 (make_St_const 48 (Ointconst I8 (repr ? 0))main52));217 (pair ?? main52 (make_St_op1 (Ocastint Signed I8) 47 48main51));218 (pair ?? main51 (make_St_store Mint8unsigned 46 47main50));219 (pair ?? main50 (make_St_const 44 (Oaddrstack 0)main49));220 (pair ?? main5 (make_St_const 6 (Ointconst I8 (repr ? 57))main4));221 (pair ?? main49 (make_St_const 45 (Ointconst I32 (repr ? 0))main48));222 (pair ?? main48 (make_St_op2 Oaddp 40 44 45main47));223 (pair ?? main47 (make_St_const 42 (Ointconst I8 (repr ? 1))main46));224 (pair ?? main46 (make_St_const 43 (Ointconst I8 (repr ? 1))main45));225 (pair ?? main45 (make_St_op2 Omul 41 42 43main44));226 (pair ?? main44 (make_St_op2 Oaddp 37 40 41main43));227 (pair ?? main43 (make_St_const 39 (Ointconst I8 (repr ? 18))main42));228 (pair ?? main42 (make_St_op1 (Ocastint Signed I8) 38 39main41));229 (pair ?? main41 (make_St_store Mint8unsigned 37 38main40));230 (pair ?? main40 (make_St_const 35 (Oaddrstack 0)main39));231 (pair ?? main4 (make_St_op1 (Ocastint Signed I8) 5 6main3));232 (pair ?? main39 (make_St_const 36 (Ointconst I32 (repr ? 0))main38));233 (pair ?? main38 (make_St_op2 Oaddp 31 35 36main37));234 (pair ?? main37 (make_St_const 33 (Ointconst I8 (repr ? 2))main36));235 (pair ?? main36 (make_St_const 34 (Ointconst I8 (repr ? 1))main35));236 (pair ?? main35 (make_St_op2 Omul 32 33 34main34));237 (pair ?? main34 (make_St_op2 Oaddp 28 31 32main33));238 (pair ?? main33 (make_St_const 30 (Ointconst I8 (repr ? 23))main32));239 (pair ?? main32 (make_St_op1 (Ocastint Signed I8) 29 30main31));240 (pair ?? main31 (make_St_store Mint8unsigned 28 29main30));241 (pair ?? main30 (make_St_const 26 (Oaddrstack 0)main29));242 (pair ?? main3 (make_St_call_id id_search [3; 4; 5] (Some ? 1)main2));243 (pair ?? main29 (make_St_const 27 (Ointconst I32 (repr ? 0))main28));244 (pair ?? main28 (make_St_op2 Oaddp 22 26 27main27));245 (pair ?? main27 (make_St_const 24 (Ointconst I8 (repr ? 3))main26));246 (pair ?? main26 (make_St_const 25 (Ointconst I8 (repr ? 1))main25));247 (pair ?? main25 (make_St_op2 Omul 23 24 25main24));248 (pair ?? main24 (make_St_op2 Oaddp 19 22 23main23));249 (pair ?? main23 (make_St_const 21 (Ointconst I8 (repr ? 57))main22));250 (pair ?? main22 (make_St_op1 (Ocastint Signed I8) 20 21main21));251 (pair ?? main21 (make_St_store Mint8unsigned 19 20main20));252 (pair ?? main20 (make_St_const 17 (Oaddrstack 0)main19));253 (pair ?? main2 (make_St_op1 Oid 0 1main1));254 (pair ?? main19 (make_St_const 18 (Ointconst I32 (repr ? 0))main18));255 (pair ?? main18 (make_St_op2 Oaddp 13 17 18main17));256 (pair ?? main17 (make_St_const 15 (Ointconst I8 (repr ? 4))main16));257 (pair ?? main16 (make_St_const 16 (Ointconst I8 (repr ? 1))main15));258 (pair ?? main15 (make_St_op2 Omul 14 15 16main14));259 (pair ?? main14 (make_St_op2 Oaddp 10 13 14main13));260 (pair ?? main13 (make_St_const 12 (Ointconst I8 (repr ? 120))main12));261 (pair ?? main12 (make_St_op1 (Ocastint Signed I8) 11 12main11));262 (pair ?? main11 (make_St_store Mint8unsigned 10 11main10));263 (pair ?? main10 (make_St_const 8 (Oaddrstack 0)main9));264 (pair ?? main1 (make_St_op1 (Ocastint Unsigned I32) 2 0main0));265 (pair ?? main0 (make_St_return))354 (pair ?? lbl_main9 (make_St_const 9 (Ointconst I32 (repr ? 0)) lbl_main8)); 355 (pair ?? lbl_main8 (make_St_op2 Oaddp 3 8 9 lbl_main7)); 356 (pair ?? lbl_main7 (make_St_const 7 (Ointconst I8 (repr ? 5)) lbl_main6)); 357 (pair ?? lbl_main61 (make_St_cost C_cost17 lbl_main60)); 358 (pair ?? lbl_main60 (make_St_const 53 (Oaddrstack 0) lbl_main59)); 359 (pair ?? lbl_main6 (make_St_op1 (Ocastint Signed I8) 4 7 lbl_main5)); 360 (pair ?? lbl_main59 (make_St_const 54 (Ointconst I32 (repr ? 0)) lbl_main58)); 361 (pair ?? lbl_main58 (make_St_op2 Oaddp 49 53 54 lbl_main57)); 362 (pair ?? lbl_main57 (make_St_const 51 (Ointconst I32 (repr ? 0)) lbl_main56)); 363 (pair ?? lbl_main56 (make_St_const 52 (Ointconst I32 (repr ? 1)) lbl_main55)); 364 (pair ?? lbl_main55 (make_St_op2 Omul 50 51 52 lbl_main54)); 365 (pair ?? lbl_main54 (make_St_op2 Oaddp 46 49 50 lbl_main53)); 366 (pair ?? lbl_main53 (make_St_const 48 (Ointconst I8 (repr ? 0)) lbl_main52)); 367 (pair ?? lbl_main52 (make_St_op1 (Ocastint Signed I8) 47 48 lbl_main51)); 368 (pair ?? lbl_main51 (make_St_store Mint8unsigned 46 47 lbl_main50)); 369 (pair ?? lbl_main50 (make_St_const 44 (Oaddrstack 0) lbl_main49)); 370 (pair ?? lbl_main5 (make_St_const 6 (Ointconst I8 (repr ? 57)) lbl_main4)); 371 (pair ?? lbl_main49 (make_St_const 45 (Ointconst I32 (repr ? 0)) lbl_main48)); 372 (pair ?? lbl_main48 (make_St_op2 Oaddp 40 44 45 lbl_main47)); 373 (pair ?? lbl_main47 (make_St_const 42 (Ointconst I32 (repr ? 1)) lbl_main46)); 374 (pair ?? lbl_main46 (make_St_const 43 (Ointconst I32 (repr ? 1)) lbl_main45)); 375 (pair ?? lbl_main45 (make_St_op2 Omul 41 42 43 lbl_main44)); 376 (pair ?? lbl_main44 (make_St_op2 Oaddp 37 40 41 lbl_main43)); 377 (pair ?? lbl_main43 (make_St_const 39 (Ointconst I8 (repr ? 18)) lbl_main42)); 378 (pair ?? lbl_main42 (make_St_op1 (Ocastint Signed I8) 38 39 lbl_main41)); 379 (pair ?? lbl_main41 (make_St_store Mint8unsigned 37 38 lbl_main40)); 380 (pair ?? lbl_main40 (make_St_const 35 (Oaddrstack 0) lbl_main39)); 381 (pair ?? lbl_main4 (make_St_op1 (Ocastint Signed I8) 5 6 lbl_main3)); 382 (pair ?? lbl_main39 (make_St_const 36 (Ointconst I32 (repr ? 0)) lbl_main38)); 383 (pair ?? lbl_main38 (make_St_op2 Oaddp 31 35 36 lbl_main37)); 384 (pair ?? lbl_main37 (make_St_const 33 (Ointconst I32 (repr ? 2)) lbl_main36)); 385 (pair ?? lbl_main36 (make_St_const 34 (Ointconst I32 (repr ? 1)) lbl_main35)); 386 (pair ?? lbl_main35 (make_St_op2 Omul 32 33 34 lbl_main34)); 387 (pair ?? lbl_main34 (make_St_op2 Oaddp 28 31 32 lbl_main33)); 388 (pair ?? lbl_main33 (make_St_const 30 (Ointconst I8 (repr ? 23)) lbl_main32)); 389 (pair ?? lbl_main32 (make_St_op1 (Ocastint Signed I8) 29 30 lbl_main31)); 390 (pair ?? lbl_main31 (make_St_store Mint8unsigned 28 29 lbl_main30)); 391 (pair ?? lbl_main30 (make_St_const 26 (Oaddrstack 0) lbl_main29)); 392 (pair ?? lbl_main3 (make_St_call_id id_search [3; 4; 5] (Some ? 1) lbl_main2)); 393 (pair ?? lbl_main29 (make_St_const 27 (Ointconst I32 (repr ? 0)) lbl_main28)); 394 (pair ?? lbl_main28 (make_St_op2 Oaddp 22 26 27 lbl_main27)); 395 (pair ?? lbl_main27 (make_St_const 24 (Ointconst I32 (repr ? 3)) lbl_main26)); 396 (pair ?? lbl_main26 (make_St_const 25 (Ointconst I32 (repr ? 1)) lbl_main25)); 397 (pair ?? lbl_main25 (make_St_op2 Omul 23 24 25 lbl_main24)); 398 (pair ?? lbl_main24 (make_St_op2 Oaddp 19 22 23 lbl_main23)); 399 (pair ?? lbl_main23 (make_St_const 21 (Ointconst I8 (repr ? 57)) lbl_main22)); 400 (pair ?? lbl_main22 (make_St_op1 (Ocastint Signed I8) 20 21 lbl_main21)); 401 (pair ?? lbl_main21 (make_St_store Mint8unsigned 19 20 lbl_main20)); 402 (pair ?? lbl_main20 (make_St_const 17 (Oaddrstack 0) lbl_main19)); 403 (pair ?? lbl_main2 (make_St_op1 Oid 0 1 lbl_main1)); 404 (pair ?? lbl_main19 (make_St_const 18 (Ointconst I32 (repr ? 0)) lbl_main18)); 405 (pair ?? lbl_main18 (make_St_op2 Oaddp 13 17 18 lbl_main17)); 406 (pair ?? lbl_main17 (make_St_const 15 (Ointconst I32 (repr ? 4)) lbl_main16)); 407 (pair ?? lbl_main16 (make_St_const 16 (Ointconst I32 (repr ? 1)) lbl_main15)); 408 (pair ?? lbl_main15 (make_St_op2 Omul 14 15 16 lbl_main14)); 409 (pair ?? lbl_main14 (make_St_op2 Oaddp 10 13 14 lbl_main13)); 410 (pair ?? lbl_main13 (make_St_const 12 (Ointconst I8 (repr ? 120)) lbl_main12)); 411 (pair ?? lbl_main12 (make_St_op1 (Ocastint Signed I8) 11 12 lbl_main11)); 412 (pair ?? lbl_main11 (make_St_store Mint8unsigned 10 11 lbl_main10)); 413 (pair ?? lbl_main10 (make_St_const 8 (Oaddrstack 0) lbl_main9)); 414 (pair ?? lbl_main1 (make_St_op1 (Ocastint Unsigned I32) 2 0 lbl_main0)); 415 (pair ?? lbl_main0 (make_St_return)) 266 416 ] 267 417 268 main61269 main0.418 lbl_main61 419 lbl_main0. 270 420 271 421 … … 274 424 do f_main \larr make_internal_function pre_main; 275 425 do f_search \larr make_internal_function pre_search; 426 do f__div32s \larr make_internal_function pre__div32s; 427 do f__div32u \larr make_internal_function pre__div32u; 276 428 277 429 OK ? (mk_program ?? 278 430 ( (pair ?? id_main f_main):: 279 431 (pair ?? id_search f_search):: 432 (pair ?? id__div32s f__div32s):: 433 (pair ?? id__div32u f__div32u):: 280 434 (nil ?)) 281 435 id_main … … 287 441 normalize (* you can examine the result here *) 288 442 @refl qed. 289
Note: See TracChangeset
for help on using the changeset viewer.