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/classifyOp.ml

    r3001 r3043  
    9696    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    9797    -> classify_add_cases -> 'a1 **)
    98 let rec classify_add_cases_rect_Type4 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_9258 x_9257 = function
     98let rec classify_add_cases_rect_Type4 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7441 x_7440 = function
    9999| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
    100100| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
     
    108108    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    109109    -> classify_add_cases -> 'a1 **)
    110 let rec classify_add_cases_rect_Type5 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_9265 x_9264 = function
     110let rec classify_add_cases_rect_Type5 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7448 x_7447 = function
    111111| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
    112112| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
     
    120120    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    121121    -> classify_add_cases -> 'a1 **)
    122 let rec classify_add_cases_rect_Type3 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_9272 x_9271 = function
     122let rec classify_add_cases_rect_Type3 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7455 x_7454 = function
    123123| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
    124124| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
     
    132132    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    133133    -> classify_add_cases -> 'a1 **)
    134 let rec classify_add_cases_rect_Type2 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_9279 x_9278 = function
     134let rec classify_add_cases_rect_Type2 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7462 x_7461 = function
    135135| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
    136136| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
     
    144144    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    145145    -> classify_add_cases -> 'a1 **)
    146 let rec classify_add_cases_rect_Type1 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_9286 x_9285 = function
     146let rec classify_add_cases_rect_Type1 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7469 x_7468 = function
    147147| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
    148148| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
     
    156156    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
    157157    -> classify_add_cases -> 'a1 **)
    158 let rec classify_add_cases_rect_Type0 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_9293 x_9292 = function
     158let rec classify_add_cases_rect_Type0 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7476 x_7475 = function
    159159| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
    160160| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
     
    319319    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    320320    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
    321 let rec classify_sub_cases_rect_Type4 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_9349 x_9348 = function
     321let rec classify_sub_cases_rect_Type4 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7532 x_7531 = function
    322322| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
    323323| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
     
    331331    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    332332    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
    333 let rec classify_sub_cases_rect_Type5 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_9356 x_9355 = function
     333let rec classify_sub_cases_rect_Type5 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7539 x_7538 = function
    334334| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
    335335| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
     
    343343    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    344344    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
    345 let rec classify_sub_cases_rect_Type3 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_9363 x_9362 = function
     345let rec classify_sub_cases_rect_Type3 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7546 x_7545 = function
    346346| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
    347347| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
     
    355355    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    356356    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
    357 let rec classify_sub_cases_rect_Type2 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_9370 x_9369 = function
     357let rec classify_sub_cases_rect_Type2 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7553 x_7552 = function
    358358| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
    359359| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
     
    367367    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    368368    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
    369 let rec classify_sub_cases_rect_Type1 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_9377 x_9376 = function
     369let rec classify_sub_cases_rect_Type1 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7560 x_7559 = function
    370370| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
    371371| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
     
    379379    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
    380380    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
    381 let rec classify_sub_cases_rect_Type0 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_9384 x_9383 = function
     381let rec classify_sub_cases_rect_Type0 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7567 x_7566 = function
    382382| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
    383383| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
     
    519519    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    520520    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
    521 let rec classify_aop_cases_rect_Type4 h_aop_case_ii h_aop_default x_9438 x_9437 = function
     521let rec classify_aop_cases_rect_Type4 h_aop_case_ii h_aop_default x_7621 x_7620 = function
    522522| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
    523523| Aop_default (ty, ty') -> h_aop_default ty ty'
     
    526526    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    527527    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
    528 let rec classify_aop_cases_rect_Type5 h_aop_case_ii h_aop_default x_9443 x_9442 = function
     528let rec classify_aop_cases_rect_Type5 h_aop_case_ii h_aop_default x_7626 x_7625 = function
    529529| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
    530530| Aop_default (ty, ty') -> h_aop_default ty ty'
     
    533533    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    534534    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
    535 let rec classify_aop_cases_rect_Type3 h_aop_case_ii h_aop_default x_9448 x_9447 = function
     535let rec classify_aop_cases_rect_Type3 h_aop_case_ii h_aop_default x_7631 x_7630 = function
    536536| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
    537537| Aop_default (ty, ty') -> h_aop_default ty ty'
     
    540540    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    541541    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
    542 let rec classify_aop_cases_rect_Type2 h_aop_case_ii h_aop_default x_9453 x_9452 = function
     542let rec classify_aop_cases_rect_Type2 h_aop_case_ii h_aop_default x_7636 x_7635 = function
    543543| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
    544544| Aop_default (ty, ty') -> h_aop_default ty ty'
     
    547547    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    548548    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
    549 let rec classify_aop_cases_rect_Type1 h_aop_case_ii h_aop_default x_9458 x_9457 = function
     549let rec classify_aop_cases_rect_Type1 h_aop_case_ii h_aop_default x_7641 x_7640 = function
    550550| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
    551551| Aop_default (ty, ty') -> h_aop_default ty ty'
     
    554554    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
    555555    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
    556 let rec classify_aop_cases_rect_Type0 h_aop_case_ii h_aop_default x_9463 x_9462 = function
     556let rec classify_aop_cases_rect_Type0 h_aop_case_ii h_aop_default x_7646 x_7645 = function
    557557| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
    558558| Aop_default (ty, ty') -> h_aop_default ty ty'
     
    636636    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    637637    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
    638 let rec classify_cmp_cases_rect_Type4 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_9504 x_9503 = function
     638let rec classify_cmp_cases_rect_Type4 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7687 x_7686 = function
    639639| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
    640640| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
     
    645645    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    646646    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
    647 let rec classify_cmp_cases_rect_Type5 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_9510 x_9509 = function
     647let rec classify_cmp_cases_rect_Type5 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7693 x_7692 = function
    648648| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
    649649| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
     
    654654    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    655655    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
    656 let rec classify_cmp_cases_rect_Type3 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_9516 x_9515 = function
     656let rec classify_cmp_cases_rect_Type3 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7699 x_7698 = function
    657657| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
    658658| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
     
    663663    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    664664    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
    665 let rec classify_cmp_cases_rect_Type2 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_9522 x_9521 = function
     665let rec classify_cmp_cases_rect_Type2 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7705 x_7704 = function
    666666| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
    667667| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
     
    672672    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    673673    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
    674 let rec classify_cmp_cases_rect_Type1 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_9528 x_9527 = function
     674let rec classify_cmp_cases_rect_Type1 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7711 x_7710 = function
    675675| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
    676676| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
     
    681681    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
    682682    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
    683 let rec classify_cmp_cases_rect_Type0 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_9534 x_9533 = function
     683let rec classify_cmp_cases_rect_Type0 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7717 x_7716 = function
    684684| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
    685685| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
     
    780780    -> 'a1 **)
    781781let rec classify_fun_cases_rect_Type4 h_fun_case_f h_fun_default = function
    782 | Fun_case_f (x_9582, x_9581) -> h_fun_case_f x_9582 x_9581
     782| Fun_case_f (x_7765, x_7764) -> h_fun_case_f x_7765 x_7764
    783783| Fun_default -> h_fun_default
    784784
     
    787787    -> 'a1 **)
    788788let rec classify_fun_cases_rect_Type5 h_fun_case_f h_fun_default = function
    789 | Fun_case_f (x_9587, x_9586) -> h_fun_case_f x_9587 x_9586
     789| Fun_case_f (x_7770, x_7769) -> h_fun_case_f x_7770 x_7769
    790790| Fun_default -> h_fun_default
    791791
     
    794794    -> 'a1 **)
    795795let rec classify_fun_cases_rect_Type3 h_fun_case_f h_fun_default = function
    796 | Fun_case_f (x_9592, x_9591) -> h_fun_case_f x_9592 x_9591
     796| Fun_case_f (x_7775, x_7774) -> h_fun_case_f x_7775 x_7774
    797797| Fun_default -> h_fun_default
    798798
     
    801801    -> 'a1 **)
    802802let rec classify_fun_cases_rect_Type2 h_fun_case_f h_fun_default = function
    803 | Fun_case_f (x_9597, x_9596) -> h_fun_case_f x_9597 x_9596
     803| Fun_case_f (x_7780, x_7779) -> h_fun_case_f x_7780 x_7779
    804804| Fun_default -> h_fun_default
    805805
     
    808808    -> 'a1 **)
    809809let rec classify_fun_cases_rect_Type1 h_fun_case_f h_fun_default = function
    810 | Fun_case_f (x_9602, x_9601) -> h_fun_case_f x_9602 x_9601
     810| Fun_case_f (x_7785, x_7784) -> h_fun_case_f x_7785 x_7784
    811811| Fun_default -> h_fun_default
    812812
     
    815815    -> 'a1 **)
    816816let rec classify_fun_cases_rect_Type0 h_fun_case_f h_fun_default = function
    817 | Fun_case_f (x_9607, x_9606) -> h_fun_case_f x_9607 x_9606
     817| Fun_case_f (x_7790, x_7789) -> h_fun_case_f x_7790 x_7789
    818818| Fun_default -> h_fun_default
    819819
Note: See TracChangeset for help on using the changeset viewer.