list.c File Reference

#include <stdbool.h>
#include <stdlib.h>
#include <stdint.h>
#include <string.h>
#include "python_types.h"

Include dependency graph for list.c:

Classes
struct	__ESBMC_pointer_cell

Macros
#define	__ESBMC_FLOAT_BUF_SIZE   4096
#define	__ESBMC_LIST_DEFAULT_DEPTH   4
#define	__ESBMC_LIST_MAX_STACK   64

Functions
int	__python_scalar_eq_obj (const PyObject *a, const PyObject *b, size_t num_type_id, size_t bool_type_id)
void *	__ESBMC_new_object ()
struct	__attribute__ ((packed, may_alias))
static uint64_t	__ESBMC_load_u64 (const void *p)
static bool	__ESBMC_values_equal (const void *a, const void *b, size_t size)
PyObject *	__ESBMC_create_inf_obj ()
PyListObject *	__ESBMC_list_create ()
size_t	__ESBMC_list_size (const PyListObject *l)
static void *	__ESBMC_copy_value (const void *value, size_t size, size_t type_id, size_t float_type_id, size_t *out_float_idx, int ptr_free)
bool	__ESBMC_list_push (PyListObject *l, const void *value, size_t type_id, size_t type_size, size_t float_type_id, int ptr_free)
static void *	__ESBMC_copy_tagged_value (const void *value, size_t type_id, size_t size, size_t float_type_id, size_t *out_float_idx)
bool	__ESBMC_list_push_tagged (PyListObject *l, const void *value, size_t type_id, size_t size, size_t float_type_id)
bool	__ESBMC_list_push_object (PyListObject *l, PyObject *o, size_t float_type_id, int ptr_free)
static bool	__ESBMC_list_push_shallow_sz (PyListObject *l, PyObject *o, size_t list_type_id, size_t elem_size, size_t float_type_id)
bool	__ESBMC_list_push_shallow_tagged (PyListObject *l, PyObject *o, size_t list_type_id, size_t float_type_id)
bool	__ESBMC_list_push_shallow (PyListObject *l, PyObject *o, size_t list_type_id, size_t elem_size)
bool	__ESBMC_list_push_dict_ptr (PyListObject *l, void *dict_ptr, size_t type_id)
bool	__ESBMC_list_set_dict_ptr (PyListObject *l, size_t index, void *dict_ptr, size_t type_id)
static size_t	__ESBMC_elem_cmp_size (const PyObject *o, size_t elem_size)
static size_t	__ESBMC_list_eq_depth_limit (size_t max_depth)
bool	__ESBMC_list_eq (const PyListObject *l1, const PyListObject *l2, size_t list_type_id, size_t max_depth, size_t float_type_id, size_t elem_size)
bool	__ESBMC_list_eq_tagged (const PyListObject *l1, const PyListObject *l2, size_t num_type_id, size_t bool_type_id)
bool	__ESBMC_list_set_eq (const PyListObject *l1, const PyListObject *l2)
PyObject *	__ESBMC_list_at (PyListObject *l, size_t index)
bool	__ESBMC_list_set_at (PyListObject *l, size_t index, const void *value, size_t type_id, size_t type_size, size_t float_type_id, int ptr_free)
bool	__ESBMC_list_insert (PyListObject *l, int64_t index, const void *value, size_t type_id, size_t type_size, size_t float_type_id, int ptr_free)
bool	__ESBMC_list_insert_tagged (PyListObject *l, int64_t index, const void *value, size_t type_id, size_t size, size_t float_type_id)
bool	__ESBMC_list_contains (const PyListObject *l, const void *item, size_t item_type_id, size_t item_size)
size_t	__ESBMC_list_count (const PyListObject *l, const void *item, size_t item_type_id, size_t item_size)
size_t	__ESBMC_list_index (const PyListObject *l, const void *item, size_t item_type_id, size_t item_size)
size_t	__ESBMC_list_index_range (const PyListObject *l, const void *item, size_t item_type_id, size_t item_size, int64_t start, int64_t end)
void	__ESBMC_list_extend (PyListObject *l, const PyListObject *other, size_t elem_size)
void	__ESBMC_list_extend_tagged (PyListObject *l, const PyListObject *other, size_t float_type_id)
void	__ESBMC_list_clear (PyListObject *l)
size_t	__ESBMC_list_find_index (PyListObject *l, const void *item, size_t item_type_id, size_t item_size)
static bool	__ESBMC_key_equal (const void *a, const void *b, size_t size)
size_t	__ESBMC_list_try_find_index (PyListObject *l, const void *item, size_t item_type_id, size_t item_size)
bool	__ESBMC_list_remove_at (PyListObject *l, size_t index)
PyObject *	__ESBMC_list_pop (PyListObject *l, int64_t index)
bool	__ESBMC_dict_eq (const PyListObject *lhs_keys, const PyListObject *lhs_values, const PyListObject *rhs_keys, const PyListObject *rhs_values, size_t float_type_id)
PyListObject *	__ESBMC_list_copy (const PyListObject *l)
PyListObject *	__ESBMC_list_copy_shallow_sz (PyListObject *l, size_t list_type_id, size_t elem_size, size_t float_type_id)
PyListObject *	__ESBMC_list_copy_shallow (PyListObject *l, size_t list_type_id)
void	__ESBMC_list_mark_tuple (PyListObject *l)
bool	__ESBMC_list_is_tuple (const PyListObject *l)
static void	__ESBMC_list_store_elem (PyObject *slot, const PyObject *o, size_t list_type_id, size_t elem_size)
bool	__ESBMC_list_slice_assign (PyListObject *l, int64_t lower, int has_lower, int64_t upper, int has_upper, int64_t step, const PyListObject *src, size_t list_type_id, size_t elem_size)
static bool	__ESBMC_list_remove_first (PyListObject *l, const void *item, size_t item_type_id, size_t item_size)
bool	__ESBMC_list_remove (PyListObject *l, const void *item, size_t item_type_id, size_t item_size)
bool	__ESBMC_set_add (PyListObject *s, const void *item, size_t item_type_id, size_t item_size)
bool	__ESBMC_set_discard (PyListObject *s, const void *item, size_t item_type_id, size_t item_size)
void	__ESBMC_list_sort (PyListObject *l, int type_flag, uint64_t float_type_id)
bool	__ESBMC_list_lt (const PyListObject *l1, const PyListObject *l2, int type_flag, size_t float_type_id)
void	__ESBMC_list_reverse (PyListObject *l)
void	__ESBMC_list_reverse_range (PyListObject *l, int64_t lower, int has_lower, int64_t upper, int has_upper)

