source: driver/clightPrinter.mli @ 2787

Last change on this file since 2787 was 2787, checked in by campbell, 8 years ago

Output stack costs in driver.

File size: 825 bytes
RevLine 
[2758]1(** This module provides functions to print elements of [Extracted.Csyntax]
2    programs. *)
3
[2759]4type cost_style =
5| Cost_plain
[2787]6| Cost_numbered of Extracted.Label.clight_cost_map * Extracted.Joint.stack_cost_model
7| Cost_instrumented of Extracted.Label.clight_cost_map * Extracted.Joint.stack_cost_model
[2758]8
[2759]9val print_program: cost_style -> Extracted.Csyntax.clight_program -> string
[2758]10
[2759]11val print_expression: cost_style -> Extracted.Csyntax.expr -> string
12
[2758]13val string_of_ctype: Extracted.Csyntax.type0 -> string
14
[2759]15val print_statement: cost_style -> Extracted.Csyntax.statement -> string
[2758]16
17val print_ctype_prot: Extracted.Csyntax.type0 -> string
18
19val print_ctype_def: Extracted.Csyntax.type0 -> string
20
21val string_of_unop : Extracted.Csyntax.unary_operation -> string
22
23val string_of_binop : Extracted.Csyntax.binary_operation -> string
Note: See TracBrowser for help on using the repository browser.