cprover
Loading...
Searching...
No Matches
jsa.h File Reference

Counterexample-Guided Inductive Synthesis. More...

#include <assert.h>
#include <string.h>
#include <setjmp.h>
#include <stdbool.h>
Include dependency graph for jsa.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

Macros

#define __CPROVER_jsa_extern
#define __CPROVER_JSA_DEFINE_TRANSFORMERS
#define __CPROVER_JSA_MAX_CONCRETE_NODES   100u
#define __CPROVER_JSA_MAX_ABSTRACT_NODES   __CPROVER_JSA_MAX_CONCRETE_NODES
#define __CPROVER_JSA_MAX_NODES
#define __CPROVER_JSA_MAX_ABSTRACT_RANGES   __CPROVER_JSA_MAX_ABSTRACT_NODES
#define __CPROVER_JSA_MAX_ITERATORS   100u
#define __CPROVER_JSA_MAX_LISTS   __CPROVER_JSA_MAX_ITERATORS
#define __CPROVER_JSA_MAX_NODES_PER_CE_LIST   __CPROVER_JSA_MAX_NODES
#define __CPROVER_jsa_null   0xFF
#define __CPROVER_jsa_word_max   0xFF
#define __CPROVER_jsa_inline   static inline
#define __CPROVER_jsa_assume(c)
#define __CPROVER_jsa_assert(c, str)
#define __CPROVER_jsa__internal_get_head_node(heap_ptr, list)
#define __CPROVER_jsa__internal_is_concrete_node(node)
#define __CPROVER_jsa__internal_is_abstract_node(node)
#define __CPROVER_jsa__internal_get_abstract_node_index(node)
#define __CPROVER_jsa__internal_get_abstract_node_id(node_index)
#define __CPROVER_jsa__internal_get_list(heap_ptr, node)
#define __CPROVER_jsa__internal_get_next(heap_ptr, node)
#define __CPROVER_jsa__internal_get_previous(heap_ptr, node)
#define __CPROVER_jsa_hasNext(heap, it)

Typedefs

typedef unsigned char __CPROVER_jsa_word_t
typedef char __CPROVER_jsa_signed_word_t
typedef __CPROVER_jsa_word_t __CPROVER_jsa_data_t
typedef __CPROVER_jsa_word_t __CPROVER_jsa_index_t
typedef __CPROVER_jsa_word_t __CPROVER_jsa__internal_index_t
typedef __CPROVER_jsa_word_t __CPROVER_jsa_id_t
typedef __CPROVER_jsa_id_t __CPROVER_jsa_node_id_t
typedef __CPROVER_jsa_id_t __CPROVER_jsa_list_id_t
typedef __CPROVER_jsa_id_t __CPROVER_jsa_iterator_id_t
typedef struct __CPROVER_jsa_concrete_node __CPROVER_jsa_concrete_nodet
 Concrete node with explicit value.
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_iterator __CPROVER_jsa_iteratort
 Iterators point to a node and give the relative index within that node.
typedef struct __CPROVER_jsa_abstract_heap __CPROVER_jsa_abstract_heapt

Functions

