Ignore:
Timestamp:
Apr 4, 2013, 9:58:03 AM (7 years ago)
Author:
sacerdot
Message:

The cost and stack* variables are now initialized with the cost of
the pre-main and the size of globals.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/compiler.mli

    r3059 r3083  
    320320val back_end :
    321321  observe_pass -> CostLabel.costlabel -> RTLabs_syntax.rTLabs_program ->
    322   ((ASM.pseudo_assembly_program, Joint.stack_cost_model) Types.prod, Nat.nat)
    323   Types.prod Errors.res
     322  (((ASM.pseudo_assembly_program, CostLabel.costlabel) Types.prod,
     323  Joint.stack_cost_model) Types.prod, Nat.nat) Types.prod Errors.res
    324324
    325325open Assembly
     
    363363                         c_stack_cost : Joint.stack_cost_model;
    364364                         c_max_stack : Nat.nat;
     365                         c_init_costlabel : CostLabel.costlabel;
    365366                         c_labelled_clight : Csyntax.clight_program;
    366367                         c_clight_cost_map : Label.clight_cost_map }
     
    368369val compiler_output_rect_Type4 :
    369370  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
    370   Csyntax.clight_program -> Label.clight_cost_map -> 'a1) -> compiler_output
    371   -> 'a1
     371  CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
     372  'a1) -> compiler_output -> 'a1
    372373
    373374val compiler_output_rect_Type5 :
    374375  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
    375   Csyntax.clight_program -> Label.clight_cost_map -> 'a1) -> compiler_output
    376   -> 'a1
     376  CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
     377  'a1) -> compiler_output -> 'a1
    377378
    378379val compiler_output_rect_Type3 :
    379380  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
    380   Csyntax.clight_program -> Label.clight_cost_map -> 'a1) -> compiler_output
    381   -> 'a1
     381  CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
     382  'a1) -> compiler_output -> 'a1
    382383
    383384val compiler_output_rect_Type2 :
    384385  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
    385   Csyntax.clight_program -> Label.clight_cost_map -> 'a1) -> compiler_output
    386   -> 'a1
     386  CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
     387  'a1) -> compiler_output -> 'a1
    387388
    388389val compiler_output_rect_Type1 :
    389390  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
    390   Csyntax.clight_program -> Label.clight_cost_map -> 'a1) -> compiler_output
    391   -> 'a1
     391  CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
     392  'a1) -> compiler_output -> 'a1
    392393
    393394val compiler_output_rect_Type0 :
    394395  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
    395   Csyntax.clight_program -> Label.clight_cost_map -> 'a1) -> compiler_output
    396   -> 'a1
     396  CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
     397  'a1) -> compiler_output -> 'a1
    397398
    398399val c_labelled_object_code : compiler_output -> ASM.labelled_object_code
     
    401402
    402403val c_max_stack : compiler_output -> Nat.nat
     404
     405val c_init_costlabel : compiler_output -> CostLabel.costlabel
    403406
    404407val c_labelled_clight : compiler_output -> Csyntax.clight_program
     
    408411val compiler_output_inv_rect_Type4 :
    409412  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
    410   Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1) ->
    411   'a1
     413  Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
     414  Label.clight_cost_map -> __ -> 'a1) -> 'a1
    412415
    413416val compiler_output_inv_rect_Type3 :
    414417  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
    415   Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1) ->
    416   'a1
     418  Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
     419  Label.clight_cost_map -> __ -> 'a1) -> 'a1
    417420
    418421val compiler_output_inv_rect_Type2 :
    419422  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
    420   Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1) ->
    421   'a1
     423  Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
     424  Label.clight_cost_map -> __ -> 'a1) -> 'a1
    422425
    423426val compiler_output_inv_rect_Type1 :
    424427  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
    425   Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1) ->
    426   'a1
     428  Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
     429  Label.clight_cost_map -> __ -> 'a1) -> 'a1
    427430
    428431val compiler_output_inv_rect_Type0 :
    429432  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
    430   Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1) ->
    431   'a1
    432 
    433 val compiler_output_discr : compiler_output -> compiler_output -> __
     433  Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
     434  Label.clight_cost_map -> __ -> 'a1) -> 'a1
    434435
    435436val compiler_output_jmdiscr : compiler_output -> compiler_output -> __
Note: See TracChangeset for help on using the changeset viewer.