]> matita.cs.unibo.it Git - pkg-cerco/acc-trusted.git/blob - clightPrinter.mli
Control and copyright added.
[pkg-cerco/acc-trusted.git] / clightPrinter.mli
1 (** This module provides functions to print elements of [Extracted.Csyntax]
2     programs. *)
3
4 type cost_style =
5 | Cost_plain
6 | Cost_numbered of Extracted.Label.clight_cost_map * Extracted.CostLabel.costlabel * Extracted.Joint.stack_cost_model * Extracted.Nat.nat
7 | Cost_instrumented of Extracted.Label.clight_cost_map * Extracted.CostLabel.costlabel * Extracted.Joint.stack_cost_model * Extracted.Nat.nat
8
9 val print_program: cost_style -> Extracted.Csyntax.clight_program -> string
10
11 val print_expression: cost_style -> Extracted.Csyntax.expr -> string
12
13 val string_of_ctype: Extracted.Csyntax.type0 -> string
14
15 val print_statement: cost_style -> Extracted.Csyntax.statement -> string
16
17 val print_ctype_prot: Extracted.Csyntax.type0 -> string
18
19 val print_ctype_def: Extracted.Csyntax.type0 -> string
20
21 val string_of_unop : Extracted.Csyntax.unary_operation -> string
22
23 val string_of_binop : Extracted.Csyntax.binary_operation -> string