Provides a wrapper for a map of lazily loaded goto_functiont. More...

#include <lazy_goto_functions_map.h>

Collaboration diagram for lazy_goto_functions_mapt:

Public Types
typedef irep_idt	key_type

typedef goto_functiont &	mapped_type

typedef const goto_functiont &	const_mapped_type
	The type of elements returned by const members. More...

typedef std::pair< const key_type, goto_functiont >	value_type

typedef value_type &	reference

typedef const value_type &	const_reference

typedef value_type *	pointer

typedef const value_type *	const_pointer

typedef std::size_t	size_type

typedef std::function< void(const irep_idt &name, goto_functionst::goto_functiont &function, journalling_symbol_tablet &function_symbols)>	post_process_functiont

typedef std::function< bool(const irep_idt &name)>	can_generate_function_bodyt

typedef std::function< bool(const irep_idt &function_name, symbol_table_baset &symbol_table, goto_functiont &function, bool body_available)>	generate_function_bodyt

Public Member Functions
	lazy_goto_functions_mapt (underlying_mapt &goto_functions, language_filest &language_files, symbol_tablet &symbol_table, post_process_functiont post_process_function, can_generate_function_bodyt driver_program_can_generate_function_body, generate_function_bodyt driver_program_generate_function_body, message_handlert &message_handler)
	Creates a lazy_goto_functions_mapt. More...

const_mapped_type	at (const key_type &name) const
	Gets the body for a given function. More...

mapped_type	at (const key_type &name)
	Gets the body for a given function. More...

bool	can_produce_function (const key_type &name) const
	Determines if this lazy GOTO functions map can produce a body for the given function. More...

std::size_t	unload (const key_type &name) const
	Remove the function named `name` from the function map, if it exists. More...

void	ensure_function_loaded (const key_type &name) const

Private Types
typedef std::map< key_type, goto_functiont >	underlying_mapt

Private Member Functions
reference	ensure_function_loaded_internal (const key_type &name) const

reference	ensure_entry_converted (const key_type &name, symbol_table_baset &function_symbol_table) const
	Convert a function if not already converted, then return a reference to its goto_functionst map entry. More...

Private Attributes
underlying_mapt &	goto_functions

std::unordered_set< irep_idt >	processed_functions
	Names of functions that are already fully available in the programt state. More...

language_filest &	language_files

symbol_tablet &	symbol_table

const post_process_functiont	post_process_function

const can_generate_function_bodyt	driver_program_can_generate_function_body

const generate_function_bodyt	driver_program_generate_function_body

message_handlert &	message_handler

Detailed Description

Provides a wrapper for a map of lazily loaded goto_functiont.

This incrementally builds a goto-functions object, while permitting access to goto programs while they are still under construction. The intended workflow:

The front-end registers the functions that are potentially available, probably by use of langapi/language_file.h
The main function registers functions that should be run on each program, in sequence, after it is converted.
Analyses will then access functions using the at function
Template Parameters

bodyt The type of the function bodies, usually goto_programt

Definition at line 29 of file lazy_goto_functions_map.h.

Member Typedef Documentation

◆ can_generate_function_bodyt

typedef std::function<bool(const irep_idt &name)> lazy_goto_functions_mapt::can_generate_function_bodyt

Definition at line 57 of file lazy_goto_functions_map.h.

◆ const_mapped_type

typedef const goto_functiont& lazy_goto_functions_mapt::const_mapped_type

The type of elements returned by const members.

Definition at line 38 of file lazy_goto_functions_map.h.

◆ const_pointer

typedef const value_type* lazy_goto_functions_mapt::const_pointer

Definition at line 48 of file lazy_goto_functions_map.h.

◆ const_reference

typedef const value_type& lazy_goto_functions_mapt::const_reference

Definition at line 44 of file lazy_goto_functions_map.h.

◆ generate_function_bodyt

typedef std::function<bool( const irep_idt &function_name, symbol_table_baset &symbol_table, goto_functiont &function, bool body_available)> lazy_goto_functions_mapt::generate_function_bodyt

Definition at line 63 of file lazy_goto_functions_map.h.

◆ key_type

typedef irep_idt lazy_goto_functions_mapt::key_type

Definition at line 33 of file lazy_goto_functions_map.h.

◆ mapped_type

typedef goto_functiont& lazy_goto_functions_mapt::mapped_type

Definition at line 35 of file lazy_goto_functions_map.h.

◆ pointer

typedef value_type* lazy_goto_functions_mapt::pointer

Definition at line 46 of file lazy_goto_functions_map.h.

◆ post_process_functiont

typedef std::function<void( const irep_idt &name, goto_functionst::goto_functiont &function, journalling_symbol_tablet &function_symbols)> lazy_goto_functions_mapt::post_process_functiont

Definition at line 56 of file lazy_goto_functions_map.h.

◆ reference

typedef value_type& lazy_goto_functions_mapt::reference

Definition at line 42 of file lazy_goto_functions_map.h.

◆ size_type

typedef std::size_t lazy_goto_functions_mapt::size_type

Definition at line 50 of file lazy_goto_functions_map.h.

◆ underlying_mapt

typedef std::map<key_type, goto_functiont> lazy_goto_functions_mapt::underlying_mapt

private

Definition at line 66 of file lazy_goto_functions_map.h.

◆ value_type

typedef std::pair<const key_type, goto_functiont> lazy_goto_functions_mapt::value_type

Definition at line 40 of file lazy_goto_functions_map.h.

