Ignore:
Timestamp:
Mar 29, 2013, 6:38:26 PM (7 years ago)
Author:
sacerdot
Message:

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/rTLabs_syntax.ml

    r3001 r3043  
    139139    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
    140140let rec statement_rect_Type4 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
    141 | St_skip x_6699 -> h_St_skip x_6699
    142 | St_cost (x_6701, x_6700) -> h_St_cost x_6701 x_6700
    143 | St_const (t, x_6704, x_6703, x_6702) -> h_St_const t x_6704 x_6703 x_6702
    144 | St_op1 (t', t, x_6708, x_6707, x_6706, x_6705) ->
    145   h_St_op1 t' t x_6708 x_6707 x_6706 x_6705
    146 | St_op2 (t', t1, t2, x_6713, x_6712, x_6711, x_6710, x_6709) ->
    147   h_St_op2 t' t1 t2 x_6713 x_6712 x_6711 x_6710 x_6709
    148 | St_load (x_6717, x_6716, x_6715, x_6714) ->
    149   h_St_load x_6717 x_6716 x_6715 x_6714
    150 | St_store (x_6721, x_6720, x_6719, x_6718) ->
    151   h_St_store x_6721 x_6720 x_6719 x_6718
    152 | St_call_id (x_6725, x_6724, x_6723, x_6722) ->
    153   h_St_call_id x_6725 x_6724 x_6723 x_6722
    154 | St_call_ptr (x_6729, x_6728, x_6727, x_6726) ->
    155   h_St_call_ptr x_6729 x_6728 x_6727 x_6726
    156 | St_cond (x_6732, x_6731, x_6730) -> h_St_cond x_6732 x_6731 x_6730
     141| St_skip x_14959 -> h_St_skip x_14959
     142| St_cost (x_14961, x_14960) -> h_St_cost x_14961 x_14960
     143| St_const (t, x_14964, x_14963, x_14962) ->
     144  h_St_const t x_14964 x_14963 x_14962
     145| St_op1 (t', t, x_14968, x_14967, x_14966, x_14965) ->
     146  h_St_op1 t' t x_14968 x_14967 x_14966 x_14965
     147| St_op2 (t', t1, t2, x_14973, x_14972, x_14971, x_14970, x_14969) ->
     148  h_St_op2 t' t1 t2 x_14973 x_14972 x_14971 x_14970 x_14969
     149| St_load (x_14977, x_14976, x_14975, x_14974) ->
     150  h_St_load x_14977 x_14976 x_14975 x_14974
     151| St_store (x_14981, x_14980, x_14979, x_14978) ->
     152  h_St_store x_14981 x_14980 x_14979 x_14978
     153| St_call_id (x_14985, x_14984, x_14983, x_14982) ->
     154  h_St_call_id x_14985 x_14984 x_14983 x_14982
     155| St_call_ptr (x_14989, x_14988, x_14987, x_14986) ->
     156  h_St_call_ptr x_14989 x_14988 x_14987 x_14986
     157| St_cond (x_14992, x_14991, x_14990) -> h_St_cond x_14992 x_14991 x_14990
    157158| St_return -> h_St_return
    158159
     
    173174    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
    174175let rec statement_rect_Type5 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
    175 | St_skip x_6745 -> h_St_skip x_6745
    176 | St_cost (x_6747, x_6746) -> h_St_cost x_6747 x_6746
    177 | St_const (t, x_6750, x_6749, x_6748) -> h_St_const t x_6750 x_6749 x_6748
    178 | St_op1 (t', t, x_6754, x_6753, x_6752, x_6751) ->
    179   h_St_op1 t' t x_6754 x_6753 x_6752 x_6751
    180 | St_op2 (t', t1, t2, x_6759, x_6758, x_6757, x_6756, x_6755) ->
    181   h_St_op2 t' t1 t2 x_6759 x_6758 x_6757 x_6756 x_6755
    182 | St_load (x_6763, x_6762, x_6761, x_6760) ->
    183   h_St_load x_6763 x_6762 x_6761 x_6760
    184 | St_store (x_6767, x_6766, x_6765, x_6764) ->
    185   h_St_store x_6767 x_6766 x_6765 x_6764
    186 | St_call_id (x_6771, x_6770, x_6769, x_6768) ->
    187   h_St_call_id x_6771 x_6770 x_6769 x_6768
    188 | St_call_ptr (x_6775, x_6774, x_6773, x_6772) ->
    189   h_St_call_ptr x_6775 x_6774 x_6773 x_6772
    190 | St_cond (x_6778, x_6777, x_6776) -> h_St_cond x_6778 x_6777 x_6776
     176| St_skip x_15005 -> h_St_skip x_15005
     177| St_cost (x_15007, x_15006) -> h_St_cost x_15007 x_15006
     178| St_const (t, x_15010, x_15009, x_15008) ->
     179  h_St_const t x_15010 x_15009 x_15008
     180| St_op1 (t', t, x_15014, x_15013, x_15012, x_15011) ->
     181  h_St_op1 t' t x_15014 x_15013 x_15012 x_15011
     182| St_op2 (t', t1, t2, x_15019, x_15018, x_15017, x_15016, x_15015) ->
     183  h_St_op2 t' t1 t2 x_15019 x_15018 x_15017 x_15016 x_15015
     184| St_load (x_15023, x_15022, x_15021, x_15020) ->
     185  h_St_load x_15023 x_15022 x_15021 x_15020
     186| St_store (x_15027, x_15026, x_15025, x_15024) ->
     187  h_St_store x_15027 x_15026 x_15025 x_15024
     188| St_call_id (x_15031, x_15030, x_15029, x_15028) ->
     189  h_St_call_id x_15031 x_15030 x_15029 x_15028
     190| St_call_ptr (x_15035, x_15034, x_15033, x_15032) ->
     191  h_St_call_ptr x_15035 x_15034 x_15033 x_15032
     192| St_cond (x_15038, x_15037, x_15036) -> h_St_cond x_15038 x_15037 x_15036
    191193| St_return -> h_St_return
    192194
     
    207209    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
    208210let rec statement_rect_Type3 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
    209 | St_skip x_6791 -> h_St_skip x_6791
    210 | St_cost (x_6793, x_6792) -> h_St_cost x_6793 x_6792
    211 | St_const (t, x_6796, x_6795, x_6794) -> h_St_const t x_6796 x_6795 x_6794
    212 | St_op1 (t', t, x_6800, x_6799, x_6798, x_6797) ->
    213   h_St_op1 t' t x_6800 x_6799 x_6798 x_6797
    214 | St_op2 (t', t1, t2, x_6805, x_6804, x_6803, x_6802, x_6801) ->
    215   h_St_op2 t' t1 t2 x_6805 x_6804 x_6803 x_6802 x_6801
    216 | St_load (x_6809, x_6808, x_6807, x_6806) ->
    217   h_St_load x_6809 x_6808 x_6807 x_6806
    218 | St_store (x_6813, x_6812, x_6811, x_6810) ->
    219   h_St_store x_6813 x_6812 x_6811 x_6810
    220 | St_call_id (x_6817, x_6816, x_6815, x_6814) ->
    221   h_St_call_id x_6817 x_6816 x_6815 x_6814
    222 | St_call_ptr (x_6821, x_6820, x_6819, x_6818) ->
    223   h_St_call_ptr x_6821 x_6820 x_6819 x_6818
    224 | St_cond (x_6824, x_6823, x_6822) -> h_St_cond x_6824 x_6823 x_6822
     211| St_skip x_15051 -> h_St_skip x_15051
     212| St_cost (x_15053, x_15052) -> h_St_cost x_15053 x_15052
     213| St_const (t, x_15056, x_15055, x_15054) ->
     214  h_St_const t x_15056 x_15055 x_15054
     215| St_op1 (t', t, x_15060, x_15059, x_15058, x_15057) ->
     216  h_St_op1 t' t x_15060 x_15059 x_15058 x_15057
     217| St_op2 (t', t1, t2, x_15065, x_15064, x_15063, x_15062, x_15061) ->
     218  h_St_op2 t' t1 t2 x_15065 x_15064 x_15063 x_15062 x_15061
     219| St_load (x_15069, x_15068, x_15067, x_15066) ->
     220  h_St_load x_15069 x_15068 x_15067 x_15066
     221| St_store (x_15073, x_15072, x_15071, x_15070) ->
     222  h_St_store x_15073 x_15072 x_15071 x_15070
     223| St_call_id (x_15077, x_15076, x_15075, x_15074) ->
     224  h_St_call_id x_15077 x_15076 x_15075 x_15074
     225| St_call_ptr (x_15081, x_15080, x_15079, x_15078) ->
     226  h_St_call_ptr x_15081 x_15080 x_15079 x_15078
     227| St_cond (x_15084, x_15083, x_15082) -> h_St_cond x_15084 x_15083 x_15082
    225228| St_return -> h_St_return
    226229
     
    241244    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
    242245let rec statement_rect_Type2 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
    243 | St_skip x_6837 -> h_St_skip x_6837
    244 | St_cost (x_6839, x_6838) -> h_St_cost x_6839 x_6838
    245 | St_const (t, x_6842, x_6841, x_6840) -> h_St_const t x_6842 x_6841 x_6840
    246 | St_op1 (t', t, x_6846, x_6845, x_6844, x_6843) ->
    247   h_St_op1 t' t x_6846 x_6845 x_6844 x_6843
    248 | St_op2 (t', t1, t2, x_6851, x_6850, x_6849, x_6848, x_6847) ->
    249   h_St_op2 t' t1 t2 x_6851 x_6850 x_6849 x_6848 x_6847
    250 | St_load (x_6855, x_6854, x_6853, x_6852) ->
    251   h_St_load x_6855 x_6854 x_6853 x_6852
    252 | St_store (x_6859, x_6858, x_6857, x_6856) ->
    253   h_St_store x_6859 x_6858 x_6857 x_6856
    254 | St_call_id (x_6863, x_6862, x_6861, x_6860) ->
    255   h_St_call_id x_6863 x_6862 x_6861 x_6860
    256 | St_call_ptr (x_6867, x_6866, x_6865, x_6864) ->
    257   h_St_call_ptr x_6867 x_6866 x_6865 x_6864
    258 | St_cond (x_6870, x_6869, x_6868) -> h_St_cond x_6870 x_6869 x_6868
     246| St_skip x_15097 -> h_St_skip x_15097
     247| St_cost (x_15099, x_15098) -> h_St_cost x_15099 x_15098
     248| St_const (t, x_15102, x_15101, x_15100) ->
     249  h_St_const t x_15102 x_15101 x_15100
     250| St_op1 (t', t, x_15106, x_15105, x_15104, x_15103) ->
     251  h_St_op1 t' t x_15106 x_15105 x_15104 x_15103
     252| St_op2 (t', t1, t2, x_15111, x_15110, x_15109, x_15108, x_15107) ->
     253  h_St_op2 t' t1 t2 x_15111 x_15110 x_15109 x_15108 x_15107
     254| St_load (x_15115, x_15114, x_15113, x_15112) ->
     255  h_St_load x_15115 x_15114 x_15113 x_15112
     256| St_store (x_15119, x_15118, x_15117, x_15116) ->
     257  h_St_store x_15119 x_15118 x_15117 x_15116
     258| St_call_id (x_15123, x_15122, x_15121, x_15120) ->
     259  h_St_call_id x_15123 x_15122 x_15121 x_15120
     260| St_call_ptr (x_15127, x_15126, x_15125, x_15124) ->
     261  h_St_call_ptr x_15127 x_15126 x_15125 x_15124
     262| St_cond (x_15130, x_15129, x_15128) -> h_St_cond x_15130 x_15129 x_15128
    259263| St_return -> h_St_return
    260264
     
    275279    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
    276280let rec statement_rect_Type1 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
    277 | St_skip x_6883 -> h_St_skip x_6883
    278 | St_cost (x_6885, x_6884) -> h_St_cost x_6885 x_6884
    279 | St_const (t, x_6888, x_6887, x_6886) -> h_St_const t x_6888 x_6887 x_6886
    280 | St_op1 (t', t, x_6892, x_6891, x_6890, x_6889) ->
    281   h_St_op1 t' t x_6892 x_6891 x_6890 x_6889
    282 | St_op2 (t', t1, t2, x_6897, x_6896, x_6895, x_6894, x_6893) ->
    283   h_St_op2 t' t1 t2 x_6897 x_6896 x_6895 x_6894 x_6893
    284 | St_load (x_6901, x_6900, x_6899, x_6898) ->
    285   h_St_load x_6901 x_6900 x_6899 x_6898
    286 | St_store (x_6905, x_6904, x_6903, x_6902) ->
    287   h_St_store x_6905 x_6904 x_6903 x_6902
    288 | St_call_id (x_6909, x_6908, x_6907, x_6906) ->
    289   h_St_call_id x_6909 x_6908 x_6907 x_6906
    290 | St_call_ptr (x_6913, x_6912, x_6911, x_6910) ->
    291   h_St_call_ptr x_6913 x_6912 x_6911 x_6910
    292 | St_cond (x_6916, x_6915, x_6914) -> h_St_cond x_6916 x_6915 x_6914
     281| St_skip x_15143 -> h_St_skip x_15143
     282| St_cost (x_15145, x_15144) -> h_St_cost x_15145 x_15144
     283| St_const (t, x_15148, x_15147, x_15146) ->
     284  h_St_const t x_15148 x_15147 x_15146
     285| St_op1 (t', t, x_15152, x_15151, x_15150, x_15149) ->
     286  h_St_op1 t' t x_15152 x_15151 x_15150 x_15149
     287| St_op2 (t', t1, t2, x_15157, x_15156, x_15155, x_15154, x_15153) ->
     288  h_St_op2 t' t1 t2 x_15157 x_15156 x_15155 x_15154 x_15153
     289| St_load (x_15161, x_15160, x_15159, x_15158) ->
     290  h_St_load x_15161 x_15160 x_15159 x_15158
     291| St_store (x_15165, x_15164, x_15163, x_15162) ->
     292  h_St_store x_15165 x_15164 x_15163 x_15162
     293| St_call_id (x_15169, x_15168, x_15167, x_15166) ->
     294  h_St_call_id x_15169 x_15168 x_15167 x_15166
     295| St_call_ptr (x_15173, x_15172, x_15171, x_15170) ->
     296  h_St_call_ptr x_15173 x_15172 x_15171 x_15170
     297| St_cond (x_15176, x_15175, x_15174) -> h_St_cond x_15176 x_15175 x_15174
    293298| St_return -> h_St_return
    294299
     
    309314    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
    310315let rec statement_rect_Type0 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
    311 | St_skip x_6929 -> h_St_skip x_6929
    312 | St_cost (x_6931, x_6930) -> h_St_cost x_6931 x_6930
    313 | St_const (t, x_6934, x_6933, x_6932) -> h_St_const t x_6934 x_6933 x_6932
    314 | St_op1 (t', t, x_6938, x_6937, x_6936, x_6935) ->
    315   h_St_op1 t' t x_6938 x_6937 x_6936 x_6935
    316 | St_op2 (t', t1, t2, x_6943, x_6942, x_6941, x_6940, x_6939) ->
    317   h_St_op2 t' t1 t2 x_6943 x_6942 x_6941 x_6940 x_6939
    318 | St_load (x_6947, x_6946, x_6945, x_6944) ->
    319   h_St_load x_6947 x_6946 x_6945 x_6944
    320 | St_store (x_6951, x_6950, x_6949, x_6948) ->
    321   h_St_store x_6951 x_6950 x_6949 x_6948
    322 | St_call_id (x_6955, x_6954, x_6953, x_6952) ->
    323   h_St_call_id x_6955 x_6954 x_6953 x_6952
    324 | St_call_ptr (x_6959, x_6958, x_6957, x_6956) ->
    325   h_St_call_ptr x_6959 x_6958 x_6957 x_6956
    326 | St_cond (x_6962, x_6961, x_6960) -> h_St_cond x_6962 x_6961 x_6960
     316| St_skip x_15189 -> h_St_skip x_15189
     317| St_cost (x_15191, x_15190) -> h_St_cost x_15191 x_15190
     318| St_const (t, x_15194, x_15193, x_15192) ->
     319  h_St_const t x_15194 x_15193 x_15192
     320| St_op1 (t', t, x_15198, x_15197, x_15196, x_15195) ->
     321  h_St_op1 t' t x_15198 x_15197 x_15196 x_15195
     322| St_op2 (t', t1, t2, x_15203, x_15202, x_15201, x_15200, x_15199) ->
     323  h_St_op2 t' t1 t2 x_15203 x_15202 x_15201 x_15200 x_15199
     324| St_load (x_15207, x_15206, x_15205, x_15204) ->
     325  h_St_load x_15207 x_15206 x_15205 x_15204
     326| St_store (x_15211, x_15210, x_15209, x_15208) ->
     327  h_St_store x_15211 x_15210 x_15209 x_15208
     328| St_call_id (x_15215, x_15214, x_15213, x_15212) ->
     329  h_St_call_id x_15215 x_15214 x_15213 x_15212
     330| St_call_ptr (x_15219, x_15218, x_15217, x_15216) ->
     331  h_St_call_ptr x_15219 x_15218 x_15217 x_15216
     332| St_cond (x_15222, x_15221, x_15220) -> h_St_cond x_15222 x_15221 x_15220
    327333| St_return -> h_St_return
    328334
     
    460466    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
    461467    internal_function -> 'a1 **)
    462 let rec internal_function_rect_Type4 h_mk_internal_function x_7252 =
     468let rec internal_function_rect_Type4 h_mk_internal_function x_15512 =
    463469  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    464470    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    465     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_7252
     471    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15512
    466472  in
    467473  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
     
    475481    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
    476482    internal_function -> 'a1 **)
    477 let rec internal_function_rect_Type5 h_mk_internal_function x_7254 =
     483let rec internal_function_rect_Type5 h_mk_internal_function x_15514 =
    478484  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    479485    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    480     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_7254
     486    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15514
    481487  in
    482488  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
     
    490496    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
    491497    internal_function -> 'a1 **)
    492 let rec internal_function_rect_Type3 h_mk_internal_function x_7256 =
     498let rec internal_function_rect_Type3 h_mk_internal_function x_15516 =
    493499  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    494500    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    495     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_7256
     501    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15516
    496502  in
    497503  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
     
    505511    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
    506512    internal_function -> 'a1 **)
    507 let rec internal_function_rect_Type2 h_mk_internal_function x_7258 =
     513let rec internal_function_rect_Type2 h_mk_internal_function x_15518 =
    508514  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    509515    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    510     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_7258
     516    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15518
    511517  in
    512518  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
     
    520526    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
    521527    internal_function -> 'a1 **)
    522 let rec internal_function_rect_Type1 h_mk_internal_function x_7260 =
     528let rec internal_function_rect_Type1 h_mk_internal_function x_15520 =
    523529  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    524530    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    525     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_7260
     531    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15520
    526532  in
    527533  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
     
    535541    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
    536542    internal_function -> 'a1 **)
    537 let rec internal_function_rect_Type0 h_mk_internal_function x_7262 =
     543let rec internal_function_rect_Type0 h_mk_internal_function x_15522 =
    538544  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    539545    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    540     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_7262
     546    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15522
    541547  in
    542548  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
Note: See TracChangeset for help on using the changeset viewer.