Changeset 3019 for extracted/traces.ml
 Timestamp:
 Mar 28, 2013, 5:27:46 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/traces.ml
r3001 r3019 157 157 Joint_semantics.sem_params > (AST.ident List.list > 158 158 Joint_semantics.genv > 'a1) > evaluation_params > 'a1 **) 159 let rec evaluation_params_rect_Type4 p h_mk_evaluation_params x_ 15969=160 let { globals = globals0; ev_genv = ev_genv0 } = x_ 15969in159 let rec evaluation_params_rect_Type4 p h_mk_evaluation_params x_316 = 160 let { globals = globals0; ev_genv = ev_genv0 } = x_316 in 161 161 h_mk_evaluation_params globals0 ev_genv0 162 162 … … 164 164 Joint_semantics.sem_params > (AST.ident List.list > 165 165 Joint_semantics.genv > 'a1) > evaluation_params > 'a1 **) 166 let rec evaluation_params_rect_Type5 p h_mk_evaluation_params x_ 15971=167 let { globals = globals0; ev_genv = ev_genv0 } = x_ 15971in166 let rec evaluation_params_rect_Type5 p h_mk_evaluation_params x_318 = 167 let { globals = globals0; ev_genv = ev_genv0 } = x_318 in 168 168 h_mk_evaluation_params globals0 ev_genv0 169 169 … … 171 171 Joint_semantics.sem_params > (AST.ident List.list > 172 172 Joint_semantics.genv > 'a1) > evaluation_params > 'a1 **) 173 let rec evaluation_params_rect_Type3 p h_mk_evaluation_params x_ 15973=174 let { globals = globals0; ev_genv = ev_genv0 } = x_ 15973in173 let rec evaluation_params_rect_Type3 p h_mk_evaluation_params x_320 = 174 let { globals = globals0; ev_genv = ev_genv0 } = x_320 in 175 175 h_mk_evaluation_params globals0 ev_genv0 176 176 … … 178 178 Joint_semantics.sem_params > (AST.ident List.list > 179 179 Joint_semantics.genv > 'a1) > evaluation_params > 'a1 **) 180 let rec evaluation_params_rect_Type2 p h_mk_evaluation_params x_ 15975=181 let { globals = globals0; ev_genv = ev_genv0 } = x_ 15975in180 let rec evaluation_params_rect_Type2 p h_mk_evaluation_params x_322 = 181 let { globals = globals0; ev_genv = ev_genv0 } = x_322 in 182 182 h_mk_evaluation_params globals0 ev_genv0 183 183 … … 185 185 Joint_semantics.sem_params > (AST.ident List.list > 186 186 Joint_semantics.genv > 'a1) > evaluation_params > 'a1 **) 187 let rec evaluation_params_rect_Type1 p h_mk_evaluation_params x_ 15977=188 let { globals = globals0; ev_genv = ev_genv0 } = x_ 15977in187 let rec evaluation_params_rect_Type1 p h_mk_evaluation_params x_324 = 188 let { globals = globals0; ev_genv = ev_genv0 } = x_324 in 189 189 h_mk_evaluation_params globals0 ev_genv0 190 190 … … 192 192 Joint_semantics.sem_params > (AST.ident List.list > 193 193 Joint_semantics.genv > 'a1) > evaluation_params > 'a1 **) 194 let rec evaluation_params_rect_Type0 p h_mk_evaluation_params x_ 15979=195 let { globals = globals0; ev_genv = ev_genv0 } = x_ 15979in194 let rec evaluation_params_rect_Type0 p h_mk_evaluation_params x_326 = 195 let { globals = globals0; ev_genv = ev_genv0 } = x_326 in 196 196 h_mk_evaluation_params globals0 ev_genv0 197 197 … … 336 336 (Joint_semantics.sem_params > Joint.joint_program > (AST.ident > 337 337 Nat.nat Types.option) > 'a1) > prog_params > 'a1 **) 338 let rec prog_params_rect_Type4 h_mk_prog_params x_ 15995=338 let rec prog_params_rect_Type4 h_mk_prog_params x_342 = 339 339 let { prog_spars = prog_spars0; prog = prog0; stack_sizes = 340 stack_sizes0 } = x_ 15995340 stack_sizes0 } = x_342 341 341 in 342 342 h_mk_prog_params prog_spars0 prog0 stack_sizes0 … … 345 345 (Joint_semantics.sem_params > Joint.joint_program > (AST.ident > 346 346 Nat.nat Types.option) > 'a1) > prog_params > 'a1 **) 347 let rec prog_params_rect_Type5 h_mk_prog_params x_ 15997=347 let rec prog_params_rect_Type5 h_mk_prog_params x_344 = 348 348 let { prog_spars = prog_spars0; prog = prog0; stack_sizes = 349 stack_sizes0 } = x_ 15997349 stack_sizes0 } = x_344 350 350 in 351 351 h_mk_prog_params prog_spars0 prog0 stack_sizes0 … … 354 354 (Joint_semantics.sem_params > Joint.joint_program > (AST.ident > 355 355 Nat.nat Types.option) > 'a1) > prog_params > 'a1 **) 356 let rec prog_params_rect_Type3 h_mk_prog_params x_ 15999=356 let rec prog_params_rect_Type3 h_mk_prog_params x_346 = 357 357 let { prog_spars = prog_spars0; prog = prog0; stack_sizes = 358 stack_sizes0 } = x_ 15999358 stack_sizes0 } = x_346 359 359 in 360 360 h_mk_prog_params prog_spars0 prog0 stack_sizes0 … … 363 363 (Joint_semantics.sem_params > Joint.joint_program > (AST.ident > 364 364 Nat.nat Types.option) > 'a1) > prog_params > 'a1 **) 365 let rec prog_params_rect_Type2 h_mk_prog_params x_ 16001=365 let rec prog_params_rect_Type2 h_mk_prog_params x_348 = 366 366 let { prog_spars = prog_spars0; prog = prog0; stack_sizes = 367 stack_sizes0 } = x_ 16001367 stack_sizes0 } = x_348 368 368 in 369 369 h_mk_prog_params prog_spars0 prog0 stack_sizes0 … … 372 372 (Joint_semantics.sem_params > Joint.joint_program > (AST.ident > 373 373 Nat.nat Types.option) > 'a1) > prog_params > 'a1 **) 374 let rec prog_params_rect_Type1 h_mk_prog_params x_ 16003=374 let rec prog_params_rect_Type1 h_mk_prog_params x_350 = 375 375 let { prog_spars = prog_spars0; prog = prog0; stack_sizes = 376 stack_sizes0 } = x_ 16003376 stack_sizes0 } = x_350 377 377 in 378 378 h_mk_prog_params prog_spars0 prog0 stack_sizes0 … … 381 381 (Joint_semantics.sem_params > Joint.joint_program > (AST.ident > 382 382 Nat.nat Types.option) > 'a1) > prog_params > 'a1 **) 383 let rec prog_params_rect_Type0 h_mk_prog_params x_ 16005=383 let rec prog_params_rect_Type0 h_mk_prog_params x_352 = 384 384 let { prog_spars = prog_spars0; prog = prog0; stack_sizes = 385 stack_sizes0 } = x_ 16005385 stack_sizes0 } = x_352 386 386 in 387 387 h_mk_prog_params prog_spars0 prog0 stack_sizes0 … … 523 523 (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 524 524 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 525 (Nat.S Nat.O)))))))))))))))) (Z.zopp (Z.z_of_nat globals_size))) } 525 (Nat.S Nat.O)))))))))))))))) 526 (Z.zopp (Z.z_of_nat (Nat.S globals_size)))) } 526 527 in 527 528 let main = AST.prog_main p.Joint.joint_prog in
Note: See TracChangeset
for help on using the changeset viewer.