static _Bool __CPROVER_jsa__internal_are_heaps_equal (const __CPROVER_jsa_abstract_heapt *const lhs, const __CPROVER_jsa_abstract_heapt *const rhs)
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 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)
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_make_null (__CPROVER_jsa_abstract_heapt *const heap, const __CPROVER_jsa_iterator_id_t it)
static _Bool __CPROVER_jsa__internal_is_valid_node_id (const __CPROVER_jsa_node_id_t node_id)
static _Bool __CPROVER_jsa__internal_is_in_valid_list (const __CPROVER_jsa_abstract_heapt *const heap, const __CPROVER_jsa_node_id_t node_id)
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 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)
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)
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 void __CPROVER_jsa_assume_valid_list (const __CPROVER_jsa_abstract_heapt *const h, const __CPROVER_jsa_list_id_t list)
static void __CPROVER_jsa_assume_new_list (const __CPROVER_jsa_abstract_heapt *const h, const __CPROVER_jsa_list_id_t list)
static void __CPROVER_jsa_assume_valid_iterator (const __CPROVER_jsa_abstract_heapt *const h, const __CPROVER_jsa_iterator_id_t it)
static void __CPROVER_jsa_assume_valid_heap (const __CPROVER_jsa_abstract_heapt *const h)
static __CPROVER_jsa_list_id_t __CPROVER_jsa_create_list (__CPROVER_jsa_abstract_heapt *const heap)
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_data_t __CPROVER_jsa_next (__CPROVER_jsa_abstract_heapt *const heap, const __CPROVER_jsa_iterator_id_t it)
static void __CPROVER_jsa_remove (__CPROVER_jsa_abstract_heapt *const heap, const __CPROVER_jsa_iterator_id_t it)
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_add (__CPROVER_jsa_abstract_heapt *const heap, const __CPROVER_jsa_list_id_t list, const __CPROVER_jsa_word_t value)
static __CPROVER_jsa_word_t __CPROVER_jsa_minus (const __CPROVER_jsa_word_t lhs, const __CPROVER_jsa_word_t rhs)
static __CPROVER_jsa_word_t __CPROVER_jsa_mod (const __CPROVER_jsa_word_t lhs, const __CPROVER_jsa_word_t rhs)
static __CPROVER_jsa_word_t __CPROVER_jsa_plus (const __CPROVER_jsa_word_t lhs, const __CPROVER_jsa_word_t rhs)
static __CPROVER_jsa_word_t __CPROVER_jsa_mult (const __CPROVER_jsa_word_t lhs, const __CPROVER_jsa_word_t rhs)
static __CPROVER_jsa_word_t __CPROVER_jsa_div (const __CPROVER_jsa_word_t lhs, const __CPROVER_jsa_word_t rhs)
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)

Variables

jmp_buf __CPROVER_jsa_jump_buffer

Detailed Description

Counterexample-Guided Inductive Synthesis.

Definition in file jsa.h.

Macro Definition Documentation

◆ __CPROVER_jsa__internal_get_abstract_node_id

#define __CPROVER_jsa__internal_get_abstract_node_id ( node_index)
Value:
(__CPROVER_JSA_MAX_CONCRETE_NODES + node_index)
__CPROVER_JSA_MAX_CONCRETE_NODES
#define __CPROVER_JSA_MAX_CONCRETE_NODES
Definition jsa.h:43

Definition at line 262 of file jsa.h.

◆ __CPROVER_jsa__internal_get_abstract_node_index

#define __CPROVER_jsa__internal_get_abstract_node_index ( node)
Value:
(node - __CPROVER_JSA_MAX_CONCRETE_NODES)

Definition at line 259 of file jsa.h.

◆ __CPROVER_jsa__internal_get_head_node

#define __CPROVER_jsa__internal_get_head_node ( heap_ptr,
list )
Value:
(heap_ptr)->list_head_nodes[list]

Definition at line 250 of file jsa.h.

◆ __CPROVER_jsa__internal_get_list

#define __CPROVER_jsa__internal_get_list ( heap_ptr,
node )
Value:
(__CPROVER_jsa_null == node ? __CPROVER_jsa_null :\
__CPROVER_jsa__internal_is_concrete_node(node) ?\
(heap_ptr)->concrete_nodes[node].list:(heap_ptr)->abstract_nodes[node].list)
__CPROVER_jsa_null
#define __CPROVER_jsa_null
Definition jsa.h:80

Definition at line 265 of file jsa.h.

◆ __CPROVER_jsa__internal_get_next

#define __CPROVER_jsa__internal_get_next ( heap_ptr,
node )
Value:
(__CPROVER_jsa__internal_is_concrete_node(node) ?\
(heap_ptr)->concrete_nodes[node].next:\
(heap_ptr)->abstract_nodes[\
__CPROVER_jsa__internal_get_abstract_node_index(node)].next)
__CPROVER_jsa__internal_get_abstract_node_index
#define __CPROVER_jsa__internal_get_abstract_node_index(node)
Definition jsa.h:259
__CPROVER_jsa__internal_is_concrete_node
#define __CPROVER_jsa__internal_is_concrete_node(node)
Definition jsa.h:253

Definition at line 290 of file jsa.h.

◆ __CPROVER_jsa__internal_get_previous

#define __CPROVER_jsa__internal_get_previous ( heap_ptr,
node )
Value:
(__CPROVER_jsa__internal_is_concrete_node(node) ?\
(heap_ptr)->concrete_nodes[node].previous:\
(heap_ptr)->abstract_nodes[\
__CPROVER_jsa__internal_get_abstract_node_index(node)].previous)

