63 open Hints_declaration
77 val max_id : AST.ident -> AST.ident -> AST.ident
80 (AST.ident, Csyntax.type0) Types.prod List.list -> AST.ident
82 val max_id_of_fn : Csyntax.function0 -> AST.ident
84 val max_id_of_fundef : Csyntax.clight_fundef -> AST.ident
86 val max_id_of_functs :
87 (AST.ident, Csyntax.clight_fundef) Types.prod List.list -> AST.ident
89 val max_id_of_globvars :
90 ((AST.ident, AST.region) Types.prod, (AST.init_data List.list,
91 Csyntax.type0) Types.prod) Types.prod List.list -> AST.ident
93 val max_id_of_program : Csyntax.clight_program -> AST.ident
95 val universe_of_max : AST.ident -> Identifiers.universe
97 val universe_for_program : Csyntax.clight_program -> Identifiers.universe