open Preamble

open CostLabel

open Coqlib

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Lists

open Positive

open Identifiers

open Exp

open Arithmetic

open Vector

open Div_and_mod

open Util

open FoldStuff

open BitVector

open Jmeq

open Russell

open List

open Setoids

open Monad

open Option

open Extranat

open Bool

open Relations

open Nat

open Integers

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open AST

open Csyntax

val labels_of_expr : Csyntax.expr -> CostLabel.costlabel List.list

val labels_of_labeled_statements :
  Csyntax.labeled_statements -> CostLabel.costlabel List.list

val labels_of_statement : Csyntax.statement -> CostLabel.costlabel List.list

val labels_of_clight_fundef :
  (AST.ident, Csyntax.clight_fundef) Types.prod -> CostLabel.costlabel
  List.list

val labels_of_clight :
  Csyntax.clight_program -> CostLabel.costlabel List.list

type in_clight_label = CostLabel.costlabel Types.sig0

type clight_cost_map = CostLabel.costlabel -> Nat.nat

val clight_label_free : Csyntax.clight_program -> Bool.bool

val add_cost_before :
  Csyntax.statement -> Identifiers.universe -> (Csyntax.statement,
  Identifiers.universe) Types.prod

val add_cost_after :
  Csyntax.statement -> Identifiers.universe -> (Csyntax.statement,
  Identifiers.universe) Types.prod

val add_cost_expr :
  Csyntax.expr -> Identifiers.universe -> (Csyntax.expr,
  Identifiers.universe) Types.prod

val const_int : AST.intsize -> Nat.nat -> Csyntax.expr

val label_expr_descr :
  Csyntax.expr_descr -> Identifiers.universe -> Csyntax.type0 ->
  (Csyntax.expr_descr, Identifiers.universe) Types.prod

val label_expr :
  Csyntax.expr -> Identifiers.universe -> (Csyntax.expr,
  Identifiers.universe) Types.prod

val label_exprs :
  Csyntax.expr List.list -> Identifiers.universe -> (Csyntax.expr List.list,
  Identifiers.universe) Types.prod

val label_opt_expr :
  Csyntax.expr Types.option -> Identifiers.universe -> (Csyntax.expr
  Types.option, Identifiers.universe) Types.prod

val label_lstatements :
  Csyntax.labeled_statements -> Identifiers.universe ->
  (Csyntax.labeled_statements, Identifiers.universe) Types.prod

val label_statement :
  Csyntax.statement -> Identifiers.universe -> (Csyntax.statement,
  Identifiers.universe) Types.prod

val label_function :
  Identifiers.universe -> Csyntax.function0 -> (Csyntax.function0,
  Identifiers.universe) Types.prod

val label_fundef :
  Identifiers.universe -> Csyntax.clight_fundef -> (Csyntax.clight_fundef,
  Identifiers.universe) Types.prod

val clight_label :
  Csyntax.clight_program -> (Csyntax.clight_program, CostLabel.costlabel)
  Types.prod