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

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/rTLabs_syntax.ml

    r2775 r2797  
    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_14777 -> h_St_skip x_14777
    142 | St_cost (x_14779, x_14778) -> h_St_cost x_14779 x_14778
    143 | St_const (t, x_14782, x_14781, x_14780) ->
    144   h_St_const t x_14782 x_14781 x_14780
    145 | St_op1 (t', t, x_14786, x_14785, x_14784, x_14783) ->
    146   h_St_op1 t' t x_14786 x_14785 x_14784 x_14783
    147 | St_op2 (t', t1, t2, x_14791, x_14790, x_14789, x_14788, x_14787) ->
    148   h_St_op2 t' t1 t2 x_14791 x_14790 x_14789 x_14788 x_14787
    149 | St_load (x_14795, x_14794, x_14793, x_14792) ->
    150   h_St_load x_14795 x_14794 x_14793 x_14792
    151 | St_store (x_14799, x_14798, x_14797, x_14796) ->
    152   h_St_store x_14799 x_14798 x_14797 x_14796
    153 | St_call_id (x_14803, x_14802, x_14801, x_14800) ->
    154   h_St_call_id x_14803 x_14802 x_14801 x_14800
    155 | St_call_ptr (x_14807, x_14806, x_14805, x_14804) ->
    156   h_St_call_ptr x_14807 x_14806 x_14805 x_14804
    157 | St_cond (x_14810, x_14809, x_14808) -> h_St_cond x_14810 x_14809 x_14808
     141| St_skip x_14790 -> h_St_skip x_14790
     142| St_cost (x_14792, x_14791) -> h_St_cost x_14792 x_14791
     143| St_const (t, x_14795, x_14794, x_14793) ->
     144  h_St_const t x_14795 x_14794 x_14793
     145| St_op1 (t', t, x_14799, x_14798, x_14797, x_14796) ->
     146  h_St_op1 t' t x_14799 x_14798 x_14797 x_14796
     147| St_op2 (t', t1, t2, x_14804, x_14803, x_14802, x_14801, x_14800) ->
     148  h_St_op2 t' t1 t2 x_14804 x_14803 x_14802 x_14801 x_14800
     149| St_load (x_14808, x_14807, x_14806, x_14805) ->
     150  h_St_load x_14808 x_14807 x_14806 x_14805
     151| St_store (x_14812, x_14811, x_14810, x_14809) ->
     152  h_St_store x_14812 x_14811 x_14810 x_14809
     153| St_call_id (x_14816, x_14815, x_14814, x_14813) ->
     154  h_St_call_id x_14816 x_14815 x_14814 x_14813
     155| St_call_ptr (x_14820, x_14819, x_14818, x_14817) ->
     156  h_St_call_ptr x_14820 x_14819 x_14818 x_14817
     157| St_cond (x_14823, x_14822, x_14821) -> h_St_cond x_14823 x_14822 x_14821
    158158| St_return -> h_St_return
    159159
     
    174174    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
    175175let 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
    176 | St_skip x_14823 -> h_St_skip x_14823
    177 | St_cost (x_14825, x_14824) -> h_St_cost x_14825 x_14824
    178 | St_const (t, x_14828, x_14827, x_14826) ->
    179   h_St_const t x_14828 x_14827 x_14826
    180 | St_op1 (t', t, x_14832, x_14831, x_14830, x_14829) ->
    181   h_St_op1 t' t x_14832 x_14831 x_14830 x_14829
    182 | St_op2 (t', t1, t2, x_14837, x_14836, x_14835, x_14834, x_14833) ->
    183   h_St_op2 t' t1 t2 x_14837 x_14836 x_14835 x_14834 x_14833
    184 | St_load (x_14841, x_14840, x_14839, x_14838) ->
    185   h_St_load x_14841 x_14840 x_14839 x_14838
    186 | St_store (x_14845, x_14844, x_14843, x_14842) ->
    187   h_St_store x_14845 x_14844 x_14843 x_14842
    188 | St_call_id (x_14849, x_14848, x_14847, x_14846) ->
    189   h_St_call_id x_14849 x_14848 x_14847 x_14846
    190 | St_call_ptr (x_14853, x_14852, x_14851, x_14850) ->
    191   h_St_call_ptr x_14853 x_14852 x_14851 x_14850
    192 | St_cond (x_14856, x_14855, x_14854) -> h_St_cond x_14856 x_14855 x_14854
     176| St_skip x_14836 -> h_St_skip x_14836
     177| St_cost (x_14838, x_14837) -> h_St_cost x_14838 x_14837
     178| St_const (t, x_14841, x_14840, x_14839) ->
     179  h_St_const t x_14841 x_14840 x_14839
     180| St_op1 (t', t, x_14845, x_14844, x_14843, x_14842) ->
     181  h_St_op1 t' t x_14845 x_14844 x_14843 x_14842
     182| St_op2 (t', t1, t2, x_14850, x_14849, x_14848, x_14847, x_14846) ->
     183  h_St_op2 t' t1 t2 x_14850 x_14849 x_14848 x_14847 x_14846
     184| St_load (x_14854, x_14853, x_14852, x_14851) ->
     185  h_St_load x_14854 x_14853 x_14852 x_14851
     186| St_store (x_14858, x_14857, x_14856, x_14855) ->
     187  h_St_store x_14858 x_14857 x_14856 x_14855
     188| St_call_id (x_14862, x_14861, x_14860, x_14859) ->
     189  h_St_call_id x_14862 x_14861 x_14860 x_14859
     190| St_call_ptr (x_14866, x_14865, x_14864, x_14863) ->
     191  h_St_call_ptr x_14866 x_14865 x_14864 x_14863
     192| St_cond (x_14869, x_14868, x_14867) -> h_St_cond x_14869 x_14868 x_14867
    193193| St_return -> h_St_return
    194194
     
    209209    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
    210210let 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
    211 | St_skip x_14869 -> h_St_skip x_14869
    212 | St_cost (x_14871, x_14870) -> h_St_cost x_14871 x_14870
    213 | St_const (t, x_14874, x_14873, x_14872) ->
    214   h_St_const t x_14874 x_14873 x_14872
    215 | St_op1 (t', t, x_14878, x_14877, x_14876, x_14875) ->
    216   h_St_op1 t' t x_14878 x_14877 x_14876 x_14875
    217 | St_op2 (t', t1, t2, x_14883, x_14882, x_14881, x_14880, x_14879) ->
    218   h_St_op2 t' t1 t2 x_14883 x_14882 x_14881 x_14880 x_14879
    219 | St_load (x_14887, x_14886, x_14885, x_14884) ->
    220   h_St_load x_14887 x_14886 x_14885 x_14884
    221 | St_store (x_14891, x_14890, x_14889, x_14888) ->
    222   h_St_store x_14891 x_14890 x_14889 x_14888
    223 | St_call_id (x_14895, x_14894, x_14893, x_14892) ->
    224   h_St_call_id x_14895 x_14894 x_14893 x_14892
    225 | St_call_ptr (x_14899, x_14898, x_14897, x_14896) ->
    226   h_St_call_ptr x_14899 x_14898 x_14897 x_14896
    227 | St_cond (x_14902, x_14901, x_14900) -> h_St_cond x_14902 x_14901 x_14900
     211| St_skip x_14882 -> h_St_skip x_14882
     212| St_cost (x_14884, x_14883) -> h_St_cost x_14884 x_14883
     213| St_const (t, x_14887, x_14886, x_14885) ->
     214  h_St_const t x_14887 x_14886 x_14885
     215| St_op1 (t', t, x_14891, x_14890, x_14889, x_14888) ->
     216  h_St_op1 t' t x_14891 x_14890 x_14889 x_14888
     217| St_op2 (t', t1, t2, x_14896, x_14895, x_14894, x_14893, x_14892) ->
     218  h_St_op2 t' t1 t2 x_14896 x_14895 x_14894 x_14893 x_14892
     219| St_load (x_14900, x_14899, x_14898, x_14897) ->
     220  h_St_load x_14900 x_14899 x_14898 x_14897
     221| St_store (x_14904, x_14903, x_14902, x_14901) ->
     222  h_St_store x_14904 x_14903 x_14902 x_14901
     223| St_call_id (x_14908, x_14907, x_14906, x_14905) ->
     224  h_St_call_id x_14908 x_14907 x_14906 x_14905
     225| St_call_ptr (x_14912, x_14911, x_14910, x_14909) ->
     226  h_St_call_ptr x_14912 x_14911 x_14910 x_14909
     227| St_cond (x_14915, x_14914, x_14913) -> h_St_cond x_14915 x_14914 x_14913
    228228| St_return -> h_St_return
    229229
     
    244244    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
    245245let 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
    246 | St_skip x_14915 -> h_St_skip x_14915
    247 | St_cost (x_14917, x_14916) -> h_St_cost x_14917 x_14916
    248 | St_const (t, x_14920, x_14919, x_14918) ->
    249   h_St_const t x_14920 x_14919 x_14918
    250 | St_op1 (t', t, x_14924, x_14923, x_14922, x_14921) ->
    251   h_St_op1 t' t x_14924 x_14923 x_14922 x_14921
    252 | St_op2 (t', t1, t2, x_14929, x_14928, x_14927, x_14926, x_14925) ->
    253   h_St_op2 t' t1 t2 x_14929 x_14928 x_14927 x_14926 x_14925
    254 | St_load (x_14933, x_14932, x_14931, x_14930) ->
    255   h_St_load x_14933 x_14932 x_14931 x_14930
    256 | St_store (x_14937, x_14936, x_14935, x_14934) ->
    257   h_St_store x_14937 x_14936 x_14935 x_14934
    258 | St_call_id (x_14941, x_14940, x_14939, x_14938) ->
    259   h_St_call_id x_14941 x_14940 x_14939 x_14938
    260 | St_call_ptr (x_14945, x_14944, x_14943, x_14942) ->
    261   h_St_call_ptr x_14945 x_14944 x_14943 x_14942
    262 | St_cond (x_14948, x_14947, x_14946) -> h_St_cond x_14948 x_14947 x_14946
     246| St_skip x_14928 -> h_St_skip x_14928
     247| St_cost (x_14930, x_14929) -> h_St_cost x_14930 x_14929
     248| St_const (t, x_14933, x_14932, x_14931) ->
     249  h_St_const t x_14933 x_14932 x_14931
     250| St_op1 (t', t, x_14937, x_14936, x_14935, x_14934) ->
     251  h_St_op1 t' t x_14937 x_14936 x_14935 x_14934
     252| St_op2 (t', t1, t2, x_14942, x_14941, x_14940, x_14939, x_14938) ->
     253  h_St_op2 t' t1 t2 x_14942 x_14941 x_14940 x_14939 x_14938
     254| St_load (x_14946, x_14945, x_14944, x_14943) ->
     255  h_St_load x_14946 x_14945 x_14944 x_14943
     256| St_store (x_14950, x_14949, x_14948, x_14947) ->
     257  h_St_store x_14950 x_14949 x_14948 x_14947
     258| St_call_id (x_14954, x_14953, x_14952, x_14951) ->
     259  h_St_call_id x_14954 x_14953 x_14952 x_14951
     260| St_call_ptr (x_14958, x_14957, x_14956, x_14955) ->
     261  h_St_call_ptr x_14958 x_14957 x_14956 x_14955
     262| St_cond (x_14961, x_14960, x_14959) -> h_St_cond x_14961 x_14960 x_14959
    263263| St_return -> h_St_return
    264264
     
    279279    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
    280280let 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
    281 | St_skip x_14961 -> h_St_skip x_14961
    282 | St_cost (x_14963, x_14962) -> h_St_cost x_14963 x_14962
    283 | St_const (t, x_14966, x_14965, x_14964) ->
    284   h_St_const t x_14966 x_14965 x_14964
    285 | St_op1 (t', t, x_14970, x_14969, x_14968, x_14967) ->
    286   h_St_op1 t' t x_14970 x_14969 x_14968 x_14967
    287 | St_op2 (t', t1, t2, x_14975, x_14974, x_14973, x_14972, x_14971) ->
    288   h_St_op2 t' t1 t2 x_14975 x_14974 x_14973 x_14972 x_14971
    289 | St_load (x_14979, x_14978, x_14977, x_14976) ->
    290   h_St_load x_14979 x_14978 x_14977 x_14976
    291 | St_store (x_14983, x_14982, x_14981, x_14980) ->
    292   h_St_store x_14983 x_14982 x_14981 x_14980
    293 | St_call_id (x_14987, x_14986, x_14985, x_14984) ->
    294   h_St_call_id x_14987 x_14986 x_14985 x_14984
    295 | St_call_ptr (x_14991, x_14990, x_14989, x_14988) ->
    296   h_St_call_ptr x_14991 x_14990 x_14989 x_14988
    297 | St_cond (x_14994, x_14993, x_14992) -> h_St_cond x_14994 x_14993 x_14992
     281| St_skip x_14974 -> h_St_skip x_14974
     282| St_cost (x_14976, x_14975) -> h_St_cost x_14976 x_14975
     283| St_const (t, x_14979, x_14978, x_14977) ->
     284  h_St_const t x_14979 x_14978 x_14977
     285| St_op1 (t', t, x_14983, x_14982, x_14981, x_14980) ->
     286  h_St_op1 t' t x_14983 x_14982 x_14981 x_14980
     287| St_op2 (t', t1, t2, x_14988, x_14987, x_14986, x_14985, x_14984) ->
     288  h_St_op2 t' t1 t2 x_14988 x_14987 x_14986 x_14985 x_14984
     289| St_load (x_14992, x_14991, x_14990, x_14989) ->
     290  h_St_load x_14992 x_14991 x_14990 x_14989
     291| St_store (x_14996, x_14995, x_14994, x_14993) ->
     292  h_St_store x_14996 x_14995 x_14994 x_14993
     293| St_call_id (x_15000, x_14999, x_14998, x_14997) ->
     294  h_St_call_id x_15000 x_14999 x_14998 x_14997
     295| St_call_ptr (x_15004, x_15003, x_15002, x_15001) ->
     296  h_St_call_ptr x_15004 x_15003 x_15002 x_15001
     297| St_cond (x_15007, x_15006, x_15005) -> h_St_cond x_15007 x_15006 x_15005
    298298| St_return -> h_St_return
    299299
     
    314314    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
    315315let 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
    316 | St_skip x_15007 -> h_St_skip x_15007
    317 | St_cost (x_15009, x_15008) -> h_St_cost x_15009 x_15008
    318 | St_const (t, x_15012, x_15011, x_15010) ->
    319   h_St_const t x_15012 x_15011 x_15010
    320 | St_op1 (t', t, x_15016, x_15015, x_15014, x_15013) ->
    321   h_St_op1 t' t x_15016 x_15015 x_15014 x_15013
    322 | St_op2 (t', t1, t2, x_15021, x_15020, x_15019, x_15018, x_15017) ->
    323   h_St_op2 t' t1 t2 x_15021 x_15020 x_15019 x_15018 x_15017
    324 | St_load (x_15025, x_15024, x_15023, x_15022) ->
    325   h_St_load x_15025 x_15024 x_15023 x_15022
    326 | St_store (x_15029, x_15028, x_15027, x_15026) ->
    327   h_St_store x_15029 x_15028 x_15027 x_15026
    328 | St_call_id (x_15033, x_15032, x_15031, x_15030) ->
    329   h_St_call_id x_15033 x_15032 x_15031 x_15030
    330 | St_call_ptr (x_15037, x_15036, x_15035, x_15034) ->
    331   h_St_call_ptr x_15037 x_15036 x_15035 x_15034
    332 | St_cond (x_15040, x_15039, x_15038) -> h_St_cond x_15040 x_15039 x_15038
     316| St_skip x_15020 -> h_St_skip x_15020
     317| St_cost (x_15022, x_15021) -> h_St_cost x_15022 x_15021
     318| St_const (t, x_15025, x_15024, x_15023) ->
     319  h_St_const t x_15025 x_15024 x_15023
     320| St_op1 (t', t, x_15029, x_15028, x_15027, x_15026) ->
     321  h_St_op1 t' t x_15029 x_15028 x_15027 x_15026
     322| St_op2 (t', t1, t2, x_15034, x_15033, x_15032, x_15031, x_15030) ->
     323  h_St_op2 t' t1 t2 x_15034 x_15033 x_15032 x_15031 x_15030
     324| St_load (x_15038, x_15037, x_15036, x_15035) ->
     325  h_St_load x_15038 x_15037 x_15036 x_15035
     326| St_store (x_15042, x_15041, x_15040, x_15039) ->
     327  h_St_store x_15042 x_15041 x_15040 x_15039
     328| St_call_id (x_15046, x_15045, x_15044, x_15043) ->
     329  h_St_call_id x_15046 x_15045 x_15044 x_15043
     330| St_call_ptr (x_15050, x_15049, x_15048, x_15047) ->
     331  h_St_call_ptr x_15050 x_15049 x_15048 x_15047
     332| St_cond (x_15053, x_15052, x_15051) -> h_St_cond x_15053 x_15052 x_15051
    333333| St_return -> h_St_return
    334334
     
    466466    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
    467467    internal_function -> 'a1 **)
    468 let rec internal_function_rect_Type4 h_mk_internal_function x_15330 =
     468let rec internal_function_rect_Type4 h_mk_internal_function x_15343 =
    469469  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    470470    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    471     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15330
     471    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15343
    472472  in
    473473  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
     
    481481    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
    482482    internal_function -> 'a1 **)
    483 let rec internal_function_rect_Type5 h_mk_internal_function x_15332 =
     483let rec internal_function_rect_Type5 h_mk_internal_function x_15345 =
    484484  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    485485    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    486     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15332
     486    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15345
    487487  in
    488488  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
     
    496496    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
    497497    internal_function -> 'a1 **)
    498 let rec internal_function_rect_Type3 h_mk_internal_function x_15334 =
     498let rec internal_function_rect_Type3 h_mk_internal_function x_15347 =
    499499  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    500500    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    501     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15334
     501    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15347
    502502  in
    503503  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
     
    511511    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
    512512    internal_function -> 'a1 **)
    513 let rec internal_function_rect_Type2 h_mk_internal_function x_15336 =
     513let rec internal_function_rect_Type2 h_mk_internal_function x_15349 =
    514514  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    515515    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    516     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15336
     516    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15349
    517517  in
    518518  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
     
    526526    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
    527527    internal_function -> 'a1 **)
    528 let rec internal_function_rect_Type1 h_mk_internal_function x_15338 =
     528let rec internal_function_rect_Type1 h_mk_internal_function x_15351 =
    529529  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    530530    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    531     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15338
     531    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15351
    532532  in
    533533  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
     
    541541    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
    542542    internal_function -> 'a1 **)
    543 let rec internal_function_rect_Type0 h_mk_internal_function x_15340 =
     543let rec internal_function_rect_Type0 h_mk_internal_function x_15353 =
    544544  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    545545    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    546     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15340
     546    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15353
    547547  in
    548548  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
Note: See TracChangeset for help on using the changeset viewer.