archetype 0.1.11 · OCaml Package

val function_name_from_storage_const : storage_const -> Ident.ident

val function_name_from_container_const : container_const -> Ident.ident

val function_name_from_function_const : function_const -> Ident.ident

val function_name_from_builtin_const : builtin_const -> Ident.ident

val get_vars : model -> var list

val get_enums : model -> enum list

val get_assets : model -> asset list

val get_var : model -> Ident.ident -> var

val get_enum : model -> Ident.ident -> enum

val get_asset : model -> Ident.ident -> asset

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 * btyp

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 * btyp

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 dest_array : mterm -> mterm list

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_fields : model -> Ident.ident -> Ident.ident list

val get_added_removed_sets : model -> specification option -> mterm__node 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 get_default_value : model -> type_ -> mterm

val with_transfer_for_mterm : mterm -> bool

val with_transfer : model -> bool

package archetype