#include <language.h>

Inheritance diagram for languaget:

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

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

virtual bool	parse (std::istream &instream, const std::string &path, message_handlert &message_handler)=0

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

virtual void	dependencies (const std::string &module, std::set< std::string > &modules)

virtual void	modules_provided (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. More...

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`. More...

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

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

virtual bool	typecheck (symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler)=0

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

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

virtual std::string	id () const =0

virtual std::string	description () const =0

virtual std::set< std::string >	extensions () const =0

virtual void	show_parse (std::ostream &out, message_handlert &message_handler)=0

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

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

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

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

virtual std::unique_ptr< languaget >	new_language ()=0

	languaget ()

virtual	~languaget ()

Detailed Description

Definition at line 36 of file language.h.

Constructor & Destructor Documentation

◆ languaget()

languaget::languaget ( )

inline

Definition at line 219 of file language.h.

◆ ~languaget()

virtual languaget::~languaget ( )

inlinevirtual

Definition at line 220 of file language.h.

Member Function Documentation

◆ can_keep_file_local()

virtual bool languaget::can_keep_file_local ( )

inlinevirtual

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

Reimplemented in statement_list_languaget, and ansi_c_languaget.

Definition at line 132 of file language.h.

◆ convert_lazy_method()

virtual void languaget::convert_lazy_method	(	const irep_idt &	function_id,
		symbol_table_baset &	symbol_table,
		message_handlert &	message_handler
	)

inlinevirtual

Requests this languaget should populate the body of method function_id in symbol_table.

This will only be called if methods_provided advertised the given function_id could be provided by this languaget instance.

Reimplemented in java_bytecode_languaget.

Definition at line 103 of file language.h.

◆ dependencies()

void languaget::dependencies	(	const std::string &	module,
		std::set< std::string > &	modules
	)

virtual

Definition at line 26 of file language.cpp.

◆ description()

virtual std::string languaget::description ( ) const

pure virtual

Implemented in statement_list_languaget, json_symtab_languaget, cpp_languaget, ansi_c_languaget, and java_bytecode_languaget.

◆ extensions()

virtual std::set<std::string> languaget::extensions ( ) const

pure virtual

Implemented in statement_list_languaget, json_symtab_languaget, cpp_languaget, ansi_c_languaget, and java_bytecode_languaget.

◆ final()

bool languaget::final ( symbol_table_baset & symbol_table )

virtual

Final adjustments, e.g.

initializing stub functions and globals that were discovered during function loading

Reimplemented in java_bytecode_languaget.

Definition at line 16 of file language.cpp.

◆ from_expr()

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

virtual

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 in statement_list_languaget, cpp_languaget, ansi_c_languaget, and java_bytecode_languaget.

Definition at line 32 of file language.cpp.

◆ from_type()

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

virtual

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 in statement_list_languaget, cpp_languaget, ansi_c_languaget, and java_bytecode_languaget.

Definition at line 41 of file language.cpp.

◆ generate_support_functions()

virtual bool languaget::generate_support_functions	(	symbol_table_baset &	symbol_table,
		message_handlert &	message_handler
	)

pure virtual

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.

Implemented in cpp_languaget, ansi_c_languaget, java_bytecode_languaget, statement_list_languaget, and json_symtab_languaget.

◆ id()

virtual std::string languaget::id ( ) const

pure virtual

Implemented in statement_list_languaget, json_symtab_languaget, cpp_languaget, ansi_c_languaget, and java_bytecode_languaget.

◆ interfaces()

bool languaget::interfaces	(	symbol_table_baset &	symbol_table,
		message_handlert &	message_handler
	)

virtual

Definition at line 21 of file language.cpp.

◆ methods_provided()

virtual void languaget::methods_provided ( std::unordered_set< irep_idt > & methods ) const

inlinevirtual

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.

there is no need to mention methods whose bodies are eagerly generated). It should be prepared to handle a convert_lazy_method call for any symbol added to methods.

Reimplemented in java_bytecode_languaget.

Definition at line 94 of file language.h.

◆ modules_provided()

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

inlinevirtual

Reimplemented in statement_list_languaget, cpp_languaget, ansi_c_languaget, and java_bytecode_languaget.

Definition at line 84 of file language.h.

◆ new_language()

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

pure virtual

Implemented in statement_list_languaget, json_symtab_languaget, cpp_languaget, ansi_c_languaget, and java_bytecode_languaget.

◆ parse()

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

pure virtual

Implemented in statement_list_languaget, json_symtab_languaget, cpp_languaget, ansi_c_languaget, and java_bytecode_languaget.

◆ preprocess()

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

inlinevirtual

Reimplemented in cpp_languaget, ansi_c_languaget, and java_bytecode_languaget.

Definition at line 46 of file language.h.

◆ set_language_options()

virtual void languaget::set_language_options	(	const optionst &	,
		message_handlert &
	)

inlinevirtual

Set language-specific options.

Reimplemented in statement_list_languaget, cpp_languaget, ansi_c_languaget, and java_bytecode_languaget.

Definition at line 40 of file language.h.

◆ show_parse()

virtual void languaget::show_parse	(	std::ostream &	out,
		message_handlert &	message_handler
	)

pure virtual

Implemented in statement_list_languaget, json_symtab_languaget, cpp_languaget, ansi_c_languaget, and java_bytecode_languaget.

◆ to_expr()

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

pure virtual

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

Implemented in statement_list_languaget, cpp_languaget, ansi_c_languaget, java_bytecode_languaget, and json_symtab_languaget.

◆ type_to_name()

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

virtual

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 in statement_list_languaget, cpp_languaget, and ansi_c_languaget.

Definition at line 50 of file language.cpp.

◆ typecheck() [1/2]

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

pure virtual

Implemented in json_symtab_languaget, cpp_languaget, ansi_c_languaget, statement_list_languaget, and java_bytecode_languaget.

◆ typecheck() [2/2]

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

inlinevirtual

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 in statement_list_languaget, and ansi_c_languaget.

Definition at line 146 of file language.h.

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

/home/runner/work/cbmc/cbmc/src/langapi/language.h
/home/runner/work/cbmc/cbmc/src/langapi/language.cpp

Public Member Functions

Detailed Description

Constructor & Destructor Documentation

◆ languaget()

◆ ~languaget()

Member Function Documentation

◆ can_keep_file_local()

◆ convert_lazy_method()

◆ dependencies()

◆ description()

◆ extensions()

◆ final()

◆ from_expr()

◆ from_type()

◆ generate_support_functions()

◆ id()

◆ interfaces()

◆ methods_provided()

◆ modules_provided()

◆ new_language()

◆ parse()

◆ preprocess()

◆ set_language_options()

◆ show_parse()

◆ to_expr()

◆ type_to_name()

◆ typecheck() [1/2]

◆ typecheck() [2/2]