#include <python-frontend/python_library.h>
#include <goto-programs/goto_binary_reader.h>
#include <goto-programs/goto_functions.h>
#include <util/symtab/context.h>
#include <c2goto/cprover_library.h>
#include <cstdlib>

Include dependency graph for python_library.cpp:

Functions
void	add_cpython_library (contextt &context)
void	link_cpython_library_bodies (goto_functionst &dest)
	Attach the blob's model bodies to `dest`.
const goto_functionst &	cpython_library_bodies ()
	The blob's model bodies.

Variables
const uint8_t	pysrc64_buf []
const unsigned int	pysrc64_buf_size

Function Documentation

◆ add_cpython_library()

void add_cpython_library ( contextt & context )

◆ cpython_library_bodies()

const goto_functionst & cpython_library_bodies ( )

The blob's model bodies.

Their symbols carry nil values, so a dependency walk over the context alone cannot see what a model calls.

◆ link_cpython_library_bodies()

void link_cpython_library_bodies ( goto_functionst & dest )

Attach the blob's model bodies to dest.

Runs after goto_convert, which creates their bodyless entries from the declarations.

Variable Documentation

◆ pysrc64_buf

const uint8_t pysrc64_buf[]

extern

◆ pysrc64_buf_size

const unsigned int pysrc64_buf_size