Definition at line 316 of file jsa.h.

◆ __CPROVER_jsa__internal_is_abstract_node

#define __CPROVER_jsa__internal_is_abstract_node ( node)
Value:
(!__CPROVER_jsa__internal_is_concrete_node(node))

Definition at line 256 of file jsa.h.

◆ __CPROVER_jsa__internal_is_concrete_node

#define __CPROVER_jsa__internal_is_concrete_node ( node)
Value:
(node < __CPROVER_JSA_MAX_CONCRETE_NODES)

Definition at line 253 of file jsa.h.

◆ __CPROVER_jsa_assert

#define __CPROVER_jsa_assert ( c,
str )
Value:
assert((c) && str)

Definition at line 182 of file jsa.h.

◆ __CPROVER_jsa_assume

#define __CPROVER_jsa_assume ( c)
Value:
do {\
if(!(c))\
longjmp(__CPROVER_jsa_jump_buffer, 1);\
}\
while(false)
__CPROVER_jsa_jump_buffer
jmp_buf __CPROVER_jsa_jump_buffer

Definition at line 176 of file jsa.h.

◆ __CPROVER_JSA_DEFINE_TRANSFORMERS

#define __CPROVER_JSA_DEFINE_TRANSFORMERS

Definition at line 31 of file jsa.h.

◆ __CPROVER_jsa_extern

#define __CPROVER_jsa_extern

Definition at line 26 of file jsa.h.

◆ __CPROVER_jsa_hasNext

#define __CPROVER_jsa_hasNext ( heap,
it )
Value:
__CPROVER_jsa_null!=(heap)->iterators[it].node_id

Definition at line 725 of file jsa.h.

◆ __CPROVER_jsa_inline

#define __CPROVER_jsa_inline   static inline

Definition at line 169 of file jsa.h.

◆ __CPROVER_JSA_MAX_ABSTRACT_NODES

#define __CPROVER_JSA_MAX_ABSTRACT_NODES   __CPROVER_JSA_MAX_CONCRETE_NODES

Definition at line 46 of file jsa.h.

◆ __CPROVER_JSA_MAX_ABSTRACT_RANGES

#define __CPROVER_JSA_MAX_ABSTRACT_RANGES   __CPROVER_JSA_MAX_ABSTRACT_NODES

Definition at line 53 of file jsa.h.

◆ __CPROVER_JSA_MAX_CONCRETE_NODES

#define __CPROVER_JSA_MAX_CONCRETE_NODES   100u

Definition at line 43 of file jsa.h.

◆ __CPROVER_JSA_MAX_ITERATORS

#define __CPROVER_JSA_MAX_ITERATORS   100u

Definition at line 56 of file jsa.h.

◆ __CPROVER_JSA_MAX_LISTS

#define __CPROVER_JSA_MAX_LISTS   __CPROVER_JSA_MAX_ITERATORS

Definition at line 59 of file jsa.h.

◆ __CPROVER_JSA_MAX_NODES

#define __CPROVER_JSA_MAX_NODES
Value:
__CPROVER_JSA_MAX_CONCRETE_NODES+\
__CPROVER_JSA_MAX_ABSTRACT_NODES
__CPROVER_JSA_MAX_ABSTRACT_NODES
#define __CPROVER_JSA_MAX_ABSTRACT_NODES
Definition jsa.h:46

Definition at line 49 of file jsa.h.

◆ __CPROVER_JSA_MAX_NODES_PER_CE_LIST

#define __CPROVER_JSA_MAX_NODES_PER_CE_LIST   __CPROVER_JSA_MAX_NODES

Definition at line 62 of file jsa.h.

◆ __CPROVER_jsa_null

#define __CPROVER_jsa_null   0xFF

Definition at line 80 of file jsa.h.

◆ __CPROVER_jsa_word_max

#define __CPROVER_jsa_word_max   0xFF

Definition at line 81 of file jsa.h.

Typedef Documentation

◆ __CPROVER_jsa__internal_index_t

typedef __CPROVER_jsa_word_t __CPROVER_jsa__internal_index_t

Definition at line 75 of file jsa.h.

◆ __CPROVER_jsa_abstract_heapt

typedef struct __CPROVER_jsa_abstract_heap __CPROVER_jsa_abstract_heapt

