Changeset 2933 for extracted/traces.ml


Ignore:
Timestamp:
Mar 21, 2013, 8:11:50 PM (6 years ago)
Author:
sacerdot
Message:

New extraction, several bug fixed. RTL_semantics fixed by hand, will be fixed
automatically when Paolo commits.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/traces.ml

    r2890 r2933  
    142142    (AST.ident List.list -> Joint_semantics.sem_params ->
    143143    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    144 let rec evaluation_params_rect_Type4 h_mk_evaluation_params x_26086 =
    145   let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } =
    146     x_26086
    147   in
     144let rec evaluation_params_rect_Type4 h_mk_evaluation_params x_3 =
     145  let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } = x_3 in
    148146  h_mk_evaluation_params globals0 sparams0 ev_genv0
    149147
     
    151149    (AST.ident List.list -> Joint_semantics.sem_params ->
    152150    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    153 let rec evaluation_params_rect_Type5 h_mk_evaluation_params x_26088 =
    154   let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } =
    155     x_26088
    156   in
     151let rec evaluation_params_rect_Type5 h_mk_evaluation_params x_5 =
     152  let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } = x_5 in
    157153  h_mk_evaluation_params globals0 sparams0 ev_genv0
    158154
     
    160156    (AST.ident List.list -> Joint_semantics.sem_params ->
    161157    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    162 let rec evaluation_params_rect_Type3 h_mk_evaluation_params x_26090 =
    163   let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } =
    164     x_26090
    165   in
     158let rec evaluation_params_rect_Type3 h_mk_evaluation_params x_7 =
     159  let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } = x_7 in
    166160  h_mk_evaluation_params globals0 sparams0 ev_genv0
    167161
     
    169163    (AST.ident List.list -> Joint_semantics.sem_params ->
    170164    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    171 let rec evaluation_params_rect_Type2 h_mk_evaluation_params x_26092 =
    172   let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } =
    173     x_26092
    174   in
     165let rec evaluation_params_rect_Type2 h_mk_evaluation_params x_9 =
     166  let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } = x_9 in
    175167  h_mk_evaluation_params globals0 sparams0 ev_genv0
    176168
     
    178170    (AST.ident List.list -> Joint_semantics.sem_params ->
    179171    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    180 let rec evaluation_params_rect_Type1 h_mk_evaluation_params x_26094 =
    181   let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } =
    182     x_26094
     172let rec evaluation_params_rect_Type1 h_mk_evaluation_params x_11 =
     173  let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } = x_11
    183174  in
    184175  h_mk_evaluation_params globals0 sparams0 ev_genv0
     
    187178    (AST.ident List.list -> Joint_semantics.sem_params ->
    188179    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    189 let rec evaluation_params_rect_Type0 h_mk_evaluation_params x_26096 =
    190   let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } =
    191     x_26096
     180let rec evaluation_params_rect_Type0 h_mk_evaluation_params x_13 =
     181  let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } = x_13
    192182  in
    193183  h_mk_evaluation_params globals0 sparams0 ev_genv0
     
    279269    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    280270    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    281 let rec prog_params_rect_Type4 h_mk_prog_params x_26112 =
     271let rec prog_params_rect_Type4 h_mk_prog_params x_29 =
    282272  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    283     stack_sizes0 } = x_26112
     273    stack_sizes0 } = x_29
    284274  in
    285275  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    288278    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    289279    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    290 let rec prog_params_rect_Type5 h_mk_prog_params x_26114 =
     280let rec prog_params_rect_Type5 h_mk_prog_params x_31 =
    291281  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    292     stack_sizes0 } = x_26114
     282    stack_sizes0 } = x_31
    293283  in
    294284  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    297287    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    298288    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    299 let rec prog_params_rect_Type3 h_mk_prog_params x_26116 =
     289let rec prog_params_rect_Type3 h_mk_prog_params x_33 =
    300290  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    301     stack_sizes0 } = x_26116
     291    stack_sizes0 } = x_33
    302292  in
    303293  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    306296    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    307297    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    308 let rec prog_params_rect_Type2 h_mk_prog_params x_26118 =
     298let rec prog_params_rect_Type2 h_mk_prog_params x_35 =
    309299  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    310     stack_sizes0 } = x_26118
     300    stack_sizes0 } = x_35
    311301  in
    312302  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    315305    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    316306    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    317 let rec prog_params_rect_Type1 h_mk_prog_params x_26120 =
     307let rec prog_params_rect_Type1 h_mk_prog_params x_37 =
    318308  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    319     stack_sizes0 } = x_26120
     309    stack_sizes0 } = x_37
    320310  in
    321311  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    324314    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    325315    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    326 let rec prog_params_rect_Type0 h_mk_prog_params x_26122 =
     316let rec prog_params_rect_Type0 h_mk_prog_params x_39 =
    327317  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    328     stack_sizes0 } = x_26122
     318    stack_sizes0 } = x_39
    329319  in
    330320  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    555545        (match s with
    556546         | Joint.COST_LABEL x0 -> dummy
    557          | Joint.CALL (x0, x1, x2) -> dummy
     547         | Joint.CALL (f', args, dest) ->
     548           (match Obj.magic
     549                    (Monad.m_bind0 (Monad.max_def Errors.res0)
     550                      (Joint_semantics.block_of_call p.sparams p.globals
     551                        (let p0 = p.sparams.Joint_semantics.spp in
     552                        let globals0 = p.globals in
     553                        let g = p.ev_genv in g.Joint_semantics.ge) f'
     554                        st.Joint_semantics.st_no_pc) (fun bl ->
     555                      Obj.magic
     556                        (Joint_semantics.fetch_internal_function
     557                          (let p0 = p.sparams.Joint_semantics.spp in
     558                          let globals0 = p.globals in
     559                          let g = p.ev_genv in g.Joint_semantics.ge) bl))) with
     560            | Errors.OK i_f -> i_f.Types.fst
     561            | Errors.Error x0 -> dummy)
    558562         | Joint.COND (x0, x1) -> dummy
    559          | Joint.Step_seq s0 ->
    560            (match Joint.Step_seq
    561             s0 with
    562             | Joint.COST_LABEL x0 -> dummy
    563             | Joint.CALL (f', args, dest) ->
    564               (match Obj.magic
    565                        (Monad.m_bind0 (Monad.max_def Errors.res0)
    566                          (Joint_semantics.block_of_call p.sparams p.globals
    567                            (let p0 = p.sparams.Joint_semantics.spp in
    568                            let globals0 = p.globals in
    569                            let g = p.ev_genv in g.Joint_semantics.ge) f'
    570                            st.Joint_semantics.st_no_pc) (fun bl ->
    571                          Obj.magic
    572                            (Joint_semantics.fetch_internal_function
    573                              (let p0 = p.sparams.Joint_semantics.spp in
    574                              let globals0 = p.globals in
    575                              let g = p.ev_genv in g.Joint_semantics.ge) bl))) with
    576                | Errors.OK i_f -> i_f.Types.fst
    577                | Errors.Error x0 -> dummy)
    578             | Joint.COND (x0, x1) -> dummy
    579             | Joint.Step_seq x0 -> dummy))
     563         | Joint.Step_seq x0 -> dummy)
    580564      | Joint.Final x0 -> dummy
    581565      | Joint.FCOND (x0, x1, x2) -> dummy)
Note: See TracChangeset for help on using the changeset viewer.