#include <ansi_c_language.h>

Inheritance diagram for ansi_c_languaget:

Collaboration diagram for ansi_c_languaget:

Public Member Functions
void	set_language_options (const optionst &options, message_handlert &) override
	Set language-specific options.

bool	preprocess (std::istream &instream, const std::string &path, std::ostream &outstream, message_handlert &message_handler) override
	ANSI-C preprocessing.

bool	parse (std::istream &instream, const std::string &path, message_handlert &message_handler) override

bool	generate_support_functions (symbol_table_baset &symbol_table, message_handlert &message_handler) override
	Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and language-specific library functions.

bool	typecheck (symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler, const bool keep_file_local) override
	typecheck without removing specified entries from the symbol table

bool	typecheck (symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler, const bool keep_file_local, const std::set< irep_idt > &keep)

bool	can_keep_file_local () override
	Is it possible to call three-argument typecheck() on this object?

bool	typecheck (symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler) override

void	show_parse (std::ostream &out, message_handlert &) override

	~ansi_c_languaget () override

	ansi_c_languaget ()

bool	from_expr (const exprt &expr, std::string &code, const namespacet &ns) override
	Formats the given expression in a language-specific way.

bool	from_type (const typet &type, std::string &code, const namespacet &ns) override
	Formats the given type in a language-specific way.

bool	type_to_name (const typet &type, std::string &name, const namespacet &ns) override
	Encodes the given type in a language-specific way.

bool	to_expr (const std::string &code, const std::string &module, exprt &expr, const namespacet &ns, message_handlert &message_handler) override
	Parses the given string into an expression.

std::unique_ptr< languaget >	new_language () override

std::string	id () const override

std::string	description () const override

std::set< std::string >	extensions () const override

void	modules_provided (std::set< std::string > &modules) override

Public Member Functions inherited from languaget
virtual void	dependencies (const std::string &module, std::set< std::string > &modules)

virtual void	methods_provided (std::unordered_set< irep_idt > &methods) const
	Should fill `methods` with the symbol identifiers of all methods this `languaget` can provide a body for, but doesn't populate that body in languaget::typecheck (i.e.

