63 open Hints_declaration
77 val labels_of_expr : Csyntax.expr -> CostLabel.costlabel List.list
79 val labels_of_labeled_statements :
80 Csyntax.labeled_statements -> CostLabel.costlabel List.list
82 val labels_of_statement : Csyntax.statement -> CostLabel.costlabel List.list
84 val labels_of_clight_fundef :
85 (AST.ident, Csyntax.clight_fundef) Types.prod -> CostLabel.costlabel
88 val labels_of_clight :
89 Csyntax.clight_program -> CostLabel.costlabel List.list
91 type in_clight_label = CostLabel.costlabel Types.sig0
93 type clight_cost_map = CostLabel.costlabel -> Nat.nat
95 val clight_label_free : Csyntax.clight_program -> Bool.bool
98 Csyntax.statement -> Identifiers.universe -> (Csyntax.statement,
99 Identifiers.universe) Types.prod
102 Csyntax.statement -> Identifiers.universe -> (Csyntax.statement,
103 Identifiers.universe) Types.prod
106 Csyntax.expr -> Identifiers.universe -> (Csyntax.expr,
107 Identifiers.universe) Types.prod
109 val const_int : AST.intsize -> Nat.nat -> Csyntax.expr
111 val label_expr_descr :
112 Csyntax.expr_descr -> Identifiers.universe -> Csyntax.type0 ->
113 (Csyntax.expr_descr, Identifiers.universe) Types.prod
116 Csyntax.expr -> Identifiers.universe -> (Csyntax.expr,
117 Identifiers.universe) Types.prod
120 Csyntax.expr List.list -> Identifiers.universe -> (Csyntax.expr List.list,
121 Identifiers.universe) Types.prod
124 Csyntax.expr Types.option -> Identifiers.universe -> (Csyntax.expr
125 Types.option, Identifiers.universe) Types.prod
127 val label_lstatements :
128 Csyntax.labeled_statements -> Identifiers.universe ->
129 (Csyntax.labeled_statements, Identifiers.universe) Types.prod
131 val label_statement :
132 Csyntax.statement -> Identifiers.universe -> (Csyntax.statement,
133 Identifiers.universe) Types.prod
136 Identifiers.universe -> Csyntax.function0 -> (Csyntax.function0,
137 Identifiers.universe) Types.prod
140 Identifiers.universe -> Csyntax.clight_fundef -> (Csyntax.clight_fundef,
141 Identifiers.universe) Types.prod
144 Csyntax.clight_program -> (Csyntax.clight_program, CostLabel.costlabel)