15 #ifndef CPROVER_ANSI_C_LIBRARY_JSA_H 16 #define CPROVER_ANSI_C_LIBRARY_JSA_H 18 #ifdef JSA_GENETIC_SYNTHESIS_H_ 19 #ifndef __CPROVER_jsa_extern 20 #define __CPROVER_jsa_extern extern 21 #define JSA_SYNTHESIS_H_ 22 #define __CPROVER_JSA_DEFINE_TRANSFORMERS 25 #ifndef __CPROVER_jsa_extern 26 #define __CPROVER_jsa_extern 30 #ifndef JSA_SYNTHESIS_H_ 31 #define __CPROVER_JSA_DEFINE_TRANSFORMERS 42 #ifndef __CPROVER_JSA_MAX_CONCRETE_NODES 43 #define __CPROVER_JSA_MAX_CONCRETE_NODES 100u 45 #ifndef __CPROVER_JSA_MAX_ABSTRACT_NODES 46 #define __CPROVER_JSA_MAX_ABSTRACT_NODES __CPROVER_JSA_MAX_CONCRETE_NODES 48 #ifndef __CPROVER_JSA_MAX_NODES 49 #define __CPROVER_JSA_MAX_NODES __CPROVER_JSA_MAX_CONCRETE_NODES+\ 50 __CPROVER_JSA_MAX_ABSTRACT_NODES 52 #ifndef __CPROVER_JSA_MAX_ABSTRACT_RANGES 53 #define __CPROVER_JSA_MAX_ABSTRACT_RANGES __CPROVER_JSA_MAX_ABSTRACT_NODES 55 #ifndef __CPROVER_JSA_MAX_ITERATORS 56 #define __CPROVER_JSA_MAX_ITERATORS 100u 58 #ifndef __CPROVER_JSA_MAX_LISTS 59 #define __CPROVER_JSA_MAX_LISTS __CPROVER_JSA_MAX_ITERATORS 61 #ifndef __CPROVER_JSA_MAX_NODES_PER_CE_LIST 62 #define __CPROVER_JSA_MAX_NODES_PER_CE_LIST __CPROVER_JSA_MAX_NODES 64 #if __CPROVER_JSA_MAX_LISTS < 1 65 #error "JSA needs at least one list variable for analysis." 67 #if __CPROVER_JSA_MAX_ABSTRACT_NODES!=0 68 #error "Currently in concrete-mode only." 80 #define __CPROVER_jsa_null 0xFF 81 #define __CPROVER_jsa_word_max 0xFF 133 #if __CPROVER_JSA_MAX_ABSTRACT_NODES > 0 140 #if __CPROVER_JSA_MAX_ABSTRACT_NODES > 0 167 #define __CPROVER_jsa_inline 169 #define __CPROVER_jsa_inline static inline 173 #define __CPROVER_jsa_assume(c) __CPROVER_assume(c) 174 #define __CPROVER_jsa_assert(c, str) __CPROVER_assert(c, str) 176 #define __CPROVER_jsa_assume(c) \ 179 longjmp(__CPROVER_jsa_jump_buffer, 1);\ 182 #define __CPROVER_jsa_assert(c, str) assert((c) && str) 187 #define __CPROVER_jsa__internal_are_heaps_equal(lhs, rhs) (*(lhs) == *(rhs)) 194 #if 0 < __CPROVER_JSA_MAX_ABSTRACT_NODES 206 #if 0 < __CPROVER_JSA_MAX_ABSTRACT_RANGES 211 if(lhs_range.
max!=rhs_range.
max ||
212 lhs_range.
min!=rhs_range.
min ||
250 #define __CPROVER_jsa__internal_get_head_node(heap_ptr, list) \ 251 (heap_ptr)->list_head_nodes[list] 253 #define __CPROVER_jsa__internal_is_concrete_node(node) \ 254 (node < __CPROVER_JSA_MAX_CONCRETE_NODES) 256 #define __CPROVER_jsa__internal_is_abstract_node(node) \ 257 (!__CPROVER_jsa__internal_is_concrete_node(node)) 259 #define __CPROVER_jsa__internal_get_abstract_node_index(node) \ 260 (node - __CPROVER_JSA_MAX_CONCRETE_NODES) 262 #define __CPROVER_jsa__internal_get_abstract_node_id(node_index) \ 263 (__CPROVER_JSA_MAX_CONCRETE_NODES + node_index) 265 #define __CPROVER_jsa__internal_get_list(heap_ptr, node) \ 266 (__CPROVER_jsa_null == node ? __CPROVER_jsa_null :\ 267 __CPROVER_jsa__internal_is_concrete_node(node) ?\ 268 (heap_ptr)->concrete_nodes[node].list:(heap_ptr)->abstract_nodes[node].list) 274 #ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS 290 #define __CPROVER_jsa__internal_get_next(heap_ptr, node) \ 291 (__CPROVER_jsa__internal_is_concrete_node(node) ?\ 292 (heap_ptr)->concrete_nodes[node].next:\ 293 (heap_ptr)->abstract_nodes[\ 294 __CPROVER_jsa__internal_get_abstract_node_index(node)].next) 300 #ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS 316 #define __CPROVER_jsa__internal_get_previous(heap_ptr, node) \ 317 (__CPROVER_jsa__internal_is_concrete_node(node) ?\ 318 (heap_ptr)->concrete_nodes[node].previous:\ 319 (heap_ptr)->abstract_nodes[\ 320 __CPROVER_jsa__internal_get_abstract_node_index(node)].previous) 325 #ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS 338 heap, previous_node_id, next_node_id);
359 #ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS 373 #ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS 384 #ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS 399 #ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS 427 #ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS 450 #ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS 459 return __CPROVER_jsa__internal_get_max_index_result;
471 #ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS 482 else if(lhs_node_id == rhs_node_id)
484 if(lhs_index < rhs_index)
492 if(node.
next == rhs_node_id)
513 #ifdef __CPROVER_JSA_DYNAMIC_TEST_RUNNER 514 void __CPROVER_jsa_internal__clear_temps(
void);
520 #ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS 531 #ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS 544 #ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS 554 #ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS 571 max_head_node=head_node;
602 #if 0 < __CPROVER_JSA_MAX_ABSTRACT_NODES 616 #if 0 < __CPROVER_JSA_MAX_ABSTRACT_RANGES 648 h, list, next_node, next_index);
650 h, list, prev_node, prev_index);
653 h, next_node, next_index, prev_node, prev_index);
667 #if 0 < __CPROVER_JSA_MAX_ABSTRACT_NODES 683 #ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS 698 #ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS 725 #define __CPROVER_jsa_hasNext(heap, it)\ 726 __CPROVER_jsa_null!=(heap)->iterators[it].node_id 731 #ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS 747 #ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS 763 #ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS 781 #ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS 832 #ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS 845 #ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS 858 #ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS 872 #ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS 887 #ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS 901 #ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS 913 #ifdef JSA_SYNTHESIS_H_ 915 #ifndef __CPROVER_JSA_NUM_PRED_OPS 916 #define __CPROVER_JSA_NUM_PRED_OPS 10 918 #ifndef __CPROVER_JSA_NUM_PRED_RESULT_OPS 919 #define __CPROVER_JSA_NUM_PRED_RESULT_OPS __CPROVER_JSA_NUM_PRED_OPS 921 #ifndef __CPROVER_JSA_MAX_QUERY_SIZE 922 #define __CPROVER_JSA_MAX_QUERY_SIZE 10 924 #ifndef __CPROVER_JSA_MAX_PRED_SIZE 925 #define __CPROVER_JSA_MAX_PRED_SIZE (__CPROVER_JSA_MAX_QUERY_SIZE - 1) 927 #ifndef __CPROVER_JSA_NUM_PREDS 928 #define __CPROVER_JSA_NUM_PREDS (__CPROVER_JSA_MAX_QUERY_SIZE - 1) 932 *__CPROVER_JSA_PRED_OPS[__CPROVER_JSA_NUM_PRED_OPS];
934 *__CPROVER_JSA_PRED_RESULT_OPS[__CPROVER_JSA_NUM_PRED_RESULT_OPS];
936 __CPROVER_JSA_MAX_PRED_SIZE_RELAY[__CPROVER_JSA_MAX_PRED_SIZE];
938 __CPROVER_JSA_MAX_QUERY_SIZE_RELAY[__CPROVER_JSA_MAX_QUERY_SIZE];
945 __CPROVER_JSA_HEAP_VARS[__CPROVER_JSA_NUM_PRED_RESULT_OPS];
947 __CPROVER_JSA_ORG_HEAP_VARS[__CPROVER_JSA_NUM_PRED_RESULT_OPS];
949 __CPROVER_JSA_QUERIED_HEAP_VARS[__CPROVER_JSA_NUM_PRED_RESULT_OPS];
954 typedef struct __CPROVER_jsa_pred_instruction
956 __CPROVER_jsa_opcodet opcode;
957 __CPROVER_jsa_opt result_op;
958 __CPROVER_jsa_opt op0;
959 __CPROVER_jsa_opt op1;
960 } __CPROVER_jsa_pred_instructiont;
963 __CPROVER_JSA_PRED_OPS_COUNT;
965 __CPROVER_JSA_PRED_RESULT_OPS_COUNT;
967 *__CPROVER_JSA_PREDICATES[__CPROVER_JSA_NUM_PREDS];
969 __CPROVER_JSA_PREDICATE_SIZES[__CPROVER_JSA_NUM_PREDS];
971 #define __CPROVER_JSA_NUM_PRED_INSTRUCTIONS 8u 976 const __CPROVER_jsa_pred_id_t pred_id)
979 __CPROVER_JSA_PRED_OPS_COUNT<=__CPROVER_JSA_NUM_PRED_OPS,
980 "__CPROVER_JSA_PRED_OPS_COUNT <= __CPROVER_JSA_NUM_PRED_OPS");
982 __CPROVER_JSA_PRED_RESULT_OPS_COUNT<=__CPROVER_JSA_NUM_PRED_RESULT_OPS,
983 "__CPROVER_JSA_PRED_RESULT_OPS_COUNT <= __CPROVER_JSA_NUM_PRED_RESULT_OPS");
986 const __CPROVER_jsa_pred_instructiont *
const pred=
987 __CPROVER_JSA_PREDICATES[pred_id];
989 __CPROVER_JSA_PREDICATE_SIZES[pred_id];
995 const __CPROVER_jsa_pred_instructiont instr=pred[i];
1002 switch (instr.opcode)
1029 const __CPROVER_jsa_pred_id_t pred_id)
1031 const __CPROVER_jsa_pred_instructiont *
const pred=
1032 __CPROVER_JSA_PREDICATES[pred_id];
1034 __CPROVER_JSA_PREDICATE_SIZES[pred_id];
1040 const __CPROVER_jsa_pred_instructiont instr=pred[i];
1041 #define __CPROVER_jsa_execute_pred_op0_ptr __CPROVER_JSA_PRED_OPS[instr.op0] 1042 #define __CPROVER_jsa_execute_pred_op1_ptr __CPROVER_JSA_PRED_OPS[instr.op1] 1043 #define __CPROVER_jsa_execute_pred_result_op_ptr \ 1044 __CPROVER_JSA_PRED_RESULT_OPS[instr.result_op] 1045 #define __CPROVER_jsa_execute_pred_op0 *__CPROVER_jsa_execute_pred_op0_ptr 1046 #define __CPROVER_jsa_execute_pred_op1 *__CPROVER_jsa_execute_pred_op1_ptr 1047 #define __CPROVER_jsa_execute_pred_result \ 1048 *__CPROVER_jsa_execute_pred_result_op_ptr 1049 switch (instr.opcode)
1052 __CPROVER_jsa_pred_opcode_0:
1053 __CPROVER_jsa_execute_pred_result=
1054 __CPROVER_jsa_execute_pred_op0<__CPROVER_jsa_execute_pred_op1;
1057 __CPROVER_jsa_pred_opcode_1:
1058 __CPROVER_jsa_execute_pred_result=
1059 __CPROVER_jsa_execute_pred_op0<=__CPROVER_jsa_execute_pred_op1;
1062 __CPROVER_jsa_pred_opcode_first_2:
1063 __CPROVER_jsa_execute_pred_result=
1065 __CPROVER_jsa_execute_pred_op0, __CPROVER_jsa_execute_pred_op1);
1066 __CPROVER_jsa_pred_opcode_last_2:
1067 __CPROVER_jsa_execute_pred_result=__CPROVER_jsa_execute_pred_result;
1070 __CPROVER_jsa_pred_opcode_3:
1071 __CPROVER_jsa_execute_pred_result=
1072 __CPROVER_jsa_execute_pred_op0!=__CPROVER_jsa_execute_pred_op1;
1075 __CPROVER_jsa_pred_opcode_first_4:
1076 __CPROVER_jsa_execute_pred_result=
1078 __CPROVER_jsa_execute_pred_op0, __CPROVER_jsa_execute_pred_op1);
1079 __CPROVER_jsa_pred_opcode_last_4:
1080 __CPROVER_jsa_execute_pred_result=
1081 __CPROVER_jsa_execute_pred_result;
1084 __CPROVER_jsa_pred_opcode_first_5:
1085 __CPROVER_jsa_execute_pred_result=
1087 __CPROVER_jsa_execute_pred_op0, __CPROVER_jsa_execute_pred_op1);
1088 __CPROVER_jsa_pred_opcode_last_5:
1089 __CPROVER_jsa_execute_pred_result=__CPROVER_jsa_execute_pred_result;
1092 __CPROVER_jsa_pred_opcode_first_6:
1093 __CPROVER_jsa_execute_pred_result=
1095 __CPROVER_jsa_execute_pred_op0, __CPROVER_jsa_execute_pred_op1);
1096 __CPROVER_jsa_pred_opcode_last_6:
1097 __CPROVER_jsa_execute_pred_result=__CPROVER_jsa_execute_pred_result;
1100 __CPROVER_jsa_pred_opcode_first_7:
1101 __CPROVER_jsa_execute_pred_result=
1103 __CPROVER_jsa_execute_pred_op0, __CPROVER_jsa_execute_pred_op1);
1104 __CPROVER_jsa_pred_opcode_last_7:
1105 __CPROVER_jsa_execute_pred_result=__CPROVER_jsa_execute_pred_result;
1108 result=__CPROVER_jsa_execute_pred_result;
1110 #ifdef __CPROVER_JSA_DYNAMIC_TEST_RUNNER 1111 __CPROVER_jsa_internal__clear_temps();
1117 #define __CPROVER_jsa__internal_lambda_op_id 0 1118 #define FILTER_QUERY_INSTR_ID 0 1123 } __CPROVER_jsa_query_idt;
1130 const __CPROVER_jsa_pred_id_t pred_id,
1159 if(node_count > distance)
1163 if(node_count>=skip_distance)
1179 *__CPROVER_JSA_PRED_OPS[__CPROVER_jsa__internal_lambda_op_id]=value;
1181 __CPROVER_jsa_execute_pred(pred_id);
1185 if(pred_result == 0)
1207 typedef struct __CPROVER_jsa_query_instruction
1209 __CPROVER_jsa_opcodet opcode;
1210 __CPROVER_jsa_opt op0;
1211 __CPROVER_jsa_opt op1;
1212 } __CPROVER_jsa_query_instructiont;
1214 #define __CPROVER_JSA_NUM_QUERY_INSTRUCTIONS 3u 1218 const __CPROVER_jsa_query_instructiont *
const query,
1231 const __CPROVER_jsa_query_instructiont instr=query[i];
1233 switch(instr.opcode)
1253 const __CPROVER_jsa_query_instructiont *
const query,
1256 __CPROVER_jsa_assume_valid_query(heap, query, query_size);
1263 const __CPROVER_jsa_query_instructiont instr=query[i];
1264 __CPROVER_jsa_query_opcode_0:
1265 __CPROVER_jsa_stream_op(
1266 heap, list, it, instr.op1, instr.op0, instr.opcode);
1272 const __CPROVER_jsa_query_instructiont *
const query,
1278 __CPROVER_jsa_query_execute(heap, query, query_size);
1293 const __CPROVER_jsa_query_instructiont *
const query,
1298 __CPROVER_jsa_verify_synchronise_iterator(heap, queried_heap, it);
1316 const _Bool heaps_equal=
1322 typedef struct __CPROVER_jsa_invariant_instruction
1324 __CPROVER_jsa_opcodet opcode;
1325 } __CPROVER_jsa_invariant_instructiont;
1327 #define __CPROVER_JSA_NUM_INV_INSTRUCTIONS 1u 1332 const __CPROVER_jsa_invariant_instructiont *
const inv,
1337 return __CPROVER_jsa_verify_invariant_execute(heap, queried_heap);
1351 #endif // CPROVER_ANSI_C_LIBRARY_JSA_H __CPROVER_jsa_index_t iterator_count
Number of iterators on the heap.
__CPROVER_jsa_abstract_nodet abstract_nodes[100u]
#define __CPROVER_JSA_MAX_ABSTRACT_RANGES
__CPROVER_jsa_node_id_t previous
__CPROVER_jsa_iteratort iterators[100u]
__CPROVER_jsa_node_id_t previous_node_id
Concrete node with explicit value.
static _Bool __CPROVER_jsa__internal_is_valid_node_id(const __CPROVER_jsa_node_id_t node_id)
#define __CPROVER_jsa__internal_is_concrete_node(node)
static void __CPROVER_jsa__internal_assume_linking_correct(const __CPROVER_jsa_abstract_heapt *const heap, const __CPROVER_jsa_node_id_t node_id, const __CPROVER_jsa_node_id_t prev, const __CPROVER_jsa_node_id_t next)
static __CPROVER_jsa_word_t __CPROVER_jsa_mult(const __CPROVER_jsa_word_t lhs, const __CPROVER_jsa_word_t rhs)
static _Bool __CPROVER_jsa__internal_is_in_valid_list(const __CPROVER_jsa_abstract_heapt *const heap, const __CPROVER_jsa_node_id_t node_id)
#define __CPROVER_JSA_MAX_ABSTRACT_NODES
#define __CPROVER_jsa_word_max
__CPROVER_jsa_list_id_t list
static void __CPROVER_jsa__internal_set_previous(__CPROVER_jsa_abstract_heapt *const heap, const __CPROVER_jsa_node_id_t node, const __CPROVER_jsa_node_id_t previous_node)
__CPROVER_jsa_word_t __CPROVER_jsa_index_t
static void __CPROVER_jsa_set(__CPROVER_jsa_abstract_heapt *const heap, const __CPROVER_jsa_iterator_id_t it, const __CPROVER_jsa_word_t value)
static void __CPROVER_jsa_assume_new_list(const __CPROVER_jsa_abstract_heapt *const h, const __CPROVER_jsa_list_id_t list)
#define __CPROVER_JSA_MAX_NODES_PER_CE_LIST
static void __CPROVER_jsa_remove(__CPROVER_jsa_abstract_heapt *const heap, const __CPROVER_jsa_iterator_id_t it)
#define __CPROVER_jsa_inline
static __CPROVER_jsa_word_t __CPROVER_jsa_minus(const __CPROVER_jsa_word_t lhs, const __CPROVER_jsa_word_t rhs)
__CPROVER_jsa_id_t value_ref
static void __CPROVER_jsa_assume_valid_heap(const __CPROVER_jsa_abstract_heapt *const h)
Set of pre-defined, possible values for abstract nodes.
#define __CPROVER_JSA_MAX_NODES
static __CPROVER_jsa_word_t __CPROVER_jsa_plus(const __CPROVER_jsa_word_t lhs, const __CPROVER_jsa_word_t rhs)
__CPROVER_jsa_concrete_nodet concrete_nodes[100u]
__CPROVER_jsa_index_t list_count
Number of lists on the heap.
struct __CPROVER_jsa_abstract_heap __CPROVER_jsa_abstract_heapt
#define __CPROVER_jsa_extern
#define __CPROVER_jsa_assert(c, str)
#define __CPROVER_JSA_MAX_LISTS
#define __CPROVER_jsa_null
__CPROVER_jsa_id_t __CPROVER_jsa_node_id_t
static void __CPROVER_jsa_assume_valid_list(const __CPROVER_jsa_abstract_heapt *const h, const __CPROVER_jsa_list_id_t list)
__CPROVER_jsa_data_t value
__CPROVER_jsa_index_t size
Iterators point to a node and give the relative index within that node.
static void __CPROVER_jsa__internal_make_null(__CPROVER_jsa_abstract_heapt *const heap, const __CPROVER_jsa_iterator_id_t it)
char __CPROVER_jsa_signed_word_t
#define __CPROVER_jsa__internal_get_previous(heap_ptr, node)
#define __CPROVER_JSA_MAX_ITERATORS
__CPROVER_jsa_list_id_t list
__CPROVER_jsa_node_id_t previous
#define __CPROVER_jsa__internal_get_abstract_node_index(node)
jmp_buf __CPROVER_jsa_jump_buffer
__CPROVER_jsa_abstract_ranget abstract_ranges[100u]
static __CPROVER_jsa_word_t __CPROVER_jsa_mod(const __CPROVER_jsa_word_t lhs, const __CPROVER_jsa_word_t rhs)
static __CPROVER_jsa_index_t __CPROVER_jsa__internal_get_max_index(const __CPROVER_jsa_abstract_heapt *const heap, const __CPROVER_jsa_node_id_t node_id)
__CPROVER_jsa_id_t __CPROVER_jsa_list_id_t
__CPROVER_jsa_index_t index
__CPROVER_jsa_list_id_t list_head_nodes[100u]
Set of node ids which are list heads.
__CPROVER_jsa_word_t __CPROVER_jsa__internal_index_t
static __CPROVER_jsa_iterator_id_t __CPROVER_jsa_iterator(__CPROVER_jsa_abstract_heapt *const heap, const __CPROVER_jsa_list_id_t list)
static __CPROVER_jsa_word_t __CPROVER_jsa_ite(const __CPROVER_jsa_word_t res, const __CPROVER_jsa_word_t lhs, const __CPROVER_jsa_word_t rhs)
static _Bool __CPROVER_jsa__internal_are_heaps_equal(const __CPROVER_jsa_abstract_heapt *const lhs, const __CPROVER_jsa_abstract_heapt *const rhs)
__CPROVER_jsa_node_id_t node_id
__CPROVER_jsa_word_t __CPROVER_jsa_data_t
#define __CPROVER_jsa__internal_get_next(heap_ptr, node)
unsigned char __CPROVER_jsa_word_t
struct __CPROVER_jsa_abstract_node __CPROVER_jsa_abstract_nodet
Abstract nodes may assume any of a set of pre-defined values (value_ref to abstract_ranget).
__CPROVER_jsa_node_id_t next
static void __CPROVER_jsa_assume_valid_iterator(const __CPROVER_jsa_abstract_heapt *const h, const __CPROVER_jsa_iterator_id_t it)
struct __CPROVER_jsa_concrete_node __CPROVER_jsa_concrete_nodet
Concrete node with explicit value.
static __CPROVER_jsa_node_id_t __CPROVER_jsa__internal_remove(__CPROVER_jsa_abstract_heapt *const heap, const __CPROVER_jsa_node_id_t node_id_to_remove)
static void __CPROVER_jsa__internal_assume_valid_iterator_linking(const __CPROVER_jsa_abstract_heapt *const h, const __CPROVER_jsa_list_id_t list, const __CPROVER_jsa_node_id_t node_id, const __CPROVER_jsa_index_t index)
#define __CPROVER_jsa__internal_get_head_node(heap_ptr, list)
__CPROVER_jsa_node_id_t next
__CPROVER_jsa_index_t previous_index
#define __CPROVER_jsa__internal_get_list(heap_ptr, node)
__CPROVER_jsa_list_id_t list
#define __CPROVER_jsa__internal_get_abstract_node_id(node_index)
Abstract nodes may assume any of a set of pre-defined values (value_ref to abstract_ranget).
struct __CPROVER_jsa_abstract_range __CPROVER_jsa_abstract_ranget
Set of pre-defined, possible values for abstract nodes.
#define __CPROVER_jsa_assume(c)
static void __CPROVER_jsa__internal_assume_is_neighbour(const __CPROVER_jsa_abstract_heapt *const heap, const __CPROVER_jsa_node_id_t lhs_node_id, const __CPROVER_jsa_index_t lhs_index, const __CPROVER_jsa_node_id_t rhs_node_id, const __CPROVER_jsa_index_t rhs_index)
static __CPROVER_jsa_data_t __CPROVER_jsa_next(__CPROVER_jsa_abstract_heapt *const heap, const __CPROVER_jsa_iterator_id_t it)
static __CPROVER_jsa_list_id_t __CPROVER_jsa_create_list(__CPROVER_jsa_abstract_heapt *const heap)
__CPROVER_jsa_word_t __CPROVER_jsa_id_t
static void __CPROVER_jsa_add(__CPROVER_jsa_abstract_heapt *const heap, const __CPROVER_jsa_list_id_t list, const __CPROVER_jsa_word_t value)
#define __CPROVER_JSA_MAX_CONCRETE_NODES
struct __CPROVER_jsa_iterator __CPROVER_jsa_iteratort
Iterators point to a node and give the relative index within that node.
__CPROVER_jsa_id_t __CPROVER_jsa_iterator_id_t
static void __CPROVER_jsa__internal_set_next(__CPROVER_jsa_abstract_heapt *const heap, const __CPROVER_jsa_node_id_t node, const __CPROVER_jsa_node_id_t next_node)
static __CPROVER_jsa_word_t __CPROVER_jsa_div(const __CPROVER_jsa_word_t lhs, const __CPROVER_jsa_word_t rhs)