#include <string>
#include <vector>
#include <util/irep/irep.h>

Include dependency graph for cprover_library.h:

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

Functions
void	register_bundled_libc ()
const std::string *	internal_libc_header_dir ()
void	add_bundled_library_sources (contextt &context, const languaget &c_language)
void	add_cprover_library (contextt &context, const languaget *language=nullptr)
void	record_library_symbol (const irep_idt &id)
	Record that `id` came from a bundled operational-model library rather than from the program.
void	prune_unreferenced_library_functions (contextt &context, const goto_functionst *prelowered=nullptr)
	Erase every library FUNCTION symbol not reachable from the program's own symbols, so goto_convert never lowers it.
void	assert_no_pruned_calls (const goto_functionst &functions)
	Abort if any call in `functions` targets a symbol the prune erased.

Function Documentation

◆ add_bundled_library_sources()

void add_bundled_library_sources	(	contextt &	context,
		const languaget &	c_language )

◆ add_cprover_library()

void add_cprover_library	(	contextt &	context,
		const languaget *	language = nullptr )

◆ assert_no_pruned_calls()

void assert_no_pruned_calls ( const goto_functionst & functions )

Abort if any call in functions targets a symbol the prune erased.

◆ internal_libc_header_dir()

const std::string * internal_libc_header_dir ( )

◆ prune_unreferenced_library_functions()

void prune_unreferenced_library_functions	(	contextt &	context,
		const goto_functionst *	prelowered = nullptr )

Erase every library FUNCTION symbol not reachable from the program's own symbols, so goto_convert never lowers it.

Frontends whose converter resolves model calls by name (Python) cannot use the declaration-driven filter in add_cprover_library, because at load time the context holds no program yet: they link the models wholesale and call this once the converter has run. Only code symbols are erased – types stay, so the closed-world exception registry (exception_typeidt) is unchanged.

Pair it with assert_no_pruned_calls after goto_convert: a pass that runs between the two can introduce a reference this closure could not see, and that must fail loudly rather than leave a bodyless function returning nondet.

prelowered carries the bodies of a library shipped as GOTO (the Python model blob), whose symbols reach the context with nil values: without it the walk sees no edge out of a model function and erases everything it calls.

◆ record_library_symbol()

void record_library_symbol ( const irep_idt & id )

Record that id came from a bundled operational-model library rather than from the program.

Loaders outside this file (the Python model blob) call it so prune_unreferenced_library_functions can tell the two apart by provenance instead of by guessing from the symbol name.

◆ register_bundled_libc()

void register_bundled_libc ( )

Functions