#include <jsil_language.h>

Inheritance diagram for jsil_languaget:

Collaboration diagram for jsil_languaget:

Public Member Functions
virtual bool	preprocess (std::istream &instream, const std::string &path, std::ostream &outstream) override

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

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

virtual bool	typecheck (symbol_tablet &context, const std::string &module) override
	Converting from parse tree and type checking. More...

virtual void	show_parse (std::ostream &out) override

virtual	~jsil_languaget ()

	jsil_languaget ()

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

virtual bool	from_type (const typet &type, std::string &code, const namespacet &ns) override
	Formats 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) override
	Parses the given string into an expression. More...

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

virtual std::string	id () const override

virtual std::string	description () const override

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

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

virtual bool	interfaces (symbol_tablet &symbol_table) override
	Adding symbols for all procedure declarations. More...

Public Member Functions inherited from languaget
virtual void	set_language_options (const optionst &)
	Set language-specific options. More...

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

virtual void	convert_lazy_method (const irep_idt &function_id, symbol_table_baset &symbol_table)
	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	can_keep_file_local ()
	Is it possible to call three-argument typecheck() on this object? More...

virtual bool	typecheck (symbol_tablet &symbol_table, const std::string &module, const bool keep_file_local)
	typecheck without removing specified entries from the symbol table 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 ()

Public Member Functions inherited from messaget
virtual void	set_message_handler (message_handlert &_message_handler)

message_handlert &	get_message_handler ()

	messaget ()

	messaget (const messaget &other)

messaget &	operator= (const messaget &other)

	messaget (message_handlert &_message_handler)

virtual	~messaget ()

mstreamt &	get_mstream (unsigned message_level) const

mstreamt &	error () const

mstreamt &	warning () const

mstreamt &	result () const

mstreamt &	status () const

mstreamt &	statistics () const

mstreamt &	progress () const

mstreamt &	debug () const

void	conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
	Generate output to `message_stream` using `output_generator` if the configured verbosity is at least as high as that of `message_stream`. More...

Protected Attributes
jsil_parse_treet	parse_tree

std::string	parse_path

Protected Attributes inherited from messaget
message_handlert *	message_handler

mstreamt	mstream

Additional Inherited Members
Public Types inherited from messaget
enum	message_levelt { M_ERROR =1, M_WARNING =2, M_RESULT =4, M_STATUS =6, M_STATISTICS =8, M_PROGRESS =9, M_DEBUG =10 }

Static Public Member Functions inherited from messaget
static unsigned	eval_verbosity (const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
	Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest. More...

static commandt	command (unsigned c)
	Create an ECMA-48 SGR (Select Graphic Rendition) command. More...

Static Public Attributes inherited from messaget
static eomt	eom

static const commandt	reset
	return to default formatting, as defined by the terminal More...

static const commandt	red
	render text with red foreground color More...

static const commandt	green
	render text with green foreground color More...

static const commandt	yellow
	render text with yellow foreground color More...

static const commandt	blue
	render text with blue foreground color More...

static const commandt	magenta
	render text with magenta foreground color More...

static const commandt	cyan
	render text with cyan foreground color More...

static const commandt	bright_red
	render text with bright red foreground color More...

static const commandt	bright_green
	render text with bright green foreground color More...

static const commandt	bright_yellow
	render text with bright yellow foreground color More...

static const commandt	bright_blue
	render text with bright blue foreground color More...

static const commandt	bright_magenta
	render text with bright magenta foreground color More...

static const commandt	bright_cyan
	render text with bright cyan foreground color More...

static const commandt	bold
	render text with bold font More...

static const commandt	faint
	render text with faint font More...

static const commandt	italic
	render italic text More...

static const commandt	underline
	render underlined text More...

Detailed Description

Definition at line 23 of file jsil_language.h.

Constructor & Destructor Documentation

◆ ~jsil_languaget()

jsil_languaget::~jsil_languaget ( )

virtual

Definition at line 169 of file jsil_language.cpp.

◆ jsil_languaget()

jsil_languaget::jsil_languaget ( )

inline

Definition at line 45 of file jsil_language.h.

Member Function Documentation

◆ description()

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

inlineoverridevirtual

Implements languaget.

Definition at line 67 of file jsil_language.h.

◆ extensions()

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

overridevirtual

Implements languaget.

Definition at line 24 of file jsil_language.cpp.

◆ from_expr()

bool jsil_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 107 of file jsil_language.cpp.

◆ from_type()

bool jsil_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 116 of file jsil_language.cpp.

◆ generate_support_functions()

bool jsil_languaget::generate_support_functions ( symbol_tablet & symbol_table )

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 89 of file jsil_language.cpp.

◆ id()

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

inlineoverridevirtual

Implements languaget.

Definition at line 66 of file jsil_language.h.

◆ interfaces()

bool jsil_languaget::interfaces ( symbol_tablet & symbol_table )

overridevirtual

Adding symbols for all procedure declarations.

Reimplemented from languaget.

Definition at line 35 of file jsil_language.cpp.

◆ modules_provided()

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

overridevirtual

Reimplemented from languaget.

Definition at line 29 of file jsil_language.cpp.

◆ new_language()

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

inlineoverridevirtual

Implements languaget.

Definition at line 63 of file jsil_language.h.

◆ parse()

bool jsil_languaget::parse	(	std::istream &	instream,
		const std::string &	path
	)

overridevirtual

Implements languaget.

Definition at line 53 of file jsil_language.cpp.

◆ preprocess()

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

overridevirtual

Reimplemented from languaget.

Definition at line 44 of file jsil_language.cpp.

◆ show_parse()

void jsil_languaget::show_parse ( std::ostream & out )

overridevirtual

Implements languaget.

Definition at line 97 of file jsil_language.cpp.

◆ to_expr()

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

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

Returns: false if the conversion succeeds

Implements languaget.

Definition at line 125 of file jsil_language.cpp.

◆ typecheck()

bool jsil_languaget::typecheck	(	symbol_tablet &	context,
		const std::string &	module
	)

overridevirtual

Converting from parse tree and type checking.

Implements languaget.

Definition at line 79 of file jsil_language.cpp.

Member Data Documentation

◆ parse_path

std::string jsil_languaget::parse_path

protected

Definition at line 76 of file jsil_language.h.

◆ parse_tree

jsil_parse_treet jsil_languaget::parse_tree

protected

Definition at line 75 of file jsil_language.h.

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

/home/runner/work/cbmc-documentation/cbmc-documentation/src/jsil/jsil_language.h
/home/runner/work/cbmc-documentation/cbmc-documentation/src/jsil/jsil_language.cpp

Public Member Functions

Protected Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ ~jsil_languaget()

◆ jsil_languaget()

Member Function Documentation

◆ description()

◆ extensions()

◆ from_expr()

◆ from_type()

◆ generate_support_functions()

◆ id()

◆ interfaces()

◆ modules_provided()

◆ new_language()

◆ parse()

◆ preprocess()

◆ show_parse()

◆ to_expr()

◆ typecheck()

Member Data Documentation

◆ parse_path

◆ parse_tree