python_types.h File Reference

#include <stdbool.h>
#include <stddef.h>

Include dependency graph for python_types.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
struct	__ESBMC_PyType
	Type object representation for Python-like types. More...
struct	__ESBMC_PyObj
	Minimal representation of a Python-like object. More...
struct	__ESBMC_PyListObj
	Minimal representation of a Python-like list object. More...
struct	__ESBMC_PySliceObj
	Minimal representation of a Python slice object. More...

Macros
#define	ESBMC_PY_STRNLEN_BOUND   256

Typedefs
typedef struct __ESBMC_PyType	PyType
	Type object representation for Python-like types.
typedef struct __ESBMC_PyObj	PyObject
	Minimal representation of a Python-like object.
typedef struct __ESBMC_PyListObj	PyListObject
	Minimal representation of a Python-like list object.
typedef struct __ESBMC_PySliceObj	PySliceObject
	Minimal representation of a Python slice object.

Macro Definition Documentation

ESBMC_PY_STRNLEN_BOUND

#define ESBMC_PY_STRNLEN_BOUND   256

Typedef Documentation

PyListObject

typedef struct __ESBMC_PyListObj PyListObject

Minimal representation of a Python-like list object.

Example usage in C:

PyListObject list = {...};
for (size_t i = 0; i < list.size; ++i) {
  PyObject *item = &list.items[i];
  // Access fields like item->type_id or item->value here
}

PyObject

typedef struct __ESBMC_PyObj PyObject

Minimal representation of a Python-like object.

In CPython, PyObject includes only a pointer to its type object. Most user-defined types embed this as their header, allowing any instance to be safely cast to PyObject* for type inspection.

This simplified version keeps both the type information and the data pointer explicit. The long-term goal is to embed only a type pointer, enabling more lightweight polymorphic casts.

PySliceObject

typedef struct __ESBMC_PySliceObj PySliceObject

Minimal representation of a Python slice object.

Mirrors CPython's slice(start, stop, step). Any of the three may be omitted by the user (e.g. slice(5) or a[i:]), in which case the corresponding has_* flag is zero and the integer field is unspecified.

PyType

typedef struct __ESBMC_PyType PyType

Type object representation for Python-like types.