cprover
|
Abstract nodes may assume any of a set of pre-defined values (value_ref to abstract_ranget). More...
#include <jsa.h>
Public Attributes | |
__CPROVER_jsa_node_id_t | next |
__CPROVER_jsa_node_id_t | previous |
__CPROVER_jsa_list_id_t | list |
__CPROVER_jsa_id_t | value_ref |
Abstract nodes may assume any of a set of pre-defined values (value_ref to abstract_ranget).
__CPROVER_jsa_list_id_t __CPROVER_jsa_abstract_node::list |
Definition at line 102 of file jsa.h.
Referenced by __CPROVER_jsa__internal_are_heaps_equal(), and __CPROVER_jsa_assume_valid_heap().
__CPROVER_jsa_node_id_t __CPROVER_jsa_abstract_node::next |
Definition at line 100 of file jsa.h.
Referenced by __CPROVER_jsa__internal_are_heaps_equal(), __CPROVER_jsa__internal_assume_is_neighbour(), __CPROVER_jsa__internal_set_next(), and __CPROVER_jsa_assume_valid_heap().
__CPROVER_jsa_node_id_t __CPROVER_jsa_abstract_node::previous |
Definition at line 101 of file jsa.h.
Referenced by __CPROVER_jsa__internal_are_heaps_equal(), __CPROVER_jsa__internal_assume_is_neighbour(), __CPROVER_jsa__internal_set_previous(), and __CPROVER_jsa_assume_valid_heap().
__CPROVER_jsa_id_t __CPROVER_jsa_abstract_node::value_ref |
Definition at line 103 of file jsa.h.
Referenced by __CPROVER_jsa__internal_are_heaps_equal(), __CPROVER_jsa__internal_assume_valid_iterator_linking(), and __CPROVER_jsa__internal_get_max_index().