Variables
static PyType	__ESBMC_generic_type
static PyType	__ESBMC_list_type
static double	__ESBMC_float_buf [__ESBMC_FLOAT_BUF_SIZE]
static size_t	__ESBMC_float_buf_idx = 0
bool	__ESBMC_list_retyped = false

Macro Definition Documentation

__ESBMC_FLOAT_BUF_SIZE

#define __ESBMC_FLOAT_BUF_SIZE   4096

__ESBMC_LIST_DEFAULT_DEPTH

#define __ESBMC_LIST_DEFAULT_DEPTH   4

__ESBMC_LIST_MAX_STACK

#define __ESBMC_LIST_MAX_STACK   64

Function Documentation

__attribute__()

struct __attribute__

(

(packed, may_alias)

)

__ESBMC_copy_tagged_value()

void * __ESBMC_copy_tagged_value ( const void * value, size_t type_id, size_t size, size_t float_type_id, size_t * out_float_idx )

static

__ESBMC_copy_value()

void * __ESBMC_copy_value ( const void * value, size_t size, size_t type_id, size_t float_type_id, size_t * out_float_idx, int ptr_free )

inlinestatic

__ESBMC_create_inf_obj()

PyObject * __ESBMC_create_inf_obj

(

)

__ESBMC_dict_eq()

bool __ESBMC_dict_eq	(	const PyListObject *	lhs_keys,
		const PyListObject *	lhs_values,
		const PyListObject *	rhs_keys,
		const PyListObject *	rhs_values,
		size_t	float_type_id )

__ESBMC_elem_cmp_size()

size_t __ESBMC_elem_cmp_size ( const PyObject * o, size_t elem_size )

inlinestatic

__ESBMC_key_equal()

bool __ESBMC_key_equal ( const void * a, const void * b, size_t size )

inlinestatic

__ESBMC_list_at()

PyObject * __ESBMC_list_at	(	PyListObject *	l,
		size_t	index )

