Changeset 2967
- Timestamp:
- Mar 26, 2013, 6:54:12 PM (5 years ago)
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
extracted/traces.ml
r2960 r2967 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_ 55=160 let { globals = globals0; ev_genv = ev_genv0 } = x_ 55in159 let rec evaluation_params_rect_Type4 p h_mk_evaluation_params x_3 = 160 let { globals = globals0; ev_genv = ev_genv0 } = x_3 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_5 7=167 let { globals = globals0; ev_genv = ev_genv0 } = x_5 7in166 let rec evaluation_params_rect_Type5 p h_mk_evaluation_params x_5 = 167 let { globals = globals0; ev_genv = ev_genv0 } = x_5 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_ 59=174 let { globals = globals0; ev_genv = ev_genv0 } = x_ 59in173 let rec evaluation_params_rect_Type3 p h_mk_evaluation_params x_7 = 174 let { globals = globals0; ev_genv = ev_genv0 } = x_7 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_ 61=181 let { globals = globals0; ev_genv = ev_genv0 } = x_ 61in180 let rec evaluation_params_rect_Type2 p h_mk_evaluation_params x_9 = 181 let { globals = globals0; ev_genv = ev_genv0 } = x_9 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_ 63=188 let { globals = globals0; ev_genv = ev_genv0 } = x_ 63in187 let rec evaluation_params_rect_Type1 p h_mk_evaluation_params x_11 = 188 let { globals = globals0; ev_genv = ev_genv0 } = x_11 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_ 65=195 let { globals = globals0; ev_genv = ev_genv0 } = x_ 65in194 let rec evaluation_params_rect_Type0 p h_mk_evaluation_params x_13 = 195 let { globals = globals0; ev_genv = ev_genv0 } = x_13 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_ 81=338 let rec prog_params_rect_Type4 h_mk_prog_params x_29 = 339 339 let { prog_spars = prog_spars0; prog = prog0; stack_sizes = 340 stack_sizes0 } = x_ 81340 stack_sizes0 } = x_29 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_ 83=347 let rec prog_params_rect_Type5 h_mk_prog_params x_31 = 348 348 let { prog_spars = prog_spars0; prog = prog0; stack_sizes = 349 stack_sizes0 } = x_ 83349 stack_sizes0 } = x_31 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_ 85=356 let rec prog_params_rect_Type3 h_mk_prog_params x_33 = 357 357 let { prog_spars = prog_spars0; prog = prog0; stack_sizes = 358 stack_sizes0 } = x_ 85358 stack_sizes0 } = x_33 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_ 87=365 let rec prog_params_rect_Type2 h_mk_prog_params x_35 = 366 366 let { prog_spars = prog_spars0; prog = prog0; stack_sizes = 367 stack_sizes0 } = x_ 87367 stack_sizes0 } = x_35 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_ 89=374 let rec prog_params_rect_Type1 h_mk_prog_params x_37 = 375 375 let { prog_spars = prog_spars0; prog = prog0; stack_sizes = 376 stack_sizes0 } = x_ 89376 stack_sizes0 } = x_37 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_ 91=383 let rec prog_params_rect_Type0 h_mk_prog_params x_39 = 384 384 let { prog_spars = prog_spars0; prog = prog0; stack_sizes = 385 stack_sizes0 } = x_ 91385 stack_sizes0 } = x_39 386 386 in 387 387 h_mk_prog_params prog_spars0 prog0 stack_sizes0 … … 674 674 (Joint_semantics.spp'__o__msu_pars p).Joint_semantics.call_dest_for_main 675 675 in 676 Errors.res_to_opt 677 (Obj.magic 678 (Monad.m_bind0 (Monad.max_def Errors.res0) 679 (Obj.magic 680 (p.Joint_semantics.spp'.Joint_semantics.msu_pars.Joint_semantics.read_result 681 pars.globals 682 (let p0 = Joint_semantics.spp'__o__spp p in 683 let globals0 = pars.globals in 684 let g = ge in g.Joint_semantics.ge) ret 685 st.Joint_semantics.st_no_pc)) (fun vals -> 686 Obj.magic (ByteValues.word_of_list_beval vals)))) 676 (match Obj.magic 677 (Monad.m_bind0 (Monad.max_def Errors.res0) 678 (Obj.magic 679 (p.Joint_semantics.spp'.Joint_semantics.msu_pars.Joint_semantics.read_result 680 pars.globals 681 (let p0 = Joint_semantics.spp'__o__spp p in 682 let globals0 = pars.globals in 683 let g = ge in g.Joint_semantics.ge) ret 684 st.Joint_semantics.st_no_pc)) (fun vals -> 685 Obj.magic (ByteValues.word_of_list_beval vals))) with 686 | Errors.OK v -> Types.Some v 687 | Errors.Error x -> Types.Some (BitVector.maximum Integers.wordsize)) 687 688 | Bool.False -> Types.None) 688 689 -
src/joint/Traces.ma
r2952 r2967 235 235 if eq_program_counter (pc … st) exit_pc' then 236 236 let ret ≝ call_dest_for_main ?? p in 237 res_to_opt …(! vals ← read_result … ge ret st ;237 match (! vals ← read_result … ge ret st ; 238 238 Word_of_list_beval vals) 239 with 240 [ OK v ⇒ Some ? v 241 | Error _ ⇒ Some … (maximum ?) ] 239 242 else None ?. 240 243
Note: See TracChangeset
for help on using the changeset viewer.