Ignore:
Timestamp:
Feb 7, 2013, 10:43:49 PM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/frontEndOps.ml

    r2601 r2649  
    1313open Identifiers
    1414
    15 open Floats
    16 
    1715open Integers
    1816
     
    3735open Pointers
    3836
     37open ErrorMessages
     38
    3939open Option
    4040
     
    4444
    4545open Positive
    46 
    47 open Char
    48 
    49 open String
    5046
    5147open PreIdentifiers
     
    10197    (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
    10298    Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
    103 let rec constant_rect_Type4 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_12056 = function
    104 | Ointconst (sz, sg, x_12058) -> h_Ointconst sz sg x_12058
    105 | Oaddrsymbol (x_12060, x_12059) -> h_Oaddrsymbol x_12060 x_12059
    106 | Oaddrstack x_12061 -> h_Oaddrstack x_12061
     99let rec constant_rect_Type4 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_9741 = function
     100| Ointconst (sz, sg, x_9743) -> h_Ointconst sz sg x_9743
     101| Oaddrsymbol (x_9745, x_9744) -> h_Oaddrsymbol x_9745 x_9744
     102| Oaddrstack x_9746 -> h_Oaddrstack x_9746
    107103
    108104(** val constant_rect_Type5 :
    109105    (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
    110106    Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
    111 let rec constant_rect_Type5 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_12065 = function
    112 | Ointconst (sz, sg, x_12067) -> h_Ointconst sz sg x_12067
    113 | Oaddrsymbol (x_12069, x_12068) -> h_Oaddrsymbol x_12069 x_12068
    114 | Oaddrstack x_12070 -> h_Oaddrstack x_12070
     107let rec constant_rect_Type5 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_9750 = function
     108| Ointconst (sz, sg, x_9752) -> h_Ointconst sz sg x_9752
     109| Oaddrsymbol (x_9754, x_9753) -> h_Oaddrsymbol x_9754 x_9753
     110| Oaddrstack x_9755 -> h_Oaddrstack x_9755
    115111
    116112(** val constant_rect_Type3 :
    117113    (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
    118114    Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
    119 let rec constant_rect_Type3 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_12074 = function
    120 | Ointconst (sz, sg, x_12076) -> h_Ointconst sz sg x_12076
    121 | Oaddrsymbol (x_12078, x_12077) -> h_Oaddrsymbol x_12078 x_12077
    122 | Oaddrstack x_12079 -> h_Oaddrstack x_12079
     115let rec constant_rect_Type3 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_9759 = function
     116| Ointconst (sz, sg, x_9761) -> h_Ointconst sz sg x_9761
     117| Oaddrsymbol (x_9763, x_9762) -> h_Oaddrsymbol x_9763 x_9762
     118| Oaddrstack x_9764 -> h_Oaddrstack x_9764
    123119
    124120(** val constant_rect_Type2 :
    125121    (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
    126122    Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
    127 let rec constant_rect_Type2 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_12083 = function
    128 | Ointconst (sz, sg, x_12085) -> h_Ointconst sz sg x_12085
    129 | Oaddrsymbol (x_12087, x_12086) -> h_Oaddrsymbol x_12087 x_12086
    130 | Oaddrstack x_12088 -> h_Oaddrstack x_12088
     123let rec constant_rect_Type2 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_9768 = function
     124| Ointconst (sz, sg, x_9770) -> h_Ointconst sz sg x_9770
     125| Oaddrsymbol (x_9772, x_9771) -> h_Oaddrsymbol x_9772 x_9771
     126| Oaddrstack x_9773 -> h_Oaddrstack x_9773
    131127
    132128(** val constant_rect_Type1 :
    133129    (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
    134130    Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
    135 let rec constant_rect_Type1 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_12092 = function
    136 | Ointconst (sz, sg, x_12094) -> h_Ointconst sz sg x_12094
    137 | Oaddrsymbol (x_12096, x_12095) -> h_Oaddrsymbol x_12096 x_12095
    138 | Oaddrstack x_12097 -> h_Oaddrstack x_12097
     131let rec constant_rect_Type1 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_9777 = function
     132| Ointconst (sz, sg, x_9779) -> h_Ointconst sz sg x_9779
     133| Oaddrsymbol (x_9781, x_9780) -> h_Oaddrsymbol x_9781 x_9780
     134| Oaddrstack x_9782 -> h_Oaddrstack x_9782
    139135
    140136(** val constant_rect_Type0 :
    141137    (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
    142138    Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
    143 let rec constant_rect_Type0 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_12101 = function
    144 | Ointconst (sz, sg, x_12103) -> h_Ointconst sz sg x_12103
    145 | Oaddrsymbol (x_12105, x_12104) -> h_Oaddrsymbol x_12105 x_12104
    146 | Oaddrstack x_12106 -> h_Oaddrstack x_12106
     139let rec constant_rect_Type0 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_9786 = function
     140| Ointconst (sz, sg, x_9788) -> h_Ointconst sz sg x_9788
     141| Oaddrsymbol (x_9790, x_9789) -> h_Oaddrsymbol x_9790 x_9789
     142| Oaddrstack x_9791 -> h_Oaddrstack x_9791
    147143
    148144(** val constant_inv_rect_Type4 :
     
    213209    (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
    214210    unary_operation -> 'a1 **)
    215 let rec unary_operation_rect_Type4 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_12176 x_12175 = function
     211let rec unary_operation_rect_Type4 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_9861 x_9860 = function
    216212| Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
    217213| Onegint (sz, sg) -> h_Onegint sz sg
     
    229225    (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
    230226    unary_operation -> 'a1 **)
    231 let rec unary_operation_rect_Type5 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_12187 x_12186 = function
     227let rec unary_operation_rect_Type5 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_9872 x_9871 = function
    232228| Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
    233229| Onegint (sz, sg) -> h_Onegint sz sg
     
    245241    (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
    246242    unary_operation -> 'a1 **)
    247 let rec unary_operation_rect_Type3 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_12198 x_12197 = function
     243let rec unary_operation_rect_Type3 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_9883 x_9882 = function
    248244| Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
    249245| Onegint (sz, sg) -> h_Onegint sz sg
     
    261257    (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
    262258    unary_operation -> 'a1 **)
    263 let rec unary_operation_rect_Type2 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_12209 x_12208 = function
     259let rec unary_operation_rect_Type2 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_9894 x_9893 = function
    264260| Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
    265261| Onegint (sz, sg) -> h_Onegint sz sg
     
    277273    (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
    278274    unary_operation -> 'a1 **)
    279 let rec unary_operation_rect_Type1 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_12220 x_12219 = function
     275let rec unary_operation_rect_Type1 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_9905 x_9904 = function
    280276| Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
    281277| Onegint (sz, sg) -> h_Onegint sz sg
     
    293289    (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
    294290    unary_operation -> 'a1 **)
    295 let rec unary_operation_rect_Type0 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_12231 x_12230 = function
     291let rec unary_operation_rect_Type0 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_9916 x_9915 = function
    296292| Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
    297293| Onegint (sz, sg) -> h_Onegint sz sg
     
    428424    (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
    429425    AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
    430 let rec binary_operation_rect_Type4 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_12336 x_12335 x_12334 = function
     426let rec binary_operation_rect_Type4 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_10021 x_10020 x_10019 = function
    431427| Oadd (sz, sg) -> h_Oadd sz sg
    432428| Osub (sz, sg) -> h_Osub sz sg
     
    442438| Oshr (sz, sg) -> h_Oshr sz sg
    443439| Oshru (sz, sg) -> h_Oshru sz sg
    444 | Ocmp (sz, sg, sg', x_12338) -> h_Ocmp sz sg sg' x_12338
    445 | Ocmpu (sz, sg', x_12339) -> h_Ocmpu sz sg' x_12339
     440| Ocmp (sz, sg, sg', x_10023) -> h_Ocmp sz sg sg' x_10023
     441| Ocmpu (sz, sg', x_10024) -> h_Ocmpu sz sg' x_10024
    446442| Oaddpi sz -> h_Oaddpi sz
    447443| Oaddip sz -> h_Oaddip sz
    448444| Osubpi sz -> h_Osubpi sz
    449445| Osubpp sz -> h_Osubpp sz
    450 | Ocmpp (sg', x_12340) -> h_Ocmpp sg' x_12340
     446| Ocmpp (sg', x_10025) -> h_Ocmpp sg' x_10025
    451447
    452448(** val binary_operation_rect_Type5 :
     
    463459    (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
    464460    AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
    465 let rec binary_operation_rect_Type5 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_12363 x_12362 x_12361 = function
     461let rec binary_operation_rect_Type5 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_10048 x_10047 x_10046 = function
    466462| Oadd (sz, sg) -> h_Oadd sz sg
    467463| Osub (sz, sg) -> h_Osub sz sg
     
    477473| Oshr (sz, sg) -> h_Oshr sz sg
    478474| Oshru (sz, sg) -> h_Oshru sz sg
    479 | Ocmp (sz, sg, sg', x_12365) -> h_Ocmp sz sg sg' x_12365
    480 | Ocmpu (sz, sg', x_12366) -> h_Ocmpu sz sg' x_12366
     475| Ocmp (sz, sg, sg', x_10050) -> h_Ocmp sz sg sg' x_10050
     476| Ocmpu (sz, sg', x_10051) -> h_Ocmpu sz sg' x_10051
    481477| Oaddpi sz -> h_Oaddpi sz
    482478| Oaddip sz -> h_Oaddip sz
    483479| Osubpi sz -> h_Osubpi sz
    484480| Osubpp sz -> h_Osubpp sz
    485 | Ocmpp (sg', x_12367) -> h_Ocmpp sg' x_12367
     481| Ocmpp (sg', x_10052) -> h_Ocmpp sg' x_10052
    486482
    487483(** val binary_operation_rect_Type3 :
     
    498494    (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
    499495    AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
    500 let rec binary_operation_rect_Type3 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_12390 x_12389 x_12388 = function
     496let rec binary_operation_rect_Type3 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_10075 x_10074 x_10073 = function
    501497| Oadd (sz, sg) -> h_Oadd sz sg
    502498| Osub (sz, sg) -> h_Osub sz sg
     
    512508| Oshr (sz, sg) -> h_Oshr sz sg
    513509| Oshru (sz, sg) -> h_Oshru sz sg
    514 | Ocmp (sz, sg, sg', x_12392) -> h_Ocmp sz sg sg' x_12392
    515 | Ocmpu (sz, sg', x_12393) -> h_Ocmpu sz sg' x_12393
     510| Ocmp (sz, sg, sg', x_10077) -> h_Ocmp sz sg sg' x_10077
     511| Ocmpu (sz, sg', x_10078) -> h_Ocmpu sz sg' x_10078
    516512| Oaddpi sz -> h_Oaddpi sz
    517513| Oaddip sz -> h_Oaddip sz
    518514| Osubpi sz -> h_Osubpi sz
    519515| Osubpp sz -> h_Osubpp sz
    520 | Ocmpp (sg', x_12394) -> h_Ocmpp sg' x_12394
     516| Ocmpp (sg', x_10079) -> h_Ocmpp sg' x_10079
    521517
    522518(** val binary_operation_rect_Type2 :
     
    533529    (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
    534530    AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
    535 let rec binary_operation_rect_Type2 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_12417 x_12416 x_12415 = function
     531let rec binary_operation_rect_Type2 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_10102 x_10101 x_10100 = function
    536532| Oadd (sz, sg) -> h_Oadd sz sg
    537533| Osub (sz, sg) -> h_Osub sz sg
     
    547543| Oshr (sz, sg) -> h_Oshr sz sg
    548544| Oshru (sz, sg) -> h_Oshru sz sg
    549 | Ocmp (sz, sg, sg', x_12419) -> h_Ocmp sz sg sg' x_12419
    550 | Ocmpu (sz, sg', x_12420) -> h_Ocmpu sz sg' x_12420
     545| Ocmp (sz, sg, sg', x_10104) -> h_Ocmp sz sg sg' x_10104
     546| Ocmpu (sz, sg', x_10105) -> h_Ocmpu sz sg' x_10105
    551547| Oaddpi sz -> h_Oaddpi sz
    552548| Oaddip sz -> h_Oaddip sz
    553549| Osubpi sz -> h_Osubpi sz
    554550| Osubpp sz -> h_Osubpp sz
    555 | Ocmpp (sg', x_12421) -> h_Ocmpp sg' x_12421
     551| Ocmpp (sg', x_10106) -> h_Ocmpp sg' x_10106
    556552
    557553(** val binary_operation_rect_Type1 :
     
    568564    (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
    569565    AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
    570 let rec binary_operation_rect_Type1 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_12444 x_12443 x_12442 = function
     566let rec binary_operation_rect_Type1 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_10129 x_10128 x_10127 = function
    571567| Oadd (sz, sg) -> h_Oadd sz sg
    572568| Osub (sz, sg) -> h_Osub sz sg
     
    582578| Oshr (sz, sg) -> h_Oshr sz sg
    583579| Oshru (sz, sg) -> h_Oshru sz sg
    584 | Ocmp (sz, sg, sg', x_12446) -> h_Ocmp sz sg sg' x_12446
    585 | Ocmpu (sz, sg', x_12447) -> h_Ocmpu sz sg' x_12447
     580| Ocmp (sz, sg, sg', x_10131) -> h_Ocmp sz sg sg' x_10131
     581| Ocmpu (sz, sg', x_10132) -> h_Ocmpu sz sg' x_10132
    586582| Oaddpi sz -> h_Oaddpi sz
    587583| Oaddip sz -> h_Oaddip sz
    588584| Osubpi sz -> h_Osubpi sz
    589585| Osubpp sz -> h_Osubpp sz
    590 | Ocmpp (sg', x_12448) -> h_Ocmpp sg' x_12448
     586| Ocmpp (sg', x_10133) -> h_Ocmpp sg' x_10133
    591587
    592588(** val binary_operation_rect_Type0 :
     
    603599    (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
    604600    AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
    605 let rec binary_operation_rect_Type0 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_12471 x_12470 x_12469 = function
     601let rec binary_operation_rect_Type0 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_10156 x_10155 x_10154 = function
    606602| Oadd (sz, sg) -> h_Oadd sz sg
    607603| Osub (sz, sg) -> h_Osub sz sg
     
    617613| Oshr (sz, sg) -> h_Oshr sz sg
    618614| Oshru (sz, sg) -> h_Oshru sz sg
    619 | Ocmp (sz, sg, sg', x_12473) -> h_Ocmp sz sg sg' x_12473
    620 | Ocmpu (sz, sg', x_12474) -> h_Ocmpu sz sg' x_12474
     615| Ocmp (sz, sg, sg', x_10158) -> h_Ocmp sz sg sg' x_10158
     616| Ocmpu (sz, sg', x_10159) -> h_Ocmpu sz sg' x_10159
    621617| Oaddpi sz -> h_Oaddpi sz
    622618| Oaddip sz -> h_Oaddip sz
    623619| Osubpi sz -> h_Osubpi sz
    624620| Osubpp sz -> h_Osubpp sz
    625 | Ocmpp (sg', x_12475) -> h_Ocmpp sg' x_12475
     621| Ocmpp (sg', x_10160) -> h_Ocmpp sg' x_10160
    626622
    627623(** val binary_operation_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.