__ESBMC_list_clear()

void __ESBMC_list_clear

(

PyListObject *

l

)

__ESBMC_list_contains()

bool __ESBMC_list_contains	(	const PyListObject *	l,
		const void *	item,
		size_t	item_type_id,
		size_t	item_size )

__ESBMC_list_copy()

PyListObject * __ESBMC_list_copy

(

const PyListObject *

l

)

__ESBMC_list_copy_shallow()

PyListObject * __ESBMC_list_copy_shallow	(	PyListObject *	l,
		size_t	list_type_id )

__ESBMC_list_copy_shallow_sz()

PyListObject * __ESBMC_list_copy_shallow_sz	(	PyListObject *	l,
		size_t	list_type_id,
		size_t	elem_size,
		size_t	float_type_id )

__ESBMC_list_count()

size_t __ESBMC_list_count	(	const PyListObject *	l,
		const void *	item,
		size_t	item_type_id,
		size_t	item_size )

__ESBMC_list_create()

PyListObject * __ESBMC_list_create

(

)

__ESBMC_list_eq()

bool __ESBMC_list_eq	(	const PyListObject *	l1,
		const PyListObject *	l2,
		size_t	list_type_id,
		size_t	max_depth,
		size_t	float_type_id,
		size_t	elem_size )

__ESBMC_list_eq_depth_limit()

size_t __ESBMC_list_eq_depth_limit ( size_t max_depth )

inlinestatic

__ESBMC_list_eq_tagged()

bool __ESBMC_list_eq_tagged	(	const PyListObject *	l1,
		const PyListObject *	l2,
		size_t	num_type_id,
		size_t	bool_type_id )

__ESBMC_list_extend()

void __ESBMC_list_extend	(	PyListObject *	l,
		const PyListObject *	other,
		size_t	elem_size )

__ESBMC_list_extend_tagged()

void __ESBMC_list_extend_tagged	(	PyListObject *	l,
		const PyListObject *	other,
		size_t	float_type_id )

__ESBMC_list_find_index()

size_t __ESBMC_list_find_index	(	PyListObject *	l,
		const void *	item,
		size_t	item_type_id,
		size_t	item_size )

__ESBMC_list_index()

size_t __ESBMC_list_index	(	const PyListObject *	l,
		const void *	item,
		size_t	item_type_id,
		size_t	item_size )

__ESBMC_list_index_range()

size_t __ESBMC_list_index_range	(	const PyListObject *	l,
		const void *	item,
		size_t	item_type_id,
		size_t	item_size,
		int64_t	start,
		int64_t	end )

__ESBMC_list_insert()

bool __ESBMC_list_insert	(	PyListObject *	l,
		int64_t	index,
		const void *	value,
		size_t	type_id,
		size_t	type_size,
		size_t	float_type_id,
		int	ptr_free )

__ESBMC_list_insert_tagged()

bool __ESBMC_list_insert_tagged	(	PyListObject *	l,
		int64_t	index,
		const void *	value,
		size_t	type_id,
		size_t	size,
		size_t	float_type_id )

__ESBMC_list_is_tuple()

bool __ESBMC_list_is_tuple

(

const PyListObject *

l

)

__ESBMC_list_lt()

bool __ESBMC_list_lt	(	const PyListObject *	l1,
		const PyListObject *	l2,
		int	type_flag,
		size_t	float_type_id )

__ESBMC_list_mark_tuple()

void __ESBMC_list_mark_tuple

(

PyListObject *

l

)

__ESBMC_list_pop()

PyObject * __ESBMC_list_pop	(	PyListObject *	l,
		int64_t	index )

__ESBMC_list_push()

bool __ESBMC_list_push	(	PyListObject *	l,
		const void *	value,
		size_t	type_id,
		size_t	type_size,
		size_t	float_type_id,
		int	ptr_free )

__ESBMC_list_push_dict_ptr()

bool __ESBMC_list_push_dict_ptr	(	PyListObject *	l,
		void *	dict_ptr,
		size_t	type_id )

__ESBMC_list_push_object()

bool __ESBMC_list_push_object	(	PyListObject *	l,
		PyObject *	o,
		size_t	float_type_id,
		int	ptr_free )

__ESBMC_list_push_shallow()

bool __ESBMC_list_push_shallow	(	PyListObject *	l,
		PyObject *	o,
		size_t	list_type_id,
		size_t	elem_size )

