Changeset 3043 for extracted/aST.ml


Ignore:
Timestamp:
Mar 29, 2013, 6:38:26 PM (7 years ago)
Author:
sacerdot
Message:

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/aST.ml

    r2997 r3043  
    418418    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
    419419let rec typ_rect_Type4 h_ASTint h_ASTptr = function
    420 | ASTint (x_411, x_410) -> h_ASTint x_411 x_410
     420| ASTint (x_3662, x_3661) -> h_ASTint x_3662 x_3661
    421421| ASTptr -> h_ASTptr
    422422
     
    424424    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
    425425let rec typ_rect_Type5 h_ASTint h_ASTptr = function
    426 | ASTint (x_416, x_415) -> h_ASTint x_416 x_415
     426| ASTint (x_3667, x_3666) -> h_ASTint x_3667 x_3666
    427427| ASTptr -> h_ASTptr
    428428
     
    430430    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
    431431let rec typ_rect_Type3 h_ASTint h_ASTptr = function
    432 | ASTint (x_421, x_420) -> h_ASTint x_421 x_420
     432| ASTint (x_3672, x_3671) -> h_ASTint x_3672 x_3671
    433433| ASTptr -> h_ASTptr
    434434
     
    436436    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
    437437let rec typ_rect_Type2 h_ASTint h_ASTptr = function
    438 | ASTint (x_426, x_425) -> h_ASTint x_426 x_425
     438| ASTint (x_3677, x_3676) -> h_ASTint x_3677 x_3676
    439439| ASTptr -> h_ASTptr
    440440
     
    442442    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
    443443let rec typ_rect_Type1 h_ASTint h_ASTptr = function
    444 | ASTint (x_431, x_430) -> h_ASTint x_431 x_430
     444| ASTint (x_3682, x_3681) -> h_ASTint x_3682 x_3681
    445445| ASTptr -> h_ASTptr
    446446
     
    448448    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
    449449let rec typ_rect_Type0 h_ASTint h_ASTptr = function
    450 | ASTint (x_436, x_435) -> h_ASTint x_436 x_435
     450| ASTint (x_3687, x_3686) -> h_ASTint x_3687 x_3686
    451451| ASTptr -> h_ASTptr
    452452
     
    877877(** val signature_rect_Type4 :
    878878    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
    879 let rec signature_rect_Type4 h_mk_signature x_471 =
    880   let { sig_args = sig_args0; sig_res = sig_res0 } = x_471 in
     879let rec signature_rect_Type4 h_mk_signature x_3722 =
     880  let { sig_args = sig_args0; sig_res = sig_res0 } = x_3722 in
    881881  h_mk_signature sig_args0 sig_res0
    882882
    883883(** val signature_rect_Type5 :
    884884    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
    885 let rec signature_rect_Type5 h_mk_signature x_473 =
    886   let { sig_args = sig_args0; sig_res = sig_res0 } = x_473 in
     885let rec signature_rect_Type5 h_mk_signature x_3724 =
     886  let { sig_args = sig_args0; sig_res = sig_res0 } = x_3724 in
    887887  h_mk_signature sig_args0 sig_res0
    888888
    889889(** val signature_rect_Type3 :
    890890    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
    891 let rec signature_rect_Type3 h_mk_signature x_475 =
    892   let { sig_args = sig_args0; sig_res = sig_res0 } = x_475 in
     891let rec signature_rect_Type3 h_mk_signature x_3726 =
     892  let { sig_args = sig_args0; sig_res = sig_res0 } = x_3726 in
    893893  h_mk_signature sig_args0 sig_res0
    894894
    895895(** val signature_rect_Type2 :
    896896    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
    897 let rec signature_rect_Type2 h_mk_signature x_477 =
    898   let { sig_args = sig_args0; sig_res = sig_res0 } = x_477 in
     897let rec signature_rect_Type2 h_mk_signature x_3728 =
     898  let { sig_args = sig_args0; sig_res = sig_res0 } = x_3728 in
    899899  h_mk_signature sig_args0 sig_res0
    900900
    901901(** val signature_rect_Type1 :
    902902    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
    903 let rec signature_rect_Type1 h_mk_signature x_479 =
    904   let { sig_args = sig_args0; sig_res = sig_res0 } = x_479 in
     903let rec signature_rect_Type1 h_mk_signature x_3730 =
     904  let { sig_args = sig_args0; sig_res = sig_res0 } = x_3730 in
    905905  h_mk_signature sig_args0 sig_res0
    906906
    907907(** val signature_rect_Type0 :
    908908    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
    909 let rec signature_rect_Type0 h_mk_signature x_481 =
    910   let { sig_args = sig_args0; sig_res = sig_res0 } = x_481 in
     909let rec signature_rect_Type0 h_mk_signature x_3732 =
     910  let { sig_args = sig_args0; sig_res = sig_res0 } = x_3732 in
    911911  h_mk_signature sig_args0 sig_res0
    912912
     
    984984    'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
    985985let rec init_data_rect_Type4 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_space h_Init_null h_Init_addrof = function
    986 | Init_int8 x_509 -> h_Init_int8 x_509
    987 | Init_int16 x_510 -> h_Init_int16 x_510
    988 | Init_int32 x_511 -> h_Init_int32 x_511
    989 | Init_space x_512 -> h_Init_space x_512
     986| Init_int8 x_3760 -> h_Init_int8 x_3760
     987| Init_int16 x_3761 -> h_Init_int16 x_3761
     988| Init_int32 x_3762 -> h_Init_int32 x_3762
     989| Init_space x_3763 -> h_Init_space x_3763
    990990| Init_null -> h_Init_null
    991 | Init_addrof (x_514, x_513) -> h_Init_addrof x_514 x_513
     991| Init_addrof (x_3765, x_3764) -> h_Init_addrof x_3765 x_3764
    992992
    993993(** val init_data_rect_Type5 :
     
    995995    'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
    996996let rec init_data_rect_Type5 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_space h_Init_null h_Init_addrof = function
    997 | Init_int8 x_522 -> h_Init_int8 x_522
    998 | Init_int16 x_523 -> h_Init_int16 x_523
    999 | Init_int32 x_524 -> h_Init_int32 x_524
    1000 | Init_space x_525 -> h_Init_space x_525
     997| Init_int8 x_3773 -> h_Init_int8 x_3773
     998| Init_int16 x_3774 -> h_Init_int16 x_3774
     999| Init_int32 x_3775 -> h_Init_int32 x_3775
     1000| Init_space x_3776 -> h_Init_space x_3776
    10011001| Init_null -> h_Init_null
    1002 | Init_addrof (x_527, x_526) -> h_Init_addrof x_527 x_526
     1002| Init_addrof (x_3778, x_3777) -> h_Init_addrof x_3778 x_3777
    10031003
    10041004(** val init_data_rect_Type3 :
     
    10061006    'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
    10071007let rec init_data_rect_Type3 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_space h_Init_null h_Init_addrof = function
    1008 | Init_int8 x_535 -> h_Init_int8 x_535
    1009 | Init_int16 x_536 -> h_Init_int16 x_536
    1010 | Init_int32 x_537 -> h_Init_int32 x_537
    1011 | Init_space x_538 -> h_Init_space x_538
     1008| Init_int8 x_3786 -> h_Init_int8 x_3786
     1009| Init_int16 x_3787 -> h_Init_int16 x_3787
     1010| Init_int32 x_3788 -> h_Init_int32 x_3788
     1011| Init_space x_3789 -> h_Init_space x_3789
    10121012| Init_null -> h_Init_null
    1013 | Init_addrof (x_540, x_539) -> h_Init_addrof x_540 x_539
     1013| Init_addrof (x_3791, x_3790) -> h_Init_addrof x_3791 x_3790
    10141014
    10151015(** val init_data_rect_Type2 :
     
    10171017    'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
    10181018let rec init_data_rect_Type2 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_space h_Init_null h_Init_addrof = function
    1019 | Init_int8 x_548 -> h_Init_int8 x_548
    1020 | Init_int16 x_549 -> h_Init_int16 x_549
    1021 | Init_int32 x_550 -> h_Init_int32 x_550
    1022 | Init_space x_551 -> h_Init_space x_551
     1019| Init_int8 x_3799 -> h_Init_int8 x_3799
     1020| Init_int16 x_3800 -> h_Init_int16 x_3800
     1021| Init_int32 x_3801 -> h_Init_int32 x_3801
     1022| Init_space x_3802 -> h_Init_space x_3802
    10231023| Init_null -> h_Init_null
    1024 | Init_addrof (x_553, x_552) -> h_Init_addrof x_553 x_552
     1024| Init_addrof (x_3804, x_3803) -> h_Init_addrof x_3804 x_3803
    10251025
    10261026(** val init_data_rect_Type1 :
     
    10281028    'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
    10291029let rec init_data_rect_Type1 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_space h_Init_null h_Init_addrof = function
    1030 | Init_int8 x_561 -> h_Init_int8 x_561
    1031 | Init_int16 x_562 -> h_Init_int16 x_562
    1032 | Init_int32 x_563 -> h_Init_int32 x_563
    1033 | Init_space x_564 -> h_Init_space x_564
     1030| Init_int8 x_3812 -> h_Init_int8 x_3812
     1031| Init_int16 x_3813 -> h_Init_int16 x_3813
     1032| Init_int32 x_3814 -> h_Init_int32 x_3814
     1033| Init_space x_3815 -> h_Init_space x_3815
    10341034| Init_null -> h_Init_null
    1035 | Init_addrof (x_566, x_565) -> h_Init_addrof x_566 x_565
     1035| Init_addrof (x_3817, x_3816) -> h_Init_addrof x_3817 x_3816
    10361036
    10371037(** val init_data_rect_Type0 :
     
    10391039    'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
    10401040let rec init_data_rect_Type0 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_space h_Init_null h_Init_addrof = function
    1041 | Init_int8 x_574 -> h_Init_int8 x_574
    1042 | Init_int16 x_575 -> h_Init_int16 x_575
    1043 | Init_int32 x_576 -> h_Init_int32 x_576
    1044 | Init_space x_577 -> h_Init_space x_577
     1041| Init_int8 x_3825 -> h_Init_int8 x_3825
     1042| Init_int16 x_3826 -> h_Init_int16 x_3826
     1043| Init_int32 x_3827 -> h_Init_int32 x_3827
     1044| Init_space x_3828 -> h_Init_space x_3828
    10451045| Init_null -> h_Init_null
    1046 | Init_addrof (x_579, x_578) -> h_Init_addrof x_579 x_578
     1046| Init_addrof (x_3830, x_3829) -> h_Init_addrof x_3830 x_3829
    10471047
    10481048(** val init_data_inv_rect_Type4 :
     
    11111111    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    11121112    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
    1113 let rec program_rect_Type4 h_mk_program x_666 =
     1113let rec program_rect_Type4 h_mk_program x_3917 =
    11141114  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1115     prog_main0 } = x_666
     1115    prog_main0 } = x_3917
    11161116  in
    11171117  h_mk_program prog_vars0 prog_funct0 prog_main0
     
    11201120    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    11211121    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
    1122 let rec program_rect_Type5 h_mk_program x_668 =
     1122let rec program_rect_Type5 h_mk_program x_3919 =
    11231123  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1124     prog_main0 } = x_668
     1124    prog_main0 } = x_3919
    11251125  in
    11261126  h_mk_program prog_vars0 prog_funct0 prog_main0
     
    11291129    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    11301130    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
    1131 let rec program_rect_Type3 h_mk_program x_670 =
     1131let rec program_rect_Type3 h_mk_program x_3921 =
    11321132  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1133     prog_main0 } = x_670
     1133    prog_main0 } = x_3921
    11341134  in
    11351135  h_mk_program prog_vars0 prog_funct0 prog_main0
     
    11381138    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    11391139    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
    1140 let rec program_rect_Type2 h_mk_program x_672 =
     1140let rec program_rect_Type2 h_mk_program x_3923 =
    11411141  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1142     prog_main0 } = x_672
     1142    prog_main0 } = x_3923
    11431143  in
    11441144  h_mk_program prog_vars0 prog_funct0 prog_main0
     
    11471147    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    11481148    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
    1149 let rec program_rect_Type1 h_mk_program x_674 =
     1149let rec program_rect_Type1 h_mk_program x_3925 =
    11501150  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1151     prog_main0 } = x_674
     1151    prog_main0 } = x_3925
    11521152  in
    11531153  h_mk_program prog_vars0 prog_funct0 prog_main0
     
    11561156    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    11571157    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
    1158 let rec program_rect_Type0 h_mk_program x_676 =
     1158let rec program_rect_Type0 h_mk_program x_3927 =
    11591159  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1160     prog_main0 } = x_676
     1160    prog_main0 } = x_3927
    11611161  in
    11621162  h_mk_program prog_vars0 prog_funct0 prog_main0
     
    14771477(** val external_function_rect_Type4 :
    14781478    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1479 let rec external_function_rect_Type4 h_mk_external_function x_880 =
    1480   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_880 in
     1479let rec external_function_rect_Type4 h_mk_external_function x_4131 =
     1480  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4131 in
    14811481  h_mk_external_function ef_id0 ef_sig0
    14821482
    14831483(** val external_function_rect_Type5 :
    14841484    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1485 let rec external_function_rect_Type5 h_mk_external_function x_882 =
    1486   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_882 in
     1485let rec external_function_rect_Type5 h_mk_external_function x_4133 =
     1486  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4133 in
    14871487  h_mk_external_function ef_id0 ef_sig0
    14881488
    14891489(** val external_function_rect_Type3 :
    14901490    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1491 let rec external_function_rect_Type3 h_mk_external_function x_884 =
    1492   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_884 in
     1491let rec external_function_rect_Type3 h_mk_external_function x_4135 =
     1492  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4135 in
    14931493  h_mk_external_function ef_id0 ef_sig0
    14941494
    14951495(** val external_function_rect_Type2 :
    14961496    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1497 let rec external_function_rect_Type2 h_mk_external_function x_886 =
    1498   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_886 in
     1497let rec external_function_rect_Type2 h_mk_external_function x_4137 =
     1498  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4137 in
    14991499  h_mk_external_function ef_id0 ef_sig0
    15001500
    15011501(** val external_function_rect_Type1 :
    15021502    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1503 let rec external_function_rect_Type1 h_mk_external_function x_888 =
    1504   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_888 in
     1503let rec external_function_rect_Type1 h_mk_external_function x_4139 =
     1504  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4139 in
    15051505  h_mk_external_function ef_id0 ef_sig0
    15061506
    15071507(** val external_function_rect_Type0 :
    15081508    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1509 let rec external_function_rect_Type0 h_mk_external_function x_890 =
    1510   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_890 in
     1509let rec external_function_rect_Type0 h_mk_external_function x_4141 =
     1510  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4141 in
    15111511  h_mk_external_function ef_id0 ef_sig0
    15121512
     
    15751575    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    15761576let rec fundef_rect_Type4 h_Internal h_External = function
    1577 | Internal x_910 -> h_Internal x_910
    1578 | External x_911 -> h_External x_911
     1577| Internal x_4161 -> h_Internal x_4161
     1578| External x_4162 -> h_External x_4162
    15791579
    15801580(** val fundef_rect_Type5 :
    15811581    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    15821582let rec fundef_rect_Type5 h_Internal h_External = function
    1583 | Internal x_915 -> h_Internal x_915
    1584 | External x_916 -> h_External x_916
     1583| Internal x_4166 -> h_Internal x_4166
     1584| External x_4167 -> h_External x_4167
    15851585
    15861586(** val fundef_rect_Type3 :
    15871587    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    15881588let rec fundef_rect_Type3 h_Internal h_External = function
    1589 | Internal x_920 -> h_Internal x_920
    1590 | External x_921 -> h_External x_921
     1589| Internal x_4171 -> h_Internal x_4171
     1590| External x_4172 -> h_External x_4172
    15911591
    15921592(** val fundef_rect_Type2 :
    15931593    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    15941594let rec fundef_rect_Type2 h_Internal h_External = function
    1595 | Internal x_925 -> h_Internal x_925
    1596 | External x_926 -> h_External x_926
     1595| Internal x_4176 -> h_Internal x_4176
     1596| External x_4177 -> h_External x_4177
    15971597
    15981598(** val fundef_rect_Type1 :
    15991599    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    16001600let rec fundef_rect_Type1 h_Internal h_External = function
    1601 | Internal x_930 -> h_Internal x_930
    1602 | External x_931 -> h_External x_931
     1601| Internal x_4181 -> h_Internal x_4181
     1602| External x_4182 -> h_External x_4182
    16031603
    16041604(** val fundef_rect_Type0 :
    16051605    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    16061606let rec fundef_rect_Type0 h_Internal h_External = function
    1607 | Internal x_935 -> h_Internal x_935
    1608 | External x_936 -> h_External x_936
     1607| Internal x_4186 -> h_Internal x_4186
     1608| External x_4187 -> h_External x_4187
    16091609
    16101610(** val fundef_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.