Changeset 2717 for extracted/csem.ml


Ignore:
Timestamp:
Feb 23, 2013, 1:16:55 AM (8 years ago)
Author:
sacerdot
Message:

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/csem.ml

    r2649 r2717  
    3737open Identifiers
    3838
     39open Exp
     40
    3941open Arithmetic
    4042
     
    9294
    9395open Globalenvs
     96
     97open BitVectorTrie
    9498
    9599open CostLabel
     
    776780let rec cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
    777781| Kstop -> h_Kstop
    778 | Kseq (x_5937, x_5936) ->
    779   h_Kseq x_5937 x_5936
     782| Kseq (x_8622, x_8621) ->
     783  h_Kseq x_8622 x_8621
    780784    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    781       h_Kswitch h_Kcall x_5936)
    782 | Kwhile (x_5940, x_5939, x_5938) ->
    783   h_Kwhile x_5940 x_5939 x_5938
     785      h_Kswitch h_Kcall x_8621)
     786| Kwhile (x_8625, x_8624, x_8623) ->
     787  h_Kwhile x_8625 x_8624 x_8623
    784788    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    785       h_Kswitch h_Kcall x_5938)
    786 | Kdowhile (x_5943, x_5942, x_5941) ->
    787   h_Kdowhile x_5943 x_5942 x_5941
     789      h_Kswitch h_Kcall x_8623)
     790| Kdowhile (x_8628, x_8627, x_8626) ->
     791  h_Kdowhile x_8628 x_8627 x_8626
    788792    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    789       h_Kswitch h_Kcall x_5941)
    790 | Kfor2 (x_5947, x_5946, x_5945, x_5944) ->
    791   h_Kfor2 x_5947 x_5946 x_5945 x_5944
     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
    792796    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    793       h_Kswitch h_Kcall x_5944)
    794 | Kfor3 (x_5951, x_5950, x_5949, x_5948) ->
    795   h_Kfor3 x_5951 x_5950 x_5949 x_5948
     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
    796800    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    797       h_Kswitch h_Kcall x_5948)
    798 | Kswitch x_5952 ->
    799   h_Kswitch x_5952
     801      h_Kswitch h_Kcall x_8633)
     802| Kswitch x_8637 ->
     803  h_Kswitch x_8637
    800804    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    801       h_Kswitch h_Kcall x_5952)
    802 | Kcall (x_5956, x_5955, x_5954, x_5953) ->
    803   h_Kcall x_5956 x_5955 x_5954 x_5953
     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
    804808    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    805       h_Kswitch h_Kcall x_5953)
     809      h_Kswitch h_Kcall x_8638)
    806810
    807811(** val cont_rect_Type3 :
     
    816820let rec cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
    817821| Kstop -> h_Kstop
    818 | Kseq (x_5997, x_5996) ->
    819   h_Kseq x_5997 x_5996
     822| Kseq (x_8682, x_8681) ->
     823  h_Kseq x_8682 x_8681
    820824    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    821       h_Kswitch h_Kcall x_5996)
    822 | Kwhile (x_6000, x_5999, x_5998) ->
    823   h_Kwhile x_6000 x_5999 x_5998
     825      h_Kswitch h_Kcall x_8681)
     826| Kwhile (x_8685, x_8684, x_8683) ->
     827  h_Kwhile x_8685 x_8684 x_8683
    824828    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    825       h_Kswitch h_Kcall x_5998)
    826 | Kdowhile (x_6003, x_6002, x_6001) ->
    827   h_Kdowhile x_6003 x_6002 x_6001
     829      h_Kswitch h_Kcall x_8683)
     830| Kdowhile (x_8688, x_8687, x_8686) ->
     831  h_Kdowhile x_8688 x_8687 x_8686
    828832    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    829       h_Kswitch h_Kcall x_6001)
    830 | Kfor2 (x_6007, x_6006, x_6005, x_6004) ->
    831   h_Kfor2 x_6007 x_6006 x_6005 x_6004
     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
    832836    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    833       h_Kswitch h_Kcall x_6004)
    834 | Kfor3 (x_6011, x_6010, x_6009, x_6008) ->
    835   h_Kfor3 x_6011 x_6010 x_6009 x_6008
     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
    836840    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    837       h_Kswitch h_Kcall x_6008)
    838 | Kswitch x_6012 ->
    839   h_Kswitch x_6012
     841      h_Kswitch h_Kcall x_8693)
     842| Kswitch x_8697 ->
     843  h_Kswitch x_8697
    840844    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    841       h_Kswitch h_Kcall x_6012)
    842 | Kcall (x_6016, x_6015, x_6014, x_6013) ->
    843   h_Kcall x_6016 x_6015 x_6014 x_6013
     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
    844848    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    845       h_Kswitch h_Kcall x_6013)
     849      h_Kswitch h_Kcall x_8698)
    846850
    847851(** val cont_rect_Type2 :
     
    856860let rec cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
    857861| Kstop -> h_Kstop
    858 | Kseq (x_6027, x_6026) ->
    859   h_Kseq x_6027 x_6026
     862| Kseq (x_8712, x_8711) ->
     863  h_Kseq x_8712 x_8711
    860864    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    861       h_Kswitch h_Kcall x_6026)
    862 | Kwhile (x_6030, x_6029, x_6028) ->
    863   h_Kwhile x_6030 x_6029 x_6028
     865      h_Kswitch h_Kcall x_8711)
     866| Kwhile (x_8715, x_8714, x_8713) ->
     867  h_Kwhile x_8715 x_8714 x_8713
    864868    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    865       h_Kswitch h_Kcall x_6028)
    866 | Kdowhile (x_6033, x_6032, x_6031) ->
    867   h_Kdowhile x_6033 x_6032 x_6031
     869      h_Kswitch h_Kcall x_8713)
     870| Kdowhile (x_8718, x_8717, x_8716) ->
     871  h_Kdowhile x_8718 x_8717 x_8716
    868872    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    869       h_Kswitch h_Kcall x_6031)
    870 | Kfor2 (x_6037, x_6036, x_6035, x_6034) ->
    871   h_Kfor2 x_6037 x_6036 x_6035 x_6034
     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
    872876    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    873       h_Kswitch h_Kcall x_6034)
    874 | Kfor3 (x_6041, x_6040, x_6039, x_6038) ->
    875   h_Kfor3 x_6041 x_6040 x_6039 x_6038
     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
    876880    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    877       h_Kswitch h_Kcall x_6038)
    878 | Kswitch x_6042 ->
    879   h_Kswitch x_6042
     881      h_Kswitch h_Kcall x_8723)
     882| Kswitch x_8727 ->
     883  h_Kswitch x_8727
    880884    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    881       h_Kswitch h_Kcall x_6042)
    882 | Kcall (x_6046, x_6045, x_6044, x_6043) ->
    883   h_Kcall x_6046 x_6045 x_6044 x_6043
     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
    884888    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    885       h_Kswitch h_Kcall x_6043)
     889      h_Kswitch h_Kcall x_8728)
    886890
    887891(** val cont_rect_Type1 :
     
    896900let rec cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
    897901| Kstop -> h_Kstop
    898 | Kseq (x_6057, x_6056) ->
    899   h_Kseq x_6057 x_6056
     902| Kseq (x_8742, x_8741) ->
     903  h_Kseq x_8742 x_8741
    900904    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    901       h_Kswitch h_Kcall x_6056)
    902 | Kwhile (x_6060, x_6059, x_6058) ->
    903   h_Kwhile x_6060 x_6059 x_6058
     905      h_Kswitch h_Kcall x_8741)
     906| Kwhile (x_8745, x_8744, x_8743) ->
     907  h_Kwhile x_8745 x_8744 x_8743
    904908    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    905       h_Kswitch h_Kcall x_6058)
    906 | Kdowhile (x_6063, x_6062, x_6061) ->
    907   h_Kdowhile x_6063 x_6062 x_6061
     909      h_Kswitch h_Kcall x_8743)
     910| Kdowhile (x_8748, x_8747, x_8746) ->
     911  h_Kdowhile x_8748 x_8747 x_8746
    908912    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    909       h_Kswitch h_Kcall x_6061)
    910 | Kfor2 (x_6067, x_6066, x_6065, x_6064) ->
    911   h_Kfor2 x_6067 x_6066 x_6065 x_6064
     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
    912916    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    913       h_Kswitch h_Kcall x_6064)
    914 | Kfor3 (x_6071, x_6070, x_6069, x_6068) ->
    915   h_Kfor3 x_6071 x_6070 x_6069 x_6068
     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
    916920    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    917       h_Kswitch h_Kcall x_6068)
    918 | Kswitch x_6072 ->
    919   h_Kswitch x_6072
     921      h_Kswitch h_Kcall x_8753)
     922| Kswitch x_8757 ->
     923  h_Kswitch x_8757
    920924    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    921       h_Kswitch h_Kcall x_6072)
    922 | Kcall (x_6076, x_6075, x_6074, x_6073) ->
    923   h_Kcall x_6076 x_6075 x_6074 x_6073
     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
    924928    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    925       h_Kswitch h_Kcall x_6073)
     929      h_Kswitch h_Kcall x_8758)
    926930
    927931(** val cont_rect_Type0 :
     
    936940let rec cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
    937941| Kstop -> h_Kstop
    938 | Kseq (x_6087, x_6086) ->
    939   h_Kseq x_6087 x_6086
     942| Kseq (x_8772, x_8771) ->
     943  h_Kseq x_8772 x_8771
    940944    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    941       h_Kswitch h_Kcall x_6086)
    942 | Kwhile (x_6090, x_6089, x_6088) ->
    943   h_Kwhile x_6090 x_6089 x_6088
     945      h_Kswitch h_Kcall x_8771)
     946| Kwhile (x_8775, x_8774, x_8773) ->
     947  h_Kwhile x_8775 x_8774 x_8773
    944948    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    945       h_Kswitch h_Kcall x_6088)
    946 | Kdowhile (x_6093, x_6092, x_6091) ->
    947   h_Kdowhile x_6093 x_6092 x_6091
     949      h_Kswitch h_Kcall x_8773)
     950| Kdowhile (x_8778, x_8777, x_8776) ->
     951  h_Kdowhile x_8778 x_8777 x_8776
    948952    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    949       h_Kswitch h_Kcall x_6091)
    950 | Kfor2 (x_6097, x_6096, x_6095, x_6094) ->
    951   h_Kfor2 x_6097 x_6096 x_6095 x_6094
     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
    952956    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    953       h_Kswitch h_Kcall x_6094)
    954 | Kfor3 (x_6101, x_6100, x_6099, x_6098) ->
    955   h_Kfor3 x_6101 x_6100 x_6099 x_6098
     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
    956960    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    957       h_Kswitch h_Kcall x_6098)
    958 | Kswitch x_6102 ->
    959   h_Kswitch x_6102
     961      h_Kswitch h_Kcall x_8783)
     962| Kswitch x_8787 ->
     963  h_Kswitch x_8787
    960964    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    961       h_Kswitch h_Kcall x_6102)
    962 | Kcall (x_6106, x_6105, x_6104, x_6103) ->
    963   h_Kcall x_6106 x_6105 x_6104 x_6103
     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
    964968    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    965       h_Kswitch h_Kcall x_6103)
     969      h_Kswitch h_Kcall x_8788)
    966970
    967971(** val cont_inv_rect_Type4 :
     
    10691073type state0 =
    10701074| State of Csyntax.function0 * Csyntax.statement * cont * env * GenMem.mem1
    1071 | Callstate of Csyntax.clight_fundef * Values.val0 List.list * cont
    1072    * GenMem.mem1
     1075| Callstate of Values.val0 * Csyntax.clight_fundef * Values.val0 List.list
     1076   * cont * GenMem.mem1
    10731077| Returnstate of Values.val0 * cont * GenMem.mem1
    10741078| Finalstate of Integers.int
     
    10761080(** val state_rect_Type4 :
    10771081    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
    1078     'a1) -> (Csyntax.clight_fundef -> Values.val0 List.list -> cont ->
    1079     GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 -> 'a1) ->
    1080     (Integers.int -> 'a1) -> state0 -> 'a1 **)
     1082    'a1) -> (Values.val0 -> Csyntax.clight_fundef -> Values.val0 List.list ->
     1083    cont -> GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 ->
     1084    'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1 **)
    10811085let rec state_rect_Type4 h_State h_Callstate h_Returnstate h_Finalstate = function
    10821086| State (f, s, k, e1, m) -> h_State f s k e1 m
    1083 | Callstate (fd, args, k, m) -> h_Callstate fd args k m
     1087| Callstate (fb, fd, args, k, m) -> h_Callstate fb fd args k m
    10841088| Returnstate (res1, k, m) -> h_Returnstate res1 k m
    10851089| Finalstate r -> h_Finalstate r
     
    10871091(** val state_rect_Type5 :
    10881092    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
    1089     'a1) -> (Csyntax.clight_fundef -> Values.val0 List.list -> cont ->
    1090     GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 -> 'a1) ->
    1091     (Integers.int -> 'a1) -> state0 -> 'a1 **)
     1093    'a1) -> (Values.val0 -> Csyntax.clight_fundef -> Values.val0 List.list ->
     1094    cont -> GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 ->
     1095    'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1 **)
    10921096let rec state_rect_Type5 h_State h_Callstate h_Returnstate h_Finalstate = function
    10931097| State (f, s, k, e1, m) -> h_State f s k e1 m
    1094 | Callstate (fd, args, k, m) -> h_Callstate fd args k m
     1098| Callstate (fb, fd, args, k, m) -> h_Callstate fb fd args k m
    10951099| Returnstate (res1, k, m) -> h_Returnstate res1 k m
    10961100| Finalstate r -> h_Finalstate r
     
    10981102(** val state_rect_Type3 :
    10991103    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
    1100     'a1) -> (Csyntax.clight_fundef -> Values.val0 List.list -> cont ->
    1101     GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 -> 'a1) ->
    1102     (Integers.int -> 'a1) -> state0 -> 'a1 **)
     1104    'a1) -> (Values.val0 -> Csyntax.clight_fundef -> Values.val0 List.list ->
     1105    cont -> GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 ->
     1106    'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1 **)
    11031107let rec state_rect_Type3 h_State h_Callstate h_Returnstate h_Finalstate = function
    11041108| State (f, s, k, e1, m) -> h_State f s k e1 m
    1105 | Callstate (fd, args, k, m) -> h_Callstate fd args k m
     1109| Callstate (fb, fd, args, k, m) -> h_Callstate fb fd args k m
    11061110| Returnstate (res1, k, m) -> h_Returnstate res1 k m
    11071111| Finalstate r -> h_Finalstate r
     
    11091113(** val state_rect_Type2 :
    11101114    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
    1111     'a1) -> (Csyntax.clight_fundef -> Values.val0 List.list -> cont ->
    1112     GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 -> 'a1) ->
    1113     (Integers.int -> 'a1) -> state0 -> 'a1 **)
     1115    'a1) -> (Values.val0 -> Csyntax.clight_fundef -> Values.val0 List.list ->
     1116    cont -> GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 ->
     1117    'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1 **)
    11141118let rec state_rect_Type2 h_State h_Callstate h_Returnstate h_Finalstate = function
    11151119| State (f, s, k, e1, m) -> h_State f s k e1 m
    1116 | Callstate (fd, args, k, m) -> h_Callstate fd args k m
     1120| Callstate (fb, fd, args, k, m) -> h_Callstate fb fd args k m
    11171121| Returnstate (res1, k, m) -> h_Returnstate res1 k m
    11181122| Finalstate r -> h_Finalstate r
     
    11201124(** val state_rect_Type1 :
    11211125    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
    1122     'a1) -> (Csyntax.clight_fundef -> Values.val0 List.list -> cont ->
    1123     GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 -> 'a1) ->
    1124     (Integers.int -> 'a1) -> state0 -> 'a1 **)
     1126    'a1) -> (Values.val0 -> Csyntax.clight_fundef -> Values.val0 List.list ->
     1127    cont -> GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 ->
     1128    'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1 **)
    11251129let rec state_rect_Type1 h_State h_Callstate h_Returnstate h_Finalstate = function
    11261130| State (f, s, k, e1, m) -> h_State f s k e1 m
    1127 | Callstate (fd, args, k, m) -> h_Callstate fd args k m
     1131| Callstate (fb, fd, args, k, m) -> h_Callstate fb fd args k m
    11281132| Returnstate (res1, k, m) -> h_Returnstate res1 k m
    11291133| Finalstate r -> h_Finalstate r
     
    11311135(** val state_rect_Type0 :
    11321136    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
    1133     'a1) -> (Csyntax.clight_fundef -> Values.val0 List.list -> cont ->
    1134     GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 -> 'a1) ->
    1135     (Integers.int -> 'a1) -> state0 -> 'a1 **)
     1137    'a1) -> (Values.val0 -> Csyntax.clight_fundef -> Values.val0 List.list ->
     1138    cont -> GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 ->
     1139    'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1 **)
    11361140let rec state_rect_Type0 h_State h_Callstate h_Returnstate h_Finalstate = function
    11371141| State (f, s, k, e1, m) -> h_State f s k e1 m
    1138 | Callstate (fd, args, k, m) -> h_Callstate fd args k m
     1142| Callstate (fb, fd, args, k, m) -> h_Callstate fb fd args k m
    11391143| Returnstate (res1, k, m) -> h_Returnstate res1 k m
    11401144| Finalstate r -> h_Finalstate r
     
    11421146(** val state_inv_rect_Type4 :
    11431147    state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
    1144     GenMem.mem1 -> __ -> 'a1) -> (Csyntax.clight_fundef -> Values.val0
    1145     List.list -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> cont ->
    1146     GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
     1148    GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> Csyntax.clight_fundef ->
     1149    Values.val0 List.list -> cont -> GenMem.mem1 -> __ -> 'a1) ->
     1150    (Values.val0 -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __
     1151    -> 'a1) -> 'a1 **)
    11471152let state_inv_rect_Type4 hterm h1 h2 h3 h4 =
    11481153  let hcut = state_rect_Type4 h1 h2 h3 h4 hterm in hcut __
     
    11501155(** val state_inv_rect_Type3 :
    11511156    state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
    1152     GenMem.mem1 -> __ -> 'a1) -> (Csyntax.clight_fundef -> Values.val0
    1153     List.list -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> cont ->
    1154     GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
     1157    GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> Csyntax.clight_fundef ->
     1158    Values.val0 List.list -> cont -> GenMem.mem1 -> __ -> 'a1) ->
     1159    (Values.val0 -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __
     1160    -> 'a1) -> 'a1 **)
    11551161let state_inv_rect_Type3 hterm h1 h2 h3 h4 =
    11561162  let hcut = state_rect_Type3 h1 h2 h3 h4 hterm in hcut __
     
    11581164(** val state_inv_rect_Type2 :
    11591165    state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
    1160     GenMem.mem1 -> __ -> 'a1) -> (Csyntax.clight_fundef -> Values.val0
    1161     List.list -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> cont ->
    1162     GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
     1166    GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> Csyntax.clight_fundef ->
     1167    Values.val0 List.list -> cont -> GenMem.mem1 -> __ -> 'a1) ->
     1168    (Values.val0 -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __
     1169    -> 'a1) -> 'a1 **)
    11631170let state_inv_rect_Type2 hterm h1 h2 h3 h4 =
    11641171  let hcut = state_rect_Type2 h1 h2 h3 h4 hterm in hcut __
     
    11661173(** val state_inv_rect_Type1 :
    11671174    state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
    1168     GenMem.mem1 -> __ -> 'a1) -> (Csyntax.clight_fundef -> Values.val0
    1169     List.list -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> cont ->
    1170     GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
     1175    GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> Csyntax.clight_fundef ->
     1176    Values.val0 List.list -> cont -> GenMem.mem1 -> __ -> 'a1) ->
     1177    (Values.val0 -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __
     1178    -> 'a1) -> 'a1 **)
    11711179let state_inv_rect_Type1 hterm h1 h2 h3 h4 =
    11721180  let hcut = state_rect_Type1 h1 h2 h3 h4 hterm in hcut __
     
    11741182(** val state_inv_rect_Type0 :
    11751183    state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
    1176     GenMem.mem1 -> __ -> 'a1) -> (Csyntax.clight_fundef -> Values.val0
    1177     List.list -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> cont ->
    1178     GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
     1184    GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> Csyntax.clight_fundef ->
     1185    Values.val0 List.list -> cont -> GenMem.mem1 -> __ -> 'a1) ->
     1186    (Values.val0 -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __
     1187    -> 'a1) -> 'a1 **)
    11791188let state_inv_rect_Type0 hterm h1 h2 h3 h4 =
    11801189  let hcut = state_rect_Type0 h1 h2 h3 h4 hterm in hcut __
     
    11861195     | State (a0, a1, a2, a3, a4) ->
    11871196       Obj.magic (fun _ dH -> dH __ __ __ __ __)
    1188      | Callstate (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
     1197     | Callstate (a0, a1, a2, a3, a4) ->
     1198       Obj.magic (fun _ dH -> dH __ __ __ __ __)
    11891199     | Returnstate (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
    11901200     | Finalstate a0 -> Obj.magic (fun _ dH -> dH __)) y
     
    11961206     | State (a0, a1, a2, a3, a4) ->
    11971207       Obj.magic (fun _ dH -> dH __ __ __ __ __)
    1198      | Callstate (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
     1208     | Callstate (a0, a1, a2, a3, a4) ->
     1209       Obj.magic (fun _ dH -> dH __ __ __ __ __)
    11991210     | Returnstate (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
    12001211     | Finalstate a0 -> Obj.magic (fun _ dH -> dH __)) y
Note: See TracChangeset for help on using the changeset viewer.