cprover
|
#include <jsa.h>
Public Attributes | |
__CPROVER_jsa_concrete_nodet | concrete_nodes [100u] |
__CPROVER_jsa_abstract_nodet | abstract_nodes [100u] |
__CPROVER_jsa_abstract_ranget | abstract_ranges [100u] |
__CPROVER_jsa_iteratort | iterators [100u] |
__CPROVER_jsa_index_t | iterator_count |
Number of iterators on the heap. More... | |
__CPROVER_jsa_list_id_t | list_head_nodes [100u] |
Set of node ids which are list heads. More... | |
__CPROVER_jsa_index_t | list_count |
Number of lists on the heap. More... | |
__CPROVER_jsa_abstract_nodet __CPROVER_jsa_abstract_heap::abstract_nodes[ 100u] |
Definition at line 135 of file jsa.h.
Referenced by __CPROVER_jsa__internal_are_heaps_equal(), __CPROVER_jsa__internal_assume_is_neighbour(), __CPROVER_jsa__internal_assume_valid_iterator_linking(), __CPROVER_jsa__internal_get_max_index(), __CPROVER_jsa__internal_set_next(), __CPROVER_jsa__internal_set_previous(), and __CPROVER_jsa_assume_valid_heap().
__CPROVER_jsa_abstract_ranget __CPROVER_jsa_abstract_heap::abstract_ranges[ 100u] |
Definition at line 142 of file jsa.h.
Referenced by __CPROVER_jsa__internal_are_heaps_equal(), __CPROVER_jsa__internal_get_max_index(), and __CPROVER_jsa_assume_valid_heap().
__CPROVER_jsa_concrete_nodet __CPROVER_jsa_abstract_heap::concrete_nodes[100u] |
Definition at line 131 of file jsa.h.
Referenced by __CPROVER_jsa__internal_are_heaps_equal(), __CPROVER_jsa__internal_assume_is_neighbour(), __CPROVER_jsa__internal_remove(), __CPROVER_jsa__internal_set_next(), __CPROVER_jsa__internal_set_previous(), __CPROVER_jsa_add(), __CPROVER_jsa_assume_valid_heap(), __CPROVER_jsa_ite(), __CPROVER_jsa_next(), and __CPROVER_jsa_set().
__CPROVER_jsa_index_t __CPROVER_jsa_abstract_heap::iterator_count |
Number of iterators on the heap.
Definition at line 152 of file jsa.h.
Referenced by __CPROVER_jsa__internal_are_heaps_equal(), __CPROVER_jsa_assume_valid_heap(), and __CPROVER_jsa_iterator().
__CPROVER_jsa_iteratort __CPROVER_jsa_abstract_heap::iterators[100u] |
Definition at line 147 of file jsa.h.
Referenced by __CPROVER_jsa__internal_are_heaps_equal(), __CPROVER_jsa__internal_make_null(), __CPROVER_jsa_assume_valid_heap(), __CPROVER_jsa_ite(), __CPROVER_jsa_iterator(), __CPROVER_jsa_next(), __CPROVER_jsa_remove(), and __CPROVER_jsa_set().
__CPROVER_jsa_index_t __CPROVER_jsa_abstract_heap::list_count |
Number of lists on the heap.
Definition at line 162 of file jsa.h.
Referenced by __CPROVER_jsa__internal_are_heaps_equal(), __CPROVER_jsa__internal_is_in_valid_list(), __CPROVER_jsa_assume_valid_heap(), and __CPROVER_jsa_create_list().
__CPROVER_jsa_list_id_t __CPROVER_jsa_abstract_heap::list_head_nodes[ 100u] |
Set of node ids which are list heads.
Definition at line 157 of file jsa.h.
Referenced by __CPROVER_jsa__internal_are_heaps_equal(), __CPROVER_jsa__internal_remove(), __CPROVER_jsa_add(), __CPROVER_jsa_assume_valid_heap(), and __CPROVER_jsa_create_list().