Changeset 2795
- Timestamp:
- Mar 7, 2013, 9:31:40 AM (8 years ago)
- Location:
- src/common
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/ErrorMessages.ma
r2751 r2795 69 69 | TerminatedEarly : ErrorMessage 70 70 | BadCostLabelling : ErrorMessage 71 | RepeatedCostLabel : ErrorMessage. 71 | RepeatedCostLabel : ErrorMessage 72 | NotTerminated : ErrorMessage. -
src/common/Measurable.ma
r2756 r2795 400 400 return 〈prefix', \snd (intensional_trace_of_trace C' cs interesting)〉. 401 401 402 (* CSC: Main debug function for the extracted code. 403 It returns the list of all observed states and their observables, 404 the last state and the reason for stopping execution. If the last 405 state is final, it also returns the exit value. *) 406 let rec observe_all_in_measurable (n:nat) (fx:classified_system) 407 (observe: intensional_event → unit) (callstack: list ident) 408 (s:state … fx (cs_global fx)) : 409 list intensional_event × (res int) ≝ 410 match n with 411 [ O ⇒ 412 let res ≝ 413 match is_final … fx (cs_global … fx) s with 414 [ Some r ⇒ OK … r 415 | None ⇒ Error … (msg NotTerminated) ] 416 in 417 〈[ ],res〉 418 | S m ⇒ 419 match is_final … fx (cs_global … fx) s with 420 [ Some r ⇒ 〈[ ],OK … r〉 421 | None ⇒ 422 match step … fx (cs_global … fx) s with 423 [ Value trs ⇒ 424 let costevents ≝ flatten ? (map … intensional_event_of_event (\fst trs)) in 425 let 〈callstack,callevent〉 ≝ 426 match cs_classify fx s 427 return λy. (match y with [cl_call ⇒ True | _ ⇒ False] → ident) → 428 list ident × (list intensional_event) 429 with 430 [ cl_call ⇒ 431 λcallee. let id ≝ callee I in 432 〈id::callstack,[IEVcall id]〉 433 | cl_return ⇒ λ_. 434 match callstack with 435 [ nil ⇒ 〈[ ],[ ]〉 436 | cons id tl ⇒ 〈tl,[IEVret id]〉] 437 | _ ⇒ λ_. 〈callstack, [ ]〉 438 ] (cs_callee fx s) in 439 let events ≝ costevents@callevent in 440 let dummy : list unit ≝ map ?? observe events in 441 let 〈tl,res〉 ≝ 442 observe_all_in_measurable m fx observe callstack (\snd trs) in 443 〈events@tl,res〉 444 | Interact _ _ ⇒ 〈[ ],Error … (msg UnexpectedIO)〉 445 | Wrong m ⇒ 〈[ ],Error … m〉 446 ] 447 ] 448 ].
Note: See TracChangeset
for help on using the changeset viewer.