Changeset 2797 for extracted/events.ml


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

    r2775 r2797  
    8989    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
    9090let rec eventval_rect_Type4 h_EVint = function
    91 | EVint (sz, x_5394) -> h_EVint sz x_5394
     91| EVint (sz, x_5407) -> h_EVint sz x_5407
    9292
    9393(** val eventval_rect_Type5 :
    9494    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
    9595let rec eventval_rect_Type5 h_EVint = function
    96 | EVint (sz, x_5397) -> h_EVint sz x_5397
     96| EVint (sz, x_5410) -> h_EVint sz x_5410
    9797
    9898(** val eventval_rect_Type3 :
    9999    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
    100100let rec eventval_rect_Type3 h_EVint = function
    101 | EVint (sz, x_5400) -> h_EVint sz x_5400
     101| EVint (sz, x_5413) -> h_EVint sz x_5413
    102102
    103103(** val eventval_rect_Type2 :
    104104    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
    105105let rec eventval_rect_Type2 h_EVint = function
    106 | EVint (sz, x_5403) -> h_EVint sz x_5403
     106| EVint (sz, x_5416) -> h_EVint sz x_5416
    107107
    108108(** val eventval_rect_Type1 :
    109109    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
    110110let rec eventval_rect_Type1 h_EVint = function
    111 | EVint (sz, x_5406) -> h_EVint sz x_5406
     111| EVint (sz, x_5419) -> h_EVint sz x_5419
    112112
    113113(** val eventval_rect_Type0 :
    114114    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
    115115let rec eventval_rect_Type0 h_EVint = function
    116 | EVint (sz, x_5409) -> h_EVint sz x_5409
     116| EVint (sz, x_5422) -> h_EVint sz x_5422
    117117
    118118(** val eventval_inv_rect_Type4 :
     
    159159    eventval -> 'a1) -> event -> 'a1 **)
    160160let rec event_rect_Type4 h_EVcost h_EVextcall = function
    161 | EVcost x_5434 -> h_EVcost x_5434
     161| EVcost x_5447 -> h_EVcost x_5447
    162162| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
    163163
     
    166166    eventval -> 'a1) -> event -> 'a1 **)
    167167let rec event_rect_Type5 h_EVcost h_EVextcall = function
    168 | EVcost x_5438 -> h_EVcost x_5438
     168| EVcost x_5451 -> h_EVcost x_5451
    169169| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
    170170
     
    173173    eventval -> 'a1) -> event -> 'a1 **)
    174174let rec event_rect_Type3 h_EVcost h_EVextcall = function
    175 | EVcost x_5442 -> h_EVcost x_5442
     175| EVcost x_5455 -> h_EVcost x_5455
    176176| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
    177177
     
    180180    eventval -> 'a1) -> event -> 'a1 **)
    181181let rec event_rect_Type2 h_EVcost h_EVextcall = function
    182 | EVcost x_5446 -> h_EVcost x_5446
     182| EVcost x_5459 -> h_EVcost x_5459
    183183| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
    184184
     
    187187    eventval -> 'a1) -> event -> 'a1 **)
    188188let rec event_rect_Type1 h_EVcost h_EVextcall = function
    189 | EVcost x_5450 -> h_EVcost x_5450
     189| EVcost x_5463 -> h_EVcost x_5463
    190190| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
    191191
     
    194194    eventval -> 'a1) -> event -> 'a1 **)
    195195let rec event_rect_Type0 h_EVcost h_EVextcall = function
    196 | EVcost x_5454 -> h_EVcost x_5454
     196| EVcost x_5467 -> h_EVcost x_5467
    197197| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
    198198
Note: See TracChangeset for help on using the changeset viewer.