virtual void	convert_lazy_method (const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
	Requests this `languaget` should populate the body of method `function_id` in `symbol_table`.

virtual bool	final (symbol_table_baset &symbol_table)
	Final adjustments, e.g.

virtual bool	interfaces (symbol_table_baset &symbol_table, message_handlert &message_handler)

	languaget ()

virtual	~languaget ()

Protected Attributes
ansi_c_parse_treet	parse_tree

std::string	parse_path

c_object_factory_parameterst	object_factory_params

Detailed Description

Definition at line 34 of file ansi_c_language.h.

Constructor & Destructor Documentation

◆ ~ansi_c_languaget()

ansi_c_languaget::~ansi_c_languaget ( )

override

Definition at line 240 of file ansi_c_language.cpp.

◆ ansi_c_languaget()

ansi_c_languaget::ansi_c_languaget ( )

inline

Definition at line 87 of file ansi_c_language.h.

Member Function Documentation

◆ can_keep_file_local()

bool ansi_c_languaget::can_keep_file_local ( )

inlineoverridevirtual

Is it possible to call three-argument typecheck() on this object?

Reimplemented from languaget.

Definition at line 71 of file ansi_c_language.h.

◆ description()

std::string ansi_c_languaget::description ( ) const

inlineoverridevirtual

Implements languaget.

Definition at line 117 of file ansi_c_language.h.

◆ extensions()

std::set< std::string > ansi_c_languaget::extensions ( ) const

overridevirtual

Implements languaget.

Definition at line 26 of file ansi_c_language.cpp.

◆ from_expr()

bool ansi_c_languaget::from_expr	(	const exprt &	expr,
		std::string &	code,
		const namespacet &	ns
	)

overridevirtual

Formats the given expression in a language-specific way.

Parameters

expr	the expression to format
code	the formatted expression
ns	a namespace

Returns: false if conversion succeeds

Reimplemented from languaget.

Definition at line 160 of file ansi_c_language.cpp.

◆ from_type()

bool ansi_c_languaget::from_type	(	const typet &	type,
		std::string &	code,
		const namespacet &	ns
	)

overridevirtual

Formats the given type in a language-specific way.

Parameters

type	the type to format
code	the formatted type
ns	a namespace

Returns: false if conversion succeeds

Reimplemented from languaget.

Definition at line 169 of file ansi_c_language.cpp.

◆ generate_support_functions()

bool ansi_c_languaget::generate_support_functions	(	symbol_table_baset &	symbol_table,
		message_handlert &	message_handler
	)

overridevirtual

Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and language-specific library functions.

This runs after the typecheck phase but before lazy function loading. Anything that must wait until lazy function loading is done can be deferred until final, which runs after lazy function loading is complete. Functions introduced here are visible to lazy loading and can influence its decisions (e.g. picking the types of input parameters and globals), whereas anything introduced during final cannot.

Implements languaget.

Definition at line 141 of file ansi_c_language.cpp.

◆ id()

std::string ansi_c_languaget::id ( ) const

inlineoverridevirtual

Implements languaget.

Definition at line 116 of file ansi_c_language.h.

◆ modules_provided()

void ansi_c_languaget::modules_provided ( std::set< std::string > & modules )

overridevirtual

Reimplemented from languaget.

Definition at line 31 of file ansi_c_language.cpp.

◆ new_language()

std::unique_ptr< languaget > ansi_c_languaget::new_language ( )

inlineoverridevirtual

Implements languaget.

Definition at line 111 of file ansi_c_language.h.

◆ parse()

bool ansi_c_languaget::parse	(	std::istream &	instream,
		const std::string &	path,
		message_handlert &	message_handler
	)

overridevirtual

Implements languaget.

Definition at line 50 of file ansi_c_language.cpp.

◆ preprocess()

bool ansi_c_languaget::preprocess	(	std::istream &	instream,
		const std::string &	path,
		std::ostream &	outstream,
		message_handlert &	message_handler
	)

overridevirtual

ANSI-C preprocessing.

Reimplemented from languaget.

Definition at line 37 of file ansi_c_language.cpp.

◆ set_language_options()

void ansi_c_languaget::set_language_options	(	const optionst &	,
		message_handlert &
	)

inlineoverridevirtual

Set language-specific options.

Reimplemented from languaget.

Definition at line 38 of file ansi_c_language.h.

◆ show_parse()

void ansi_c_languaget::show_parse	(	std::ostream &	out,
		message_handlert &
	)

overridevirtual

Implements languaget.

Definition at line 150 of file ansi_c_language.cpp.

◆ to_expr()

bool ansi_c_languaget::to_expr	(	const std::string &	code,
		const std::string &	module,
		exprt &	expr,
		const namespacet &	ns,
		message_handlert &	message_handler
	)

overridevirtual

Parses the given string into an expression.

Parameters

code	the string to parse
module	prefix to be used for identifiers
expr	the parsed expression
ns	a namespace
message_handler	a message handler

Returns: false if the conversion succeeds

Implements languaget.

Definition at line 187 of file ansi_c_language.cpp.

◆ type_to_name()

bool ansi_c_languaget::type_to_name	(	const typet &	type,
		std::string &	name,
		const namespacet &	ns
	)

overridevirtual

Encodes the given type in a language-specific way.

Parameters

type	the type to encode
name	the encoded type
ns	a namespace

Returns: false if the conversion succeeds

Reimplemented from languaget.

Definition at line 178 of file ansi_c_language.cpp.

◆ typecheck() [1/3]

bool ansi_c_languaget::typecheck	(	symbol_table_baset &	symbol_table,
		const std::string &	module,
		message_handlert &	message_handler
	)

inlineoverridevirtual

Implements languaget.

Definition at line 76 of file ansi_c_language.h.

◆ typecheck() [2/3]

bool ansi_c_languaget::typecheck	(	symbol_table_baset &	symbol_table,
		const std::string &	module,
		message_handlert &	message_handler,
		const bool	keep_file_local
	)

overridevirtual

typecheck without removing specified entries from the symbol table

Some concrete subclasses of languaget discard unused symbols from a goto binary as part of typechecking it. This function allows the caller to specify a list of symbols that should be kept, even if that language's typecheck() implementation would normally discard those symbols.

This function should only be called on objects for which a call to can_keep_symbols() returns true.

Reimplemented from languaget.

Definition at line 109 of file ansi_c_language.cpp.

◆ typecheck() [3/3]

bool ansi_c_languaget::typecheck	(	symbol_table_baset &	symbol_table,
		const std::string &	module,
		message_handlert &	message_handler,
		const bool	keep_file_local,
		const std::set< irep_idt > &	keep
	)

Definition at line 118 of file ansi_c_language.cpp.

Member Data Documentation

◆ object_factory_params

c_object_factory_parameterst ansi_c_languaget::object_factory_params

protected

Definition at line 126 of file ansi_c_language.h.

◆ parse_path

std::string ansi_c_languaget::parse_path

protected

Definition at line 124 of file ansi_c_language.h.

◆ parse_tree

ansi_c_parse_treet ansi_c_languaget::parse_tree

protected

Definition at line 123 of file ansi_c_language.h.

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

/home/runner/work/cbmc/cbmc/src/ansi-c/ansi_c_language.h
/home/runner/work/cbmc/cbmc/src/ansi-c/ansi_c_language.cpp

Public Member Functions

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ ~ansi_c_languaget()

◆ ansi_c_languaget()

Member Function Documentation

◆ can_keep_file_local()

◆ description()

◆ extensions()

◆ from_expr()

◆ from_type()

◆ generate_support_functions()

◆ id()

◆ modules_provided()

◆ new_language()

◆ parse()

◆ preprocess()

◆ set_language_options()

◆ show_parse()

◆ to_expr()

◆ type_to_name()

◆ typecheck() [1/3]

◆ typecheck() [2/3]

◆ typecheck() [3/3]

Member Data Documentation

◆ object_factory_params

◆ parse_path

◆ parse_tree