cprover
jsil_languaget Class Reference

#include <jsil_language.h>

Inheritance diagram for jsil_languaget:
[legend]
Collaboration diagram for jsil_languaget:
[legend]

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< languagetnew_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 get_language_options (const cmdlinet &)
 
virtual void dependencies (const std::string &module, std::set< std::string > &modules)
 
virtual void methods_provided (std::unordered_set< irep_idt > &methods) const
 
virtual void convert_lazy_method (const irep_idt &function_id, symbol_table_baset &symbol_table)
 
virtual bool final (symbol_table_baset &symbol_table)
 Final adjustments, e.g. 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...
 
void set_should_generate_opaque_method_stubs (bool should_generate_stubs)
 Turn on or off stub generation. More...
 
 languaget ()
 
virtual ~languaget ()
 
- Public Member Functions inherited from messaget
virtual void set_message_handler (message_handlert &_message_handler)
 
message_handlertget_message_handler ()
 
 messaget ()
 
 messaget (const messaget &other)
 
messagetoperator= (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level) const
 
mstreamterror () const
 
mstreamtwarning () const
 
mstreamtresult () const
 
mstreamtstatus () const
 
mstreamtstatistics () const
 
mstreamtprogress () const
 
mstreamtdebug () const
 
void conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
 Generate output to mstream using output_generator if the configured verbosity is at least as high as that of mstream. More...
 

Protected Attributes

jsil_parse_treet parse_tree
 
std::string parse_path
 
- Protected Attributes inherited from languaget
bool generate_opaque_stubs =false
 
bool language_options_initialized =false
 
- Protected Attributes inherited from messaget
message_handlertmessage_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 mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 
- Protected Member Functions inherited from languaget
void generate_opaque_method_stubs (symbol_tablet &symbol_table)
 When there are opaque methods (e.g. More...
 
virtual irep_idt generate_opaque_stub_body (symbolt &symbol, symbol_tablet &symbol_table)
 To generate the stub function for the opaque function in question. More...
 
virtual parameter_symbolt build_stub_parameter_symbol (const symbolt &function_symbol, size_t parameter_index, const code_typet::parametert &parameter)
 To build the parameter symbol and choose its name. More...
 
- Static Protected Member Functions inherited from languaget
static irep_idt get_stub_return_symbol_name (const irep_idt &function_id)
 To get the name of the symbol to be used for the return value of the function. 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

Reimplemented from languaget.

Definition at line 67 of file jsil_language.h.

◆ extensions()

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

Reimplemented from 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
exprthe expression to format
codethe formatted expression
nsa namespace
Returns
false if conversion succeeds

Reimplemented from languaget.

Definition at line 107 of file jsil_language.cpp.

References expr2jsil().

◆ 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
typethe type to format
codethe formatted type
nsa namespace
Returns
false if conversion succeeds

Reimplemented from languaget.

Definition at line 116 of file jsil_language.cpp.

References type2jsil().

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

References messaget::get_message_handler(), and jsil_entry_point().

◆ id()

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

Reimplemented from 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.

References messaget::get_message_handler(), jsil_convert(), jsil_internal_additions(), and parse_tree.

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

References get_base_name(), and parse_path.

◆ 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

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

References jsil_parse_treet::output(), and parse_tree.

◆ 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
codethe string to parse
moduleprefix to be used for identifiers
exprthe parsed expression
nsa namespace
Returns
false if the conversion succeeds

Implements languaget.

Definition at line 125 of file jsil_language.cpp.

References jsil_parsert::clear(), messaget::get_message_handler(), parsert::in, jsil_parse_treet::items, jsil_convert(), jsil_parser, jsil_scanner_init(), jsil_typecheck(), irept::make_nil(), jsil_parsert::parse(), jsil_parsert::parse_tree, parse_tree, messaget::result(), parsert::set_file(), messaget::set_message_handler(), and symbol_table_baset::symbols.

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

References messaget::get_message_handler(), and jsil_typecheck().

Member Data Documentation

◆ parse_path

std::string jsil_languaget::parse_path
protected

Definition at line 76 of file jsil_language.h.

Referenced by modules_provided(), and parse().

◆ parse_tree

jsil_parse_treet jsil_languaget::parse_tree
protected

Definition at line 75 of file jsil_language.h.

Referenced by interfaces(), parse(), show_parse(), and to_expr().


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