Constructor & Destructor Documentation

◆ lazy_goto_functions_mapt()

lazy_goto_functions_mapt::lazy_goto_functions_mapt	(	underlying_mapt &	goto_functions,
		language_filest &	language_files,
		symbol_tablet &	symbol_table,
		post_process_functiont	post_process_function,
		can_generate_function_bodyt	driver_program_can_generate_function_body,
		generate_function_bodyt	driver_program_generate_function_body,
		message_handlert &	message_handler
	)

inline

Creates a lazy_goto_functions_mapt.

Definition at line 82 of file lazy_goto_functions_map.h.

Member Function Documentation

◆ at() [1/2]

mapped_type lazy_goto_functions_mapt::at ( const key_type & name )

inline

Gets the body for a given function.

Parameters

name	The name of the function to search for.

Returns: The function body corresponding to the given function.

Definition at line 113 of file lazy_goto_functions_map.h.

◆ at() [2/2]

const_mapped_type lazy_goto_functions_mapt::at ( const key_type & name ) const

inline

Gets the body for a given function.

Parameters

name	The name of the function to search for.

Returns: The function body corresponding to the given function.

Definition at line 105 of file lazy_goto_functions_map.h.

◆ can_produce_function()

bool lazy_goto_functions_mapt::can_produce_function ( const key_type & name ) const

inline

Determines if this lazy GOTO functions map can produce a body for the given function.

Parameters

name	function ID to query

Returns: true if we can produce a function body, or false if we would leave it a bodyless stub.

Definition at line 123 of file lazy_goto_functions_map.h.

◆ ensure_entry_converted()

reference lazy_goto_functions_mapt::ensure_entry_converted	(	const key_type &	name,
		symbol_table_baset &	function_symbol_table
	)		const

inlineprivate

Convert a function if not already converted, then return a reference to its goto_functionst map entry.

Parameters

name	ID of the function to convert
function_symbol_table	mutable symbol table reference to be used when converting the function (e.g. to add new local variables). Note we should not use a global pre-cached symbol table reference for this so that our callers can insert a journalling table here if needed.

Returns: reference to the new or existing goto_functions map entry.

Definition at line 174 of file lazy_goto_functions_map.h.

◆ ensure_function_loaded()

void lazy_goto_functions_mapt::ensure_function_loaded ( const key_type & name ) const

inline

Definition at line 137 of file lazy_goto_functions_map.h.

◆ ensure_function_loaded_internal()

reference lazy_goto_functions_mapt::ensure_function_loaded_internal ( const key_type & name ) const

inlineprivate

Definition at line 146 of file lazy_goto_functions_map.h.

◆ unload()

std::size_t lazy_goto_functions_mapt::unload ( const key_type & name ) const

inline

Remove the function named name from the function map, if it exists.

Returns: Returns 0 when name was not present, and 1 when name was removed.

Definition at line 132 of file lazy_goto_functions_map.h.

Member Data Documentation

◆ driver_program_can_generate_function_body

const can_generate_function_bodyt lazy_goto_functions_mapt::driver_program_can_generate_function_body

private

Definition at line 76 of file lazy_goto_functions_map.h.

◆ driver_program_generate_function_body

const generate_function_bodyt lazy_goto_functions_mapt::driver_program_generate_function_body

private

Definition at line 77 of file lazy_goto_functions_map.h.

◆ goto_functions

underlying_mapt& lazy_goto_functions_mapt::goto_functions

private

Definition at line 67 of file lazy_goto_functions_map.h.

◆ language_files

language_filest& lazy_goto_functions_mapt::language_files

private

Definition at line 73 of file lazy_goto_functions_map.h.

◆ message_handler

message_handlert& lazy_goto_functions_mapt::message_handler

private

Definition at line 78 of file lazy_goto_functions_map.h.

◆ post_process_function

const post_process_functiont lazy_goto_functions_mapt::post_process_function

private

Definition at line 75 of file lazy_goto_functions_map.h.

◆ processed_functions

std::unordered_set<irep_idt> lazy_goto_functions_mapt::processed_functions

mutableprivate

Names of functions that are already fully available in the programt state.

Remarks: These functions do not need processing before being returned whenever they are requested

Definition at line 71 of file lazy_goto_functions_map.h.

◆ symbol_table

symbol_tablet& lazy_goto_functions_mapt::symbol_table

private

Definition at line 74 of file lazy_goto_functions_map.h.

The documentation for this class was generated from the following file:

/home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/lazy_goto_functions_map.h

Public Types

Public Member Functions

Private Types

Private Member Functions

Private Attributes

Detailed Description

Member Typedef Documentation

◆ can_generate_function_bodyt

◆ const_mapped_type

◆ const_pointer

◆ const_reference

◆ generate_function_bodyt

◆ key_type

◆ mapped_type

◆ pointer

◆ post_process_functiont

◆ reference

◆ size_type

◆ underlying_mapt

◆ value_type

Constructor & Destructor Documentation

◆ lazy_goto_functions_mapt()

Member Function Documentation

◆ at() [1/2]

◆ at() [2/2]

◆ can_produce_function()

◆ ensure_entry_converted()

◆ ensure_function_loaded()

◆ ensure_function_loaded_internal()

◆ unload()

Member Data Documentation

◆ driver_program_can_generate_function_body

◆ driver_program_generate_function_body

◆ goto_functions

◆ language_files

◆ message_handler

◆ post_process_function

◆ processed_functions

◆ symbol_table