Changeset 2773 for extracted/events.ml
 Timestamp:
 Mar 4, 2013, 10:03:33 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/events.ml
r2743 r2773 80 80 81 81 open Values 82 83 open BitVectorTrie84 82 85 83 open CostLabel … … 91 89 (AST.intsize > AST.bvint > 'a1) > eventval > 'a1 **) 92 90 let rec eventval_rect_Type4 h_EVint = function 93  EVint (sz, x_ 5485) > h_EVint sz x_548591  EVint (sz, x_993) > h_EVint sz x_993 94 92 95 93 (** val eventval_rect_Type5 : 96 94 (AST.intsize > AST.bvint > 'a1) > eventval > 'a1 **) 97 95 let rec eventval_rect_Type5 h_EVint = function 98  EVint (sz, x_ 5488) > h_EVint sz x_548896  EVint (sz, x_996) > h_EVint sz x_996 99 97 100 98 (** val eventval_rect_Type3 : 101 99 (AST.intsize > AST.bvint > 'a1) > eventval > 'a1 **) 102 100 let rec eventval_rect_Type3 h_EVint = function 103  EVint (sz, x_ 5491) > h_EVint sz x_5491101  EVint (sz, x_999) > h_EVint sz x_999 104 102 105 103 (** val eventval_rect_Type2 : 106 104 (AST.intsize > AST.bvint > 'a1) > eventval > 'a1 **) 107 105 let rec eventval_rect_Type2 h_EVint = function 108  EVint (sz, x_ 5494) > h_EVint sz x_5494106  EVint (sz, x_1002) > h_EVint sz x_1002 109 107 110 108 (** val eventval_rect_Type1 : 111 109 (AST.intsize > AST.bvint > 'a1) > eventval > 'a1 **) 112 110 let rec eventval_rect_Type1 h_EVint = function 113  EVint (sz, x_ 5497) > h_EVint sz x_5497111  EVint (sz, x_1005) > h_EVint sz x_1005 114 112 115 113 (** val eventval_rect_Type0 : 116 114 (AST.intsize > AST.bvint > 'a1) > eventval > 'a1 **) 117 115 let rec eventval_rect_Type0 h_EVint = function 118  EVint (sz, x_ 5500) > h_EVint sz x_5500116  EVint (sz, x_1008) > h_EVint sz x_1008 119 117 120 118 (** val eventval_inv_rect_Type4 : … … 161 159 eventval > 'a1) > event > 'a1 **) 162 160 let rec event_rect_Type4 h_EVcost h_EVextcall = function 163  EVcost x_ 5525 > h_EVcost x_5525161  EVcost x_1033 > h_EVcost x_1033 164 162  EVextcall (ev_name, ev_args, ev_res) > h_EVextcall ev_name ev_args ev_res 165 163 … … 168 166 eventval > 'a1) > event > 'a1 **) 169 167 let rec event_rect_Type5 h_EVcost h_EVextcall = function 170  EVcost x_ 5529 > h_EVcost x_5529168  EVcost x_1037 > h_EVcost x_1037 171 169  EVextcall (ev_name, ev_args, ev_res) > h_EVextcall ev_name ev_args ev_res 172 170 … … 175 173 eventval > 'a1) > event > 'a1 **) 176 174 let rec event_rect_Type3 h_EVcost h_EVextcall = function 177  EVcost x_ 5533 > h_EVcost x_5533175  EVcost x_1041 > h_EVcost x_1041 178 176  EVextcall (ev_name, ev_args, ev_res) > h_EVextcall ev_name ev_args ev_res 179 177 … … 182 180 eventval > 'a1) > event > 'a1 **) 183 181 let rec event_rect_Type2 h_EVcost h_EVextcall = function 184  EVcost x_ 5537 > h_EVcost x_5537182  EVcost x_1045 > h_EVcost x_1045 185 183  EVextcall (ev_name, ev_args, ev_res) > h_EVextcall ev_name ev_args ev_res 186 184 … … 189 187 eventval > 'a1) > event > 'a1 **) 190 188 let rec event_rect_Type1 h_EVcost h_EVextcall = function 191  EVcost x_ 5541 > h_EVcost x_5541189  EVcost x_1049 > h_EVcost x_1049 192 190  EVextcall (ev_name, ev_args, ev_res) > h_EVextcall ev_name ev_args ev_res 193 191 … … 196 194 eventval > 'a1) > event > 'a1 **) 197 195 let rec event_rect_Type0 h_EVcost h_EVextcall = function 198  EVcost x_ 5545 > h_EVcost x_5545196  EVcost x_1053 > h_EVcost x_1053 199 197  EVextcall (ev_name, ev_args, ev_res) > h_EVextcall ev_name ev_args ev_res 200 198 … … 254 252 255 253 (** val eextcall : AST.ident > eventval List.list > eventval > trace **) 256 let eextcall name args res 1=257 List.Cons ((EVextcall (name, args, res 1)), List.Nil)254 let eextcall name args res = 255 List.Cons ((EVextcall (name, args, res)), List.Nil) 258 256 259 257 (** val eapp : trace > trace > trace **) … … 310 308 (** val remove_costs : trace > trace **) 311 309 let remove_costs = 312 List.filter (fun e 1>313 match e 1with310 List.filter (fun e > 311 match e with 314 312  EVcost x > Bool.False 315 313  EVextcall (x, x0, x1) > Bool.True) … … 366 364 (match t with 367 365  List.Nil > (fun _ > Logic.false_rect_Type0 __) 368  List.Cons (e 1, t') >366  List.Cons (e, t') > 369 367 (fun _ > 370 368 (match t' with 371  List.Nil > (fun _ > { Types.fst = e 1; Types.snd = t0 })369  List.Nil > (fun _ > { Types.fst = e; Types.snd = t0 }) 372 370  List.Cons (e', t'') > 373 (fun _ > { Types.fst = e 1; Types.snd = (lazy (Econsinf' (t',371 (fun _ > { Types.fst = e; Types.snd = (lazy (Econsinf' (t', 374 372 t0))) })) __)) __ 375 373 … … 377 375 let rec traceinf_of_traceinf' t' = 378 376 let Econsinf' (t, t'') = Lazy.force t' in 379 let { Types.fst = e 1; Types.snd = tl } = split_traceinf' t t'' in380 lazy (Econsinf (e 1, (traceinf_of_traceinf' tl)))381 377 let { Types.fst = e; Types.snd = tl } = split_traceinf' t t'' in 378 lazy (Econsinf (e, (traceinf_of_traceinf' tl))) 379
Note: See TracChangeset
for help on using the changeset viewer.