Ignore:
Timestamp:
Mar 25, 2013, 11:30:01 PM (7 years ago)
Author:
sacerdot
Message:

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/measurable.mli

    r2903 r2951  
    100100
    101101open StructuredTraces
     102
     103open Stacksize
    102104
    103105type classified_system = { cs_exec : (IO.io_out, IO.io_in)
     
    197199
    198200val measure_stack :
    199   (AST.ident -> Nat.nat) -> Nat.nat -> StructuredTraces.intensional_event
    200   List.list -> (Nat.nat, Nat.nat) Types.prod
    201 
    202 val max_stack :
    203   (AST.ident -> Nat.nat) -> Nat.nat -> StructuredTraces.intensional_event
    204   List.list -> Nat.nat
     201  (AST.ident -> Nat.nat Types.option) -> Stacksize.stacksize_info ->
     202  StructuredTraces.intensional_event List.list -> Stacksize.stacksize_info
    205203
    206204val will_return_aux :
Note: See TracChangeset for help on using the changeset viewer.