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

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/rTLabs_traces.ml
r2873 r2951 296 296 'a1) > Nat.nat > RTLabs_semantics.state > (IO.io_out, IO.io_in) 297 297 flat_trace > will_return > 'a1 **) 298 let rec will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_1 7878 s x_17877= function299  Wr_step (s0, tr, s', depth, trace, x_1 7880) >300 h_wr_step s0 tr s' depth __ trace __ x_1 7880298 let rec will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_1409 s x_1408 = function 299  Wr_step (s0, tr, s', depth, trace, x_1411) > 300 h_wr_step s0 tr s' depth __ trace __ x_1411 301 301 (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth 302 s' trace x_1 7880)303  Wr_call (s0, tr, s', depth, trace, x_1 7882) >304 h_wr_call s0 tr s' depth __ trace __ x_1 7882302 s' trace x_1411) 303  Wr_call (s0, tr, s', depth, trace, x_1413) > 304 h_wr_call s0 tr s' depth __ trace __ x_1413 305 305 (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S 306 depth) s' trace x_1 7882)307  Wr_ret (s0, tr, s', depth, trace, x_1 7884) >308 h_wr_ret s0 tr s' depth __ trace __ x_1 7884306 depth) s' trace x_1413) 307  Wr_ret (s0, tr, s', depth, trace, x_1415) > 308 h_wr_ret s0 tr s' depth __ trace __ x_1415 309 309 (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth 310 s' trace x_1 7884)310 s' trace x_1415) 311 311  Wr_base (s0, tr, s', trace) > h_wr_base s0 tr s' __ trace __ 312 312 … … 323 323 'a1) > Nat.nat > RTLabs_semantics.state > (IO.io_out, IO.io_in) 324 324 flat_trace > will_return > 'a1 **) 325 let rec will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_1 7906 s x_17905= function326  Wr_step (s0, tr, s', depth, trace, x_1 7908) >327 h_wr_step s0 tr s' depth __ trace __ x_1 7908325 let rec will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_1437 s x_1436 = function 326  Wr_step (s0, tr, s', depth, trace, x_1439) > 327 h_wr_step s0 tr s' depth __ trace __ x_1439 328 328 (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth 329 s' trace x_1 7908)330  Wr_call (s0, tr, s', depth, trace, x_1 7910) >331 h_wr_call s0 tr s' depth __ trace __ x_1 7910329 s' trace x_1439) 330  Wr_call (s0, tr, s', depth, trace, x_1441) > 331 h_wr_call s0 tr s' depth __ trace __ x_1441 332 332 (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S 333 depth) s' trace x_1 7910)334  Wr_ret (s0, tr, s', depth, trace, x_1 7912) >335 h_wr_ret s0 tr s' depth __ trace __ x_1 7912333 depth) s' trace x_1441) 334  Wr_ret (s0, tr, s', depth, trace, x_1443) > 335 h_wr_ret s0 tr s' depth __ trace __ x_1443 336 336 (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth 337 s' trace x_1 7912)337 s' trace x_1443) 338 338  Wr_base (s0, tr, s', trace) > h_wr_base s0 tr s' __ trace __ 339 339 … … 350 350 'a1) > Nat.nat > RTLabs_semantics.state > (IO.io_out, IO.io_in) 351 351 flat_trace > will_return > 'a1 **) 352 let rec will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_1 7920 s x_17919= function353  Wr_step (s0, tr, s', depth, trace, x_1 7922) >354 h_wr_step s0 tr s' depth __ trace __ x_1 7922352 let rec will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_1451 s x_1450 = function 353  Wr_step (s0, tr, s', depth, trace, x_1453) > 354 h_wr_step s0 tr s' depth __ trace __ x_1453 355 355 (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth 356 s' trace x_1 7922)357  Wr_call (s0, tr, s', depth, trace, x_1 7924) >358 h_wr_call s0 tr s' depth __ trace __ x_1 7924356 s' trace x_1453) 357  Wr_call (s0, tr, s', depth, trace, x_1455) > 358 h_wr_call s0 tr s' depth __ trace __ x_1455 359 359 (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S 360 depth) s' trace x_1 7924)361  Wr_ret (s0, tr, s', depth, trace, x_1 7926) >362 h_wr_ret s0 tr s' depth __ trace __ x_1 7926360 depth) s' trace x_1455) 361  Wr_ret (s0, tr, s', depth, trace, x_1457) > 362 h_wr_ret s0 tr s' depth __ trace __ x_1457 363 363 (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth 364 s' trace x_1 7926)364 s' trace x_1457) 365 365  Wr_base (s0, tr, s', trace) > h_wr_base s0 tr s' __ trace __ 366 366 … … 377 377 'a1) > Nat.nat > RTLabs_semantics.state > (IO.io_out, IO.io_in) 378 378 flat_trace > will_return > 'a1 **) 379 let rec will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_1 7934 s x_17933= function380  Wr_step (s0, tr, s', depth, trace, x_1 7936) >381 h_wr_step s0 tr s' depth __ trace __ x_1 7936379 let rec will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_1465 s x_1464 = function 380  Wr_step (s0, tr, s', depth, trace, x_1467) > 381 h_wr_step s0 tr s' depth __ trace __ x_1467 382 382 (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth 383 s' trace x_1 7936)384  Wr_call (s0, tr, s', depth, trace, x_1 7938) >385 h_wr_call s0 tr s' depth __ trace __ x_1 7938383 s' trace x_1467) 384  Wr_call (s0, tr, s', depth, trace, x_1469) > 385 h_wr_call s0 tr s' depth __ trace __ x_1469 386 386 (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S 387 depth) s' trace x_1 7938)388  Wr_ret (s0, tr, s', depth, trace, x_1 7940) >389 h_wr_ret s0 tr s' depth __ trace __ x_1 7940387 depth) s' trace x_1469) 388  Wr_ret (s0, tr, s', depth, trace, x_1471) > 389 h_wr_ret s0 tr s' depth __ trace __ x_1471 390 390 (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth 391 s' trace x_1 7940)391 s' trace x_1471) 392 392  Wr_base (s0, tr, s', trace) > h_wr_base s0 tr s' __ trace __ 393 393 … … 404 404 'a1) > Nat.nat > RTLabs_semantics.state > (IO.io_out, IO.io_in) 405 405 flat_trace > will_return > 'a1 **) 406 let rec will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_1 7948 s x_17947= function407  Wr_step (s0, tr, s', depth, trace, x_1 7950) >408 h_wr_step s0 tr s' depth __ trace __ x_1 7950406 let rec will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_1479 s x_1478 = function 407  Wr_step (s0, tr, s', depth, trace, x_1481) > 408 h_wr_step s0 tr s' depth __ trace __ x_1481 409 409 (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth 410 s' trace x_1 7950)411  Wr_call (s0, tr, s', depth, trace, x_1 7952) >412 h_wr_call s0 tr s' depth __ trace __ x_1 7952410 s' trace x_1481) 411  Wr_call (s0, tr, s', depth, trace, x_1483) > 412 h_wr_call s0 tr s' depth __ trace __ x_1483 413 413 (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S 414 depth) s' trace x_1 7952)415  Wr_ret (s0, tr, s', depth, trace, x_1 7954) >416 h_wr_ret s0 tr s' depth __ trace __ x_1 7954414 depth) s' trace x_1483) 415  Wr_ret (s0, tr, s', depth, trace, x_1485) > 416 h_wr_ret s0 tr s' depth __ trace __ x_1485 417 417 (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth 418 s' trace x_1 7954)418 s' trace x_1485) 419 419  Wr_base (s0, tr, s', trace) > h_wr_base s0 tr s' __ trace __ 420 420 … … 839 839 (IO.io_out, IO.io_in) flat_trace > __ > 'a1 > __ > __ > 'a2) > 'a1 840 840 trace_result > 'a2 **) 841 let rec trace_result_rect_Type4 ge depth ends start full original_terminates limit h_mk_trace_result x_ 18489=841 let rec trace_result_rect_Type4 ge depth ends start full original_terminates limit h_mk_trace_result x_2020 = 842 842 let { new_state = new_state0; remainder = remainder0; new_trace = 843 new_trace0; terminates = terminates0 } = x_ 18489843 new_trace0; terminates = terminates0 } = x_2020 844 844 in 845 845 h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0 … … 851 851 (IO.io_out, IO.io_in) flat_trace > __ > 'a1 > __ > __ > 'a2) > 'a1 852 852 trace_result > 'a2 **) 853 let rec trace_result_rect_Type5 ge depth ends start full original_terminates limit h_mk_trace_result x_ 18491=853 let rec trace_result_rect_Type5 ge depth ends start full original_terminates limit h_mk_trace_result x_2022 = 854 854 let { new_state = new_state0; remainder = remainder0; new_trace = 855 new_trace0; terminates = terminates0 } = x_ 18491855 new_trace0; terminates = terminates0 } = x_2022 856 856 in 857 857 h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0 … … 863 863 (IO.io_out, IO.io_in) flat_trace > __ > 'a1 > __ > __ > 'a2) > 'a1 864 864 trace_result > 'a2 **) 865 let rec trace_result_rect_Type3 ge depth ends start full original_terminates limit h_mk_trace_result x_ 18493=865 let rec trace_result_rect_Type3 ge depth ends start full original_terminates limit h_mk_trace_result x_2024 = 866 866 let { new_state = new_state0; remainder = remainder0; new_trace = 867 new_trace0; terminates = terminates0 } = x_ 18493867 new_trace0; terminates = terminates0 } = x_2024 868 868 in 869 869 h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0 … … 875 875 (IO.io_out, IO.io_in) flat_trace > __ > 'a1 > __ > __ > 'a2) > 'a1 876 876 trace_result > 'a2 **) 877 let rec trace_result_rect_Type2 ge depth ends start full original_terminates limit h_mk_trace_result x_ 18495=877 let rec trace_result_rect_Type2 ge depth ends start full original_terminates limit h_mk_trace_result x_2026 = 878 878 let { new_state = new_state0; remainder = remainder0; new_trace = 879 new_trace0; terminates = terminates0 } = x_ 18495879 new_trace0; terminates = terminates0 } = x_2026 880 880 in 881 881 h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0 … … 887 887 (IO.io_out, IO.io_in) flat_trace > __ > 'a1 > __ > __ > 'a2) > 'a1 888 888 trace_result > 'a2 **) 889 let rec trace_result_rect_Type1 ge depth ends start full original_terminates limit h_mk_trace_result x_ 18497=889 let rec trace_result_rect_Type1 ge depth ends start full original_terminates limit h_mk_trace_result x_2028 = 890 890 let { new_state = new_state0; remainder = remainder0; new_trace = 891 new_trace0; terminates = terminates0 } = x_ 18497891 new_trace0; terminates = terminates0 } = x_2028 892 892 in 893 893 h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0 … … 899 899 (IO.io_out, IO.io_in) flat_trace > __ > 'a1 > __ > __ > 'a2) > 'a1 900 900 trace_result > 'a2 **) 901 let rec trace_result_rect_Type0 ge depth ends start full original_terminates limit h_mk_trace_result x_ 18499=901 let rec trace_result_rect_Type0 ge depth ends start full original_terminates limit h_mk_trace_result x_2030 = 902 902 let { new_state = new_state0; remainder = remainder0; new_trace = 903 new_trace0; terminates = terminates0 } = x_ 18499903 new_trace0; terminates = terminates0 } = x_2030 904 904 in 905 905 h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0 … … 999 999 (StructuredTraces.trace_ends_with_ret > 'a1 trace_result > 'a2) > 'a1 1000 1000 sub_trace_result > 'a2 **) 1001 let rec sub_trace_result_rect_Type4 ge depth start full original_terminates limit h_mk_sub_trace_result x_ 18517=1002 let { ends = ends0; trace_res = trace_res0 } = x_ 18517in1001 let rec sub_trace_result_rect_Type4 ge depth start full original_terminates limit h_mk_sub_trace_result x_2048 = 1002 let { ends = ends0; trace_res = trace_res0 } = x_2048 in 1003 1003 h_mk_sub_trace_result ends0 trace_res0 1004 1004 … … 1008 1008 (StructuredTraces.trace_ends_with_ret > 'a1 trace_result > 'a2) > 'a1 1009 1009 sub_trace_result > 'a2 **) 1010 let rec sub_trace_result_rect_Type5 ge depth start full original_terminates limit h_mk_sub_trace_result x_ 18519=1011 let { ends = ends0; trace_res = trace_res0 } = x_ 18519in1010 let rec sub_trace_result_rect_Type5 ge depth start full original_terminates limit h_mk_sub_trace_result x_2050 = 1011 let { ends = ends0; trace_res = trace_res0 } = x_2050 in 1012 1012 h_mk_sub_trace_result ends0 trace_res0 1013 1013 … … 1017 1017 (StructuredTraces.trace_ends_with_ret > 'a1 trace_result > 'a2) > 'a1 1018 1018 sub_trace_result > 'a2 **) 1019 let rec sub_trace_result_rect_Type3 ge depth start full original_terminates limit h_mk_sub_trace_result x_ 18521=1020 let { ends = ends0; trace_res = trace_res0 } = x_ 18521in1019 let rec sub_trace_result_rect_Type3 ge depth start full original_terminates limit h_mk_sub_trace_result x_2052 = 1020 let { ends = ends0; trace_res = trace_res0 } = x_2052 in 1021 1021 h_mk_sub_trace_result ends0 trace_res0 1022 1022 … … 1026 1026 (StructuredTraces.trace_ends_with_ret > 'a1 trace_result > 'a2) > 'a1 1027 1027 sub_trace_result > 'a2 **) 1028 let rec sub_trace_result_rect_Type2 ge depth start full original_terminates limit h_mk_sub_trace_result x_ 18523=1029 let { ends = ends0; trace_res = trace_res0 } = x_ 18523in1028 let rec sub_trace_result_rect_Type2 ge depth start full original_terminates limit h_mk_sub_trace_result x_2054 = 1029 let { ends = ends0; trace_res = trace_res0 } = x_2054 in 1030 1030 h_mk_sub_trace_result ends0 trace_res0 1031 1031 … … 1035 1035 (StructuredTraces.trace_ends_with_ret > 'a1 trace_result > 'a2) > 'a1 1036 1036 sub_trace_result > 'a2 **) 1037 let rec sub_trace_result_rect_Type1 ge depth start full original_terminates limit h_mk_sub_trace_result x_ 18525=1038 let { ends = ends0; trace_res = trace_res0 } = x_ 18525in1037 let rec sub_trace_result_rect_Type1 ge depth start full original_terminates limit h_mk_sub_trace_result x_2056 = 1038 let { ends = ends0; trace_res = trace_res0 } = x_2056 in 1039 1039 h_mk_sub_trace_result ends0 trace_res0 1040 1040 … … 1044 1044 (StructuredTraces.trace_ends_with_ret > 'a1 trace_result > 'a2) > 'a1 1045 1045 sub_trace_result > 'a2 **) 1046 let rec sub_trace_result_rect_Type0 ge depth start full original_terminates limit h_mk_sub_trace_result x_ 18527=1047 let { ends = ends0; trace_res = trace_res0 } = x_ 18527in1046 let rec sub_trace_result_rect_Type0 ge depth start full original_terminates limit h_mk_sub_trace_result x_2058 = 1047 let { ends = ends0; trace_res = trace_res0 } = x_2058 in 1048 1048 h_mk_sub_trace_result ends0 trace_res0 1049 1049 … … 1472 1472 (Pointers.block, __) Types.dPair **) 1473 1473 let init_state_is p s = 1474 RTLabs_semantics.bind_ok 1475 (Globalenvs.init_mem (fun x > List.Cons ((AST.Init_space x), List.Nil)) 1476 p) (fun x > 1474 RTLabs_semantics.bind_ok (Globalenvs.init_mem (fun x > x) p) (fun x > 1477 1475 let main = p.AST.prog_main in 1478 1476 Obj.magic … … 1558 1556 ('a1, 'a2) partial_flat_trace > 'a3 > 'a3) > RTLabs_semantics.state > 1559 1557 RTLabs_semantics.state > ('a1, 'a2) partial_flat_trace > 'a3 **) 1560 let rec partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step x_ 18862 x_18861= function1558 let rec partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step x_2393 x_2392 = function 1561 1559  Pft_base (s, tr, s') > h_pft_base s tr s' __ 1562  Pft_step (s, tr, s', s'', x_ 18865) >1563 h_pft_step s tr s' s'' __ x_ 188651564 (partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step s' s'' x_ 18865)1560  Pft_step (s, tr, s', s'', x_2396) > 1561 h_pft_step s tr s' s'' __ x_2396 1562 (partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step s' s'' x_2396) 1565 1563 1566 1564 (** val partial_flat_trace_rect_Type3 : … … 1570 1568 ('a1, 'a2) partial_flat_trace > 'a3 > 'a3) > RTLabs_semantics.state > 1571 1569 RTLabs_semantics.state > ('a1, 'a2) partial_flat_trace > 'a3 **) 1572 let rec partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step x_ 18878 x_18877= function1570 let rec partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step x_2409 x_2408 = function 1573 1571  Pft_base (s, tr, s') > h_pft_base s tr s' __ 1574  Pft_step (s, tr, s', s'', x_ 18881) >1575 h_pft_step s tr s' s'' __ x_ 188811576 (partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step s' s'' x_ 18881)1572  Pft_step (s, tr, s', s'', x_2412) > 1573 h_pft_step s tr s' s'' __ x_2412 1574 (partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step s' s'' x_2412) 1577 1575 1578 1576 (** val partial_flat_trace_rect_Type2 : … … 1582 1580 ('a1, 'a2) partial_flat_trace > 'a3 > 'a3) > RTLabs_semantics.state > 1583 1581 RTLabs_semantics.state > ('a1, 'a2) partial_flat_trace > 'a3 **) 1584 let rec partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step x_ 18886 x_18885= function1582 let rec partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step x_2417 x_2416 = function 1585 1583  Pft_base (s, tr, s') > h_pft_base s tr s' __ 1586  Pft_step (s, tr, s', s'', x_ 18889) >1587 h_pft_step s tr s' s'' __ x_ 188891588 (partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step s' s'' x_ 18889)1584  Pft_step (s, tr, s', s'', x_2420) > 1585 h_pft_step s tr s' s'' __ x_2420 1586 (partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step s' s'' x_2420) 1589 1587 1590 1588 (** val partial_flat_trace_rect_Type1 : … … 1594 1592 ('a1, 'a2) partial_flat_trace > 'a3 > 'a3) > RTLabs_semantics.state > 1595 1593 RTLabs_semantics.state > ('a1, 'a2) partial_flat_trace > 'a3 **) 1596 let rec partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step x_ 18894 x_18893= function1594 let rec partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step x_2425 x_2424 = function 1597 1595  Pft_base (s, tr, s') > h_pft_base s tr s' __ 1598  Pft_step (s, tr, s', s'', x_ 18897) >1599 h_pft_step s tr s' s'' __ x_ 188971600 (partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step s' s'' x_ 18897)1596  Pft_step (s, tr, s', s'', x_2428) > 1597 h_pft_step s tr s' s'' __ x_2428 1598 (partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step s' s'' x_2428) 1601 1599 1602 1600 (** val partial_flat_trace_rect_Type0 : … … 1606 1604 ('a1, 'a2) partial_flat_trace > 'a3 > 'a3) > RTLabs_semantics.state > 1607 1605 RTLabs_semantics.state > ('a1, 'a2) partial_flat_trace > 'a3 **) 1608 let rec partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step x_ 18902 x_18901= function1606 let rec partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step x_2433 x_2432 = function 1609 1607  Pft_base (s, tr, s') > h_pft_base s tr s' __ 1610  Pft_step (s, tr, s', s'', x_ 18905) >1611 h_pft_step s tr s' s'' __ x_ 189051612 (partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step s' s'' x_ 18905)1608  Pft_step (s, tr, s', s'', x_2436) > 1609 h_pft_step s tr s' s'' __ x_2436 1610 (partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step s' s'' x_2436) 1613 1611 1614 1612 (** val partial_flat_trace_inv_rect_Type4 :
Note: See TracChangeset
for help on using the changeset viewer.