#include <json_symtab_language.h>

Inheritance diagram for json_symtab_languaget:

Collaboration diagram for json_symtab_languaget:

Public Member Functions
bool	parse (std::istream &instream, const std::string &path, message_handlert &message_handler) override
	Parse a goto program in json form. More...

bool	typecheck (symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler) override
	Typecheck a goto program in json form. More...

void	show_parse (std::ostream &out, message_handlert &) override
	Output the result of the parsed json file to the output stream passed as a parameter to this function. More...

bool	to_expr (const std::string &, const std::string &, exprt &, const namespacet &, message_handlert &) override
	Parses the given string into an expression. More...

std::string	id () const override

std::string	description () const override

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

std::unique_ptr< languaget >	new_language () override

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

	~json_symtab_languaget () override=default

Public Member Functions inherited from languaget
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 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	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 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...

	languaget ()

virtual	~languaget ()

Protected Attributes
jsont	parsed_json_file

Detailed Description

Definition at line 24 of file json_symtab_language.h.

Constructor & Destructor Documentation

◆ ~json_symtab_languaget()

json_symtab_languaget::~json_symtab_languaget ( )

overridedefault

Member Function Documentation

◆ description()

std::string json_symtab_languaget::description ( ) const

inlineoverridevirtual

Implements languaget.

Definition at line 53 of file json_symtab_language.h.

◆ extensions()

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

inlineoverridevirtual

Implements languaget.

Definition at line 58 of file json_symtab_language.h.

◆ generate_support_functions()

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

inlineoverridevirtual

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 68 of file json_symtab_language.h.

◆ id()

std::string json_symtab_languaget::id ( ) const

inlineoverridevirtual

Implements languaget.

Definition at line 49 of file json_symtab_language.h.

◆ new_language()

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

inlineoverridevirtual

Implements languaget.

Definition at line 63 of file json_symtab_language.h.

◆ parse()

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

overridevirtual

Parse a goto program in json form.

Parameters

instream	The input stream
path	A file path
message_handler	A message handler

Returns: boolean signifying success or failure of the parsing

Implements languaget.

Definition at line 25 of file json_symtab_language.cpp.

◆ show_parse()

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

overridevirtual

Output the result of the parsed json file to the output stream passed as a parameter to this function.

Parameters

out	The stream to use to output the parsed_json_file.
message_handler	A message handler

Implements languaget.

Definition at line 64 of file json_symtab_language.cpp.

◆ to_expr()

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

inlineoverridevirtual

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 39 of file json_symtab_language.h.

◆ typecheck()

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

overridevirtual

Typecheck a goto program in json form.

Parameters

symbol_table	The symbol table containing symbols read from file.
module	A useless parameter, there for interface consistency.
message_handler	A message handler

Returns: boolean signifying success or failure of the typechecking.

Implements languaget.

Definition at line 38 of file json_symtab_language.cpp.

Member Data Documentation

◆ parsed_json_file

jsont json_symtab_languaget::parsed_json_file

protected

Definition at line 82 of file json_symtab_language.h.

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

/home/runner/work/cbmc/cbmc/src/json-symtab-language/json_symtab_language.h
/home/runner/work/cbmc/cbmc/src/json-symtab-language/json_symtab_language.cpp

Public Member Functions

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ ~json_symtab_languaget()

Member Function Documentation

◆ description()

◆ extensions()

◆ generate_support_functions()

◆ id()

◆ new_language()

◆ parse()

◆ show_parse()

◆ to_expr()

◆ typecheck()

Member Data Documentation

◆ parsed_json_file