Changeset 2951 for extracted/toRTLabs.ml
 Timestamp:
 Mar 25, 2013, 11:30:01 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/toRTLabs.ml
r2827 r2951 142 142 (Identifiers.identifier_set > env > AST.typ Types.option > 'a1) > 143 143 fixed > 'a1 **) 144 let rec fixed_rect_Type4 h_mk_fixed x_15 486=144 let rec fixed_rect_Type4 h_mk_fixed x_15525 = 145 145 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 146 x_15 486146 x_15525 147 147 in 148 148 h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0 … … 151 151 (Identifiers.identifier_set > env > AST.typ Types.option > 'a1) > 152 152 fixed > 'a1 **) 153 let rec fixed_rect_Type5 h_mk_fixed x_15 488=153 let rec fixed_rect_Type5 h_mk_fixed x_15527 = 154 154 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 155 x_15 488155 x_15527 156 156 in 157 157 h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0 … … 160 160 (Identifiers.identifier_set > env > AST.typ Types.option > 'a1) > 161 161 fixed > 'a1 **) 162 let rec fixed_rect_Type3 h_mk_fixed x_15 490=162 let rec fixed_rect_Type3 h_mk_fixed x_15529 = 163 163 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 164 x_15 490164 x_15529 165 165 in 166 166 h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0 … … 169 169 (Identifiers.identifier_set > env > AST.typ Types.option > 'a1) > 170 170 fixed > 'a1 **) 171 let rec fixed_rect_Type2 h_mk_fixed x_15 492=171 let rec fixed_rect_Type2 h_mk_fixed x_15531 = 172 172 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 173 x_15 492173 x_15531 174 174 in 175 175 h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0 … … 178 178 (Identifiers.identifier_set > env > AST.typ Types.option > 'a1) > 179 179 fixed > 'a1 **) 180 let rec fixed_rect_Type1 h_mk_fixed x_15 494=180 let rec fixed_rect_Type1 h_mk_fixed x_15533 = 181 181 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 182 x_15 494182 x_15533 183 183 in 184 184 h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0 … … 187 187 (Identifiers.identifier_set > env > AST.typ Types.option > 'a1) > 188 188 fixed > 'a1 **) 189 let rec fixed_rect_Type0 h_mk_fixed x_15 496=189 let rec fixed_rect_Type0 h_mk_fixed x_15535 = 190 190 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 191 x_15 496191 x_15535 192 192 in 193 193 h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0 … … 257 257 (PreIdentifiers.identifier Identifiers.identifier_map > __ > __ > 'a1) 258 258 > goto_map > 'a1 **) 259 let rec goto_map_rect_Type4 fx g h_mk_goto_map x_155 12=260 let gm_map = x_155 12in h_mk_goto_map gm_map __ __259 let rec goto_map_rect_Type4 fx g h_mk_goto_map x_15551 = 260 let gm_map = x_15551 in h_mk_goto_map gm_map __ __ 261 261 262 262 (** val goto_map_rect_Type5 : … … 264 264 (PreIdentifiers.identifier Identifiers.identifier_map > __ > __ > 'a1) 265 265 > goto_map > 'a1 **) 266 let rec goto_map_rect_Type5 fx g h_mk_goto_map x_155 14=267 let gm_map = x_155 14in h_mk_goto_map gm_map __ __266 let rec goto_map_rect_Type5 fx g h_mk_goto_map x_15553 = 267 let gm_map = x_15553 in h_mk_goto_map gm_map __ __ 268 268 269 269 (** val goto_map_rect_Type3 : … … 271 271 (PreIdentifiers.identifier Identifiers.identifier_map > __ > __ > 'a1) 272 272 > goto_map > 'a1 **) 273 let rec goto_map_rect_Type3 fx g h_mk_goto_map x_155 16=274 let gm_map = x_155 16in h_mk_goto_map gm_map __ __273 let rec goto_map_rect_Type3 fx g h_mk_goto_map x_15555 = 274 let gm_map = x_15555 in h_mk_goto_map gm_map __ __ 275 275 276 276 (** val goto_map_rect_Type2 : … … 278 278 (PreIdentifiers.identifier Identifiers.identifier_map > __ > __ > 'a1) 279 279 > goto_map > 'a1 **) 280 let rec goto_map_rect_Type2 fx g h_mk_goto_map x_155 18=281 let gm_map = x_155 18in h_mk_goto_map gm_map __ __280 let rec goto_map_rect_Type2 fx g h_mk_goto_map x_15557 = 281 let gm_map = x_15557 in h_mk_goto_map gm_map __ __ 282 282 283 283 (** val goto_map_rect_Type1 : … … 285 285 (PreIdentifiers.identifier Identifiers.identifier_map > __ > __ > 'a1) 286 286 > goto_map > 'a1 **) 287 let rec goto_map_rect_Type1 fx g h_mk_goto_map x_155 20=288 let gm_map = x_155 20in h_mk_goto_map gm_map __ __287 let rec goto_map_rect_Type1 fx g h_mk_goto_map x_15559 = 288 let gm_map = x_15559 in h_mk_goto_map gm_map __ __ 289 289 290 290 (** val goto_map_rect_Type0 : … … 292 292 (PreIdentifiers.identifier Identifiers.identifier_map > __ > __ > 'a1) 293 293 > goto_map > 'a1 **) 294 let rec goto_map_rect_Type0 fx g h_mk_goto_map x_155 22=295 let gm_map = x_155 22in h_mk_goto_map gm_map __ __294 let rec goto_map_rect_Type0 fx g h_mk_goto_map x_15561 = 295 let gm_map = x_15561 in h_mk_goto_map gm_map __ __ 296 296 297 297 (** val gm_map : … … 401 401 Graphs.label Types.sig0 > Graphs.label Types.sig0 > 'a1) > partial_fn 402 402 > 'a1 **) 403 let rec partial_fn_rect_Type4 fx h_mk_partial_fn x_155 40=403 let rec partial_fn_rect_Type4 fx h_mk_partial_fn x_15579 = 404 404 let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params = 405 405 pf_params0; pf_locals = pf_locals0; pf_result = pf_result0; 406 406 pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0; 407 407 pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } = 408 x_155 40408 x_15579 409 409 in 410 410 h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __ … … 419 419 Graphs.label Types.sig0 > Graphs.label Types.sig0 > 'a1) > partial_fn 420 420 > 'a1 **) 421 let rec partial_fn_rect_Type5 fx h_mk_partial_fn x_155 42=421 let rec partial_fn_rect_Type5 fx h_mk_partial_fn x_15581 = 422 422 let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params = 423 423 pf_params0; pf_locals = pf_locals0; pf_result = pf_result0; 424 424 pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0; 425 425 pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } = 426 x_155 42426 x_15581 427 427 in 428 428 h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __ … … 437 437 Graphs.label Types.sig0 > Graphs.label Types.sig0 > 'a1) > partial_fn 438 438 > 'a1 **) 439 let rec partial_fn_rect_Type3 fx h_mk_partial_fn x_155 44=439 let rec partial_fn_rect_Type3 fx h_mk_partial_fn x_15583 = 440 440 let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params = 441 441 pf_params0; pf_locals = pf_locals0; pf_result = pf_result0; 442 442 pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0; 443 443 pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } = 444 x_155 44444 x_15583 445 445 in 446 446 h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __ … … 455 455 Graphs.label Types.sig0 > Graphs.label Types.sig0 > 'a1) > partial_fn 456 456 > 'a1 **) 457 let rec partial_fn_rect_Type2 fx h_mk_partial_fn x_155 46=457 let rec partial_fn_rect_Type2 fx h_mk_partial_fn x_15585 = 458 458 let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params = 459 459 pf_params0; pf_locals = pf_locals0; pf_result = pf_result0; 460 460 pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0; 461 461 pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } = 462 x_155 46462 x_15585 463 463 in 464 464 h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __ … … 473 473 Graphs.label Types.sig0 > Graphs.label Types.sig0 > 'a1) > partial_fn 474 474 > 'a1 **) 475 let rec partial_fn_rect_Type1 fx h_mk_partial_fn x_155 48=475 let rec partial_fn_rect_Type1 fx h_mk_partial_fn x_15587 = 476 476 let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params = 477 477 pf_params0; pf_locals = pf_locals0; pf_result = pf_result0; 478 478 pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0; 479 479 pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } = 480 x_155 48480 x_15587 481 481 in 482 482 h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __ … … 491 491 Graphs.label Types.sig0 > Graphs.label Types.sig0 > 'a1) > partial_fn 492 492 > 'a1 **) 493 let rec partial_fn_rect_Type0 fx h_mk_partial_fn x_155 50=493 let rec partial_fn_rect_Type0 fx h_mk_partial_fn x_15589 = 494 494 let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params = 495 495 pf_params0; pf_locals = pf_locals0; pf_result = pf_result0; 496 496 pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0; 497 497 pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } = 498 x_155 50498 x_15589 499 499 in 500 500 h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __ … … 874 874 Cminor_syntax.stmt > partial_fn Types.sig0 > 'a1) > partial_fn > 875 875 fn_con_because > 'a1 **) 876 let rec fn_con_because_rect_Type4 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_156 26= function876 let rec fn_con_because_rect_Type4 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15665 = function 877 877  Fn_con_eq f > h_fn_con_eq f 878 878  Fn_con_sig (f1, f2, f3) > h_fn_con_sig f1 f2 __ f3 … … 884 884 Cminor_syntax.stmt > partial_fn Types.sig0 > 'a1) > partial_fn > 885 885 fn_con_because > 'a1 **) 886 let rec fn_con_because_rect_Type5 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_156 33= function886 let rec fn_con_because_rect_Type5 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15672 = function 887 887  Fn_con_eq f > h_fn_con_eq f 888 888  Fn_con_sig (f1, f2, f3) > h_fn_con_sig f1 f2 __ f3 … … 894 894 Cminor_syntax.stmt > partial_fn Types.sig0 > 'a1) > partial_fn > 895 895 fn_con_because > 'a1 **) 896 let rec fn_con_because_rect_Type3 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_156 40= function896 let rec fn_con_because_rect_Type3 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15679 = function 897 897  Fn_con_eq f > h_fn_con_eq f 898 898  Fn_con_sig (f1, f2, f3) > h_fn_con_sig f1 f2 __ f3 … … 904 904 Cminor_syntax.stmt > partial_fn Types.sig0 > 'a1) > partial_fn > 905 905 fn_con_because > 'a1 **) 906 let rec fn_con_because_rect_Type2 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_156 47= function906 let rec fn_con_because_rect_Type2 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15686 = function 907 907  Fn_con_eq f > h_fn_con_eq f 908 908  Fn_con_sig (f1, f2, f3) > h_fn_con_sig f1 f2 __ f3 … … 914 914 Cminor_syntax.stmt > partial_fn Types.sig0 > 'a1) > partial_fn > 915 915 fn_con_because > 'a1 **) 916 let rec fn_con_because_rect_Type1 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_156 54= function916 let rec fn_con_because_rect_Type1 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15693 = function 917 917  Fn_con_eq f > h_fn_con_eq f 918 918  Fn_con_sig (f1, f2, f3) > h_fn_con_sig f1 f2 __ f3 … … 924 924 Cminor_syntax.stmt > partial_fn Types.sig0 > 'a1) > partial_fn > 925 925 fn_con_because > 'a1 **) 926 let rec fn_con_because_rect_Type0 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15 661= function926 let rec fn_con_because_rect_Type0 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15700 = function 927 927  Fn_con_eq f > h_fn_con_eq f 928 928  Fn_con_sig (f1, f2, f3) > h_fn_con_sig f1 f2 __ f3 … … 1163 1163 Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH > dH __ __ __)) __ 1164 1164 1165 (** val expr_is_ Id:1165 (** val expr_is_cst_ident : 1166 1166 AST.typ > Cminor_syntax.expr > AST.ident Types.option **) 1167 let expr_is_Id t = function 1168  Cminor_syntax.Id (x, id) > Types.Some id 1169  Cminor_syntax.Cst (x, x0) > Types.None 1167 let expr_is_cst_ident t = function 1168  Cminor_syntax.Id (x, x0) > Types.None 1169  Cminor_syntax.Cst (x, c) > 1170 (match c with 1171  FrontEndOps.Ointconst (x0, x1, x2) > Types.None 1172  FrontEndOps.Oaddrsymbol (id, n) > 1173 (match n with 1174  Nat.O > Types.Some id 1175  Nat.S x0 > Types.None) 1176  FrontEndOps.Oaddrstack x0 > Types.None) 1170 1177  Cminor_syntax.Op1 (x, x0, x1, x2) > Types.None 1171 1178  Cminor_syntax.Op2 (x, x0, x1, x2, x3, x4) > Types.None … … 1268 1275 in 1269 1276 let f1 = 1270 match expr_is_ IdAST.ASTptr e with1277 match expr_is_cst_ident AST.ASTptr e with 1271 1278  Types.None > 1272 1279 let { Types.dpi1 = f1; Types.dpi2 = fnr } = … … 1390 1397 RTLabs_syntax.f_exit = (Types.pi1 f1).pf_exit })) __)) __)) __ 1391 1398 1392 (** val cminor_ noinit_to_rtlabs :1393 Cminor_syntax.cminor_ noinit_program > RTLabs_syntax.rTLabs_program **)1394 let cminor_ noinit_to_rtlabs p =1399 (** val cminor_to_rtlabs : 1400 Cminor_syntax.cminor_program > RTLabs_syntax.rTLabs_program **) 1401 let cminor_to_rtlabs p = 1395 1402 AST.transform_program p (fun x > AST.transf_fundef c2ra_function) 1396 1403 1397 open Initialisation1398 1399 (** val cminor_to_rtlabs :1400 CostLabel.costlabel > Cminor_syntax.cminor_program >1401 RTLabs_syntax.rTLabs_program **)1402 let cminor_to_rtlabs init_cost p =1403 let p' = Initialisation.replace_init init_cost p in1404 cminor_noinit_to_rtlabs p'1405
Note: See TracChangeset
for help on using the changeset viewer.