Changeset 2812 for extracted


Ignore:
Timestamp:
Mar 7, 2013, 9:23:23 PM (8 years ago)
Author:
sacerdot
Message:

Pre-classified system for RTLabs.

Location:
extracted
Files:
1 added
2 edited

Legend:

Unmodified
Added
Removed

  • extracted/rTLabs_abstract.ml

    r2797 r2812  
    150150    RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
    151151    List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **)
    152 let rec rTLabs_ext_state_rect_Type4 ge h_mk_RTLabs_ext_state x_17319 =
    153   let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_17319 in
     152let rec rTLabs_ext_state_rect_Type4 ge h_mk_RTLabs_ext_state x_341 =
     153  let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_341 in
    154154  h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __
    155155
    … …  
    157157    RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
    158158    List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **)
    159 let rec rTLabs_ext_state_rect_Type5 ge h_mk_RTLabs_ext_state x_17321 =
    160   let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_17321 in
     159let rec rTLabs_ext_state_rect_Type5 ge h_mk_RTLabs_ext_state x_343 =
     160  let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_343 in
    161161  h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __
    162162
    … …  
    164164    RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
    165165    List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **)
    166 let rec rTLabs_ext_state_rect_Type3 ge h_mk_RTLabs_ext_state x_17323 =
    167   let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_17323 in
     166let rec rTLabs_ext_state_rect_Type3 ge h_mk_RTLabs_ext_state x_345 =
     167  let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_345 in
    168168  h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __
    169169
    … …  
    171171    RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
    172172    List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **)
    173 let rec rTLabs_ext_state_rect_Type2 ge h_mk_RTLabs_ext_state x_17325 =
    174   let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_17325 in
     173let rec rTLabs_ext_state_rect_Type2 ge h_mk_RTLabs_ext_state x_347 =
     174  let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_347 in
    175175  h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __
    176176
    … …  
    178178    RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
    179179    List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **)
    180 let rec rTLabs_ext_state_rect_Type1 ge h_mk_RTLabs_ext_state x_17327 =
    181   let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_17327 in
     180let rec rTLabs_ext_state_rect_Type1 ge h_mk_RTLabs_ext_state x_349 =
     181  let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_349 in
    182182  h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __
    183183
    … …  
    185185    RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
    186186    List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **)
    187 let rec rTLabs_ext_state_rect_Type0 ge h_mk_RTLabs_ext_state x_17329 =
    188   let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_17329 in
     187let rec rTLabs_ext_state_rect_Type0 ge h_mk_RTLabs_ext_state x_351 =
     188  let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_351 in
    189189  h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __
    190190
    … …  
    340340    rTLabs_pc -> 'a1 **)
    341341let rec rTLabs_pc_rect_Type4 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function
    342 | Rapc_state (x_17355, x_17354) -> h_rapc_state x_17355 x_17354
    343 | Rapc_call (x_17357, x_17356) -> h_rapc_call x_17357 x_17356
    344 | Rapc_ret x_17358 -> h_rapc_ret x_17358
     342| Rapc_state (x_377, x_376) -> h_rapc_state x_377 x_376
     343| Rapc_call (x_379, x_378) -> h_rapc_call x_379 x_378
     344| Rapc_ret x_380 -> h_rapc_ret x_380
    345345| Rapc_fin -> h_rapc_fin
    346346
    … …  
    350350    rTLabs_pc -> 'a1 **)
    351351let rec rTLabs_pc_rect_Type5 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function
    352 | Rapc_state (x_17365, x_17364) -> h_rapc_state x_17365 x_17364
    353 | Rapc_call (x_17367, x_17366) -> h_rapc_call x_17367 x_17366
    354 | Rapc_ret x_17368 -> h_rapc_ret x_17368
     352| Rapc_state (x_387, x_386) -> h_rapc_state x_387 x_386
     353| Rapc_call (x_389, x_388) -> h_rapc_call x_389 x_388
     354| Rapc_ret x_390 -> h_rapc_ret x_390
    355355| Rapc_fin -> h_rapc_fin
    356356
    … …  
    360360    rTLabs_pc -> 'a1 **)
    361361let rec rTLabs_pc_rect_Type3 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function
    362 | Rapc_state (x_17375, x_17374) -> h_rapc_state x_17375 x_17374
    363 | Rapc_call (x_17377, x_17376) -> h_rapc_call x_17377 x_17376
    364 | Rapc_ret x_17378 -> h_rapc_ret x_17378
     362| Rapc_state (x_397, x_396) -> h_rapc_state x_397 x_396
     363| Rapc_call (x_399, x_398) -> h_rapc_call x_399 x_398
     364| Rapc_ret x_400 -> h_rapc_ret x_400
    365365| Rapc_fin -> h_rapc_fin
    366366
    … …  
    370370    rTLabs_pc -> 'a1 **)
    371371let rec rTLabs_pc_rect_Type2 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function
    372 | Rapc_state (x_17385, x_17384) -> h_rapc_state x_17385 x_17384
    373 | Rapc_call (x_17387, x_17386) -> h_rapc_call x_17387 x_17386
    374 | Rapc_ret x_17388 -> h_rapc_ret x_17388
     372| Rapc_state (x_407, x_406) -> h_rapc_state x_407 x_406
     373| Rapc_call (x_409, x_408) -> h_rapc_call x_409 x_408
     374| Rapc_ret x_410 -> h_rapc_ret x_410
    375375| Rapc_fin -> h_rapc_fin
    376376
    … …  
    380380    rTLabs_pc -> 'a1 **)
    381381let rec rTLabs_pc_rect_Type1 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function
    382 | Rapc_state (x_17395, x_17394) -> h_rapc_state x_17395 x_17394
    383 | Rapc_call (x_17397, x_17396) -> h_rapc_call x_17397 x_17396
    384 | Rapc_ret x_17398 -> h_rapc_ret x_17398
     382| Rapc_state (x_417, x_416) -> h_rapc_state x_417 x_416
     383| Rapc_call (x_419, x_418) -> h_rapc_call x_419 x_418
     384| Rapc_ret x_420 -> h_rapc_ret x_420
    385385| Rapc_fin -> h_rapc_fin
    386386
    … …  
    390390    rTLabs_pc -> 'a1 **)
    391391let rec rTLabs_pc_rect_Type0 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function
    392 | Rapc_state (x_17405, x_17404) -> h_rapc_state x_17405 x_17404
    393 | Rapc_call (x_17407, x_17406) -> h_rapc_call x_17407 x_17406
    394 | Rapc_ret x_17408 -> h_rapc_ret x_17408
     392| Rapc_state (x_427, x_426) -> h_rapc_state x_427 x_426
     393| Rapc_call (x_429, x_428) -> h_rapc_call x_429 x_428
     394| Rapc_ret x_430 -> h_rapc_ret x_430
    395395| Rapc_fin -> h_rapc_fin
    396396

  • extracted/rTLabs_semantics.ml

    r2797 r2812  
    128128    Graphs.label -> __ -> Pointers.block -> Registers.register Types.option
    129129    -> 'a1) -> frame -> 'a1 **)
    130 let rec frame_rect_Type4 h_mk_frame x_16011 =
     130let rec frame_rect_Type4 h_mk_frame x_3 =
    131131  let { func = func0; locals = locals0; next = next0; sp = sp0; retdst =
    132     retdst0 } = x_16011
     132    retdst0 } = x_3
    133133  in
    134134  h_mk_frame func0 locals0 next0 __ sp0 retdst0
    … …  
    138138    Graphs.label -> __ -> Pointers.block -> Registers.register Types.option
    139139    -> 'a1) -> frame -> 'a1 **)
    140 let rec frame_rect_Type5 h_mk_frame x_16013 =
     140let rec frame_rect_Type5 h_mk_frame x_5 =
    141141  let { func = func0; locals = locals0; next = next0; sp = sp0; retdst =
    142     retdst0 } = x_16013
     142    retdst0 } = x_5
    143143  in
    144144  h_mk_frame func0 locals0 next0 __ sp0 retdst0
    … …  
    148148    Graphs.label -> __ -> Pointers.block -> Registers.register Types.option
    149149    -> 'a1) -> frame -> 'a1 **)
    150 let rec frame_rect_Type3 h_mk_frame x_16015 =
     150let rec frame_rect_Type3 h_mk_frame x_7 =
    151151  let { func = func0; locals = locals0; next = next0; sp = sp0; retdst =
    152     retdst0 } = x_16015
     152    retdst0 } = x_7
    153153  in
    154154  h_mk_frame func0 locals0 next0 __ sp0 retdst0
    … …  
    158158    Graphs.label -> __ -> Pointers.block -> Registers.register Types.option
    159159    -> 'a1) -> frame -> 'a1 **)
    160 let rec frame_rect_Type2 h_mk_frame x_16017 =
     160let rec frame_rect_Type2 h_mk_frame x_9 =
    161161  let { func = func0; locals = locals0; next = next0; sp = sp0; retdst =
    162     retdst0 } = x_16017
     162    retdst0 } = x_9
    163163  in
    164164  h_mk_frame func0 locals0 next0 __ sp0 retdst0
    … …  
    168168    Graphs.label -> __ -> Pointers.block -> Registers.register Types.option
    169169    -> 'a1) -> frame -> 'a1 **)
    170 let rec frame_rect_Type1 h_mk_frame x_16019 =
     170let rec frame_rect_Type1 h_mk_frame x_11 =
    171171  let { func = func0; locals = locals0; next = next0; sp = sp0; retdst =
    172     retdst0 } = x_16019
     172    retdst0 } = x_11
    173173  in
    174174  h_mk_frame func0 locals0 next0 __ sp0 retdst0
    … …  
    178178    Graphs.label -> __ -> Pointers.block -> Registers.register Types.option
    179179    -> 'a1) -> frame -> 'a1 **)
    180 let rec frame_rect_Type0 h_mk_frame x_16021 =
     180let rec frame_rect_Type0 h_mk_frame x_13 =
    181181  let { func = func0; locals = locals0; next = next0; sp = sp0; retdst =
    182     retdst0 } = x_16021
     182    retdst0 } = x_13
    183183  in
    184184  h_mk_frame func0 locals0 next0 __ sp0 retdst0
    … …  
    632632         (Obj.magic
    633633           (IOMonad.err_to_io
    634              (IO.check_eventval_list params fn.AST.ef_sig.AST.sig_args)))
     634             (IO.check_eventval_list params (AST.sig_args (AST.ef_sig fn)))))
    635635         (fun evargs ->
    636636         Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
    637637           (Obj.magic
    638              (IO.do_io fn.AST.ef_id evargs (AST.proj_sig_res fn.AST.ef_sig)))
    639            (fun evres ->
     638             (IO.do_io (AST.ef_id fn) evargs
     639               (AST.proj_sig_res (AST.ef_sig fn)))) (fun evres ->
    640640           Monad.m_return0 (Monad.max_def IOMonad.iOMonad) { Types.fst =
    641              (Events.eextcall fn.AST.ef_id evargs
    642                (IO.mk_eventval (AST.proj_sig_res fn.AST.ef_sig) evres));
     641             (Events.eextcall (AST.ef_id fn) evargs
     642               (IO.mk_eventval (AST.proj_sig_res (AST.ef_sig fn)) evres));
    643643             Types.snd = (Returnstate ((Types.Some
    644              (IO.mk_val (AST.proj_sig_res fn.AST.ef_sig) evres)), dst, fs,
     644             (IO.mk_val (AST.proj_sig_res (AST.ef_sig fn)) evres)), dst, fs,
    645645             m)) }))))
    646646| Returnstate (v, dst, fs, m) ->
    … …  
    735735        (Globalenvs.init_mem (fun x -> List.Cons ((AST.Init_space x),
    736736          List.Nil)) p)) (fun m ->
    737       let main = p.AST.prog_main in
     737      let main = AST.prog_main p in
    738738      Monad.m_bind0 (Monad.max_def Errors.res0)
    739739        (Obj.magic
    … …  
    15621562          IOMonad.bindIO_value
    15631563            (IOMonad.err_to_io
    1564               (IO.check_eventval_list args0 fn.AST.ef_sig.AST.sig_args))
     1564              (IO.check_eventval_list args0 (AST.sig_args (AST.ef_sig fn))))
    15651565            (fun evargs ->
    15661566            Obj.magic
    15671567              (Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
    15681568                (Obj.magic
    1569                   (IO.do_io fn.AST.ef_id evargs
    1570                     (AST.proj_sig_res fn.AST.ef_sig))) (fun evres ->
     1569                  (IO.do_io (AST.ef_id fn) evargs
     1570                    (AST.proj_sig_res (AST.ef_sig fn)))) (fun evres ->
    15711571                Monad.m_return0 (Monad.max_def IOMonad.iOMonad) { Types.fst =
    1572                   (Events.eextcall fn.AST.ef_id evargs
    1573                     (IO.mk_eventval (AST.proj_sig_res fn.AST.ef_sig) evres));
     1572                  (Events.eextcall (AST.ef_id fn) evargs
     1573                    (IO.mk_eventval (AST.proj_sig_res (AST.ef_sig fn)) evres));
    15741574                  Types.snd = (Returnstate ((Types.Some
    1575                   (IO.mk_val (AST.proj_sig_res fn.AST.ef_sig) evres)),
     1575                  (IO.mk_val (AST.proj_sig_res (AST.ef_sig fn)) evres)),
    15761576                  retdst0, stk, m0)) }))) { Types.fst = tr; Types.snd =
    15771577            (Callstate (vf', fd', args', dst', fs', m')) } (fun evargs _ _ ->
    15781578            Obj.magic IOMonad.iO_discr (IOMonad.Interact ({ IO.io_function =
    1579               fn.AST.ef_id; IO.io_args = evargs; IO.io_in_typ =
    1580               (AST.proj_sig_res fn.AST.ef_sig) }, (fun res ->
     1579              (AST.ef_id fn); IO.io_args = evargs; IO.io_in_typ =
     1580              (AST.proj_sig_res (AST.ef_sig fn)) }, (fun res ->
    15811581              IOMonad.bindIO (IOMonad.Value res) (fun evres ->
    15821582                Obj.magic
    15831583                  (Monad.m_return0 (Monad.max_def IOMonad.iOMonad)
    15841584                    { Types.fst =
    1585                     (Events.eextcall fn.AST.ef_id evargs
    1586                       (IO.mk_eventval (AST.proj_sig_res fn.AST.ef_sig) evres));
    1587                     Types.snd = (Returnstate ((Types.Some
    1588                     (IO.mk_val (AST.proj_sig_res fn.AST.ef_sig) evres)),
     1585                    (Events.eextcall (AST.ef_id fn) evargs
     1586                      (IO.mk_eventval (AST.proj_sig_res (AST.ef_sig fn))
     1587                        evres)); Types.snd = (Returnstate ((Types.Some
     1588                    (IO.mk_val (AST.proj_sig_res (AST.ef_sig fn)) evres)),
    15891589                    retdst0, stk, m0)) }))))) (IOMonad.Value { Types.fst =
    15901590              tr; Types.snd = (Callstate (vf', fd', args', dst', fs', m')) })
Note: See TracChangeset for help on using the changeset viewer.