Changeset 2797 for extracted/compiler.ml


Ignore:
Timestamp:
Mar 7, 2013, 12:55:34 PM (7 years ago)
Author:
sacerdot
Message:

Extracted again after James's cleanup and the implementation of the
new testing function to be used in the untrusted code.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/compiler.ml

    r2775 r2797  
    286286  let { Types.fst = p3; Types.snd = stack_cost } = eta29073 in
    287287  let p4 = LTLToLIN.ltl_to_lin p3 in
    288   let p5 = LINToASM.lin_to_asm p4 in
    289   (match p5 with
    290    | Types.None -> Errors.Error (Errors.msg ErrorMessages.AssemblyTooLarge)
    291    | Types.Some p6 ->
    292      Errors.OK { Types.fst = { Types.fst = p6; Types.snd = stack_cost };
    293        Types.snd = max_stack })
     288  Obj.magic
     289    (Monad.m_bind0 (Monad.max_def Errors.res0)
     290      (Obj.magic
     291        (Errors.opt_to_res (Errors.msg ErrorMessages.AssemblyTooLarge)
     292          (LINToASM.lin_to_asm p4))) (fun p5 ->
     293      Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = { Types.fst =
     294        p5; Types.snd = stack_cost }; Types.snd = max_stack }))
    294295
    295296open Assembly
     
    351352    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    352353    compiler_output -> 'a1 **)
    353 let rec compiler_output_rect_Type4 h_mk_compiler_output x_24820 =
     354let rec compiler_output_rect_Type4 h_mk_compiler_output x_24899 =
    354355  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    355356    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    356     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_24820
     357    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_24899
    357358  in
    358359  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    363364    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    364365    compiler_output -> 'a1 **)
    365 let rec compiler_output_rect_Type5 h_mk_compiler_output x_24822 =
     366let rec compiler_output_rect_Type5 h_mk_compiler_output x_24901 =
    366367  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    367368    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    368     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_24822
     369    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_24901
    369370  in
    370371  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    375376    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    376377    compiler_output -> 'a1 **)
    377 let rec compiler_output_rect_Type3 h_mk_compiler_output x_24824 =
     378let rec compiler_output_rect_Type3 h_mk_compiler_output x_24903 =
    378379  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    379380    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    380     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_24824
     381    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_24903
    381382  in
    382383  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    387388    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    388389    compiler_output -> 'a1 **)
    389 let rec compiler_output_rect_Type2 h_mk_compiler_output x_24826 =
     390let rec compiler_output_rect_Type2 h_mk_compiler_output x_24905 =
    390391  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    391392    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    392     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_24826
     393    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_24905
    393394  in
    394395  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    399400    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    400401    compiler_output -> 'a1 **)
    401 let rec compiler_output_rect_Type1 h_mk_compiler_output x_24828 =
     402let rec compiler_output_rect_Type1 h_mk_compiler_output x_24907 =
    402403  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    403404    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    404     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_24828
     405    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_24907
    405406  in
    406407  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    411412    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    412413    compiler_output -> 'a1 **)
    413 let rec compiler_output_rect_Type0 h_mk_compiler_output x_24830 =
     414let rec compiler_output_rect_Type0 h_mk_compiler_output x_24909 =
    414415  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    415416    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    416     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_24830
     417    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_24909
    417418  in
    418419  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
Note: See TracChangeset for help on using the changeset viewer.