◆ __CPROVER_jsa_abstract_nodet

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).

◆ __CPROVER_jsa_abstract_ranget

typedef struct __CPROVER_jsa_abstract_range __CPROVER_jsa_abstract_ranget

Set of pre-defined, possible values for abstract nodes.

◆ __CPROVER_jsa_concrete_nodet

typedef struct __CPROVER_jsa_concrete_node __CPROVER_jsa_concrete_nodet

Concrete node with explicit value.

◆ __CPROVER_jsa_data_t

typedef __CPROVER_jsa_word_t __CPROVER_jsa_data_t

Definition at line 73 of file jsa.h.

◆ __CPROVER_jsa_id_t

typedef __CPROVER_jsa_word_t __CPROVER_jsa_id_t

Definition at line 76 of file jsa.h.

◆ __CPROVER_jsa_index_t

typedef __CPROVER_jsa_word_t __CPROVER_jsa_index_t

Definition at line 74 of file jsa.h.

◆ __CPROVER_jsa_iterator_id_t

typedef __CPROVER_jsa_id_t __CPROVER_jsa_iterator_id_t

Definition at line 79 of file jsa.h.

◆ __CPROVER_jsa_iteratort

typedef struct __CPROVER_jsa_iterator __CPROVER_jsa_iteratort

Iterators point to a node and give the relative index within that node.

◆ __CPROVER_jsa_list_id_t

typedef __CPROVER_jsa_id_t __CPROVER_jsa_list_id_t

Definition at line 78 of file jsa.h.

◆ __CPROVER_jsa_node_id_t

typedef __CPROVER_jsa_id_t __CPROVER_jsa_node_id_t

Definition at line 77 of file jsa.h.

◆ __CPROVER_jsa_signed_word_t

typedef char __CPROVER_jsa_signed_word_t

Definition at line 72 of file jsa.h.

◆ __CPROVER_jsa_word_t

typedef unsigned char __CPROVER_jsa_word_t

Definition at line 71 of file jsa.h.

Function Documentation

◆ __CPROVER_jsa__internal_are_heaps_equal()

_Bool __CPROVER_jsa__internal_are_heaps_equal ( const __CPROVER_jsa_abstract_heapt *const lhs,
const __CPROVER_jsa_abstract_heapt *const rhs )
inlinestatic

Definition at line 189 of file jsa.h.

◆ __CPROVER_jsa__internal_assume_is_neighbour()

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 )
inlinestatic

Definition at line 465 of file jsa.h.

◆ __CPROVER_jsa__internal_assume_linking_correct()

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 )
inlinestatic

Definition at line 394 of file jsa.h.

◆ __CPROVER_jsa__internal_assume_valid_iterator_linking()

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 )
inlinestatic

Definition at line 422 of file jsa.h.

◆ __CPROVER_jsa__internal_get_max_index()

__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 )
inlinestatic

Definition at line 447 of file jsa.h.

◆ __CPROVER_jsa__internal_is_in_valid_list()

_Bool __CPROVER_jsa__internal_is_in_valid_list ( const __CPROVER_jsa_abstract_heapt *const heap,
const __CPROVER_jsa_node_id_t node_id )
inlinestatic

Definition at line 381 of file jsa.h.

◆ __CPROVER_jsa__internal_is_valid_node_id()

_Bool __CPROVER_jsa__internal_is_valid_node_id ( const __CPROVER_jsa_node_id_t node_id)
inlinestatic

Definition at line 371 of file jsa.h.

◆ __CPROVER_jsa__internal_make_null()

void __CPROVER_jsa__internal_make_null ( __CPROVER_jsa_abstract_heapt *const heap,
const __CPROVER_jsa_iterator_id_t it )
inlinestatic

Definition at line 356 of file jsa.h.

◆ __CPROVER_jsa__internal_remove()

__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 )
inlinestatic

Definition at line 322 of file jsa.h.

◆ __CPROVER_jsa__internal_set_next()

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 )
inlinestatic

Definition at line 270 of file jsa.h.

◆ __CPROVER_jsa__internal_set_previous()

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 )
inlinestatic

Definition at line 296 of file jsa.h.

◆ __CPROVER_jsa_add()

