Changeset 2960 for extracted/compiler.ml


Ignore:
Timestamp:
Mar 26, 2013, 4:51:40 PM (7 years ago)
Author:
sacerdot
Message:

New extraction, it diverges in RTL execution now.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/compiler.ml

    r2951 r2960  
    496496(** val compute_fixpoint : Fixpoints.fixpoint_computer **)
    497497let compute_fixpoint = Compute_fixpoints.compute_fixpoint
    498 
     498 
    499499(** val colour_graph : Interference.coloured_graph_computer **)
    500500let colour_graph = Compute_colouring.colour_graph
     
    531531  let i2 = Obj.magic observe Ertlptr_pass { Types.fst = p2; Types.snd = st1 }
    532532  in
    533   let { Types.fst = eta24710; Types.snd = max_stack } =
     533  let { Types.fst = eta665; Types.snd = max_stack } =
    534534    ERTLptrToLTL.ertlptr_to_ltl compute_fixpoint colour_graph p2
    535535  in
    536   let { Types.fst = p3; Types.snd = stack_cost } = eta24710 in
     536  let { Types.fst = p3; Types.snd = stack_cost } = eta665 in
    537537  let st2 = lookup_stack_cost (Joint.graph_params_to_params LTL.lTL) p3 in
    538538  let i3 = Obj.magic observe Ltl_pass { Types.fst = p3; Types.snd = st2 } in
     
    615615    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    616616    compiler_output -> 'a1 **)
    617 let rec compiler_output_rect_Type4 h_mk_compiler_output x_4341 =
     617let rec compiler_output_rect_Type4 h_mk_compiler_output x_589 =
    618618  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    619619    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    620     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_4341
     620    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_589
    621621  in
    622622  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    627627    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    628628    compiler_output -> 'a1 **)
    629 let rec compiler_output_rect_Type5 h_mk_compiler_output x_4343 =
     629let rec compiler_output_rect_Type5 h_mk_compiler_output x_591 =
    630630  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    631631    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    632     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_4343
     632    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_591
    633633  in
    634634  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    639639    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    640640    compiler_output -> 'a1 **)
    641 let rec compiler_output_rect_Type3 h_mk_compiler_output x_4345 =
     641let rec compiler_output_rect_Type3 h_mk_compiler_output x_593 =
    642642  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    643643    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    644     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_4345
     644    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_593
    645645  in
    646646  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    651651    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    652652    compiler_output -> 'a1 **)
    653 let rec compiler_output_rect_Type2 h_mk_compiler_output x_4347 =
     653let rec compiler_output_rect_Type2 h_mk_compiler_output x_595 =
    654654  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    655655    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    656     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_4347
     656    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_595
    657657  in
    658658  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    663663    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    664664    compiler_output -> 'a1 **)
    665 let rec compiler_output_rect_Type1 h_mk_compiler_output x_4349 =
     665let rec compiler_output_rect_Type1 h_mk_compiler_output x_597 =
    666666  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    667667    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    668     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_4349
     668    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_597
    669669  in
    670670  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    675675    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    676676    compiler_output -> 'a1 **)
    677 let rec compiler_output_rect_Type0 h_mk_compiler_output x_4351 =
     677let rec compiler_output_rect_Type0 h_mk_compiler_output x_599 =
    678678  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    679679    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    680     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_4351
     680    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_599
    681681  in
    682682  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
Note: See TracChangeset for help on using the changeset viewer.