Changeset 2903


Ignore:
Timestamp:
Mar 19, 2013, 1:25:59 AM (8 years ago)
Author:
sacerdot
Message:

Extracted again.

Location:
extracted
Files:
4 edited

Legend:

Unmodified
Added
Removed

  • extracted/measurable.ml

    r2890 r2903  
    254254let intensional_events_of_events tr =
    255255  List.flatten (List.map intensional_event_of_event tr)
     256
     257(** val intensional_state_change :
     258    classified_system -> AST.ident List.list -> __ -> (AST.ident List.list,
     259    StructuredTraces.intensional_event List.list) Types.prod **)
     260let intensional_state_change c callstack s =
     261  (match c.cs_classify s with
     262   | StructuredTraces.Cl_return ->
     263     (fun x ->
     264       match callstack with
     265       | List.Nil -> { Types.fst = List.Nil; Types.snd = List.Nil }
     266       | List.Cons (id, tl) ->
     267         { Types.fst = tl; Types.snd = (List.Cons ((StructuredTraces.IEVret
     268           id), List.Nil)) })
     269   | StructuredTraces.Cl_jump ->
     270     (fun x -> { Types.fst = callstack; Types.snd = List.Nil })
     271   | StructuredTraces.Cl_call ->
     272     (fun callee ->
     273       let id = callee __ in
     274       { Types.fst = (List.Cons (id, callstack)); Types.snd = (List.Cons
     275       ((StructuredTraces.IEVcall id), List.Nil)) })
     276   | StructuredTraces.Cl_tailcall ->
     277     (fun x -> { Types.fst = callstack; Types.snd = List.Nil })
     278   | StructuredTraces.Cl_other ->
     279     (fun x -> { Types.fst = callstack; Types.snd = List.Nil })) (fun _ ->
     280    cs_callee0 c s)
    256281
    257282(** val intensional_trace_of_trace :
    … …  
    264289  let { Types.fst = s; Types.snd = tr } = str in
    265290  let { Types.fst = callstack0; Types.snd = call_event } =
    266     (match c.cs_classify s with
    267      | StructuredTraces.Cl_return ->
    268        (fun x ->
    269          match callstack with
    270          | List.Nil -> { Types.fst = List.Nil; Types.snd = List.Nil }
    271          | List.Cons (id, tl0) ->
    272            { Types.fst = tl0; Types.snd = (List.Cons
    273              ((StructuredTraces.IEVret id), List.Nil)) })
    274      | StructuredTraces.Cl_jump ->
    275        (fun x -> { Types.fst = callstack; Types.snd = List.Nil })
    276      | StructuredTraces.Cl_call ->
    277        (fun callee ->
    278          let id = callee __ in
    279          { Types.fst = (List.Cons (id, callstack)); Types.snd = (List.Cons
    280          ((StructuredTraces.IEVcall id), List.Nil)) })
    281      | StructuredTraces.Cl_tailcall ->
    282        (fun x -> { Types.fst = callstack; Types.snd = List.Nil })
    283      | StructuredTraces.Cl_other ->
    284        (fun x -> { Types.fst = callstack; Types.snd = List.Nil })) (fun _ ->
    285       cs_callee0 c s)
     291    intensional_state_change c callstack s
    286292  in
    287293  let other_events = intensional_events_of_events tr in

  • extracted/measurable.mli

    r2803 r2903  
    185185  Events.trace -> StructuredTraces.intensional_event List.list
    186186
     187val intensional_state_change :
     188  classified_system -> AST.ident List.list -> __ -> (AST.ident List.list,
     189  StructuredTraces.intensional_event List.list) Types.prod
     190
    187191val intensional_trace_of_trace :
    188192  classified_system -> AST.ident List.list -> (cs_state, Events.trace)

  • extracted/rTLabs_abstract.ml

    r2873 r2903  
    541541  (match s' with
    542542   | RTLabs_semantics.State (f, x, x0) ->
    543      (fun _ _ -> assert false (* absurd case *))
    544    | RTLabs_semantics.Callstate (x, fd, x0, x1, x2, x3) ->
    545      (match stk with
    546       | List.Nil -> (fun _ _ -> assert false (* absurd case *))
    547       | List.Cons (b, x4) ->
    548         (fun _ _ _ -> Globalenvs.symbol_of_function_block ge b)) __
     543     (fun _ -> assert false (* absurd case *))
     544   | RTLabs_semantics.Callstate (fid, x, x0, x1, x2, x3) -> (fun _ -> fid)
    549545   | RTLabs_semantics.Returnstate (x, x0, x1, x2) ->
    550      (fun _ _ -> assert false (* absurd case *))
     546     (fun _ -> assert false (* absurd case *))
    551547   | RTLabs_semantics.Finalstate x ->
    552      (fun _ _ -> assert false (* absurd case *))) __) __
     548     (fun _ -> assert false (* absurd case *)))) __
    553549
    554550(** val rTLabs_status :

  • extracted/rTLabs_semantics.ml

    r2827 r2903  
    777777    Registers.register Types.option -> frame List.list -> GenMem.mem ->
    778778    Pointers.block Types.sig0 **)
    779 let func_block_of_exec ge clearme t vf fd args dst fs m =
     779let func_block_of_exec ge clearme t fid fd args dst fs m =
    780780  (match clearme with
    781781   | State (clearme0, x, x0) ->
    … …  
    783783        dst0 } = clearme0
    784784      in
    785      (fun fs0 m0 tr fid fd0 args0 dst' fs' m' ->
     785     (fun fs0 m0 tr fid0 fd0 args0 dst' fs' m' ->
    786786     (match next_instruction { func = func0; locals = locals0; next = next0;
    787787              sp = sp0; retdst = dst0 } with
    … …  
    791791            (build_state { func = func0; locals = locals0; next = next0; sp =
    792792              sp0; retdst = dst0 } fs0 m0 l) }) (IOMonad.Value { Types.fst =
    793             tr; Types.snd = (Callstate (fid, fd0, args0, dst', fs', m')) })
     793            tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) })
    794794            (fun _ ->
    795795            Obj.magic IOMonad.iO_jmdiscr (IOMonad.Value { Types.fst =
    … …  
    797797              (build_state { func = func0; locals = locals0; next = next0;
    798798                sp = sp0; retdst = dst0 } fs0 m0 l) }) (IOMonad.Value
    799               { Types.fst = tr; Types.snd = (Callstate (fid, fd0, args0,
     799              { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0,
    800800              dst', fs', m')) }) __ (fun _ ->
    801801              Obj.magic Globalenvs.prod_jmdiscr { Types.fst = Events.e0;
    … …  
    803803                (build_state { func = func0; locals = locals0; next = next0;
    804804                  sp = sp0; retdst = dst0 } fs0 m0 l) } { Types.fst = tr;
    805                 Types.snd = (Callstate (fid, fd0, args0, dst', fs', m')) } __
    806                 (fun _ ->
     805                Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) }
     806                __ (fun _ ->
    807807                Logic.eq_rect_Type0 List.Nil (fun _ _ _ ->
    808808                  Obj.magic state_jmdiscr (State
    809809                    ((adv l { func = func0; locals = locals0; next = next0;
    810                        sp = sp0; retdst = dst0 }), fs0, m0)) (Callstate (fid,
    811                     fd0, args0, dst', fs', m')) __) tr __ __))))
     810                       sp = sp0; retdst = dst0 }), fs0, m0)) (Callstate
     811                    (fid0, fd0, args0, dst', fs', m')) __) tr __ __))))
    812812      | RTLabs_syntax.St_cost (c, l) ->
    813813        (fun _ _ ->
    … …  
    816816            (build_state { func = func0; locals = locals0; next = next0; sp =
    817817              sp0; retdst = dst0 } fs0 m0 l) }) (IOMonad.Value { Types.fst =
    818             tr; Types.snd = (Callstate (fid, fd0, args0, dst', fs', m')) })
     818            tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) })
    819819            (fun _ ->
    820820            Obj.magic IOMonad.iO_jmdiscr (IOMonad.Value { Types.fst =
    … …  
    822822              (build_state { func = func0; locals = locals0; next = next0;
    823823                sp = sp0; retdst = dst0 } fs0 m0 l) }) (IOMonad.Value
    824               { Types.fst = tr; Types.snd = (Callstate (fid, fd0, args0,
     824              { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0,
    825825              dst', fs', m')) }) __ (fun _ ->
    826826              Obj.magic Globalenvs.prod_jmdiscr { Types.fst =
    … …  
    828828                (build_state { func = func0; locals = locals0; next = next0;
    829829                  sp = sp0; retdst = dst0 } fs0 m0 l) } { Types.fst = tr;
    830                 Types.snd = (Callstate (fid, fd0, args0, dst', fs', m')) } __
    831                 (fun _ ->
     830                Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) }
     831                __ (fun _ ->
    832832                Logic.eq_rect_Type0 (List.Cons ((Events.EVcost c), List.Nil))
    833833                  (fun _ _ _ ->
    834834                  Obj.magic state_jmdiscr (State
    835835                    ((adv l { func = func0; locals = locals0; next = next0;
    836                        sp = sp0; retdst = dst0 }), fs0, m0)) (Callstate (fid,
    837                     fd0, args0, dst', fs', m')) __) tr __ __))))
     836                       sp = sp0; retdst = dst0 }), fs0, m0)) (Callstate
     837                    (fid0, fd0, args0, dst', fs', m')) __) tr __ __))))
    838838      | RTLabs_syntax.St_const (t0, r, c, l) ->
    839839        (fun _ _ ->
    … …  
    848848                  Events.e0; Types.snd = (State ({ func = func0; locals =
    849849                  locals1; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })))
    850             { Types.fst = tr; Types.snd = (Callstate (fid, fd0, args0, dst',
     850            { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst',
    851851            fs', m')) } (fun v _ _ ->
    852852            bind_ok (reg_store r v locals0) (fun x1 ->
    … …  
    855855                  Events.e0; Types.snd = (State ({ func = func0; locals = x1;
    856856                  next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }))
    857               { Types.fst = tr; Types.snd = (Callstate (fid, fd0, args0,
     857              { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0,
    858858              dst', fs', m')) } (fun locals' _ _ ->
    859859              jmeq_hackT
    … …  
    862862                  locals'; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })
    863863                (Obj.magic (Errors.OK { Types.fst = tr; Types.snd =
    864                   (Callstate (fid, fd0, args0, dst', fs', m')) })) (fun _ ->
     864                  (Callstate (fid0, fd0, args0, dst', fs', m')) })) (fun _ ->
    865865                Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst =
    866866                  Events.e0; Types.snd = (State ({ func = func0; locals =
    867867                  locals'; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })
    868                   (Errors.OK { Types.fst = tr; Types.snd = (Callstate (fid,
     868                  (Errors.OK { Types.fst = tr; Types.snd = (Callstate (fid0,
    869869                  fd0, args0, dst', fs', m')) }) __ (fun _ ->
    870870                  Obj.magic Globalenvs.prod_jmdiscr { Types.fst = Events.e0;
    871871                    Types.snd = (State ({ func = func0; locals = locals';
    872872                    next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }
    873                     { Types.fst = tr; Types.snd = (Callstate (fid, fd0,
     873                    { Types.fst = tr; Types.snd = (Callstate (fid0, fd0,
    874874                    args0, dst', fs', m')) } __ (fun _ ->
    875875                    Logic.eq_rect_Type0 List.Nil (fun _ _ _ ->
    876876                      Obj.magic state_jmdiscr (State ({ func = func0;
    877877                        locals = locals'; next = l; sp = sp0; retdst =
    878                         dst0 }, fs0, m0)) (Callstate (fid, fd0, args0, dst',
     878                        dst0 }, fs0, m0)) (Callstate (fid0, fd0, args0, dst',
    879879                        fs', m')) __) tr __ __))))))
    880880      | RTLabs_syntax.St_op1 (t1, t2, op, r1, r2, l) ->
    … …  
    891891                    Events.e0; Types.snd = (State ({ func = func0; locals =
    892892                    locals1; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }))))
    893             { Types.fst = tr; Types.snd = (Callstate (fid, fd0, args0, dst',
     893            { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst',
    894894            fs', m')) } (fun v _ _ ->
    895895            bind_ok
    … …  
    902902                    Events.e0; Types.snd = (State ({ func = func0; locals =
    903903                    locals1; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })))
    904               { Types.fst = tr; Types.snd = (Callstate (fid, fd0, args0,
     904              { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0,
    905905              dst', fs', m')) } (fun v' _ _ ->
    906906              bind_ok (reg_store r1 v' locals0) (fun x1 ->
    … …  
    909909                    Events.e0; Types.snd = (State ({ func = func0; locals =
    910910                    x1; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }))
    911                 { Types.fst = tr; Types.snd = (Callstate (fid, fd0, args0,
     911                { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0,
    912912                dst', fs', m')) } (fun loc _ _ ->
    913913                jmeq_hackT
    … …  
    916916                    loc; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })
    917917                  (Obj.magic (Errors.OK { Types.fst = tr; Types.snd =
    918                     (Callstate (fid, fd0, args0, dst', fs', m')) }))
     918                    (Callstate (fid0, fd0, args0, dst', fs', m')) }))
    919919                  (fun _ ->
    920920                  Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst =
    921921                    Events.e0; Types.snd = (State ({ func = func0; locals =
    922922                    loc; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })
    923                     (Errors.OK { Types.fst = tr; Types.snd = (Callstate (fid,
    924                     fd0, args0, dst', fs', m')) }) __ (fun _ ->
     923                    (Errors.OK { Types.fst = tr; Types.snd = (Callstate
     924                    (fid0, fd0, args0, dst', fs', m')) }) __ (fun _ ->
    925925                    Obj.magic Globalenvs.prod_jmdiscr { Types.fst =
    926926                      Events.e0; Types.snd = (State ({ func = func0; locals =
    927927                      loc; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }
    928                       { Types.fst = tr; Types.snd = (Callstate (fid, fd0,
     928                      { Types.fst = tr; Types.snd = (Callstate (fid0, fd0,
    929929                      args0, dst', fs', m')) } __ (fun _ ->
    930930                      Logic.eq_rect_Type0 List.Nil (fun _ _ _ ->
    931931                        Obj.magic state_jmdiscr (State ({ func = func0;
    932932                          locals = loc; next = l; sp = sp0; retdst = dst0 },
    933                           fs0, m0)) (Callstate (fid, fd0, args0, dst', fs',
     933                          fs0, m0)) (Callstate (fid0, fd0, args0, dst', fs',
    934934                          m')) __) tr __ __)))))))
    935935      | RTLabs_syntax.St_op2 (t1, t2, t', op, r1, r2, r3, l) ->
    … …  
    950950                      locals1; next = l; sp = sp0; retdst = dst0 }, fs0,
    951951                      m0)) }))))) { Types.fst = tr; Types.snd = (Callstate
    952             (fid, fd0, args0, dst', fs', m')) } (fun v1 _ _ ->
     952            (fid0, fd0, args0, dst', fs', m')) } (fun v1 _ _ ->
    953953            bind_ok (reg_retrieve locals0 r3) (fun x1 ->
    954954              Obj.magic
    … …  
    964964                      locals1; next = l; sp = sp0; retdst = dst0 }, fs0,
    965965                      m0)) })))) { Types.fst = tr; Types.snd = (Callstate
    966               (fid, fd0, args0, dst', fs', m')) } (fun v2 _ _ ->
     966              (fid0, fd0, args0, dst', fs', m')) } (fun v2 _ _ ->
    967967              bind_ok
    968968                (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp)
    … …  
    975975                      locals1; next = l; sp = sp0; retdst = dst0 }, fs0,
    976976                      m0)) }))) { Types.fst = tr; Types.snd = (Callstate
    977                 (fid, fd0, args0, dst', fs', m')) } (fun v' _ _ ->
     977                (fid0, fd0, args0, dst', fs', m')) } (fun v' _ _ ->
    978978                bind_ok (reg_store r1 v' locals0) (fun x1 ->
    979979                  Obj.magic
    … …  
    982982                      func0; locals = x1; next = l; sp = sp0; retdst =
    983983                      dst0 }, fs0, m0)) })) { Types.fst = tr; Types.snd =
    984                   (Callstate (fid, fd0, args0, dst', fs', m')) }
     984                  (Callstate (fid0, fd0, args0, dst', fs', m')) }
    985985                  (fun loc _ _ ->
    986986                  jmeq_hackT
    … …  
    990990                      dst0 }, fs0, m0)) })
    991991                    (Obj.magic (Errors.OK { Types.fst = tr; Types.snd =
    992                       (Callstate (fid, fd0, args0, dst', fs', m')) }))
     992                      (Callstate (fid0, fd0, args0, dst', fs', m')) }))
    993993                    (fun _ ->
    994994                    Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst =
    … …  
    996996                      loc; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })
    997997                      (Errors.OK { Types.fst = tr; Types.snd = (Callstate
    998                       (fid, fd0, args0, dst', fs', m')) }) __ (fun _ ->
     998                      (fid0, fd0, args0, dst', fs', m')) }) __ (fun _ ->
    999999                      Obj.magic Globalenvs.prod_jmdiscr { Types.fst =
    10001000                        Events.e0; Types.snd = (State ({ func = func0;
    10011001                        locals = loc; next = l; sp = sp0; retdst = dst0 },
    10021002                        fs0, m0)) } { Types.fst = tr; Types.snd = (Callstate
    1003                         (fid, fd0, args0, dst', fs', m')) } __ (fun _ ->
     1003                        (fid0, fd0, args0, dst', fs', m')) } __ (fun _ ->
    10041004                        Logic.eq_rect_Type0 List.Nil (fun _ _ _ ->
    10051005                          Obj.magic state_jmdiscr (State ({ func = func0;
    10061006                            locals = loc; next = l; sp = sp0; retdst =
    1007                             dst0 }, fs0, m0)) (Callstate (fid, fd0, args0,
     1007                            dst0 }, fs0, m0)) (Callstate (fid0, fd0, args0,
    10081008                            dst', fs', m')) __) tr __ __))))))))
    10091009      | RTLabs_syntax.St_load (ch, r1, r2, l) ->
    … …  
    10201020                    Events.e0; Types.snd = (State ({ func = func0; locals =
    10211021                    locals1; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }))))
    1022             { Types.fst = tr; Types.snd = (Callstate (fid, fd0, args0, dst',
     1022            { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst',
    10231023            fs', m')) } (fun v _ _ ->
    10241024            bind_ok
    … …  
    10311031                    Events.e0; Types.snd = (State ({ func = func0; locals =
    10321032                    locals1; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })))
    1033               { Types.fst = tr; Types.snd = (Callstate (fid, fd0, args0,
     1033              { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0,
    10341034              dst', fs', m')) } (fun v' _ _ ->
    10351035              bind_ok (reg_store r2 v' locals0) (fun x1 ->
    … …  
    10381038                    Events.e0; Types.snd = (State ({ func = func0; locals =
    10391039                    x1; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }))
    1040                 { Types.fst = tr; Types.snd = (Callstate (fid, fd0, args0,
     1040                { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0,
    10411041                dst', fs', m')) } (fun loc _ _ ->
    10421042                jmeq_hackT
    … …  
    10451045                    loc; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })
    10461046                  (Obj.magic (Errors.OK { Types.fst = tr; Types.snd =
    1047                     (Callstate (fid, fd0, args0, dst', fs', m')) }))
     1047                    (Callstate (fid0, fd0, args0, dst', fs', m')) }))
    10481048                  (fun _ ->
    10491049                  Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst =
    10501050                    Events.e0; Types.snd = (State ({ func = func0; locals =
    10511051                    loc; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })
    1052                     (Errors.OK { Types.fst = tr; Types.snd = (Callstate (fid,
    1053                     fd0, args0, dst', fs', m')) }) __ (fun _ ->
     1052                    (Errors.OK { Types.fst = tr; Types.snd = (Callstate
     1053                    (fid0, fd0, args0, dst', fs', m')) }) __ (fun _ ->
    10541054                    Obj.magic Globalenvs.prod_jmdiscr { Types.fst =
    10551055                      Events.e0; Types.snd = (State ({ func = func0; locals =
    10561056                      loc; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }
    1057                       { Types.fst = tr; Types.snd = (Callstate (fid, fd0,
     1057                      { Types.fst = tr; Types.snd = (Callstate (fid0, fd0,
    10581058                      args0, dst', fs', m')) } __ (fun _ ->
    10591059                      Logic.eq_rect_Type0 List.Nil (fun _ _ _ ->
    10601060                        Obj.magic state_jmdiscr (State ({ func = func0;
    10611061                          locals = loc; next = l; sp = sp0; retdst = dst0 },
    1062                           fs0, m0)) (Callstate (fid, fd0, args0, dst', fs',
     1062                          fs0, m0)) (Callstate (fid0, fd0, args0, dst', fs',
    10631063                          m')) __) tr __ __)))))))
    10641064      | RTLabs_syntax.St_store (ch, r1, r2, l) ->
    … …  
    10761076                    (build_state { func = func0; locals = locals0; next =
    10771077                      next0; sp = sp0; retdst = dst0 } fs0 m'0 l) }))))
    1078             { Types.fst = tr; Types.snd = (Callstate (fid, fd0, args0, dst',
     1078            { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst',
    10791079            fs', m')) } (fun v _ _ ->
    10801080            bind_ok (reg_retrieve locals0 r2) (fun x1 ->
    … …  
    10881088                    (build_state { func = func0; locals = locals0; next =
    10891089                      next0; sp = sp0; retdst = dst0 } fs0 m'0 l) })))
    1090               { Types.fst = tr; Types.snd = (Callstate (fid, fd0, args0,
     1090              { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0,
    10911091              dst', fs', m')) } (fun v' _ _ ->
    10921092              bind_ok
    … …  
    10981098                    (build_state { func = func0; locals = locals0; next =
    10991099                      next0; sp = sp0; retdst = dst0 } fs0 x1 l) }))
    1100                 { Types.fst = tr; Types.snd = (Callstate (fid, fd0, args0,
     1100                { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0,
    11011101                dst', fs', m')) } (fun loc _ _ ->
    11021102                jmeq_hackT
    … …  
    11061106                      next0; sp = sp0; retdst = dst0 } fs0 loc l) })
    11071107                  (Obj.magic (Errors.OK { Types.fst = tr; Types.snd =
    1108                     (Callstate (fid, fd0, args0, dst', fs', m')) }))
     1108                    (Callstate (fid0, fd0, args0, dst', fs', m')) }))
    11091109                  (fun _ ->
    11101110                  Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst =
    … …  
    11121112                    (build_state { func = func0; locals = locals0; next =
    11131113                      next0; sp = sp0; retdst = dst0 } fs0 loc l) })
    1114                     (Errors.OK { Types.fst = tr; Types.snd = (Callstate (fid,
    1115                     fd0, args0, dst', fs', m')) }) __ (fun _ ->
     1114                    (Errors.OK { Types.fst = tr; Types.snd = (Callstate
     1115                    (fid0, fd0, args0, dst', fs', m')) }) __ (fun _ ->
    11161116                    Obj.magic Globalenvs.prod_jmdiscr { Types.fst =
    11171117                      Events.e0; Types.snd =
    11181118                      (build_state { func = func0; locals = locals0; next =
    11191119                        next0; sp = sp0; retdst = dst0 } fs0 loc l) }
    1120                       { Types.fst = tr; Types.snd = (Callstate (fid, fd0,
     1120                      { Types.fst = tr; Types.snd = (Callstate (fid0, fd0,
    11211121                      args0, dst', fs', m')) } __ (fun _ ->
    11221122                      Logic.eq_rect_Type0 List.Nil (fun _ _ _ ->
    … …  
    11241124                          ((adv l { func = func0; locals = locals0; next =
    11251125                             next0; sp = sp0; retdst = dst0 }), fs0, loc))
    1126                           (Callstate (fid, fd0, args0, dst', fs', m')) __) tr
    1127                         __ __)))))))
     1126                          (Callstate (fid0, fd0, args0, dst', fs', m')) __)
     1127                        tr __ __)))))))
    11281128      | RTLabs_syntax.St_call_id (x1, rs, or0, l) ->
    11291129        (fun _ _ ->
    … …  
    11481148                    ((adv l { func = func0; locals = locals0; next = next0;
    11491149                       sp = sp0; retdst = dst0 }), fs0)), m0)) }))))
    1150             { Types.fst = tr; Types.snd = (Callstate (fid, fd0, args0, dst',
     1150            { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst',
    11511151            fs', m')) } (fun v _ _ ->
    11521152            bind_ok
    … …  
    11641164                    ((adv l { func = func0; locals = locals0; next = next0;
    11651165                       sp = sp0; retdst = dst0 }), fs0)), m0)) })))
    1166               { Types.fst = tr; Types.snd = (Callstate (fid, fd0, args0,
     1166              { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0,
    11671167              dst', fs', m')) } (fun fd' _ _ ->
    11681168              bind_ok
    … …  
    11761176                    ((adv l { func = func0; locals = locals0; next = next0;
    11771177                       sp = sp0; retdst = dst0 }), fs0)), m0)) }))
    1178                 { Types.fst = tr; Types.snd = (Callstate (fid, fd0, args0,
     1178                { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0,
    11791179                dst', fs', m')) } (fun vs _ _ ->
    11801180                jmeq_hackT
    … …  
    11851185                       sp = sp0; retdst = dst0 }), fs0)), m0)) })
    11861186                  (Obj.magic (Errors.OK { Types.fst = tr; Types.snd =
    1187                     (Callstate (fid, fd0, args0, dst', fs', m')) }))
     1187                    (Callstate (fid0, fd0, args0, dst', fs', m')) }))
    11881188                  (fun _ ->
    11891189                  Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst =
    … …  
    11911191                    (List.Cons ({ func = func0; locals = locals0; next = l;
    11921192                    sp = sp0; retdst = dst0 }, fs0)), m0)) }) (Errors.OK
    1193                     { Types.fst = tr; Types.snd = (Callstate (fid, fd0,
     1193                    { Types.fst = tr; Types.snd = (Callstate (fid0, fd0,
    11941194                    args0, dst', fs', m')) }) __ (fun _ ->
    11951195                    Obj.magic Globalenvs.prod_jmdiscr { Types.fst = List.Nil;
    … …  
    11971197                      ({ func = func0; locals = locals0; next = l; sp = sp0;
    11981198                      retdst = dst0 }, fs0)), m0)) } { Types.fst = tr;
    1199                       Types.snd = (Callstate (fid, fd0, args0, dst', fs',
     1199                      Types.snd = (Callstate (fid0, fd0, args0, dst', fs',
    12001200                      m')) } __ (fun _ ->
    12011201                      Logic.eq_rect_Type0 List.Nil (fun _ _ _ ->
    … …  
    12031203                          (List.Cons ({ func = func0; locals = locals0;
    12041204                          next = l; sp = sp0; retdst = dst0 }, fs0)), m0))
    1205                           (Callstate (fid, fd0, args0, dst', fs', m')) __
     1205                          (Callstate (fid0, fd0, args0, dst', fs', m')) __
    12061206                          (fun _ ->
    1207                           Extralib.eq_rect_Type0_r fid (fun _ _ _ _ _ _ _ ->
     1207                          Extralib.eq_rect_Type0_r fid0 (fun _ _ _ _ _ _ _ ->
    12081208                            Extralib.eq_rect_Type0_r fd0 (fun _ _ _ _ _ ->
    12091209                              Extralib.eq_rect_Type0_r args0
    … …  
    12181218                                      Logic.streicherK (Errors.OK
    12191219                                        { Types.fst = List.Nil; Types.snd =
    1220                                         (Callstate (fid, fd0, args0, dst',
     1220                                        (Callstate (fid0, fd0, args0, dst',
    12211221                                        (List.Cons ({ func = func0; locals =
    12221222                                        locals0; next = l; sp = sp0; retdst =
    … …  
    12241224                                        (Logic.streicherK { Types.fst =
    12251225                                          List.Nil; Types.snd = (Callstate
    1226                                           (fid, fd0, args0, dst', (List.Cons
     1226                                          (fid0, fd0, args0, dst', (List.Cons
    12271227                                          ({ func = func0; locals = locals0;
    12281228                                          next = l; sp = sp0; retdst =
    12291229                                          dst0 }, fs0)), m')) }
    1230                                           (Logic.streicherK (Callstate (fid,
     1230                                          (Logic.streicherK (Callstate (fid0,
    12311231                                            fd0, args0, dst', (List.Cons
    12321232                                            ({ func = func0; locals =
    … …  
    12521252                    ((adv l { func = func0; locals = locals0; next = next0;
    12531253                       sp = sp0; retdst = dst0 }), fs0)), m0)) }))))
    1254             { Types.fst = tr; Types.snd = (Callstate (fid, fd0, args0, dst',
     1254            { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst',
    12551255            fs', m')) } (fun v _ _ ->
    12561256            bind_ok
    … …  
    12661266                    ((adv l { func = func0; locals = locals0; next = next0;
    12671267                       sp = sp0; retdst = dst0 }), fs0)), m0)) })))
    1268               { Types.fst = tr; Types.snd = (Callstate (fid, fd0, args0,
     1268              { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0,
    12691269              dst', fs', m')) } (fun fd' _ _ ->
    12701270              bind_ok
    … …  
    12781278                    ((adv l { func = func0; locals = locals0; next = next0;
    12791279                       sp = sp0; retdst = dst0 }), fs0)), m0)) }))
    1280                 { Types.fst = tr; Types.snd = (Callstate (fid, fd0, args0,
     1280                { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0,
    12811281                dst', fs', m')) } (fun vs _ _ ->
    12821282                jmeq_hackT
    … …  
    12871287                       sp = sp0; retdst = dst0 }), fs0)), m0)) })
    12881288                  (Obj.magic (Errors.OK { Types.fst = tr; Types.snd =
    1289                     (Callstate (fid, fd0, args0, dst', fs', m')) }))
     1289                    (Callstate (fid0, fd0, args0, dst', fs', m')) }))
    12901290                  (fun _ ->
    12911291                  Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst =
    … …  
    12941294                    locals = locals0; next = l; sp = sp0; retdst = dst0 },
    12951295                    fs0)), m0)) }) (Errors.OK { Types.fst = tr; Types.snd =
    1296                     (Callstate (fid, fd0, args0, dst', fs', m')) }) __
     1296                    (Callstate (fid0, fd0, args0, dst', fs', m')) }) __
    12971297                    (fun _ ->
    12981298                    Obj.magic Globalenvs.prod_jmdiscr { Types.fst = List.Nil;
    … …  
    13001300                      vs, or0, (List.Cons ({ func = func0; locals = locals0;
    13011301                      next = l; sp = sp0; retdst = dst0 }, fs0)), m0)) }
    1302                       { Types.fst = tr; Types.snd = (Callstate (fid, fd0,
     1302                      { Types.fst = tr; Types.snd = (Callstate (fid0, fd0,
    13031303                      args0, dst', fs', m')) } __ (fun _ ->
    13041304                      Logic.eq_rect_Type0 List.Nil (fun _ _ _ ->
    … …  
    13061306                          fd'.Types.fst, vs, or0, (List.Cons ({ func = func0;
    13071307                          locals = locals0; next = l; sp = sp0; retdst =
    1308                           dst0 }, fs0)), m0)) (Callstate (fid, fd0, args0,
     1308                          dst0 }, fs0)), m0)) (Callstate (fid0, fd0, args0,
    13091309                          dst', fs', m')) __ (fun _ ->
    13101310                          Logic.eq_rect_Type0 fd'.Types.snd (fun _ _ _ _ ->
    … …  
    13741374                                                (fun _ -> b)) __)))) m0 __ __
    13751375                                      __) fs' __ __ __) or0 __ __ __ __) vs
    1376                                 __ __ __ __) fd0 __ __ __) fid __ __ __)) tr
     1376                                __ __ __ __) fd0 __ __ __) fid0 __ __ __)) tr
    13771377                        __ __)))))))
    13781378      | RTLabs_syntax.St_cond (r, l1, l2) ->
    … …  
    13891389                     | Bool.True -> l1
    13901390                     | Bool.False -> l2)) }))) { Types.fst = tr; Types.snd =
    1391             (Callstate (fid, fd0, args0, dst', fs', m')) } (fun v _ _ ->
     1391            (Callstate (fid0, fd0, args0, dst', fs', m')) } (fun v _ _ ->
    13921392            bind_ok (Values.eval_bool_of_val v) (fun x1 ->
    13931393              Obj.magic
    … …  
    13991399                     | Bool.True -> l1
    14001400                     | Bool.False -> l2)) })) { Types.fst = tr; Types.snd =
    1401               (Callstate (fid, fd0, args0, dst', fs', m')) } (fun b _ _ ->
     1401              (Callstate (fid0, fd0, args0, dst', fs', m')) } (fun b _ _ ->
    14021402              jmeq_hackT
    14031403                (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
    … …  
    14091409                     | Bool.False -> l2)) })
    14101410                (Obj.magic (Errors.OK { Types.fst = tr; Types.snd =
    1411                   (Callstate (fid, fd0, args0, dst', fs', m')) })) (fun _ ->
     1411                  (Callstate (fid0, fd0, args0, dst', fs', m')) })) (fun _ ->
    14121412                Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst =
    14131413                  Events.e0; Types.snd =
    … …  
    14171417                     | Bool.True -> l1
    14181418                     | Bool.False -> l2)) }) (Errors.OK { Types.fst = tr;
    1419                   Types.snd = (Callstate (fid, fd0, args0, dst', fs', m')) })
    1420                   __ (fun _ ->
     1419                  Types.snd = (Callstate (fid0, fd0, args0, dst', fs',
     1420                  m')) }) __ (fun _ ->
    14211421                  Obj.magic Globalenvs.prod_jmdiscr { Types.fst = Events.e0;
    14221422                    Types.snd =
    … …  
    14261426                       | Bool.True -> l1
    14271427                       | Bool.False -> l2)) } { Types.fst = tr; Types.snd =
    1428                     (Callstate (fid, fd0, args0, dst', fs', m')) } __
     1428                    (Callstate (fid0, fd0, args0, dst', fs', m')) } __
    14291429                    (fun _ ->
    14301430                    Logic.eq_rect_Type0 List.Nil (fun _ _ _ ->
    … …  
    14351435                            | Bool.False -> l2) { func = func0; locals =
    14361436                           locals0; next = next0; sp = sp0; retdst = dst0 }),
    1437                         fs0, m0)) (Callstate (fid, fd0, args0, dst', fs',
     1437                        fs0, m0)) (Callstate (fid0, fd0, args0, dst', fs',
    14381438                        m')) __) tr __ __))))))
    14391439      | RTLabs_syntax.St_return ->
    … …  
    14551455                Events.e0; Types.snd = (Returnstate (v, dst0, fs0,
    14561456                (GenMem.free m0 sp0))) })) { Types.fst = tr; Types.snd =
    1457             (Callstate (fid, fd0, args0, dst', fs', m')) } (fun v ->
     1457            (Callstate (fid0, fd0, args0, dst', fs', m')) } (fun v ->
    14581458            match func0.RTLabs_syntax.f_result with
    14591459            | Types.None ->
    … …  
    14641464                    (GenMem.free m0 sp0))) })
    14651465                  (Obj.magic (Errors.OK { Types.fst = tr; Types.snd =
    1466                     (Callstate (fid, fd0, args0, dst', fs', m')) }))
     1466                    (Callstate (fid0, fd0, args0, dst', fs', m')) }))
    14671467                  (fun _ ->
    14681468                  Obj.magic Errors.res_discr (Errors.OK Types.None)
    … …  
    14711471                      Events.e0; Types.snd = (Returnstate (v, dst0, fs0,
    14721472                      (GenMem.free m0 sp0))) }) (Errors.OK { Types.fst = tr;
    1473                       Types.snd = (Callstate (fid, fd0, args0, dst', fs',
     1473                      Types.snd = (Callstate (fid0, fd0, args0, dst', fs',
    14741474                      m')) }) __ (fun _ ->
    14751475                      Obj.magic Globalenvs.prod_jmdiscr { Types.fst =
    14761476                        Events.e0; Types.snd = (Returnstate (v, dst0, fs0,
    14771477                        (GenMem.free m0 sp0))) } { Types.fst = tr;
    1478                         Types.snd = (Callstate (fid, fd0, args0, dst', fs',
     1478                        Types.snd = (Callstate (fid0, fd0, args0, dst', fs',
    14791479                        m')) } __ (fun _ ->
    14801480                        Logic.eq_rect_Type0 List.Nil (fun _ _ _ ->
    14811481                          Obj.magic state_jmdiscr (Returnstate (v, dst0, fs0,
    1482                             (GenMem.free m0 sp0))) (Callstate (fid, fd0,
     1482                            (GenMem.free m0 sp0))) (Callstate (fid0, fd0,
    14831483                            args0, dst', fs', m')) __) tr __ __)))))
    14841484            | Types.Some clearme1 ->
    … …  
    14941494                    (GenMem.free m0 sp0))) })
    14951495                  (Obj.magic (Errors.OK { Types.fst = tr; Types.snd =
    1496                     (Callstate (fid, fd0, args0, dst', fs', m')) }))
     1496                    (Callstate (fid0, fd0, args0, dst', fs', m')) }))
    14971497                  (fun _ ->
    14981498                  Obj.magic Errors.res_discr (Errors.OK (Types.Some v0))
    … …  
    15011501                      Events.e0; Types.snd = (Returnstate (v, dst0, fs0,
    15021502                      (GenMem.free m0 sp0))) }) (Errors.OK { Types.fst = tr;
    1503                       Types.snd = (Callstate (fid, fd0, args0, dst', fs',
     1503                      Types.snd = (Callstate (fid0, fd0, args0, dst', fs',
    15041504                      m')) }) __ (fun _ ->
    15051505                      Obj.magic Globalenvs.prod_jmdiscr { Types.fst =
    15061506                        Events.e0; Types.snd = (Returnstate (v, dst0, fs0,
    15071507                        (GenMem.free m0 sp0))) } { Types.fst = tr;
    1508                         Types.snd = (Callstate (fid, fd0, args0, dst', fs',
     1508                        Types.snd = (Callstate (fid0, fd0, args0, dst', fs',
    15091509                        m')) } __ (fun _ ->
    15101510                        Logic.eq_rect_Type0 List.Nil (fun _ _ _ ->
    15111511                          Obj.magic state_jmdiscr (Returnstate (v, dst0, fs0,
    1512                             (GenMem.free m0 sp0))) (Callstate (fid, fd0,
     1512                            (GenMem.free m0 sp0))) (Callstate (fid0, fd0,
    15131513                            args0, dst', fs', m')) __) tr __ __))))))))) __))
    15141514       x x0
    1515    | Callstate (vf0, clearme0, x, x0, x1, x2) ->
     1515   | Callstate (vf, clearme0, x, x0, x1, x2) ->
    15161516     (match clearme0 with
    15171517      | AST.Internal fn ->
    … …  
    17101710         ErrorMessages.FinalState), List.Nil))) (IOMonad.Value { Types.fst =
    17111711         tr; Types.snd = (Callstate (vf', fd', args', dst', fs', m')) }) __))
    1712     t vf fd args dst fs m __
    1713 
     1712    t fid fd args dst fs m __
     1713
Note: See TracChangeset for help on using the changeset viewer.