Changeset 2730 for extracted/csem.ml


Ignore:
Timestamp:
Feb 25, 2013, 9:54:49 PM (8 years ago)
Author:
sacerdot
Message:

Exported again.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/csem.ml

    r2717 r2730  
    780780let rec cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
    781781| Kstop -> h_Kstop
    782 | Kseq (x_8622, x_8621) ->
    783   h_Kseq x_8622 x_8621
     782| Kseq (x_6713, x_6712) ->
     783  h_Kseq x_6713 x_6712
    784784    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    785       h_Kswitch h_Kcall x_8621)
    786 | Kwhile (x_8625, x_8624, x_8623) ->
    787   h_Kwhile x_8625 x_8624 x_8623
     785      h_Kswitch h_Kcall x_6712)
     786| Kwhile (x_6716, x_6715, x_6714) ->
     787  h_Kwhile x_6716 x_6715 x_6714
    788788    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    789       h_Kswitch h_Kcall x_8623)
    790 | Kdowhile (x_8628, x_8627, x_8626) ->
    791   h_Kdowhile x_8628 x_8627 x_8626
     789      h_Kswitch h_Kcall x_6714)
     790| Kdowhile (x_6719, x_6718, x_6717) ->
     791  h_Kdowhile x_6719 x_6718 x_6717
    792792    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    793       h_Kswitch h_Kcall x_8626)
    794 | Kfor2 (x_8632, x_8631, x_8630, x_8629) ->
    795   h_Kfor2 x_8632 x_8631 x_8630 x_8629
     793      h_Kswitch h_Kcall x_6717)
     794| Kfor2 (x_6723, x_6722, x_6721, x_6720) ->
     795  h_Kfor2 x_6723 x_6722 x_6721 x_6720
    796796    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    797       h_Kswitch h_Kcall x_8629)
    798 | Kfor3 (x_8636, x_8635, x_8634, x_8633) ->
    799   h_Kfor3 x_8636 x_8635 x_8634 x_8633
     797      h_Kswitch h_Kcall x_6720)
     798| Kfor3 (x_6727, x_6726, x_6725, x_6724) ->
     799  h_Kfor3 x_6727 x_6726 x_6725 x_6724
    800800    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    801       h_Kswitch h_Kcall x_8633)
    802 | Kswitch x_8637 ->
    803   h_Kswitch x_8637
     801      h_Kswitch h_Kcall x_6724)
     802| Kswitch x_6728 ->
     803  h_Kswitch x_6728
    804804    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    805       h_Kswitch h_Kcall x_8637)
    806 | Kcall (x_8641, x_8640, x_8639, x_8638) ->
    807   h_Kcall x_8641 x_8640 x_8639 x_8638
     805      h_Kswitch h_Kcall x_6728)
     806| Kcall (x_6732, x_6731, x_6730, x_6729) ->
     807  h_Kcall x_6732 x_6731 x_6730 x_6729
    808808    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    809       h_Kswitch h_Kcall x_8638)
     809      h_Kswitch h_Kcall x_6729)
    810810
    811811(** val cont_rect_Type3 :
     
    820820let rec cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
    821821| Kstop -> h_Kstop
    822 | Kseq (x_8682, x_8681) ->
    823   h_Kseq x_8682 x_8681
     822| Kseq (x_6773, x_6772) ->
     823  h_Kseq x_6773 x_6772
    824824    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    825       h_Kswitch h_Kcall x_8681)
    826 | Kwhile (x_8685, x_8684, x_8683) ->
    827   h_Kwhile x_8685 x_8684 x_8683
     825      h_Kswitch h_Kcall x_6772)
     826| Kwhile (x_6776, x_6775, x_6774) ->
     827  h_Kwhile x_6776 x_6775 x_6774
    828828    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    829       h_Kswitch h_Kcall x_8683)
    830 | Kdowhile (x_8688, x_8687, x_8686) ->
    831   h_Kdowhile x_8688 x_8687 x_8686
     829      h_Kswitch h_Kcall x_6774)
     830| Kdowhile (x_6779, x_6778, x_6777) ->
     831  h_Kdowhile x_6779 x_6778 x_6777
    832832    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    833       h_Kswitch h_Kcall x_8686)
    834 | Kfor2 (x_8692, x_8691, x_8690, x_8689) ->
    835   h_Kfor2 x_8692 x_8691 x_8690 x_8689
     833      h_Kswitch h_Kcall x_6777)
     834| Kfor2 (x_6783, x_6782, x_6781, x_6780) ->
     835  h_Kfor2 x_6783 x_6782 x_6781 x_6780
    836836    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    837       h_Kswitch h_Kcall x_8689)
    838 | Kfor3 (x_8696, x_8695, x_8694, x_8693) ->
    839   h_Kfor3 x_8696 x_8695 x_8694 x_8693
     837      h_Kswitch h_Kcall x_6780)
     838| Kfor3 (x_6787, x_6786, x_6785, x_6784) ->
     839  h_Kfor3 x_6787 x_6786 x_6785 x_6784
    840840    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    841       h_Kswitch h_Kcall x_8693)
    842 | Kswitch x_8697 ->
    843   h_Kswitch x_8697
     841      h_Kswitch h_Kcall x_6784)
     842| Kswitch x_6788 ->
     843  h_Kswitch x_6788
    844844    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    845       h_Kswitch h_Kcall x_8697)
    846 | Kcall (x_8701, x_8700, x_8699, x_8698) ->
    847   h_Kcall x_8701 x_8700 x_8699 x_8698
     845      h_Kswitch h_Kcall x_6788)
     846| Kcall (x_6792, x_6791, x_6790, x_6789) ->
     847  h_Kcall x_6792 x_6791 x_6790 x_6789
    848848    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    849       h_Kswitch h_Kcall x_8698)
     849      h_Kswitch h_Kcall x_6789)
    850850
    851851(** val cont_rect_Type2 :
     
    860860let rec cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
    861861| Kstop -> h_Kstop
    862 | Kseq (x_8712, x_8711) ->
    863   h_Kseq x_8712 x_8711
     862| Kseq (x_6803, x_6802) ->
     863  h_Kseq x_6803 x_6802
    864864    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    865       h_Kswitch h_Kcall x_8711)
    866 | Kwhile (x_8715, x_8714, x_8713) ->
    867   h_Kwhile x_8715 x_8714 x_8713
     865      h_Kswitch h_Kcall x_6802)
     866| Kwhile (x_6806, x_6805, x_6804) ->
     867  h_Kwhile x_6806 x_6805 x_6804
    868868    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    869       h_Kswitch h_Kcall x_8713)
    870 | Kdowhile (x_8718, x_8717, x_8716) ->
    871   h_Kdowhile x_8718 x_8717 x_8716
     869      h_Kswitch h_Kcall x_6804)
     870| Kdowhile (x_6809, x_6808, x_6807) ->
     871  h_Kdowhile x_6809 x_6808 x_6807
    872872    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    873       h_Kswitch h_Kcall x_8716)
    874 | Kfor2 (x_8722, x_8721, x_8720, x_8719) ->
    875   h_Kfor2 x_8722 x_8721 x_8720 x_8719
     873      h_Kswitch h_Kcall x_6807)
     874| Kfor2 (x_6813, x_6812, x_6811, x_6810) ->
     875  h_Kfor2 x_6813 x_6812 x_6811 x_6810
    876876    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    877       h_Kswitch h_Kcall x_8719)
    878 | Kfor3 (x_8726, x_8725, x_8724, x_8723) ->
    879   h_Kfor3 x_8726 x_8725 x_8724 x_8723
     877      h_Kswitch h_Kcall x_6810)
     878| Kfor3 (x_6817, x_6816, x_6815, x_6814) ->
     879  h_Kfor3 x_6817 x_6816 x_6815 x_6814
    880880    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    881       h_Kswitch h_Kcall x_8723)
    882 | Kswitch x_8727 ->
    883   h_Kswitch x_8727
     881      h_Kswitch h_Kcall x_6814)
     882| Kswitch x_6818 ->
     883  h_Kswitch x_6818
    884884    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    885       h_Kswitch h_Kcall x_8727)
    886 | Kcall (x_8731, x_8730, x_8729, x_8728) ->
    887   h_Kcall x_8731 x_8730 x_8729 x_8728
     885      h_Kswitch h_Kcall x_6818)
     886| Kcall (x_6822, x_6821, x_6820, x_6819) ->
     887  h_Kcall x_6822 x_6821 x_6820 x_6819
    888888    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    889       h_Kswitch h_Kcall x_8728)
     889      h_Kswitch h_Kcall x_6819)
    890890
    891891(** val cont_rect_Type1 :
     
    900900let rec cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
    901901| Kstop -> h_Kstop
    902 | Kseq (x_8742, x_8741) ->
    903   h_Kseq x_8742 x_8741
     902| Kseq (x_6833, x_6832) ->
     903  h_Kseq x_6833 x_6832
    904904    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    905       h_Kswitch h_Kcall x_8741)
    906 | Kwhile (x_8745, x_8744, x_8743) ->
    907   h_Kwhile x_8745 x_8744 x_8743
     905      h_Kswitch h_Kcall x_6832)
     906| Kwhile (x_6836, x_6835, x_6834) ->
     907  h_Kwhile x_6836 x_6835 x_6834
    908908    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    909       h_Kswitch h_Kcall x_8743)
    910 | Kdowhile (x_8748, x_8747, x_8746) ->
    911   h_Kdowhile x_8748 x_8747 x_8746
     909      h_Kswitch h_Kcall x_6834)
     910| Kdowhile (x_6839, x_6838, x_6837) ->
     911  h_Kdowhile x_6839 x_6838 x_6837
    912912    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    913       h_Kswitch h_Kcall x_8746)
    914 | Kfor2 (x_8752, x_8751, x_8750, x_8749) ->
    915   h_Kfor2 x_8752 x_8751 x_8750 x_8749
     913      h_Kswitch h_Kcall x_6837)
     914| Kfor2 (x_6843, x_6842, x_6841, x_6840) ->
     915  h_Kfor2 x_6843 x_6842 x_6841 x_6840
    916916    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    917       h_Kswitch h_Kcall x_8749)
    918 | Kfor3 (x_8756, x_8755, x_8754, x_8753) ->
    919   h_Kfor3 x_8756 x_8755 x_8754 x_8753
     917      h_Kswitch h_Kcall x_6840)
     918| Kfor3 (x_6847, x_6846, x_6845, x_6844) ->
     919  h_Kfor3 x_6847 x_6846 x_6845 x_6844
    920920    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    921       h_Kswitch h_Kcall x_8753)
    922 | Kswitch x_8757 ->
    923   h_Kswitch x_8757
     921      h_Kswitch h_Kcall x_6844)
     922| Kswitch x_6848 ->
     923  h_Kswitch x_6848
    924924    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    925       h_Kswitch h_Kcall x_8757)
    926 | Kcall (x_8761, x_8760, x_8759, x_8758) ->
    927   h_Kcall x_8761 x_8760 x_8759 x_8758
     925      h_Kswitch h_Kcall x_6848)
     926| Kcall (x_6852, x_6851, x_6850, x_6849) ->
     927  h_Kcall x_6852 x_6851 x_6850 x_6849
    928928    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    929       h_Kswitch h_Kcall x_8758)
     929      h_Kswitch h_Kcall x_6849)
    930930
    931931(** val cont_rect_Type0 :
     
    940940let rec cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
    941941| Kstop -> h_Kstop
    942 | Kseq (x_8772, x_8771) ->
    943   h_Kseq x_8772 x_8771
     942| Kseq (x_6863, x_6862) ->
     943  h_Kseq x_6863 x_6862
    944944    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    945       h_Kswitch h_Kcall x_8771)
    946 | Kwhile (x_8775, x_8774, x_8773) ->
    947   h_Kwhile x_8775 x_8774 x_8773
     945      h_Kswitch h_Kcall x_6862)
     946| Kwhile (x_6866, x_6865, x_6864) ->
     947  h_Kwhile x_6866 x_6865 x_6864
    948948    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    949       h_Kswitch h_Kcall x_8773)
    950 | Kdowhile (x_8778, x_8777, x_8776) ->
    951   h_Kdowhile x_8778 x_8777 x_8776
     949      h_Kswitch h_Kcall x_6864)
     950| Kdowhile (x_6869, x_6868, x_6867) ->
     951  h_Kdowhile x_6869 x_6868 x_6867
    952952    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    953       h_Kswitch h_Kcall x_8776)
    954 | Kfor2 (x_8782, x_8781, x_8780, x_8779) ->
    955   h_Kfor2 x_8782 x_8781 x_8780 x_8779
     953      h_Kswitch h_Kcall x_6867)
     954| Kfor2 (x_6873, x_6872, x_6871, x_6870) ->
     955  h_Kfor2 x_6873 x_6872 x_6871 x_6870
    956956    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    957       h_Kswitch h_Kcall x_8779)
    958 | Kfor3 (x_8786, x_8785, x_8784, x_8783) ->
    959   h_Kfor3 x_8786 x_8785 x_8784 x_8783
     957      h_Kswitch h_Kcall x_6870)
     958| Kfor3 (x_6877, x_6876, x_6875, x_6874) ->
     959  h_Kfor3 x_6877 x_6876 x_6875 x_6874
    960960    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    961       h_Kswitch h_Kcall x_8783)
    962 | Kswitch x_8787 ->
    963   h_Kswitch x_8787
     961      h_Kswitch h_Kcall x_6874)
     962| Kswitch x_6878 ->
     963  h_Kswitch x_6878
    964964    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    965       h_Kswitch h_Kcall x_8787)
    966 | Kcall (x_8791, x_8790, x_8789, x_8788) ->
    967   h_Kcall x_8791 x_8790 x_8789 x_8788
     965      h_Kswitch h_Kcall x_6878)
     966| Kcall (x_6882, x_6881, x_6880, x_6879) ->
     967  h_Kcall x_6882 x_6881 x_6880 x_6879
    968968    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    969       h_Kswitch h_Kcall x_8788)
     969      h_Kswitch h_Kcall x_6879)
    970970
    971971(** val cont_inv_rect_Type4 :
     
    10731073type state0 =
    10741074| State of Csyntax.function0 * Csyntax.statement * cont * env * GenMem.mem1
    1075 | Callstate of Values.val0 * Csyntax.clight_fundef * Values.val0 List.list
     1075| Callstate of AST.ident * Csyntax.clight_fundef * Values.val0 List.list
    10761076   * cont * GenMem.mem1
    10771077| Returnstate of Values.val0 * cont * GenMem.mem1
     
    10801080(** val state_rect_Type4 :
    10811081    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
    1082     'a1) -> (Values.val0 -> Csyntax.clight_fundef -> Values.val0 List.list ->
     1082    'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
    10831083    cont -> GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 ->
    10841084    'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1 **)
    10851085let rec state_rect_Type4 h_State h_Callstate h_Returnstate h_Finalstate = function
    10861086| State (f, s, k, e1, m) -> h_State f s k e1 m
    1087 | Callstate (fb, fd, args, k, m) -> h_Callstate fb fd args k m
     1087| Callstate (id, fd, args, k, m) -> h_Callstate id fd args k m
    10881088| Returnstate (res1, k, m) -> h_Returnstate res1 k m
    10891089| Finalstate r -> h_Finalstate r
     
    10911091(** val state_rect_Type5 :
    10921092    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
    1093     'a1) -> (Values.val0 -> Csyntax.clight_fundef -> Values.val0 List.list ->
     1093    'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
    10941094    cont -> GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 ->
    10951095    'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1 **)
    10961096let rec state_rect_Type5 h_State h_Callstate h_Returnstate h_Finalstate = function
    10971097| State (f, s, k, e1, m) -> h_State f s k e1 m
    1098 | Callstate (fb, fd, args, k, m) -> h_Callstate fb fd args k m
     1098| Callstate (id, fd, args, k, m) -> h_Callstate id fd args k m
    10991099| Returnstate (res1, k, m) -> h_Returnstate res1 k m
    11001100| Finalstate r -> h_Finalstate r
     
    11021102(** val state_rect_Type3 :
    11031103    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
    1104     'a1) -> (Values.val0 -> Csyntax.clight_fundef -> Values.val0 List.list ->
     1104    'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
    11051105    cont -> GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 ->
    11061106    'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1 **)
    11071107let rec state_rect_Type3 h_State h_Callstate h_Returnstate h_Finalstate = function
    11081108| State (f, s, k, e1, m) -> h_State f s k e1 m
    1109 | Callstate (fb, fd, args, k, m) -> h_Callstate fb fd args k m
     1109| Callstate (id, fd, args, k, m) -> h_Callstate id fd args k m
    11101110| Returnstate (res1, k, m) -> h_Returnstate res1 k m
    11111111| Finalstate r -> h_Finalstate r
     
    11131113(** val state_rect_Type2 :
    11141114    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
    1115     'a1) -> (Values.val0 -> Csyntax.clight_fundef -> Values.val0 List.list ->
     1115    'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
    11161116    cont -> GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 ->
    11171117    'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1 **)
    11181118let rec state_rect_Type2 h_State h_Callstate h_Returnstate h_Finalstate = function
    11191119| State (f, s, k, e1, m) -> h_State f s k e1 m
    1120 | Callstate (fb, fd, args, k, m) -> h_Callstate fb fd args k m
     1120| Callstate (id, fd, args, k, m) -> h_Callstate id fd args k m
    11211121| Returnstate (res1, k, m) -> h_Returnstate res1 k m
    11221122| Finalstate r -> h_Finalstate r
     
    11241124(** val state_rect_Type1 :
    11251125    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
    1126     'a1) -> (Values.val0 -> Csyntax.clight_fundef -> Values.val0 List.list ->
     1126    'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
    11271127    cont -> GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 ->
    11281128    'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1 **)
    11291129let rec state_rect_Type1 h_State h_Callstate h_Returnstate h_Finalstate = function
    11301130| State (f, s, k, e1, m) -> h_State f s k e1 m
    1131 | Callstate (fb, fd, args, k, m) -> h_Callstate fb fd args k m
     1131| Callstate (id, fd, args, k, m) -> h_Callstate id fd args k m
    11321132| Returnstate (res1, k, m) -> h_Returnstate res1 k m
    11331133| Finalstate r -> h_Finalstate r
     
    11351135(** val state_rect_Type0 :
    11361136    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
    1137     'a1) -> (Values.val0 -> Csyntax.clight_fundef -> Values.val0 List.list ->
     1137    'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
    11381138    cont -> GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 ->
    11391139    'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1 **)
    11401140let rec state_rect_Type0 h_State h_Callstate h_Returnstate h_Finalstate = function
    11411141| State (f, s, k, e1, m) -> h_State f s k e1 m
    1142 | Callstate (fb, fd, args, k, m) -> h_Callstate fb fd args k m
     1142| Callstate (id, fd, args, k, m) -> h_Callstate id fd args k m
    11431143| Returnstate (res1, k, m) -> h_Returnstate res1 k m
    11441144| Finalstate r -> h_Finalstate r
     
    11461146(** val state_inv_rect_Type4 :
    11471147    state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
    1148     GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> Csyntax.clight_fundef ->
     1148    GenMem.mem1 -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
    11491149    Values.val0 List.list -> cont -> GenMem.mem1 -> __ -> 'a1) ->
    11501150    (Values.val0 -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __
     
    11551155(** val state_inv_rect_Type3 :
    11561156    state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
    1157     GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> Csyntax.clight_fundef ->
     1157    GenMem.mem1 -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
    11581158    Values.val0 List.list -> cont -> GenMem.mem1 -> __ -> 'a1) ->
    11591159    (Values.val0 -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __
     
    11641164(** val state_inv_rect_Type2 :
    11651165    state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
    1166     GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> Csyntax.clight_fundef ->
     1166    GenMem.mem1 -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
    11671167    Values.val0 List.list -> cont -> GenMem.mem1 -> __ -> 'a1) ->
    11681168    (Values.val0 -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __
     
    11731173(** val state_inv_rect_Type1 :
    11741174    state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
    1175     GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> Csyntax.clight_fundef ->
     1175    GenMem.mem1 -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
    11761176    Values.val0 List.list -> cont -> GenMem.mem1 -> __ -> 'a1) ->
    11771177    (Values.val0 -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __
     
    11821182(** val state_inv_rect_Type0 :
    11831183    state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
    1184     GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> Csyntax.clight_fundef ->
     1184    GenMem.mem1 -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
    11851185    Values.val0 List.list -> cont -> GenMem.mem1 -> __ -> 'a1) ->
    11861186    (Values.val0 -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __
Note: See TracChangeset for help on using the changeset viewer.