__ESBMC_list_push_shallow_sz()

bool __ESBMC_list_push_shallow_sz ( PyListObject * l, PyObject * o, size_t list_type_id, size_t elem_size, size_t float_type_id )

static

__ESBMC_list_push_shallow_tagged()

bool __ESBMC_list_push_shallow_tagged	(	PyListObject *	l,
		PyObject *	o,
		size_t	list_type_id,
		size_t	float_type_id )

__ESBMC_list_push_tagged()

bool __ESBMC_list_push_tagged	(	PyListObject *	l,
		const void *	value,
		size_t	type_id,
		size_t	size,
		size_t	float_type_id )

__ESBMC_list_remove()

bool __ESBMC_list_remove	(	PyListObject *	l,
		const void *	item,
		size_t	item_type_id,
		size_t	item_size )

__ESBMC_list_remove_at()

bool __ESBMC_list_remove_at	(	PyListObject *	l,
		size_t	index )

__ESBMC_list_remove_first()

bool __ESBMC_list_remove_first ( PyListObject * l, const void * item, size_t item_type_id, size_t item_size )

static

__ESBMC_list_reverse()

void __ESBMC_list_reverse

(

PyListObject *

l

)

__ESBMC_list_reverse_range()

void __ESBMC_list_reverse_range	(	PyListObject *	l,
		int64_t	lower,
		int	has_lower,
		int64_t	upper,
		int	has_upper )

__ESBMC_list_set_at()

bool __ESBMC_list_set_at	(	PyListObject *	l,
		size_t	index,
		const void *	value,
		size_t	type_id,
		size_t	type_size,
		size_t	float_type_id,
		int	ptr_free )

__ESBMC_list_set_dict_ptr()

bool __ESBMC_list_set_dict_ptr	(	PyListObject *	l,
		size_t	index,
		void *	dict_ptr,
		size_t	type_id )

__ESBMC_list_set_eq()

bool __ESBMC_list_set_eq	(	const PyListObject *	l1,
		const PyListObject *	l2 )

__ESBMC_list_size()

size_t __ESBMC_list_size

(

const PyListObject *

l

)

__ESBMC_list_slice_assign()

bool __ESBMC_list_slice_assign	(	PyListObject *	l,
		int64_t	lower,
		int	has_lower,
		int64_t	upper,
		int	has_upper,
		int64_t	step,
		const PyListObject *	src,
		size_t	list_type_id,
		size_t	elem_size )

__ESBMC_list_sort()

void __ESBMC_list_sort	(	PyListObject *	l,
		int	type_flag,
		uint64_t	float_type_id )

__ESBMC_list_store_elem()

void __ESBMC_list_store_elem ( PyObject * slot, const PyObject * o, size_t list_type_id, size_t elem_size )

static

__ESBMC_list_try_find_index()

size_t __ESBMC_list_try_find_index	(	PyListObject *	l,
		const void *	item,
		size_t	item_type_id,
		size_t	item_size )

__ESBMC_load_u64()

uint64_t __ESBMC_load_u64 ( const void * p )

inlinestatic

__ESBMC_new_object()

void * __ESBMC_new_object

(

)

__ESBMC_set_add()

bool __ESBMC_set_add	(	PyListObject *	s,
		const void *	item,
		size_t	item_type_id,
		size_t	item_size )

__ESBMC_set_discard()

bool __ESBMC_set_discard	(	PyListObject *	s,
		const void *	item,
		size_t	item_type_id,
		size_t	item_size )

__ESBMC_values_equal()

bool __ESBMC_values_equal ( const void * a, const void * b, size_t size )

inlinestatic

__python_scalar_eq_obj()

int __python_scalar_eq_obj	(	const PyObject *	a,
		const PyObject *	b,
		size_t	num_type_id,
		size_t	bool_type_id )

Variable Documentation

__ESBMC_float_buf

double __ESBMC_float_buf[__ESBMC_FLOAT_BUF_SIZE]

static

__ESBMC_float_buf_idx

size_t __ESBMC_float_buf_idx = 0

static

__ESBMC_generic_type

PyType __ESBMC_generic_type

static

__ESBMC_list_retyped

bool __ESBMC_list_retyped = false

__ESBMC_list_type

PyType __ESBMC_list_type

static