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

    r2775 r2797  
    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_12992 = function
    102 | Ointconst (sz, sg, x_12994) -> h_Ointconst sz sg x_12994
    103 | Oaddrsymbol (x_12996, x_12995) -> h_Oaddrsymbol x_12996 x_12995
    104 | Oaddrstack x_12997 -> h_Oaddrstack x_12997
     101let rec constant_rect_Type4 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13005 = function
     102| Ointconst (sz, sg, x_13007) -> h_Ointconst sz sg x_13007
     103| Oaddrsymbol (x_13009, x_13008) -> h_Oaddrsymbol x_13009 x_13008
     104| Oaddrstack x_13010 -> h_Oaddrstack x_13010
    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_13001 = function
    110 | Ointconst (sz, sg, x_13003) -> h_Ointconst sz sg x_13003
    111 | Oaddrsymbol (x_13005, x_13004) -> h_Oaddrsymbol x_13005 x_13004
    112 | Oaddrstack x_13006 -> h_Oaddrstack x_13006
     109let rec constant_rect_Type5 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13014 = function
     110| Ointconst (sz, sg, x_13016) -> h_Ointconst sz sg x_13016
     111| Oaddrsymbol (x_13018, x_13017) -> h_Oaddrsymbol x_13018 x_13017
     112| Oaddrstack x_13019 -> h_Oaddrstack x_13019
    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_13010 = function
    118 | Ointconst (sz, sg, x_13012) -> h_Ointconst sz sg x_13012
    119 | Oaddrsymbol (x_13014, x_13013) -> h_Oaddrsymbol x_13014 x_13013
    120 | Oaddrstack x_13015 -> h_Oaddrstack x_13015
     117let rec constant_rect_Type3 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13023 = function
     118| Ointconst (sz, sg, x_13025) -> h_Ointconst sz sg x_13025
     119| Oaddrsymbol (x_13027, x_13026) -> h_Oaddrsymbol x_13027 x_13026
     120| Oaddrstack x_13028 -> h_Oaddrstack x_13028
    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_13019 = function
    126 | Ointconst (sz, sg, x_13021) -> h_Ointconst sz sg x_13021
    127 | Oaddrsymbol (x_13023, x_13022) -> h_Oaddrsymbol x_13023 x_13022
    128 | Oaddrstack x_13024 -> h_Oaddrstack x_13024
     125let rec constant_rect_Type2 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13032 = function
     126| Ointconst (sz, sg, x_13034) -> h_Ointconst sz sg x_13034
     127| Oaddrsymbol (x_13036, x_13035) -> h_Oaddrsymbol x_13036 x_13035
     128| Oaddrstack x_13037 -> h_Oaddrstack x_13037
    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_13028 = function
    134 | Ointconst (sz, sg, x_13030) -> h_Ointconst sz sg x_13030
    135 | Oaddrsymbol (x_13032, x_13031) -> h_Oaddrsymbol x_13032 x_13031
    136 | Oaddrstack x_13033 -> h_Oaddrstack x_13033
     133let rec constant_rect_Type1 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13041 = function
     134| Ointconst (sz, sg, x_13043) -> h_Ointconst sz sg x_13043
     135| Oaddrsymbol (x_13045, x_13044) -> h_Oaddrsymbol x_13045 x_13044
     136| Oaddrstack x_13046 -> h_Oaddrstack x_13046
    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_13037 = function
    142 | Ointconst (sz, sg, x_13039) -> h_Ointconst sz sg x_13039
    143 | Oaddrsymbol (x_13041, x_13040) -> h_Oaddrsymbol x_13041 x_13040
    144 | Oaddrstack x_13042 -> h_Oaddrstack x_13042
     141let rec constant_rect_Type0 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13050 = function
     142| Ointconst (sz, sg, x_13052) -> h_Ointconst sz sg x_13052
     143| Oaddrsymbol (x_13054, x_13053) -> h_Oaddrsymbol x_13054 x_13053
     144| Oaddrstack x_13055 -> h_Oaddrstack x_13055
    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_13112 x_13111 = function
     213let rec unary_operation_rect_Type4 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13125 x_13124 = 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_13123 x_13122 = function
     229let rec unary_operation_rect_Type5 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13136 x_13135 = 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_13134 x_13133 = function
     245let rec unary_operation_rect_Type3 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13147 x_13146 = 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_13145 x_13144 = function
     261let rec unary_operation_rect_Type2 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13158 x_13157 = 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_13156 x_13155 = function
     277let rec unary_operation_rect_Type1 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13169 x_13168 = 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_13167 x_13166 = function
     293let rec unary_operation_rect_Type0 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13180 x_13179 = 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_13272 x_13271 x_13270 = 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_13285 x_13284 x_13283 = 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_13274) -> h_Ocmp sz sg sg' x_13274
    443 | Ocmpu (sz, sg', x_13275) -> h_Ocmpu sz sg' x_13275
     442| Ocmp (sz, sg, sg', x_13287) -> h_Ocmp sz sg sg' x_13287
     443| Ocmpu (sz, sg', x_13288) -> h_Ocmpu sz sg' x_13288
    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_13276) -> h_Ocmpp sg' x_13276
     448| Ocmpp (sg', x_13289) -> h_Ocmpp sg' x_13289
    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_13299 x_13298 x_13297 = 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_13312 x_13311 x_13310 = 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_13301) -> h_Ocmp sz sg sg' x_13301
    478 | Ocmpu (sz, sg', x_13302) -> h_Ocmpu sz sg' x_13302
     477| Ocmp (sz, sg, sg', x_13314) -> h_Ocmp sz sg sg' x_13314
     478| Ocmpu (sz, sg', x_13315) -> h_Ocmpu sz sg' x_13315
    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_13303) -> h_Ocmpp sg' x_13303
     483| Ocmpp (sg', x_13316) -> h_Ocmpp sg' x_13316
    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_13326 x_13325 x_13324 = 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_13339 x_13338 x_13337 = 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_13328) -> h_Ocmp sz sg sg' x_13328
    513 | Ocmpu (sz, sg', x_13329) -> h_Ocmpu sz sg' x_13329
     512| Ocmp (sz, sg, sg', x_13341) -> h_Ocmp sz sg sg' x_13341
     513| Ocmpu (sz, sg', x_13342) -> h_Ocmpu sz sg' x_13342
    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_13330) -> h_Ocmpp sg' x_13330
     518| Ocmpp (sg', x_13343) -> h_Ocmpp sg' x_13343
    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_13353 x_13352 x_13351 = 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_13366 x_13365 x_13364 = 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_13355) -> h_Ocmp sz sg sg' x_13355
    548 | Ocmpu (sz, sg', x_13356) -> h_Ocmpu sz sg' x_13356
     547| Ocmp (sz, sg, sg', x_13368) -> h_Ocmp sz sg sg' x_13368
     548| Ocmpu (sz, sg', x_13369) -> h_Ocmpu sz sg' x_13369
    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_13357) -> h_Ocmpp sg' x_13357
     553| Ocmpp (sg', x_13370) -> h_Ocmpp sg' x_13370
    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_13380 x_13379 x_13378 = 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_13393 x_13392 x_13391 = 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_13382) -> h_Ocmp sz sg sg' x_13382
    583 | Ocmpu (sz, sg', x_13383) -> h_Ocmpu sz sg' x_13383
     582| Ocmp (sz, sg, sg', x_13395) -> h_Ocmp sz sg sg' x_13395
     583| Ocmpu (sz, sg', x_13396) -> h_Ocmpu sz sg' x_13396
    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_13384) -> h_Ocmpp sg' x_13384
     588| Ocmpp (sg', x_13397) -> h_Ocmpp sg' x_13397
    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_13407 x_13406 x_13405 = 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_13420 x_13419 x_13418 = 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_13409) -> h_Ocmp sz sg sg' x_13409
    618 | Ocmpu (sz, sg', x_13410) -> h_Ocmpu sz sg' x_13410
     617| Ocmp (sz, sg, sg', x_13422) -> h_Ocmp sz sg sg' x_13422
     618| Ocmpu (sz, sg', x_13423) -> h_Ocmpu sz sg' x_13423
    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_13411) -> h_Ocmpp sg' x_13411
     623| Ocmpp (sg', x_13424) -> h_Ocmpp sg' x_13424
    624624
    625625(** val binary_operation_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.