Module `Model.Utils`Source

Sourceval function_name_from_storage_const : storage_const -> string

Sourceval function_name_from_container_const : container_const -> string

Sourceval function_name_from_function_const : function_const -> string

Sourceval function_name_from_builtin_const : builtin_const -> string

Sourceval get_assets : model -> info_asset list

Sourceval get_records : model -> record list

Sourceval get_variables : model -> storage_item list

Sourceval get_storage : model -> storage

Sourceval get_info_asset : model -> lident -> info_asset

Source

val get_asset_field : 
  model ->
  (lident * Ident.ident) ->
  Ident.ident * type_ * mterm option

Sourceval get_asset_key : model -> lident -> Ident.ident * btyp

Source

val get_field_container : 
  model ->
  Ident.ident ->
  Ident.ident ->
  Ident.ident * container

Sourceval is_storage_attribute : model -> lident -> bool

Source

val get_named_field_list : 
  model ->
  lident ->
  'a list ->
  (Ident.ident * 'a) list

Sourceval get_partitions : model -> (Ident.ident * Ident.ident * type_) list

Sourceval dest_partition : type_ -> lident

Source

val get_partition_asset_key : 
  model ->
  lident ->
  lident ->
  Ident.ident * Ident.ident * btyp

Sourceval get_partition_assets : model -> Ident.ident -> Ident.ident list

Sourceval get_entries : model -> (specification option * function_struct) list

Source

val get_functions : 
  model ->
  (specification option * function_struct * type_) list

Sourceval has_partition : model -> Ident.ident -> bool

Source

val get_asset_partitions : 
  model ->
  Ident.ident ->
  (Ident.ident * type_ * mterm option) list

Sourceval get_field_list : model -> lident -> Ident.ident list

Sourceval get_field_pos : model -> lident -> lident -> int

Sourceval get_nth_record_val : int -> mterm -> mterm

Sourceval dest_array : mterm -> mterm list

Sourceval get_asset_type : mterm -> lident

Sourceval is_local_assigned : lident -> mterm -> bool

Sourceval get_function_args : function__ -> argument list

Sourceval set_function_args : function__ -> argument list -> function__

Sourceval map_function_terms : (mterm -> mterm) -> function__ -> function__

Sourceval is_record : mterm -> bool

Sourceval is_varlocal : mterm -> bool

Sourceval dest_varlocal : mterm -> lident

Sourceval is_container : type_ -> bool

Sourceval get_key_pos : model -> lident -> int

Source

val get_loop_invariants : 
  model ->
  (lident * mterm) list ->
  Ident.ident ->
  (lident * mterm) list

Sourceval get_formula : model -> mterm option -> Ident.ident -> mterm option

Sourceval is_post : postcondition -> bool

Sourceval get_sum_fields : model -> Ident.ident -> Ident.ident list

Source

val get_added_removed_sets : 
  model ->
  specification option ->
  (lident, lident mterm_gen) mterm_node list

Source

val get_storage_invariants : 
  model ->
  Ident.ident option ->
  (Ident.ident * Ident.ident * mterm) list

Sourceval is_field_storage : model -> Ident.ident -> bool

Sourceval with_trace : model -> bool

Sourceval get_callers : model -> Ident.ident -> Ident.ident list

Sourceval no_fail : model -> Ident.ident -> lident option

Sourceval type_to_asset : type_ -> lident

Sourceval get_map_function : model -> (Ident.ident * Ident.ident list) list

Sourceval retrieve_all_properties : model -> (Ident.ident * property) list

Sourceval retrieve_property : model -> Ident.ident -> property

package archetype

Module Model.UtilsSource

Module `Model.Utils`Source