Changeset 2773 for extracted/csem.ml


Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (8 years ago)
Author:
sacerdot
Message:
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/csem.ml

    r2743 r2773  
    9494
    9595open Globalenvs
    96 
    97 open BitVectorTrie
    9896
    9997open CostLabel
     
    137135  Types.Some (Values.Vint (sz,
    138136    (BitVector.exclusive_disjunction_bv (AST.bitsize_of_intsize sz) n
    139       (Values.mone0 sz))))
     137      (Values.mone sz))))
    140138| Values.Vnull -> Types.None
    141139| Values.Vptr x -> Types.None
     
    584582(** val sem_cmp :
    585583    Integers.comparison -> Values.val0 -> Csyntax.type0 -> Values.val0 ->
    586     Csyntax.type0 -> GenMem.mem1 -> Values.val0 Types.option **)
     584    Csyntax.type0 -> GenMem.mem -> Values.val0 Types.option **)
    587585let rec sem_cmp c v1 t1 v2 t2 m =
    588586  match ClassifyOp.classify_cmp t1 t2 with
     
    646644  (match ty with
    647645   | Csyntax.Tvoid -> Types.None
    648    | Csyntax.Tint (sz, sg) -> Types.Some (Values.zero_ext1 sz v)
     646   | Csyntax.Tint (sz, sg) -> Types.Some (Values.zero_ext sz v)
    649647   | Csyntax.Tpointer x -> Types.None
    650648   | Csyntax.Tarray (x, x0) -> Types.None
     
    657655    Csyntax.unary_operation -> Values.val0 -> Csyntax.type0 -> Values.val0
    658656    Types.option **)
    659 let sem_unary_operation op0 v ty =
    660   match op0 with
     657let sem_unary_operation op v ty =
     658  match op with
    661659  | Csyntax.Onotbool -> sem_notbool v ty
    662660  | Csyntax.Onotint -> sem_notint v
     
    665663(** val sem_binary_operation :
    666664    Csyntax.binary_operation -> Values.val0 -> Csyntax.type0 -> Values.val0
    667     -> Csyntax.type0 -> GenMem.mem1 -> Csyntax.type0 -> Values.val0
     665    -> Csyntax.type0 -> GenMem.mem -> Csyntax.type0 -> Values.val0
    668666    Types.option **)
    669 let rec sem_binary_operation op0 v1 t1 v2 t2 m ty =
    670   match op0 with
     667let rec sem_binary_operation op v1 t1 v2 t2 m ty =
     668  match op with
    671669  | Csyntax.Oadd -> sem_add v1 t1 v2 t2
    672670  | Csyntax.Osub -> sem_sub v1 t1 v2 t2 ty
     
    681679  | Csyntax.Oeq ->
    682680    cast_bool_to_target ty (sem_cmp Integers.Ceq v1 t1 v2 t2 m)
    683   | Csyntax.One0 ->
     681  | Csyntax.One ->
    684682    cast_bool_to_target ty (sem_cmp Integers.Cne v1 t1 v2 t2 m)
    685683  | Csyntax.Olt ->
     
    704702      (AST.bitsize_of_intsize dstsz) i
    705703
    706 type genv0 = Csyntax.clight_fundef Globalenvs.genv_t
     704type genv = Csyntax.clight_fundef Globalenvs.genv_t
    707705
    708706type env = Pointers.block Identifiers.identifier_map
     
    713711
    714712(** val load_value_of_type :
    715     Csyntax.type0 -> GenMem.mem1 -> Pointers.block -> Pointers.offset ->
     713    Csyntax.type0 -> GenMem.mem -> Pointers.block -> Pointers.offset ->
    716714    Values.val0 Types.option **)
    717715let rec load_value_of_type ty m b ofs =
     
    725723
    726724(** val store_value_of_type :
    727     Csyntax.type0 -> GenMem.mem1 -> Pointers.block -> Pointers.offset ->
    728     Values.val0 -> GenMem.mem1 Types.option **)
     725    Csyntax.type0 -> GenMem.mem -> Pointers.block -> Pointers.offset ->
     726    Values.val0 -> GenMem.mem Types.option **)
    729727let rec store_value_of_type ty_dest m loc ofs v =
    730728  match Csyntax.access_mode ty_dest with
     
    736734
    737735(** val blocks_of_env : env -> Pointers.block List.list **)
    738 let blocks_of_env e1 =
     736let blocks_of_env e =
    739737  List.map (fun x -> x.Types.snd)
    740     (Identifiers.elements PreIdentifiers.SymbolTag e1)
     738    (Identifiers.elements PreIdentifiers.SymbolTag e)
    741739
    742740(** val select_switch :
     
    780778let rec cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
    781779| Kstop -> h_Kstop
    782 | Kseq (x_8648, x_8647) ->
    783   h_Kseq x_8648 x_8647
     780| Kseq (x_3726, x_3725) ->
     781  h_Kseq x_3726 x_3725
    784782    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    785       h_Kswitch h_Kcall x_8647)
    786 | Kwhile (x_8651, x_8650, x_8649) ->
    787   h_Kwhile x_8651 x_8650 x_8649
     783      h_Kswitch h_Kcall x_3725)
     784| Kwhile (x_3729, x_3728, x_3727) ->
     785  h_Kwhile x_3729 x_3728 x_3727
    788786    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    789       h_Kswitch h_Kcall x_8649)
    790 | Kdowhile (x_8654, x_8653, x_8652) ->
    791   h_Kdowhile x_8654 x_8653 x_8652
     787      h_Kswitch h_Kcall x_3727)
     788| Kdowhile (x_3732, x_3731, x_3730) ->
     789  h_Kdowhile x_3732 x_3731 x_3730
    792790    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    793       h_Kswitch h_Kcall x_8652)
    794 | Kfor2 (x_8658, x_8657, x_8656, x_8655) ->
    795   h_Kfor2 x_8658 x_8657 x_8656 x_8655
     791      h_Kswitch h_Kcall x_3730)
     792| Kfor2 (x_3736, x_3735, x_3734, x_3733) ->
     793  h_Kfor2 x_3736 x_3735 x_3734 x_3733
    796794    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    797       h_Kswitch h_Kcall x_8655)
    798 | Kfor3 (x_8662, x_8661, x_8660, x_8659) ->
    799   h_Kfor3 x_8662 x_8661 x_8660 x_8659
     795      h_Kswitch h_Kcall x_3733)
     796| Kfor3 (x_3740, x_3739, x_3738, x_3737) ->
     797  h_Kfor3 x_3740 x_3739 x_3738 x_3737
    800798    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    801       h_Kswitch h_Kcall x_8659)
    802 | Kswitch x_8663 ->
    803   h_Kswitch x_8663
     799      h_Kswitch h_Kcall x_3737)
     800| Kswitch x_3741 ->
     801  h_Kswitch x_3741
    804802    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    805       h_Kswitch h_Kcall x_8663)
    806 | Kcall (x_8667, x_8666, x_8665, x_8664) ->
    807   h_Kcall x_8667 x_8666 x_8665 x_8664
     803      h_Kswitch h_Kcall x_3741)
     804| Kcall (x_3745, x_3744, x_3743, x_3742) ->
     805  h_Kcall x_3745 x_3744 x_3743 x_3742
    808806    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    809       h_Kswitch h_Kcall x_8664)
     807      h_Kswitch h_Kcall x_3742)
    810808
    811809(** val cont_rect_Type3 :
     
    820818let rec cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
    821819| Kstop -> h_Kstop
    822 | Kseq (x_8708, x_8707) ->
    823   h_Kseq x_8708 x_8707
     820| Kseq (x_3786, x_3785) ->
     821  h_Kseq x_3786 x_3785
    824822    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    825       h_Kswitch h_Kcall x_8707)
    826 | Kwhile (x_8711, x_8710, x_8709) ->
    827   h_Kwhile x_8711 x_8710 x_8709
     823      h_Kswitch h_Kcall x_3785)
     824| Kwhile (x_3789, x_3788, x_3787) ->
     825  h_Kwhile x_3789 x_3788 x_3787
    828826    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    829       h_Kswitch h_Kcall x_8709)
    830 | Kdowhile (x_8714, x_8713, x_8712) ->
    831   h_Kdowhile x_8714 x_8713 x_8712
     827      h_Kswitch h_Kcall x_3787)
     828| Kdowhile (x_3792, x_3791, x_3790) ->
     829  h_Kdowhile x_3792 x_3791 x_3790
    832830    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    833       h_Kswitch h_Kcall x_8712)
    834 | Kfor2 (x_8718, x_8717, x_8716, x_8715) ->
    835   h_Kfor2 x_8718 x_8717 x_8716 x_8715
     831      h_Kswitch h_Kcall x_3790)
     832| Kfor2 (x_3796, x_3795, x_3794, x_3793) ->
     833  h_Kfor2 x_3796 x_3795 x_3794 x_3793
    836834    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    837       h_Kswitch h_Kcall x_8715)
    838 | Kfor3 (x_8722, x_8721, x_8720, x_8719) ->
    839   h_Kfor3 x_8722 x_8721 x_8720 x_8719
     835      h_Kswitch h_Kcall x_3793)
     836| Kfor3 (x_3800, x_3799, x_3798, x_3797) ->
     837  h_Kfor3 x_3800 x_3799 x_3798 x_3797
    840838    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    841       h_Kswitch h_Kcall x_8719)
    842 | Kswitch x_8723 ->
    843   h_Kswitch x_8723
     839      h_Kswitch h_Kcall x_3797)
     840| Kswitch x_3801 ->
     841  h_Kswitch x_3801
    844842    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    845       h_Kswitch h_Kcall x_8723)
    846 | Kcall (x_8727, x_8726, x_8725, x_8724) ->
    847   h_Kcall x_8727 x_8726 x_8725 x_8724
     843      h_Kswitch h_Kcall x_3801)
     844| Kcall (x_3805, x_3804, x_3803, x_3802) ->
     845  h_Kcall x_3805 x_3804 x_3803 x_3802
    848846    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    849       h_Kswitch h_Kcall x_8724)
     847      h_Kswitch h_Kcall x_3802)
    850848
    851849(** val cont_rect_Type2 :
     
    860858let rec cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
    861859| Kstop -> h_Kstop
    862 | Kseq (x_8738, x_8737) ->
    863   h_Kseq x_8738 x_8737
     860| Kseq (x_3816, x_3815) ->
     861  h_Kseq x_3816 x_3815
    864862    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    865       h_Kswitch h_Kcall x_8737)
    866 | Kwhile (x_8741, x_8740, x_8739) ->
    867   h_Kwhile x_8741 x_8740 x_8739
     863      h_Kswitch h_Kcall x_3815)
     864| Kwhile (x_3819, x_3818, x_3817) ->
     865  h_Kwhile x_3819 x_3818 x_3817
    868866    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    869       h_Kswitch h_Kcall x_8739)
    870 | Kdowhile (x_8744, x_8743, x_8742) ->
    871   h_Kdowhile x_8744 x_8743 x_8742
     867      h_Kswitch h_Kcall x_3817)
     868| Kdowhile (x_3822, x_3821, x_3820) ->
     869  h_Kdowhile x_3822 x_3821 x_3820
    872870    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    873       h_Kswitch h_Kcall x_8742)
    874 | Kfor2 (x_8748, x_8747, x_8746, x_8745) ->
    875   h_Kfor2 x_8748 x_8747 x_8746 x_8745
     871      h_Kswitch h_Kcall x_3820)
     872| Kfor2 (x_3826, x_3825, x_3824, x_3823) ->
     873  h_Kfor2 x_3826 x_3825 x_3824 x_3823
    876874    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    877       h_Kswitch h_Kcall x_8745)
    878 | Kfor3 (x_8752, x_8751, x_8750, x_8749) ->
    879   h_Kfor3 x_8752 x_8751 x_8750 x_8749
     875      h_Kswitch h_Kcall x_3823)
     876| Kfor3 (x_3830, x_3829, x_3828, x_3827) ->
     877  h_Kfor3 x_3830 x_3829 x_3828 x_3827
    880878    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    881       h_Kswitch h_Kcall x_8749)
    882 | Kswitch x_8753 ->
    883   h_Kswitch x_8753
     879      h_Kswitch h_Kcall x_3827)
     880| Kswitch x_3831 ->
     881  h_Kswitch x_3831
    884882    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    885       h_Kswitch h_Kcall x_8753)
    886 | Kcall (x_8757, x_8756, x_8755, x_8754) ->
    887   h_Kcall x_8757 x_8756 x_8755 x_8754
     883      h_Kswitch h_Kcall x_3831)
     884| Kcall (x_3835, x_3834, x_3833, x_3832) ->
     885  h_Kcall x_3835 x_3834 x_3833 x_3832
    888886    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    889       h_Kswitch h_Kcall x_8754)
     887      h_Kswitch h_Kcall x_3832)
    890888
    891889(** val cont_rect_Type1 :
     
    900898let rec cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
    901899| Kstop -> h_Kstop
    902 | Kseq (x_8768, x_8767) ->
    903   h_Kseq x_8768 x_8767
     900| Kseq (x_3846, x_3845) ->
     901  h_Kseq x_3846 x_3845
    904902    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    905       h_Kswitch h_Kcall x_8767)
    906 | Kwhile (x_8771, x_8770, x_8769) ->
    907   h_Kwhile x_8771 x_8770 x_8769
     903      h_Kswitch h_Kcall x_3845)
     904| Kwhile (x_3849, x_3848, x_3847) ->
     905  h_Kwhile x_3849 x_3848 x_3847
    908906    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    909       h_Kswitch h_Kcall x_8769)
    910 | Kdowhile (x_8774, x_8773, x_8772) ->
    911   h_Kdowhile x_8774 x_8773 x_8772
     907      h_Kswitch h_Kcall x_3847)
     908| Kdowhile (x_3852, x_3851, x_3850) ->
     909  h_Kdowhile x_3852 x_3851 x_3850
    912910    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    913       h_Kswitch h_Kcall x_8772)
    914 | Kfor2 (x_8778, x_8777, x_8776, x_8775) ->
    915   h_Kfor2 x_8778 x_8777 x_8776 x_8775
     911      h_Kswitch h_Kcall x_3850)
     912| Kfor2 (x_3856, x_3855, x_3854, x_3853) ->
     913  h_Kfor2 x_3856 x_3855 x_3854 x_3853
    916914    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    917       h_Kswitch h_Kcall x_8775)
    918 | Kfor3 (x_8782, x_8781, x_8780, x_8779) ->
    919   h_Kfor3 x_8782 x_8781 x_8780 x_8779
     915      h_Kswitch h_Kcall x_3853)
     916| Kfor3 (x_3860, x_3859, x_3858, x_3857) ->
     917  h_Kfor3 x_3860 x_3859 x_3858 x_3857
    920918    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    921       h_Kswitch h_Kcall x_8779)
    922 | Kswitch x_8783 ->
    923   h_Kswitch x_8783
     919      h_Kswitch h_Kcall x_3857)
     920| Kswitch x_3861 ->
     921  h_Kswitch x_3861
    924922    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    925       h_Kswitch h_Kcall x_8783)
    926 | Kcall (x_8787, x_8786, x_8785, x_8784) ->
    927   h_Kcall x_8787 x_8786 x_8785 x_8784
     923      h_Kswitch h_Kcall x_3861)
     924| Kcall (x_3865, x_3864, x_3863, x_3862) ->
     925  h_Kcall x_3865 x_3864 x_3863 x_3862
    928926    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    929       h_Kswitch h_Kcall x_8784)
     927      h_Kswitch h_Kcall x_3862)
    930928
    931929(** val cont_rect_Type0 :
     
    940938let rec cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
    941939| Kstop -> h_Kstop
    942 | Kseq (x_8798, x_8797) ->
    943   h_Kseq x_8798 x_8797
     940| Kseq (x_3876, x_3875) ->
     941  h_Kseq x_3876 x_3875
    944942    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    945       h_Kswitch h_Kcall x_8797)
    946 | Kwhile (x_8801, x_8800, x_8799) ->
    947   h_Kwhile x_8801 x_8800 x_8799
     943      h_Kswitch h_Kcall x_3875)
     944| Kwhile (x_3879, x_3878, x_3877) ->
     945  h_Kwhile x_3879 x_3878 x_3877
    948946    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    949       h_Kswitch h_Kcall x_8799)
    950 | Kdowhile (x_8804, x_8803, x_8802) ->
    951   h_Kdowhile x_8804 x_8803 x_8802
     947      h_Kswitch h_Kcall x_3877)
     948| Kdowhile (x_3882, x_3881, x_3880) ->
     949  h_Kdowhile x_3882 x_3881 x_3880
    952950    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    953       h_Kswitch h_Kcall x_8802)
    954 | Kfor2 (x_8808, x_8807, x_8806, x_8805) ->
    955   h_Kfor2 x_8808 x_8807 x_8806 x_8805
     951      h_Kswitch h_Kcall x_3880)
     952| Kfor2 (x_3886, x_3885, x_3884, x_3883) ->
     953  h_Kfor2 x_3886 x_3885 x_3884 x_3883
    956954    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    957       h_Kswitch h_Kcall x_8805)
    958 | Kfor3 (x_8812, x_8811, x_8810, x_8809) ->
    959   h_Kfor3 x_8812 x_8811 x_8810 x_8809
     955      h_Kswitch h_Kcall x_3883)
     956| Kfor3 (x_3890, x_3889, x_3888, x_3887) ->
     957  h_Kfor3 x_3890 x_3889 x_3888 x_3887
    960958    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    961       h_Kswitch h_Kcall x_8809)
    962 | Kswitch x_8813 ->
    963   h_Kswitch x_8813
     959      h_Kswitch h_Kcall x_3887)
     960| Kswitch x_3891 ->
     961  h_Kswitch x_3891
    964962    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    965       h_Kswitch h_Kcall x_8813)
    966 | Kcall (x_8817, x_8816, x_8815, x_8814) ->
    967   h_Kcall x_8817 x_8816 x_8815 x_8814
     963      h_Kswitch h_Kcall x_3891)
     964| Kcall (x_3895, x_3894, x_3893, x_3892) ->
     965  h_Kcall x_3895 x_3894 x_3893 x_3892
    968966    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    969       h_Kswitch h_Kcall x_8814)
     967      h_Kswitch h_Kcall x_3892)
    970968
    971969(** val cont_inv_rect_Type4 :
     
    10641062| Kstop -> k
    10651063| Kseq (s, k0) -> call_cont k0
    1066 | Kwhile (e1, s, k0) -> call_cont k0
    1067 | Kdowhile (e1, s, k0) -> call_cont k0
     1064| Kwhile (e, s, k0) -> call_cont k0
     1065| Kdowhile (e, s, k0) -> call_cont k0
    10681066| Kfor2 (e2, e3, s, k0) -> call_cont k0
    10691067| Kfor3 (e2, e3, s, k0) -> call_cont k0
     
    10711069| Kcall (x, x0, x1, x2) -> k
    10721070
    1073 type state0 =
    1074 | State of Csyntax.function0 * Csyntax.statement * cont * env * GenMem.mem1
     1071type state =
     1072| State of Csyntax.function0 * Csyntax.statement * cont * env * GenMem.mem
    10751073| Callstate of AST.ident * Csyntax.clight_fundef * Values.val0 List.list
    1076    * cont * GenMem.mem1
    1077 | Returnstate of Values.val0 * cont * GenMem.mem1
     1074   * cont * GenMem.mem
     1075| Returnstate of Values.val0 * cont * GenMem.mem
    10781076| Finalstate of Integers.int
    10791077
    10801078(** val state_rect_Type4 :
    1081     (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
     1079    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
    10821080    'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
    1083     cont -> GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 ->
    1084     'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1 **)
     1081    cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1)
     1082    -> (Integers.int -> 'a1) -> state -> 'a1 **)
    10851083let rec state_rect_Type4 h_State h_Callstate h_Returnstate h_Finalstate = function
    1086 | State (f, s, k, e1, m) -> h_State f s k e1 m
     1084| State (f, s, k, e, m) -> h_State f s k e m
    10871085| Callstate (id, fd, args, k, m) -> h_Callstate id fd args k m
    1088 | Returnstate (res1, k, m) -> h_Returnstate res1 k m
     1086| Returnstate (res, k, m) -> h_Returnstate res k m
    10891087| Finalstate r -> h_Finalstate r
    10901088
    10911089(** val state_rect_Type5 :
    1092     (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
     1090    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
    10931091    'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
    1094     cont -> GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 ->
    1095     'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1 **)
     1092    cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1)
     1093    -> (Integers.int -> 'a1) -> state -> 'a1 **)
    10961094let rec state_rect_Type5 h_State h_Callstate h_Returnstate h_Finalstate = function
    1097 | State (f, s, k, e1, m) -> h_State f s k e1 m
     1095| State (f, s, k, e, m) -> h_State f s k e m
    10981096| Callstate (id, fd, args, k, m) -> h_Callstate id fd args k m
    1099 | Returnstate (res1, k, m) -> h_Returnstate res1 k m
     1097| Returnstate (res, k, m) -> h_Returnstate res k m
    11001098| Finalstate r -> h_Finalstate r
    11011099
    11021100(** val state_rect_Type3 :
    1103     (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
     1101    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
    11041102    'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
    1105     cont -> GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 ->
    1106     'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1 **)
     1103    cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1)
     1104    -> (Integers.int -> 'a1) -> state -> 'a1 **)
    11071105let rec state_rect_Type3 h_State h_Callstate h_Returnstate h_Finalstate = function
    1108 | State (f, s, k, e1, m) -> h_State f s k e1 m
     1106| State (f, s, k, e, m) -> h_State f s k e m
    11091107| Callstate (id, fd, args, k, m) -> h_Callstate id fd args k m
    1110 | Returnstate (res1, k, m) -> h_Returnstate res1 k m
     1108| Returnstate (res, k, m) -> h_Returnstate res k m
    11111109| Finalstate r -> h_Finalstate r
    11121110
    11131111(** val state_rect_Type2 :
    1114     (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
     1112    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
    11151113    'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
    1116     cont -> GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 ->
    1117     'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1 **)
     1114    cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1)
     1115    -> (Integers.int -> 'a1) -> state -> 'a1 **)
    11181116let rec state_rect_Type2 h_State h_Callstate h_Returnstate h_Finalstate = function
    1119 | State (f, s, k, e1, m) -> h_State f s k e1 m
     1117| State (f, s, k, e, m) -> h_State f s k e m
    11201118| Callstate (id, fd, args, k, m) -> h_Callstate id fd args k m
    1121 | Returnstate (res1, k, m) -> h_Returnstate res1 k m
     1119| Returnstate (res, k, m) -> h_Returnstate res k m
    11221120| Finalstate r -> h_Finalstate r
    11231121
    11241122(** val state_rect_Type1 :
    1125     (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
     1123    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
    11261124    'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
    1127     cont -> GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 ->
    1128     'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1 **)
     1125    cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1)
     1126    -> (Integers.int -> 'a1) -> state -> 'a1 **)
    11291127let rec state_rect_Type1 h_State h_Callstate h_Returnstate h_Finalstate = function
    1130 | State (f, s, k, e1, m) -> h_State f s k e1 m
     1128| State (f, s, k, e, m) -> h_State f s k e m
    11311129| Callstate (id, fd, args, k, m) -> h_Callstate id fd args k m
    1132 | Returnstate (res1, k, m) -> h_Returnstate res1 k m
     1130| Returnstate (res, k, m) -> h_Returnstate res k m
    11331131| Finalstate r -> h_Finalstate r
    11341132
    11351133(** val state_rect_Type0 :
    1136     (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
     1134    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
    11371135    'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
    1138     cont -> GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 ->
    1139     'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1 **)
     1136    cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1)
     1137    -> (Integers.int -> 'a1) -> state -> 'a1 **)
    11401138let rec state_rect_Type0 h_State h_Callstate h_Returnstate h_Finalstate = function
    1141 | State (f, s, k, e1, m) -> h_State f s k e1 m
     1139| State (f, s, k, e, m) -> h_State f s k e m
    11421140| Callstate (id, fd, args, k, m) -> h_Callstate id fd args k m
    1143 | Returnstate (res1, k, m) -> h_Returnstate res1 k m
     1141| Returnstate (res, k, m) -> h_Returnstate res k m
    11441142| Finalstate r -> h_Finalstate r
    11451143
    11461144(** val state_inv_rect_Type4 :
    1147     state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
    1148     GenMem.mem1 -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
    1149     Values.val0 List.list -> cont -> GenMem.mem1 -> __ -> 'a1) ->
    1150     (Values.val0 -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __
    1151     -> 'a1) -> 'a1 **)
     1145    state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
     1146    GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
     1147    Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
     1148    -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
    11521149let state_inv_rect_Type4 hterm h1 h2 h3 h4 =
    11531150  let hcut = state_rect_Type4 h1 h2 h3 h4 hterm in hcut __
    11541151
    11551152(** val state_inv_rect_Type3 :
    1156     state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
    1157     GenMem.mem1 -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
    1158     Values.val0 List.list -> cont -> GenMem.mem1 -> __ -> 'a1) ->
    1159     (Values.val0 -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __
    1160     -> 'a1) -> 'a1 **)
     1153    state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
     1154    GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
     1155    Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
     1156    -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
    11611157let state_inv_rect_Type3 hterm h1 h2 h3 h4 =
    11621158  let hcut = state_rect_Type3 h1 h2 h3 h4 hterm in hcut __
    11631159
    11641160(** val state_inv_rect_Type2 :
    1165     state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
    1166     GenMem.mem1 -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
    1167     Values.val0 List.list -> cont -> GenMem.mem1 -> __ -> 'a1) ->
    1168     (Values.val0 -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __
    1169     -> 'a1) -> 'a1 **)
     1161    state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
     1162    GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
     1163    Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
     1164    -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
    11701165let state_inv_rect_Type2 hterm h1 h2 h3 h4 =
    11711166  let hcut = state_rect_Type2 h1 h2 h3 h4 hterm in hcut __
    11721167
    11731168(** val state_inv_rect_Type1 :
    1174     state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
    1175     GenMem.mem1 -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
    1176     Values.val0 List.list -> cont -> GenMem.mem1 -> __ -> 'a1) ->
    1177     (Values.val0 -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __
    1178     -> 'a1) -> 'a1 **)
     1169    state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
     1170    GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
     1171    Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
     1172    -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
    11791173let state_inv_rect_Type1 hterm h1 h2 h3 h4 =
    11801174  let hcut = state_rect_Type1 h1 h2 h3 h4 hterm in hcut __
    11811175
    11821176(** val state_inv_rect_Type0 :
    1183     state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
    1184     GenMem.mem1 -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
    1185     Values.val0 List.list -> cont -> GenMem.mem1 -> __ -> 'a1) ->
    1186     (Values.val0 -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __
    1187     -> 'a1) -> 'a1 **)
     1177    state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
     1178    GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
     1179    Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
     1180    -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
    11881181let state_inv_rect_Type0 hterm h1 h2 h3 h4 =
    11891182  let hcut = state_rect_Type0 h1 h2 h3 h4 hterm in hcut __
    11901183
    1191 (** val state_discr : state0 -> state0 -> __ **)
     1184(** val state_discr : state -> state -> __ **)
    11921185let state_discr x y =
    11931186  Logic.eq_rect_Type2 x
     
    12001193     | Finalstate a0 -> Obj.magic (fun _ dH -> dH __)) y
    12011194
    1202 (** val state_jmdiscr : state0 -> state0 -> __ **)
     1195(** val state_jmdiscr : state -> state -> __ **)
    12031196let state_jmdiscr x y =
    12041197  Logic.eq_rect_Type2 x
     
    12401233  | Csyntax.Scontinue -> Types.None
    12411234  | Csyntax.Sreturn x -> Types.None
    1242   | Csyntax.Sswitch (e1, sl) -> find_label_ls lbl sl (Kswitch k)
     1235  | Csyntax.Sswitch (e, sl) -> find_label_ls lbl sl (Kswitch k)
    12431236  | Csyntax.Slabel (lbl', s') ->
    12441237    (match AST.ident_eq lbl lbl' with
     
    12591252
    12601253(** val fun_typeof : Csyntax.expr -> Csyntax.type0 **)
    1261 let fun_typeof e1 =
    1262   match Csyntax.typeof e1 with
     1254let fun_typeof e =
     1255  match Csyntax.typeof e with
    12631256  | Csyntax.Tvoid -> Csyntax.Tvoid
    12641257  | Csyntax.Tint (a, b) -> Csyntax.Tint (a, b)
Note: See TracChangeset for help on using the changeset viewer.