void __CPROVER_jsa_add ( __CPROVER_jsa_abstract_heapt *const heap,
const __CPROVER_jsa_list_id_t list,
const __CPROVER_jsa_word_t value )
inlinestatic

Definition at line 777 of file jsa.h.

◆ __CPROVER_jsa_assume_new_list()

void __CPROVER_jsa_assume_new_list ( const __CPROVER_jsa_abstract_heapt *const h,
const __CPROVER_jsa_list_id_t list )
inlinestatic

Definition at line 528 of file jsa.h.

◆ __CPROVER_jsa_assume_valid_heap()

void __CPROVER_jsa_assume_valid_heap ( const __CPROVER_jsa_abstract_heapt *const h)
inlinestatic

Definition at line 552 of file jsa.h.

◆ __CPROVER_jsa_assume_valid_iterator()

void __CPROVER_jsa_assume_valid_iterator ( const __CPROVER_jsa_abstract_heapt *const h,
const __CPROVER_jsa_iterator_id_t it )
inlinestatic

Definition at line 541 of file jsa.h.

◆ __CPROVER_jsa_assume_valid_list()

void __CPROVER_jsa_assume_valid_list ( const __CPROVER_jsa_abstract_heapt *const h,
const __CPROVER_jsa_list_id_t list )
inlinestatic

Definition at line 517 of file jsa.h.

◆ __CPROVER_jsa_create_list()

__CPROVER_jsa_list_id_t __CPROVER_jsa_create_list ( __CPROVER_jsa_abstract_heapt *const heap)
inlinestatic

Definition at line 681 of file jsa.h.

◆ __CPROVER_jsa_div()

__CPROVER_jsa_word_t __CPROVER_jsa_div ( const __CPROVER_jsa_word_t lhs,
const __CPROVER_jsa_word_t rhs )
inlinestatic

Definition at line 884 of file jsa.h.

◆ __CPROVER_jsa_ite()

__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 )
inlinestatic

Definition at line 897 of file jsa.h.

◆ __CPROVER_jsa_iterator()

__CPROVER_jsa_iterator_id_t __CPROVER_jsa_iterator ( __CPROVER_jsa_abstract_heapt *const heap,
const __CPROVER_jsa_list_id_t list )
inlinestatic

Definition at line 695 of file jsa.h.

◆ __CPROVER_jsa_minus()

__CPROVER_jsa_word_t __CPROVER_jsa_minus ( const __CPROVER_jsa_word_t lhs,
const __CPROVER_jsa_word_t rhs )
inlinestatic

Definition at line 829 of file jsa.h.

◆ __CPROVER_jsa_mod()

__CPROVER_jsa_word_t __CPROVER_jsa_mod ( const __CPROVER_jsa_word_t lhs,
const __CPROVER_jsa_word_t rhs )
inlinestatic

Definition at line 842 of file jsa.h.

◆ __CPROVER_jsa_mult()

__CPROVER_jsa_word_t __CPROVER_jsa_mult ( const __CPROVER_jsa_word_t lhs,
const __CPROVER_jsa_word_t rhs )
inlinestatic

Definition at line 869 of file jsa.h.

◆ __CPROVER_jsa_next()

__CPROVER_jsa_data_t __CPROVER_jsa_next ( __CPROVER_jsa_abstract_heapt *const heap,
const __CPROVER_jsa_iterator_id_t it )
inlinestatic

Definition at line 728 of file jsa.h.

◆ __CPROVER_jsa_plus()

__CPROVER_jsa_word_t __CPROVER_jsa_plus ( const __CPROVER_jsa_word_t lhs,
const __CPROVER_jsa_word_t rhs )
inlinestatic

Definition at line 855 of file jsa.h.

◆ __CPROVER_jsa_remove()

void __CPROVER_jsa_remove ( __CPROVER_jsa_abstract_heapt *const heap,
const __CPROVER_jsa_iterator_id_t it )
inlinestatic

Definition at line 744 of file jsa.h.

◆ __CPROVER_jsa_set()

void __CPROVER_jsa_set ( __CPROVER_jsa_abstract_heapt *const heap,
const __CPROVER_jsa_iterator_id_t it,
const __CPROVER_jsa_word_t value )
inlinestatic

Definition at line 759 of file jsa.h.

Variable Documentation

◆ __CPROVER_jsa_jump_buffer

jmp_buf __CPROVER_jsa_jump_buffer
extern