cprover
|
Counterexample-Guided Inductive Synthesis. More...
#include <assert.h>
#include <string.h>
#include <setjmp.h>
#include <stdbool.h>
Go to the source code of this file.
Classes | |
struct | __CPROVER_jsa_concrete_node |
Concrete node with explicit value. More... | |
struct | __CPROVER_jsa_abstract_node |
Abstract nodes may assume any of a set of pre-defined values (value_ref to abstract_ranget). More... | |
struct | __CPROVER_jsa_abstract_range |
Set of pre-defined, possible values for abstract nodes. More... | |
struct | __CPROVER_jsa_iterator |
Iterators point to a node and give the relative index within that node. More... | |
struct | __CPROVER_jsa_abstract_heap |
Variables | |
jmp_buf | __CPROVER_jsa_jump_buffer |
Counterexample-Guided Inductive Synthesis.
Definition in file jsa.h.
#define __CPROVER_jsa__internal_get_abstract_node_id | ( | node_index | ) | (__CPROVER_JSA_MAX_CONCRETE_NODES + node_index) |
Definition at line 262 of file jsa.h.
Referenced by __CPROVER_jsa_assume_valid_heap().
#define __CPROVER_jsa__internal_get_abstract_node_index | ( | node | ) | (node - __CPROVER_JSA_MAX_CONCRETE_NODES) |
Definition at line 259 of file jsa.h.
Referenced by __CPROVER_jsa__internal_assume_valid_iterator_linking(), __CPROVER_jsa__internal_get_max_index(), __CPROVER_jsa__internal_set_next(), and __CPROVER_jsa__internal_set_previous().
#define __CPROVER_jsa__internal_get_head_node | ( | heap_ptr, | |
list | |||
) | (heap_ptr)->list_head_nodes[list] |
Definition at line 250 of file jsa.h.
Referenced by __CPROVER_jsa_add(), __CPROVER_jsa_assume_new_list(), __CPROVER_jsa_ite(), and __CPROVER_jsa_iterator().
#define __CPROVER_jsa__internal_get_list | ( | heap_ptr, | |
node | |||
) |
Definition at line 265 of file jsa.h.
Referenced by __CPROVER_jsa__internal_assume_linking_correct(), __CPROVER_jsa__internal_assume_valid_iterator_linking(), __CPROVER_jsa__internal_is_in_valid_list(), __CPROVER_jsa__internal_remove(), __CPROVER_jsa_add(), and __CPROVER_jsa_assume_valid_heap().
#define __CPROVER_jsa__internal_get_next | ( | heap_ptr, | |
node | |||
) |
Definition at line 290 of file jsa.h.
Referenced by __CPROVER_jsa__internal_assume_linking_correct(), __CPROVER_jsa_add(), and __CPROVER_jsa_ite().
#define __CPROVER_jsa__internal_get_previous | ( | heap_ptr, | |
node | |||
) |
Definition at line 316 of file jsa.h.
Referenced by __CPROVER_jsa__internal_assume_linking_correct().
#define __CPROVER_jsa__internal_is_abstract_node | ( | node | ) | (!__CPROVER_jsa__internal_is_concrete_node(node)) |
#define __CPROVER_jsa__internal_is_concrete_node | ( | node | ) | (node < __CPROVER_JSA_MAX_CONCRETE_NODES) |
Definition at line 253 of file jsa.h.
Referenced by __CPROVER_jsa__internal_assume_is_neighbour(), __CPROVER_jsa__internal_assume_valid_iterator_linking(), __CPROVER_jsa__internal_get_max_index(), __CPROVER_jsa__internal_remove(), __CPROVER_jsa__internal_set_next(), __CPROVER_jsa__internal_set_previous(), __CPROVER_jsa_ite(), __CPROVER_jsa_next(), and __CPROVER_jsa_set().
#define __CPROVER_jsa_assert | ( | c, | |
str | |||
) | assert((c) && str) |
Definition at line 182 of file jsa.h.
Referenced by __CPROVER_jsa_ite().
#define __CPROVER_jsa_assume | ( | c | ) |
Definition at line 176 of file jsa.h.
Referenced by __CPROVER_jsa__internal_assume_is_neighbour(), __CPROVER_jsa__internal_assume_linking_correct(), __CPROVER_jsa__internal_assume_valid_iterator_linking(), __CPROVER_jsa__internal_remove(), __CPROVER_jsa_add(), __CPROVER_jsa_assume_new_list(), __CPROVER_jsa_assume_valid_heap(), __CPROVER_jsa_assume_valid_iterator(), __CPROVER_jsa_assume_valid_list(), __CPROVER_jsa_create_list(), __CPROVER_jsa_ite(), __CPROVER_jsa_iterator(), __CPROVER_jsa_next(), and __CPROVER_jsa_set().
#define __CPROVER_jsa_extern |
Definition at line 26 of file jsa.h.
Referenced by __CPROVER_jsa_ite().
#define __CPROVER_jsa_hasNext | ( | heap, | |
it | |||
) | __CPROVER_jsa_null!=(heap)->iterators[it].node_id |
#define __CPROVER_jsa_inline static inline |
Definition at line 169 of file jsa.h.
Referenced by __CPROVER_jsa_ite().
#define __CPROVER_JSA_MAX_ABSTRACT_NODES __CPROVER_JSA_MAX_CONCRETE_NODES |
Definition at line 46 of file jsa.h.
Referenced by __CPROVER_jsa__internal_are_heaps_equal(), and __CPROVER_jsa_assume_valid_heap().
#define __CPROVER_JSA_MAX_ABSTRACT_RANGES __CPROVER_JSA_MAX_ABSTRACT_NODES |
Definition at line 53 of file jsa.h.
Referenced by __CPROVER_jsa__internal_are_heaps_equal(), and __CPROVER_jsa_assume_valid_heap().
#define __CPROVER_JSA_MAX_CONCRETE_NODES 100u |
Definition at line 43 of file jsa.h.
Referenced by __CPROVER_jsa__internal_are_heaps_equal(), __CPROVER_jsa_add(), and __CPROVER_jsa_assume_valid_heap().
#define __CPROVER_JSA_MAX_ITERATORS 100u |
Definition at line 56 of file jsa.h.
Referenced by __CPROVER_jsa_assume_valid_heap(), __CPROVER_jsa_ite(), and __CPROVER_jsa_iterator().
#define __CPROVER_JSA_MAX_LISTS __CPROVER_JSA_MAX_ITERATORS |
Definition at line 59 of file jsa.h.
Referenced by __CPROVER_jsa_assume_valid_heap(), __CPROVER_jsa_create_list(), and __CPROVER_jsa_ite().
#define __CPROVER_JSA_MAX_NODES |
Definition at line 49 of file jsa.h.
Referenced by __CPROVER_jsa__internal_is_valid_node_id(), __CPROVER_jsa_add(), and __CPROVER_jsa_ite().
#define __CPROVER_JSA_MAX_NODES_PER_CE_LIST __CPROVER_JSA_MAX_NODES |
Definition at line 62 of file jsa.h.
Referenced by __CPROVER_jsa_assume_valid_heap().
#define __CPROVER_jsa_null 0xFF |
Definition at line 80 of file jsa.h.
Referenced by __CPROVER_jsa__internal_assume_linking_correct(), __CPROVER_jsa__internal_assume_valid_iterator_linking(), __CPROVER_jsa__internal_is_in_valid_list(), __CPROVER_jsa__internal_is_valid_node_id(), __CPROVER_jsa__internal_make_null(), __CPROVER_jsa__internal_remove(), __CPROVER_jsa_add(), __CPROVER_jsa_assume_new_list(), __CPROVER_jsa_assume_valid_heap(), __CPROVER_jsa_create_list(), __CPROVER_jsa_ite(), __CPROVER_jsa_iterator(), __CPROVER_jsa_remove(), and __CPROVER_jsa_set().
#define __CPROVER_jsa_word_max 0xFF |
Definition at line 81 of file jsa.h.
Referenced by __CPROVER_jsa_div(), __CPROVER_jsa_minus(), __CPROVER_jsa_mult(), and __CPROVER_jsa_plus().
typedef struct __CPROVER_jsa_abstract_heap __CPROVER_jsa_abstract_heapt |
typedef 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).
typedef struct __CPROVER_jsa_abstract_range __CPROVER_jsa_abstract_ranget |
Set of pre-defined, possible values for abstract nodes.
typedef struct __CPROVER_jsa_concrete_node __CPROVER_jsa_concrete_nodet |
Concrete node with explicit value.
typedef struct __CPROVER_jsa_iterator __CPROVER_jsa_iteratort |
Iterators point to a node and give the relative index within that node.
typedef char __CPROVER_jsa_signed_word_t |
typedef unsigned char __CPROVER_jsa_word_t |
|
inlinestatic |
Definition at line 189 of file jsa.h.
References __CPROVER_JSA_MAX_ABSTRACT_NODES, __CPROVER_JSA_MAX_ABSTRACT_RANGES, __CPROVER_JSA_MAX_CONCRETE_NODES, __CPROVER_jsa_abstract_heap::abstract_nodes, __CPROVER_jsa_abstract_heap::abstract_ranges, __CPROVER_jsa_abstract_heap::concrete_nodes, __CPROVER_jsa_iterator::index, __CPROVER_jsa_abstract_heap::iterator_count, __CPROVER_jsa_abstract_heap::iterators, __CPROVER_jsa_concrete_node::list, __CPROVER_jsa_abstract_node::list, __CPROVER_jsa_iterator::list, __CPROVER_jsa_abstract_heap::list_count, __CPROVER_jsa_abstract_heap::list_head_nodes, __CPROVER_jsa_abstract_range::max, __CPROVER_jsa_abstract_range::min, __CPROVER_jsa_concrete_node::next, __CPROVER_jsa_abstract_node::next, __CPROVER_jsa_iterator::node_id, __CPROVER_jsa_concrete_node::previous, __CPROVER_jsa_abstract_node::previous, __CPROVER_jsa_iterator::previous_index, __CPROVER_jsa_iterator::previous_node_id, __CPROVER_jsa_abstract_range::size, __CPROVER_jsa_concrete_node::value, and __CPROVER_jsa_abstract_node::value_ref.
Referenced by __CPROVER_jsa_ite().
|
inlinestatic |
Definition at line 465 of file jsa.h.
References __CPROVER_jsa__internal_get_max_index(), __CPROVER_jsa__internal_is_concrete_node, __CPROVER_jsa_assume, __CPROVER_jsa_abstract_heap::abstract_nodes, __CPROVER_jsa_abstract_heap::concrete_nodes, __CPROVER_jsa_concrete_node::next, __CPROVER_jsa_abstract_node::next, __CPROVER_jsa_concrete_node::previous, and __CPROVER_jsa_abstract_node::previous.
Referenced by __CPROVER_jsa_assume_valid_heap().
|
inlinestatic |
Definition at line 394 of file jsa.h.
References __CPROVER_jsa__internal_get_list, __CPROVER_jsa__internal_get_next, __CPROVER_jsa__internal_get_previous, __CPROVER_jsa__internal_is_in_valid_list(), __CPROVER_jsa_assume, and __CPROVER_jsa_null.
Referenced by __CPROVER_jsa_assume_valid_heap().
|
inlinestatic |
Definition at line 422 of file jsa.h.
References __CPROVER_jsa__internal_get_abstract_node_index, __CPROVER_jsa__internal_get_list, __CPROVER_jsa__internal_is_concrete_node, __CPROVER_jsa__internal_is_valid_node_id(), __CPROVER_jsa_assume, __CPROVER_jsa_null, __CPROVER_jsa_abstract_heap::abstract_nodes, and __CPROVER_jsa_abstract_node::value_ref.
Referenced by __CPROVER_jsa_assume_valid_heap().
|
inlinestatic |
Definition at line 447 of file jsa.h.
References __CPROVER_jsa__internal_get_abstract_node_index, __CPROVER_jsa__internal_is_concrete_node, __CPROVER_jsa_abstract_heap::abstract_nodes, __CPROVER_jsa_abstract_heap::abstract_ranges, __CPROVER_jsa_abstract_range::size, and __CPROVER_jsa_abstract_node::value_ref.
Referenced by __CPROVER_jsa__internal_assume_is_neighbour().
|
inlinestatic |
Definition at line 381 of file jsa.h.
References __CPROVER_jsa__internal_get_list, __CPROVER_jsa_null, __CPROVER_jsa_concrete_node::list, and __CPROVER_jsa_abstract_heap::list_count.
Referenced by __CPROVER_jsa__internal_assume_linking_correct().
|
inlinestatic |
Definition at line 371 of file jsa.h.
References __CPROVER_JSA_MAX_NODES, and __CPROVER_jsa_null.
Referenced by __CPROVER_jsa__internal_assume_valid_iterator_linking(), __CPROVER_jsa_add(), and __CPROVER_jsa_assume_valid_heap().
|
inlinestatic |
Definition at line 356 of file jsa.h.
References __CPROVER_jsa_null, __CPROVER_jsa_iterator::index, __CPROVER_jsa_abstract_heap::iterators, __CPROVER_jsa_iterator::node_id, __CPROVER_jsa_iterator::previous_index, and __CPROVER_jsa_iterator::previous_node_id.
Referenced by __CPROVER_jsa_ite().
|
inlinestatic |
Definition at line 322 of file jsa.h.
References __CPROVER_jsa__internal_get_list, __CPROVER_jsa__internal_is_concrete_node, __CPROVER_jsa__internal_set_next(), __CPROVER_jsa__internal_set_previous(), __CPROVER_jsa_assume, __CPROVER_jsa_null, __CPROVER_jsa_abstract_heap::concrete_nodes, __CPROVER_jsa_concrete_node::list, __CPROVER_jsa_abstract_heap::list_head_nodes, __CPROVER_jsa_concrete_node::next, __CPROVER_jsa_concrete_node::previous, and __CPROVER_jsa_concrete_node::value.
Referenced by __CPROVER_jsa_ite(), and __CPROVER_jsa_remove().
|
inlinestatic |
Definition at line 270 of file jsa.h.
References __CPROVER_jsa__internal_get_abstract_node_index, __CPROVER_jsa__internal_is_concrete_node, __CPROVER_jsa_abstract_heap::abstract_nodes, __CPROVER_jsa_abstract_heap::concrete_nodes, __CPROVER_jsa_concrete_node::next, and __CPROVER_jsa_abstract_node::next.
Referenced by __CPROVER_jsa__internal_remove(), and __CPROVER_jsa_add().
|
inlinestatic |
Definition at line 296 of file jsa.h.
References __CPROVER_jsa__internal_get_abstract_node_index, __CPROVER_jsa__internal_is_concrete_node, __CPROVER_jsa_abstract_heap::abstract_nodes, __CPROVER_jsa_abstract_heap::concrete_nodes, __CPROVER_jsa_concrete_node::previous, and __CPROVER_jsa_abstract_node::previous.
Referenced by __CPROVER_jsa__internal_remove().
|
inlinestatic |
Definition at line 777 of file jsa.h.
References __CPROVER_jsa__internal_get_head_node, __CPROVER_jsa__internal_get_list, __CPROVER_jsa__internal_get_next, __CPROVER_jsa__internal_is_valid_node_id(), __CPROVER_jsa__internal_set_next(), __CPROVER_jsa_assume, __CPROVER_JSA_MAX_CONCRETE_NODES, __CPROVER_JSA_MAX_NODES, __CPROVER_jsa_null, __CPROVER_jsa_abstract_heap::concrete_nodes, __CPROVER_jsa_concrete_node::list, __CPROVER_jsa_abstract_heap::list_head_nodes, __CPROVER_jsa_concrete_node::next, __CPROVER_jsa_concrete_node::previous, and __CPROVER_jsa_concrete_node::value.
Referenced by __CPROVER_jsa_ite().
|
inlinestatic |
Definition at line 528 of file jsa.h.
References __CPROVER_jsa__internal_get_head_node, __CPROVER_jsa_assume, __CPROVER_jsa_assume_valid_list(), and __CPROVER_jsa_null.
|
inlinestatic |
Definition at line 552 of file jsa.h.
References __CPROVER_jsa__internal_assume_is_neighbour(), __CPROVER_jsa__internal_assume_linking_correct(), __CPROVER_jsa__internal_assume_valid_iterator_linking(), __CPROVER_jsa__internal_get_abstract_node_id, __CPROVER_jsa__internal_get_list, __CPROVER_jsa__internal_is_valid_node_id(), __CPROVER_jsa_assume, __CPROVER_JSA_MAX_ABSTRACT_NODES, __CPROVER_JSA_MAX_ABSTRACT_RANGES, __CPROVER_JSA_MAX_CONCRETE_NODES, __CPROVER_JSA_MAX_ITERATORS, __CPROVER_JSA_MAX_LISTS, __CPROVER_JSA_MAX_NODES_PER_CE_LIST, __CPROVER_jsa_null, __CPROVER_jsa_abstract_heap::abstract_nodes, __CPROVER_jsa_abstract_heap::abstract_ranges, __CPROVER_jsa_abstract_heap::concrete_nodes, __CPROVER_jsa_iterator::index, __CPROVER_jsa_abstract_heap::iterator_count, __CPROVER_jsa_abstract_heap::iterators, __CPROVER_jsa_concrete_node::list, __CPROVER_jsa_abstract_node::list, __CPROVER_jsa_iterator::list, __CPROVER_jsa_abstract_heap::list_count, __CPROVER_jsa_abstract_heap::list_head_nodes, __CPROVER_jsa_abstract_range::max, __CPROVER_jsa_abstract_range::min, __CPROVER_jsa_concrete_node::next, __CPROVER_jsa_abstract_node::next, __CPROVER_jsa_iterator::node_id, __CPROVER_jsa_concrete_node::previous, __CPROVER_jsa_abstract_node::previous, __CPROVER_jsa_iterator::previous_index, __CPROVER_jsa_iterator::previous_node_id, r, __CPROVER_jsa_abstract_range::size, and __CPROVER_jsa_concrete_node::value.
|
inlinestatic |
Definition at line 541 of file jsa.h.
References __CPROVER_jsa_assume.
Referenced by __CPROVER_jsa_ite().
|
inlinestatic |
Definition at line 517 of file jsa.h.
References __CPROVER_jsa_assume.
Referenced by __CPROVER_jsa_assume_new_list(), and __CPROVER_jsa_ite().
|
inlinestatic |
Definition at line 681 of file jsa.h.
References __CPROVER_jsa_assume, __CPROVER_JSA_MAX_LISTS, __CPROVER_jsa_null, __CPROVER_jsa_abstract_heap::list_count, and __CPROVER_jsa_abstract_heap::list_head_nodes.
|
inlinestatic |
Definition at line 884 of file jsa.h.
References __CPROVER_jsa_word_max.
Referenced by __CPROVER_jsa_ite().
|
inlinestatic |
Definition at line 897 of file jsa.h.
References __CPROVER_jsa__internal_are_heaps_equal(), __CPROVER_jsa__internal_get_head_node, __CPROVER_jsa__internal_get_next, __CPROVER_jsa__internal_is_concrete_node, __CPROVER_jsa__internal_make_null(), __CPROVER_jsa__internal_remove(), __CPROVER_jsa_add(), __CPROVER_jsa_assert, __CPROVER_jsa_assume, __CPROVER_jsa_assume_valid_iterator(), __CPROVER_jsa_assume_valid_list(), __CPROVER_jsa_div(), __CPROVER_jsa_extern, __CPROVER_jsa_inline, __CPROVER_JSA_MAX_ITERATORS, __CPROVER_JSA_MAX_LISTS, __CPROVER_JSA_MAX_NODES, __CPROVER_jsa_minus(), __CPROVER_jsa_mod(), __CPROVER_jsa_mult(), __CPROVER_jsa_null, __CPROVER_jsa_plus(), __CPROVER_jsa_abstract_heap::concrete_nodes, __CPROVER_jsa_abstract_heap::iterators, __CPROVER_jsa_iterator::list, __CPROVER_jsa_iterator::node_id, and __CPROVER_jsa_concrete_node::value.
|
inlinestatic |
Definition at line 695 of file jsa.h.
References __CPROVER_jsa__internal_get_head_node, __CPROVER_jsa_assume, __CPROVER_JSA_MAX_ITERATORS, __CPROVER_jsa_null, __CPROVER_jsa_abstract_heap::iterator_count, __CPROVER_jsa_abstract_heap::iterators, and __CPROVER_jsa_iterator::node_id.
|
inlinestatic |
Definition at line 829 of file jsa.h.
References __CPROVER_jsa_word_max.
Referenced by __CPROVER_jsa_ite().
|
inlinestatic |
Definition at line 842 of file jsa.h.
Referenced by __CPROVER_jsa_ite().
|
inlinestatic |
Definition at line 869 of file jsa.h.
References __CPROVER_jsa_word_max.
Referenced by __CPROVER_jsa_ite().
|
inlinestatic |
Definition at line 728 of file jsa.h.
References __CPROVER_jsa__internal_is_concrete_node, __CPROVER_jsa_assume, __CPROVER_jsa_abstract_heap::concrete_nodes, __CPROVER_jsa_abstract_heap::iterators, __CPROVER_jsa_concrete_node::next, __CPROVER_jsa_iterator::node_id, __CPROVER_jsa_iterator::previous_node_id, and __CPROVER_jsa_concrete_node::value.
|
inlinestatic |
Definition at line 855 of file jsa.h.
References __CPROVER_jsa_word_max.
Referenced by __CPROVER_jsa_ite().
|
inlinestatic |
Definition at line 744 of file jsa.h.
References __CPROVER_jsa__internal_remove(), __CPROVER_jsa_null, __CPROVER_jsa_abstract_heap::iterators, __CPROVER_jsa_iterator::node_id, and __CPROVER_jsa_iterator::previous_node_id.
|
inlinestatic |
jmp_buf __CPROVER_jsa_jump_buffer |