Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (7 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/frontEndOps.ml

    r2743 r2773  
    9999    (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
    100100    Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
    101 let rec constant_rect_Type4 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13083 = function
    102 | Ointconst (sz, sg, x_13085) -> h_Ointconst sz sg x_13085
    103 | Oaddrsymbol (x_13087, x_13086) -> h_Oaddrsymbol x_13087 x_13086
    104 | Oaddrstack x_13088 -> h_Oaddrstack x_13088
     101let rec constant_rect_Type4 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_8161 = function
     102| Ointconst (sz, sg, x_8163) -> h_Ointconst sz sg x_8163
     103| Oaddrsymbol (x_8165, x_8164) -> h_Oaddrsymbol x_8165 x_8164
     104| Oaddrstack x_8166 -> h_Oaddrstack x_8166
    105105
    106106(** val constant_rect_Type5 :
    107107    (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
    108108    Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
    109 let rec constant_rect_Type5 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13092 = function
    110 | Ointconst (sz, sg, x_13094) -> h_Ointconst sz sg x_13094
    111 | Oaddrsymbol (x_13096, x_13095) -> h_Oaddrsymbol x_13096 x_13095
    112 | Oaddrstack x_13097 -> h_Oaddrstack x_13097
     109let rec constant_rect_Type5 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_8170 = function
     110| Ointconst (sz, sg, x_8172) -> h_Ointconst sz sg x_8172
     111| Oaddrsymbol (x_8174, x_8173) -> h_Oaddrsymbol x_8174 x_8173
     112| Oaddrstack x_8175 -> h_Oaddrstack x_8175
    113113
    114114(** val constant_rect_Type3 :
    115115    (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
    116116    Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
    117 let rec constant_rect_Type3 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13101 = function
    118 | Ointconst (sz, sg, x_13103) -> h_Ointconst sz sg x_13103
    119 | Oaddrsymbol (x_13105, x_13104) -> h_Oaddrsymbol x_13105 x_13104
    120 | Oaddrstack x_13106 -> h_Oaddrstack x_13106
     117let rec constant_rect_Type3 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_8179 = function
     118| Ointconst (sz, sg, x_8181) -> h_Ointconst sz sg x_8181
     119| Oaddrsymbol (x_8183, x_8182) -> h_Oaddrsymbol x_8183 x_8182
     120| Oaddrstack x_8184 -> h_Oaddrstack x_8184
    121121
    122122(** val constant_rect_Type2 :
    123123    (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
    124124    Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
    125 let rec constant_rect_Type2 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13110 = function
    126 | Ointconst (sz, sg, x_13112) -> h_Ointconst sz sg x_13112
    127 | Oaddrsymbol (x_13114, x_13113) -> h_Oaddrsymbol x_13114 x_13113
    128 | Oaddrstack x_13115 -> h_Oaddrstack x_13115
     125let rec constant_rect_Type2 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_8188 = function
     126| Ointconst (sz, sg, x_8190) -> h_Ointconst sz sg x_8190
     127| Oaddrsymbol (x_8192, x_8191) -> h_Oaddrsymbol x_8192 x_8191
     128| Oaddrstack x_8193 -> h_Oaddrstack x_8193
    129129
    130130(** val constant_rect_Type1 :
    131131    (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
    132132    Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
    133 let rec constant_rect_Type1 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13119 = function
    134 | Ointconst (sz, sg, x_13121) -> h_Ointconst sz sg x_13121
    135 | Oaddrsymbol (x_13123, x_13122) -> h_Oaddrsymbol x_13123 x_13122
    136 | Oaddrstack x_13124 -> h_Oaddrstack x_13124
     133let rec constant_rect_Type1 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_8197 = function
     134| Ointconst (sz, sg, x_8199) -> h_Ointconst sz sg x_8199
     135| Oaddrsymbol (x_8201, x_8200) -> h_Oaddrsymbol x_8201 x_8200
     136| Oaddrstack x_8202 -> h_Oaddrstack x_8202
    137137
    138138(** val constant_rect_Type0 :
    139139    (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
    140140    Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
    141 let rec constant_rect_Type0 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13128 = function
    142 | Ointconst (sz, sg, x_13130) -> h_Ointconst sz sg x_13130
    143 | Oaddrsymbol (x_13132, x_13131) -> h_Oaddrsymbol x_13132 x_13131
    144 | Oaddrstack x_13133 -> h_Oaddrstack x_13133
     141let rec constant_rect_Type0 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_8206 = function
     142| Ointconst (sz, sg, x_8208) -> h_Ointconst sz sg x_8208
     143| Oaddrsymbol (x_8210, x_8209) -> h_Oaddrsymbol x_8210 x_8209
     144| Oaddrstack x_8211 -> h_Oaddrstack x_8211
    145145
    146146(** val constant_inv_rect_Type4 :
     
    211211    (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
    212212    unary_operation -> 'a1 **)
    213 let rec unary_operation_rect_Type4 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13203 x_13202 = function
     213let rec unary_operation_rect_Type4 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_8281 x_8280 = function
    214214| Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
    215215| Onegint (sz, sg) -> h_Onegint sz sg
     
    227227    (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
    228228    unary_operation -> 'a1 **)
    229 let rec unary_operation_rect_Type5 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13214 x_13213 = function
     229let rec unary_operation_rect_Type5 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_8292 x_8291 = function
    230230| Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
    231231| Onegint (sz, sg) -> h_Onegint sz sg
     
    243243    (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
    244244    unary_operation -> 'a1 **)
    245 let rec unary_operation_rect_Type3 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13225 x_13224 = function
     245let rec unary_operation_rect_Type3 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_8303 x_8302 = function
    246246| Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
    247247| Onegint (sz, sg) -> h_Onegint sz sg
     
    259259    (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
    260260    unary_operation -> 'a1 **)
    261 let rec unary_operation_rect_Type2 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13236 x_13235 = function
     261let rec unary_operation_rect_Type2 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_8314 x_8313 = function
    262262| Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
    263263| Onegint (sz, sg) -> h_Onegint sz sg
     
    275275    (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
    276276    unary_operation -> 'a1 **)
    277 let rec unary_operation_rect_Type1 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13247 x_13246 = function
     277let rec unary_operation_rect_Type1 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_8325 x_8324 = function
    278278| Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
    279279| Onegint (sz, sg) -> h_Onegint sz sg
     
    291291    (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
    292292    unary_operation -> 'a1 **)
    293 let rec unary_operation_rect_Type0 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13258 x_13257 = function
     293let rec unary_operation_rect_Type0 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_8336 x_8335 = function
    294294| Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
    295295| Onegint (sz, sg) -> h_Onegint sz sg
     
    426426    (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
    427427    AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
    428 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_13363 x_13362 x_13361 = function
     428let 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_8441 x_8440 x_8439 = function
    429429| Oadd (sz, sg) -> h_Oadd sz sg
    430430| Osub (sz, sg) -> h_Osub sz sg
     
    440440| Oshr (sz, sg) -> h_Oshr sz sg
    441441| Oshru (sz, sg) -> h_Oshru sz sg
    442 | Ocmp (sz, sg, sg', x_13365) -> h_Ocmp sz sg sg' x_13365
    443 | Ocmpu (sz, sg', x_13366) -> h_Ocmpu sz sg' x_13366
     442| Ocmp (sz, sg, sg', x_8443) -> h_Ocmp sz sg sg' x_8443
     443| Ocmpu (sz, sg', x_8444) -> h_Ocmpu sz sg' x_8444
    444444| Oaddpi sz -> h_Oaddpi sz
    445445| Oaddip sz -> h_Oaddip sz
    446446| Osubpi sz -> h_Osubpi sz
    447447| Osubpp sz -> h_Osubpp sz
    448 | Ocmpp (sg', x_13367) -> h_Ocmpp sg' x_13367
     448| Ocmpp (sg', x_8445) -> h_Ocmpp sg' x_8445
    449449
    450450(** val binary_operation_rect_Type5 :
     
    461461    (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
    462462    AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
    463 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_13390 x_13389 x_13388 = function
     463let 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_8468 x_8467 x_8466 = function
    464464| Oadd (sz, sg) -> h_Oadd sz sg
    465465| Osub (sz, sg) -> h_Osub sz sg
     
    475475| Oshr (sz, sg) -> h_Oshr sz sg
    476476| Oshru (sz, sg) -> h_Oshru sz sg
    477 | Ocmp (sz, sg, sg', x_13392) -> h_Ocmp sz sg sg' x_13392
    478 | Ocmpu (sz, sg', x_13393) -> h_Ocmpu sz sg' x_13393
     477| Ocmp (sz, sg, sg', x_8470) -> h_Ocmp sz sg sg' x_8470
     478| Ocmpu (sz, sg', x_8471) -> h_Ocmpu sz sg' x_8471
    479479| Oaddpi sz -> h_Oaddpi sz
    480480| Oaddip sz -> h_Oaddip sz
    481481| Osubpi sz -> h_Osubpi sz
    482482| Osubpp sz -> h_Osubpp sz
    483 | Ocmpp (sg', x_13394) -> h_Ocmpp sg' x_13394
     483| Ocmpp (sg', x_8472) -> h_Ocmpp sg' x_8472
    484484
    485485(** val binary_operation_rect_Type3 :
     
    496496    (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
    497497    AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
    498 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_13417 x_13416 x_13415 = function
     498let 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_8495 x_8494 x_8493 = function
    499499| Oadd (sz, sg) -> h_Oadd sz sg
    500500| Osub (sz, sg) -> h_Osub sz sg
     
    510510| Oshr (sz, sg) -> h_Oshr sz sg
    511511| Oshru (sz, sg) -> h_Oshru sz sg
    512 | Ocmp (sz, sg, sg', x_13419) -> h_Ocmp sz sg sg' x_13419
    513 | Ocmpu (sz, sg', x_13420) -> h_Ocmpu sz sg' x_13420
     512| Ocmp (sz, sg, sg', x_8497) -> h_Ocmp sz sg sg' x_8497
     513| Ocmpu (sz, sg', x_8498) -> h_Ocmpu sz sg' x_8498
    514514| Oaddpi sz -> h_Oaddpi sz
    515515| Oaddip sz -> h_Oaddip sz
    516516| Osubpi sz -> h_Osubpi sz
    517517| Osubpp sz -> h_Osubpp sz
    518 | Ocmpp (sg', x_13421) -> h_Ocmpp sg' x_13421
     518| Ocmpp (sg', x_8499) -> h_Ocmpp sg' x_8499
    519519
    520520(** val binary_operation_rect_Type2 :
     
    531531    (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
    532532    AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
    533 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_13444 x_13443 x_13442 = function
     533let 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_8522 x_8521 x_8520 = function
    534534| Oadd (sz, sg) -> h_Oadd sz sg
    535535| Osub (sz, sg) -> h_Osub sz sg
     
    545545| Oshr (sz, sg) -> h_Oshr sz sg
    546546| Oshru (sz, sg) -> h_Oshru sz sg
    547 | Ocmp (sz, sg, sg', x_13446) -> h_Ocmp sz sg sg' x_13446
    548 | Ocmpu (sz, sg', x_13447) -> h_Ocmpu sz sg' x_13447
     547| Ocmp (sz, sg, sg', x_8524) -> h_Ocmp sz sg sg' x_8524
     548| Ocmpu (sz, sg', x_8525) -> h_Ocmpu sz sg' x_8525
    549549| Oaddpi sz -> h_Oaddpi sz
    550550| Oaddip sz -> h_Oaddip sz
    551551| Osubpi sz -> h_Osubpi sz
    552552| Osubpp sz -> h_Osubpp sz
    553 | Ocmpp (sg', x_13448) -> h_Ocmpp sg' x_13448
     553| Ocmpp (sg', x_8526) -> h_Ocmpp sg' x_8526
    554554
    555555(** val binary_operation_rect_Type1 :
     
    566566    (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
    567567    AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
    568 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_13471 x_13470 x_13469 = function
     568let 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_8549 x_8548 x_8547 = function
    569569| Oadd (sz, sg) -> h_Oadd sz sg
    570570| Osub (sz, sg) -> h_Osub sz sg
     
    580580| Oshr (sz, sg) -> h_Oshr sz sg
    581581| Oshru (sz, sg) -> h_Oshru sz sg
    582 | Ocmp (sz, sg, sg', x_13473) -> h_Ocmp sz sg sg' x_13473
    583 | Ocmpu (sz, sg', x_13474) -> h_Ocmpu sz sg' x_13474
     582| Ocmp (sz, sg, sg', x_8551) -> h_Ocmp sz sg sg' x_8551
     583| Ocmpu (sz, sg', x_8552) -> h_Ocmpu sz sg' x_8552
    584584| Oaddpi sz -> h_Oaddpi sz
    585585| Oaddip sz -> h_Oaddip sz
    586586| Osubpi sz -> h_Osubpi sz
    587587| Osubpp sz -> h_Osubpp sz
    588 | Ocmpp (sg', x_13475) -> h_Ocmpp sg' x_13475
     588| Ocmpp (sg', x_8553) -> h_Ocmpp sg' x_8553
    589589
    590590(** val binary_operation_rect_Type0 :
     
    601601    (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
    602602    AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
    603 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_13498 x_13497 x_13496 = function
     603let 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_8576 x_8575 x_8574 = function
    604604| Oadd (sz, sg) -> h_Oadd sz sg
    605605| Osub (sz, sg) -> h_Osub sz sg
     
    615615| Oshr (sz, sg) -> h_Oshr sz sg
    616616| Oshru (sz, sg) -> h_Oshru sz sg
    617 | Ocmp (sz, sg, sg', x_13500) -> h_Ocmp sz sg sg' x_13500
    618 | Ocmpu (sz, sg', x_13501) -> h_Ocmpu sz sg' x_13501
     617| Ocmp (sz, sg, sg', x_8578) -> h_Ocmp sz sg sg' x_8578
     618| Ocmpu (sz, sg', x_8579) -> h_Ocmpu sz sg' x_8579
    619619| Oaddpi sz -> h_Oaddpi sz
    620620| Oaddip sz -> h_Oaddip sz
    621621| Osubpi sz -> h_Osubpi sz
    622622| Osubpp sz -> h_Osubpp sz
    623 | Ocmpp (sg', x_13502) -> h_Ocmpp sg' x_13502
     623| Ocmpp (sg', x_8580) -> h_Ocmpp sg' x_8580
    624624
    625625(** val binary_operation_inv_rect_Type4 :
     
    823823     Types.Some (Values.Vptr { Pointers.pblock = b; Pointers.poff =
    824824       (Pointers.shift_offset (AST.bitsize_of_intsize AST.I16)
    825          Pointers.zero_offset (AST.repr0 AST.I16 ofs)) }))
     825         Pointers.zero_offset (AST.repr AST.I16 ofs)) }))
    826826| Oaddrstack ofs ->
    827827  Types.Some (Values.Vptr { Pointers.pblock = sp; Pointers.poff =
    828828    (Pointers.shift_offset (AST.bitsize_of_intsize AST.I16)
    829       Pointers.zero_offset (AST.repr0 AST.I16 ofs)) })
     829      Pointers.zero_offset (AST.repr AST.I16 ofs)) })
    830830
    831831(** val eval_unop :
    832832    AST.typ -> AST.typ -> unary_operation -> Values.val0 -> Values.val0
    833833    Types.option **)
    834 let eval_unop t t' op0 arg =
    835   match op0 with
     834let eval_unop t t' op arg =
     835  match op with
    836836  | Ocastint (sz, sg, sz', sg') ->
    837837    (match sg with
    838      | AST.Signed -> Types.Some (Values.sign_ext1 sz' arg)
    839      | AST.Unsigned -> Types.Some (Values.zero_ext1 sz' arg))
     838     | AST.Signed -> Types.Some (Values.sign_ext sz' arg)
     839     | AST.Unsigned -> Types.Some (Values.zero_ext sz' arg))
    840840  | Onegint (sz, sg) ->
    841841    (match arg with
     
    853853         (match BitVector.eq_bv (AST.bitsize_of_intsize sz1) n1
    854854                  (BitVector.zero (AST.bitsize_of_intsize sz1)) with
    855           | Bool.True -> AST.repr0 sz (Nat.S Nat.O)
     855          | Bool.True -> AST.repr sz (Nat.S Nat.O)
    856856          | Bool.False -> BitVector.zero (AST.bitsize_of_intsize sz))))
    857857     | Values.Vnull ->
    858        Types.Some (Values.Vint (sz, (AST.repr0 sz (Nat.S Nat.O))))
     858       Types.Some (Values.Vint (sz, (AST.repr sz (Nat.S Nat.O))))
    859859     | Values.Vptr x0 ->
    860860       Types.Some (Values.Vint (sz,
     
    866866       Types.Some (Values.Vint (sz1,
    867867         (BitVector.exclusive_disjunction_bv (AST.bitsize_of_intsize sz1) n1
    868            (Values.mone0 sz1))))
     868           (Values.mone sz1))))
    869869     | Values.Vnull -> Types.None
    870870     | Values.Vptr x -> Types.None)
     
    12321232(** val fEtrue : Values.val0 **)
    12331233let fEtrue =
    1234   Values.Vint (AST.I8, (AST.repr0 AST.I8 (Nat.S Nat.O)))
     1234  Values.Vint (AST.I8, (AST.repr AST.I8 (Nat.S Nat.O)))
    12351235
    12361236(** val fEfalse : Values.val0 **)
    12371237let fEfalse =
    1238   Values.Vint (AST.I8, (AST.repr0 AST.I8 Nat.O))
     1238  Values.Vint (AST.I8, (AST.repr AST.I8 Nat.O))
    12391239
    12401240(** val fE_of_bool : Bool.bool -> Values.val0 **)
     
    12801280
    12811281(** val ev_cmpp :
    1282     GenMem.mem1 -> Integers.comparison -> Values.val0 -> Values.val0 ->
     1282    GenMem.mem -> Integers.comparison -> Values.val0 -> Values.val0 ->
    12831283    Values.val0 Types.option **)
    12841284let ev_cmpp m c v1 v2 =
     
    13281328
    13291329(** val eval_binop :
    1330     GenMem.mem1 -> AST.typ -> AST.typ -> AST.typ -> binary_operation ->
     1330    GenMem.mem -> AST.typ -> AST.typ -> AST.typ -> binary_operation ->
    13311331    Values.val0 -> Values.val0 -> Values.val0 Types.option **)
    13321332let eval_binop m t1 t2 t' = function
Note: See TracChangeset for help on using the changeset viewer.