Crate (soteria-rust.Soteria_rust

exception MissingDecl of string

type t = Charon.UllbcAst.crate

type Stdlib.Effect.t +=

val get_crate : unit -> t

val with_crate : t -> (unit -> 'a) -> 'a

val pointer_size : unit -> int

val as_namematcher_ctx : unit -> Charon.UllbcAst.blocks Charon.NameMatcher.ctx

val as_fmt_env : unit -> Charon__PrintUllbcAst.fmt_env

val mk_pp : 
  (Charon__PrintUllbcAst.fmt_env -> 'a -> string) ->
  Stdlib.Format.formatter ->
  'a ->
  unit

val mk_pp_indent : 
  (Charon__PrintUllbcAst.fmt_env -> string -> 'a -> string) ->
  Stdlib.Format.formatter ->
  'a ->
  unit

val pp_constant_expr : 
  Stdlib.Format.formatter ->
  Charon.Types.constant_expr ->
  unit

val pp_fn_operand : Stdlib.Format.formatter -> Charon.GAst.fn_operand -> unit

val pp_fun_decl_ref : 
  Stdlib.Format.formatter ->
  Charon.Types.fun_decl_ref ->
  unit

val pp_generic_args : 
  Stdlib.Format.formatter ->
  Charon.Types.generic_args ->
  unit

val pp_generic_params : 
  Stdlib.Format.formatter ->
  Charon.Types.generic_params ->
  unit

val pp_global_decl_ref : 
  Stdlib.Format.formatter ->
  Charon.Types.global_decl_ref ->
  unit

val pp_name : Stdlib.Format.formatter -> Charon.Types.name -> unit

val pp_place : Stdlib.Format.formatter -> Charon.Expressions.place -> unit

val pp_trait_ref : Stdlib.Format.formatter -> Charon.Types.trait_ref -> unit

val pp_statement : Stdlib.Format.formatter -> Charon.UllbcAst.statement -> unit

val pp_terminator : 
  Stdlib.Format.formatter ->
  Charon.UllbcAst.terminator ->
  unit

val get_adt_raw : Charon.Types.TypeDeclId.Map.key -> Charon.Types.type_decl

val get_adt : Charon.Types.type_decl_ref -> Charon.Types.type_decl

Gets an ADT in the crate, and applies the given generic arguments to it.

val get_fun : 
  Charon.UllbcAst.FunDeclId.Map.key ->
  Charon.UllbcAst.blocks Charon.UllbcAst.gfun_decl

val get_global : 
  Charon.UllbcAst.GlobalDeclId.Map.key ->
  Charon.UllbcAst.global_decl

val get_trait_impl_raw : 
  Charon.UllbcAst.TraitImplId.Map.key ->
  Charon.UllbcAst.trait_impl

val get_trait_impl : Charon.Types.trait_impl_ref -> Charon.GAst.trait_impl

val get_trait_decl_raw : 
  Charon.Types.TraitDeclId.Map.key ->
  Charon.UllbcAst.trait_decl

val get_trait_decl : Charon.Types.trait_decl_ref -> Charon.GAst.trait_decl

val is_enum : Charon.Types.type_decl_ref -> bool

val is_struct : Charon.Types.type_decl_ref -> bool

val is_union : Charon.Types.type_decl_ref -> bool

val as_enum : Charon.Types.type_decl_ref -> Charon.Types.variant list

val as_struct : Charon.Types.type_decl_ref -> Charon.Types.field list

val as_struct_or_tuple : Charon.Types.type_decl_ref -> Charon.Types.ty list

val as_union : Charon.Types.type_decl_ref -> Charon.Types.field list