package archetype

  1. Overview
  2. Docs
val get_vars : model -> var list
val get_enums : model -> enum list
val get_assets : model -> asset list
val get_records : model -> record list
val get_var : model -> Ident.ident -> var
val get_var_opt : model -> Ident.ident -> var option
val get_enum : model -> Ident.ident -> enum
val get_enum_opt : model -> Ident.ident -> enum option
val get_enum_values : model -> Ident.ident -> Ident.ident list
val get_asset : model -> Ident.ident -> asset
val get_record : model -> Ident.ident -> record
val get_event : model -> Ident.ident -> record
val get_events : model -> record list
val get_storage : model -> storage
val get_asset_field : model -> (Ident.ident * Ident.ident) -> Ident.ident * type_ * mterm option
val get_asset_key : model -> Ident.ident -> Ident.ident * type_
val get_asset_value : model -> Ident.ident -> type_
val get_field_container : model -> Ident.ident -> Ident.ident -> Ident.ident * container
val is_storage_attribute : model -> Ident.ident -> bool
val get_named_field_list : model -> Ident.ident -> 'a list -> (Ident.ident * 'a) list
val get_containers : model -> (Ident.ident * Ident.ident * type_) list
val get_partitions : model -> (Ident.ident * Ident.ident * type_) list
val dest_container : type_ -> Ident.ident
val get_container_asset_key : model -> Ident.ident -> Ident.ident -> Ident.ident * Ident.ident * type_
val get_container_assets : model -> Ident.ident -> Ident.ident list
val get_entries : model -> (specification option * function_struct) list
val get_functions : model -> (specification option * function_struct * type_) list
val has_container : model -> Ident.ident -> bool
val get_asset_containers : model -> Ident.ident -> (Ident.ident * type_ * mterm option) list
val get_field_list : model -> Ident.ident -> Ident.ident list
val get_field_pos : model -> Ident.ident -> Ident.ident -> int
val get_nth_asset_val : int -> mterm -> mterm
val get_asset_type : mterm -> Ident.ident
val is_local_assigned : Ident.ident -> mterm -> bool
val get_function_args : function__ -> argument list
val set_function_args : function__ -> argument list -> function__
val map_function_terms : (mterm -> mterm) -> function__ -> function__
val is_asset : mterm -> bool
val is_varlocal : mterm -> bool
val dest_varlocal : mterm -> Ident.ident
val is_container : type_ -> bool
val get_key_pos : model -> Ident.ident -> int
val get_loop_invariants : model -> (Ident.ident * mterm) list -> Ident.ident -> (Ident.ident * mterm) list
val get_formula : model -> mterm option -> Ident.ident -> mterm option
val is_post : postcondition -> bool
val get_sum_idxs : model -> Ident.ident -> int list
val get_storage_invariants : model -> Ident.ident option -> (Ident.ident * Ident.ident * mterm) list
val is_field_storage : model -> Ident.ident -> bool
val with_trace : model -> bool
val get_callers : model -> Ident.ident -> Ident.ident list
val no_fail : model -> Ident.ident -> Ident.ident option
val type_to_asset : type_ -> Ident.ident
val get_map_function : model -> (Ident.ident * Ident.ident list) list
val retrieve_all_properties : model -> (Ident.ident * property) list
val retrieve_property : model -> Ident.ident -> property
val with_operations_for_mterm : mterm -> bool
val with_operations : model -> bool
val get_source_for : model -> ctx_model -> mterm -> mterm option
val cmp : mterm -> mterm -> int
val eval : (Ident.ident * mterm) list -> mterm -> mterm
val mk_rat : Core.big_int -> Core.big_int -> mterm
val get_select_idx : model -> Ident.ident -> mterm -> int
val get_sum_idx : model -> Ident.ident -> mterm -> int
val get_removeif_idx : model -> Ident.ident -> mterm -> int
val with_division : model -> bool
val with_min_max : model -> bool
val with_count : model -> Ident.ident -> bool
val get_asset_collection : Ident.ident -> mterm
val is_asset_single_field : model -> Ident.ident -> bool
val is_asset_map : model -> Ident.ident -> bool
val get_labeled_value_from : model -> Ident.ident -> mterm list -> (Ident.ident * mterm) list
val add_api_storage_in_list : api_storage list -> api_storage -> api_storage list
val sort_api_storage : model -> bool -> api_storage list -> api_storage list
val get_all_set_types : model -> type_ list
val get_all_list_types : model -> type_ list
val get_all_map_types : model -> type_ list
val get_all_fail_types : model -> type_ list
val get_all_gen_mterm_type : ('a list -> mterm -> 'a list) -> ('a list -> type_ -> 'a list) -> (decl_node -> 'a list -> 'a list) -> model -> 'a list
val get_all_type_for_mterm : ('a -> type_ -> 'a) -> 'a -> mterm -> 'a
val extract_key_value_from_masset : model -> mterm -> mterm
val is_not_string_nat_int : type_ -> bool
val get_function : model -> Ident.ident -> function_struct
val get_asset_partitions : model -> Ident.ident -> (Ident.ident * Ident.ident) list
val get_specifications : model -> specification list
val get_specification : model -> Ident.ident -> specification option
val get_fss : model -> function_struct list
val get_fs : model -> Ident.ident -> function_struct
val extract_assign_kind : mterm -> assign_kind list
val extract_asset_effect : model -> mterm -> effect list
val extract_var_idents : model -> mterm -> Ident.ident list
val get_record_pos : model -> Ident.ident -> Ident.ident -> (int * int) list
val is_partition : model -> Ident.ident -> Ident.ident -> bool
OCaml

Innovation. Community. Security.