Changeset 2797 for extracted/csem.ml


Ignore:
Timestamp:
Mar 7, 2013, 12:55:34 PM (7 years ago)
Author:
sacerdot
Message:

Extracted again after James's cleanup and the implementation of the
new testing function to be used in the untrusted code.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/csem.ml

    r2775 r2797  
    778778let rec cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
    779779| Kstop -> h_Kstop
    780 | Kseq (x_8557, x_8556) ->
    781   h_Kseq x_8557 x_8556
     780| Kseq (x_8570, x_8569) ->
     781  h_Kseq x_8570 x_8569
    782782    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    783       h_Kswitch h_Kcall x_8556)
    784 | Kwhile (x_8560, x_8559, x_8558) ->
    785   h_Kwhile x_8560 x_8559 x_8558
     783      h_Kswitch h_Kcall x_8569)
     784| Kwhile (x_8573, x_8572, x_8571) ->
     785  h_Kwhile x_8573 x_8572 x_8571
    786786    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    787       h_Kswitch h_Kcall x_8558)
    788 | Kdowhile (x_8563, x_8562, x_8561) ->
    789   h_Kdowhile x_8563 x_8562 x_8561
     787      h_Kswitch h_Kcall x_8571)
     788| Kdowhile (x_8576, x_8575, x_8574) ->
     789  h_Kdowhile x_8576 x_8575 x_8574
    790790    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    791       h_Kswitch h_Kcall x_8561)
    792 | Kfor2 (x_8567, x_8566, x_8565, x_8564) ->
    793   h_Kfor2 x_8567 x_8566 x_8565 x_8564
     791      h_Kswitch h_Kcall x_8574)
     792| Kfor2 (x_8580, x_8579, x_8578, x_8577) ->
     793  h_Kfor2 x_8580 x_8579 x_8578 x_8577
    794794    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    795       h_Kswitch h_Kcall x_8564)
    796 | Kfor3 (x_8571, x_8570, x_8569, x_8568) ->
    797   h_Kfor3 x_8571 x_8570 x_8569 x_8568
     795      h_Kswitch h_Kcall x_8577)
     796| Kfor3 (x_8584, x_8583, x_8582, x_8581) ->
     797  h_Kfor3 x_8584 x_8583 x_8582 x_8581
    798798    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    799       h_Kswitch h_Kcall x_8568)
    800 | Kswitch x_8572 ->
    801   h_Kswitch x_8572
     799      h_Kswitch h_Kcall x_8581)
     800| Kswitch x_8585 ->
     801  h_Kswitch x_8585
    802802    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    803       h_Kswitch h_Kcall x_8572)
    804 | Kcall (x_8576, x_8575, x_8574, x_8573) ->
    805   h_Kcall x_8576 x_8575 x_8574 x_8573
     803      h_Kswitch h_Kcall x_8585)
     804| Kcall (x_8589, x_8588, x_8587, x_8586) ->
     805  h_Kcall x_8589 x_8588 x_8587 x_8586
    806806    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    807       h_Kswitch h_Kcall x_8573)
     807      h_Kswitch h_Kcall x_8586)
    808808
    809809(** val cont_rect_Type3 :
     
    818818let rec cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
    819819| Kstop -> h_Kstop
    820 | Kseq (x_8617, x_8616) ->
    821   h_Kseq x_8617 x_8616
     820| Kseq (x_8630, x_8629) ->
     821  h_Kseq x_8630 x_8629
    822822    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    823       h_Kswitch h_Kcall x_8616)
    824 | Kwhile (x_8620, x_8619, x_8618) ->
    825   h_Kwhile x_8620 x_8619 x_8618
     823      h_Kswitch h_Kcall x_8629)
     824| Kwhile (x_8633, x_8632, x_8631) ->
     825  h_Kwhile x_8633 x_8632 x_8631
    826826    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    827       h_Kswitch h_Kcall x_8618)
    828 | Kdowhile (x_8623, x_8622, x_8621) ->
    829   h_Kdowhile x_8623 x_8622 x_8621
     827      h_Kswitch h_Kcall x_8631)
     828| Kdowhile (x_8636, x_8635, x_8634) ->
     829  h_Kdowhile x_8636 x_8635 x_8634
    830830    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    831       h_Kswitch h_Kcall x_8621)
    832 | Kfor2 (x_8627, x_8626, x_8625, x_8624) ->
    833   h_Kfor2 x_8627 x_8626 x_8625 x_8624
     831      h_Kswitch h_Kcall x_8634)
     832| Kfor2 (x_8640, x_8639, x_8638, x_8637) ->
     833  h_Kfor2 x_8640 x_8639 x_8638 x_8637
    834834    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    835       h_Kswitch h_Kcall x_8624)
    836 | Kfor3 (x_8631, x_8630, x_8629, x_8628) ->
    837   h_Kfor3 x_8631 x_8630 x_8629 x_8628
     835      h_Kswitch h_Kcall x_8637)
     836| Kfor3 (x_8644, x_8643, x_8642, x_8641) ->
     837  h_Kfor3 x_8644 x_8643 x_8642 x_8641
    838838    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    839       h_Kswitch h_Kcall x_8628)
    840 | Kswitch x_8632 ->
    841   h_Kswitch x_8632
     839      h_Kswitch h_Kcall x_8641)
     840| Kswitch x_8645 ->
     841  h_Kswitch x_8645
    842842    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    843       h_Kswitch h_Kcall x_8632)
    844 | Kcall (x_8636, x_8635, x_8634, x_8633) ->
    845   h_Kcall x_8636 x_8635 x_8634 x_8633
     843      h_Kswitch h_Kcall x_8645)
     844| Kcall (x_8649, x_8648, x_8647, x_8646) ->
     845  h_Kcall x_8649 x_8648 x_8647 x_8646
    846846    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    847       h_Kswitch h_Kcall x_8633)
     847      h_Kswitch h_Kcall x_8646)
    848848
    849849(** val cont_rect_Type2 :
     
    858858let rec cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
    859859| Kstop -> h_Kstop
    860 | Kseq (x_8647, x_8646) ->
    861   h_Kseq x_8647 x_8646
     860| Kseq (x_8660, x_8659) ->
     861  h_Kseq x_8660 x_8659
    862862    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    863       h_Kswitch h_Kcall x_8646)
    864 | Kwhile (x_8650, x_8649, x_8648) ->
    865   h_Kwhile x_8650 x_8649 x_8648
     863      h_Kswitch h_Kcall x_8659)
     864| Kwhile (x_8663, x_8662, x_8661) ->
     865  h_Kwhile x_8663 x_8662 x_8661
    866866    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    867       h_Kswitch h_Kcall x_8648)
    868 | Kdowhile (x_8653, x_8652, x_8651) ->
    869   h_Kdowhile x_8653 x_8652 x_8651
     867      h_Kswitch h_Kcall x_8661)
     868| Kdowhile (x_8666, x_8665, x_8664) ->
     869  h_Kdowhile x_8666 x_8665 x_8664
    870870    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    871       h_Kswitch h_Kcall x_8651)
    872 | Kfor2 (x_8657, x_8656, x_8655, x_8654) ->
    873   h_Kfor2 x_8657 x_8656 x_8655 x_8654
     871      h_Kswitch h_Kcall x_8664)
     872| Kfor2 (x_8670, x_8669, x_8668, x_8667) ->
     873  h_Kfor2 x_8670 x_8669 x_8668 x_8667
    874874    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    875       h_Kswitch h_Kcall x_8654)
    876 | Kfor3 (x_8661, x_8660, x_8659, x_8658) ->
    877   h_Kfor3 x_8661 x_8660 x_8659 x_8658
     875      h_Kswitch h_Kcall x_8667)
     876| Kfor3 (x_8674, x_8673, x_8672, x_8671) ->
     877  h_Kfor3 x_8674 x_8673 x_8672 x_8671
    878878    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    879       h_Kswitch h_Kcall x_8658)
    880 | Kswitch x_8662 ->
    881   h_Kswitch x_8662
     879      h_Kswitch h_Kcall x_8671)
     880| Kswitch x_8675 ->
     881  h_Kswitch x_8675
    882882    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    883       h_Kswitch h_Kcall x_8662)
    884 | Kcall (x_8666, x_8665, x_8664, x_8663) ->
    885   h_Kcall x_8666 x_8665 x_8664 x_8663
     883      h_Kswitch h_Kcall x_8675)
     884| Kcall (x_8679, x_8678, x_8677, x_8676) ->
     885  h_Kcall x_8679 x_8678 x_8677 x_8676
    886886    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    887       h_Kswitch h_Kcall x_8663)
     887      h_Kswitch h_Kcall x_8676)
    888888
    889889(** val cont_rect_Type1 :
     
    898898let rec cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
    899899| Kstop -> h_Kstop
    900 | Kseq (x_8677, x_8676) ->
    901   h_Kseq x_8677 x_8676
     900| Kseq (x_8690, x_8689) ->
     901  h_Kseq x_8690 x_8689
    902902    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    903       h_Kswitch h_Kcall x_8676)
    904 | Kwhile (x_8680, x_8679, x_8678) ->
    905   h_Kwhile x_8680 x_8679 x_8678
     903      h_Kswitch h_Kcall x_8689)
     904| Kwhile (x_8693, x_8692, x_8691) ->
     905  h_Kwhile x_8693 x_8692 x_8691
    906906    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    907       h_Kswitch h_Kcall x_8678)
    908 | Kdowhile (x_8683, x_8682, x_8681) ->
    909   h_Kdowhile x_8683 x_8682 x_8681
     907      h_Kswitch h_Kcall x_8691)
     908| Kdowhile (x_8696, x_8695, x_8694) ->
     909  h_Kdowhile x_8696 x_8695 x_8694
    910910    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    911       h_Kswitch h_Kcall x_8681)
    912 | Kfor2 (x_8687, x_8686, x_8685, x_8684) ->
    913   h_Kfor2 x_8687 x_8686 x_8685 x_8684
     911      h_Kswitch h_Kcall x_8694)
     912| Kfor2 (x_8700, x_8699, x_8698, x_8697) ->
     913  h_Kfor2 x_8700 x_8699 x_8698 x_8697
    914914    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    915       h_Kswitch h_Kcall x_8684)
    916 | Kfor3 (x_8691, x_8690, x_8689, x_8688) ->
    917   h_Kfor3 x_8691 x_8690 x_8689 x_8688
     915      h_Kswitch h_Kcall x_8697)
     916| Kfor3 (x_8704, x_8703, x_8702, x_8701) ->
     917  h_Kfor3 x_8704 x_8703 x_8702 x_8701
    918918    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    919       h_Kswitch h_Kcall x_8688)
    920 | Kswitch x_8692 ->
    921   h_Kswitch x_8692
     919      h_Kswitch h_Kcall x_8701)
     920| Kswitch x_8705 ->
     921  h_Kswitch x_8705
    922922    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    923       h_Kswitch h_Kcall x_8692)
    924 | Kcall (x_8696, x_8695, x_8694, x_8693) ->
    925   h_Kcall x_8696 x_8695 x_8694 x_8693
     923      h_Kswitch h_Kcall x_8705)
     924| Kcall (x_8709, x_8708, x_8707, x_8706) ->
     925  h_Kcall x_8709 x_8708 x_8707 x_8706
    926926    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    927       h_Kswitch h_Kcall x_8693)
     927      h_Kswitch h_Kcall x_8706)
    928928
    929929(** val cont_rect_Type0 :
     
    938938let rec cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
    939939| Kstop -> h_Kstop
    940 | Kseq (x_8707, x_8706) ->
    941   h_Kseq x_8707 x_8706
     940| Kseq (x_8720, x_8719) ->
     941  h_Kseq x_8720 x_8719
    942942    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    943       h_Kswitch h_Kcall x_8706)
    944 | Kwhile (x_8710, x_8709, x_8708) ->
    945   h_Kwhile x_8710 x_8709 x_8708
     943      h_Kswitch h_Kcall x_8719)
     944| Kwhile (x_8723, x_8722, x_8721) ->
     945  h_Kwhile x_8723 x_8722 x_8721
    946946    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    947       h_Kswitch h_Kcall x_8708)
    948 | Kdowhile (x_8713, x_8712, x_8711) ->
    949   h_Kdowhile x_8713 x_8712 x_8711
     947      h_Kswitch h_Kcall x_8721)
     948| Kdowhile (x_8726, x_8725, x_8724) ->
     949  h_Kdowhile x_8726 x_8725 x_8724
    950950    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    951       h_Kswitch h_Kcall x_8711)
    952 | Kfor2 (x_8717, x_8716, x_8715, x_8714) ->
    953   h_Kfor2 x_8717 x_8716 x_8715 x_8714
     951      h_Kswitch h_Kcall x_8724)
     952| Kfor2 (x_8730, x_8729, x_8728, x_8727) ->
     953  h_Kfor2 x_8730 x_8729 x_8728 x_8727
    954954    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    955       h_Kswitch h_Kcall x_8714)
    956 | Kfor3 (x_8721, x_8720, x_8719, x_8718) ->
    957   h_Kfor3 x_8721 x_8720 x_8719 x_8718
     955      h_Kswitch h_Kcall x_8727)
     956| Kfor3 (x_8734, x_8733, x_8732, x_8731) ->
     957  h_Kfor3 x_8734 x_8733 x_8732 x_8731
    958958    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    959       h_Kswitch h_Kcall x_8718)
    960 | Kswitch x_8722 ->
    961   h_Kswitch x_8722
     959      h_Kswitch h_Kcall x_8731)
     960| Kswitch x_8735 ->
     961  h_Kswitch x_8735
    962962    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    963       h_Kswitch h_Kcall x_8722)
    964 | Kcall (x_8726, x_8725, x_8724, x_8723) ->
    965   h_Kcall x_8726 x_8725 x_8724 x_8723
     963      h_Kswitch h_Kcall x_8735)
     964| Kcall (x_8739, x_8738, x_8737, x_8736) ->
     965  h_Kcall x_8739 x_8738 x_8737 x_8736
    966966    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    967       h_Kswitch h_Kcall x_8723)
     967      h_Kswitch h_Kcall x_8736)
    968968
    969969(** val cont_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.