CBMC
Classes | Macros | Typedefs | Functions | Variables
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)   assert((c) && str)
 
#define __CPROVER_jsa__internal_get_head_node(heap_ptr, list)    (heap_ptr)->list_head_nodes[list]
 
#define __CPROVER_jsa__internal_is_concrete_node(node)    (node < __CPROVER_JSA_MAX_CONCRETE_NODES)
 
#define __CPROVER_jsa__internal_is_abstract_node(node)    (!__CPROVER_jsa__internal_is_concrete_node(node))
 
#define __CPROVER_jsa__internal_get_abstract_node_index(node)    (node - __CPROVER_JSA_MAX_CONCRETE_NODES)
 
#define __CPROVER_jsa__internal_get_abstract_node_id(node_index)    (__CPROVER_JSA_MAX_CONCRETE_NODES + 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)    __CPROVER_jsa_null!=(heap)->iterators[it].node_id
 

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. More...
 
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). More...
 
typedef struct __CPROVER_jsa_abstract_range __CPROVER_jsa_abstract_ranget
 Set of pre-defined, possible values for abstract nodes. More...
 
typedef struct __CPROVER_jsa_iterator __CPROVER_jsa_iteratort
 Iterators point to a node and give the relative index within that node. More...
 
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)     (__CPROVER_JSA_MAX_CONCRETE_NODES + node_index)

Definition at line 262 of file jsa.h.

◆ __CPROVER_jsa__internal_get_abstract_node_index

#define __CPROVER_jsa__internal_get_abstract_node_index (   node)     (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 
)     (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_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)     (!__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)     (node < __CPROVER_JSA_MAX_CONCRETE_NODES)

Definition at line 253 of file jsa.h.

◆ __CPROVER_jsa_assert

#define __CPROVER_jsa_assert (   c,
  str 
)    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 
)     __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_CONCRETE_NODES
#define __CPROVER_JSA_MAX_CONCRETE_NODES
Definition: jsa.h:43

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

static _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()

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

Definition at line 465 of file jsa.h.

◆ __CPROVER_jsa__internal_assume_linking_correct()

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

Definition at line 394 of file jsa.h.

◆ __CPROVER_jsa__internal_assume_valid_iterator_linking()

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

Definition at line 422 of file jsa.h.

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

Definition at line 447 of file jsa.h.

◆ __CPROVER_jsa__internal_is_in_valid_list()

static _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()

static _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()

static 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()

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

Definition at line 322 of file jsa.h.

◆ __CPROVER_jsa__internal_set_next()

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

Definition at line 270 of file jsa.h.

◆ __CPROVER_jsa__internal_set_previous()

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

Definition at line 296 of file jsa.h.

◆ __CPROVER_jsa_add()

static 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()

static 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()

static 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()

static 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()

static 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()

static __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()

static __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()

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

Definition at line 897 of file jsa.h.

◆ __CPROVER_jsa_iterator()

static __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()

static __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()

static __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()

static __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()

static __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()

static __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()

static 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()

static 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