cprover
|
#include <jsil_language.h>
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... | |
![]() | |
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 () |
Protected Attributes | |
jsil_parse_treet | parse_tree |
std::string | parse_path |
![]() | |
bool | generate_opaque_stubs =false |
bool | language_options_initialized =false |
Additional Inherited Members | |
![]() | |
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 ¶meter) |
To build the parameter symbol and choose its name. More... | |
![]() | |
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... | |
Definition at line 23 of file jsil_language.h.
|
virtual |
Definition at line 169 of file jsil_language.cpp.
|
inline |
Definition at line 45 of file jsil_language.h.
|
inlineoverridevirtual |
Reimplemented from languaget.
Definition at line 67 of file jsil_language.h.
|
overridevirtual |
Reimplemented from languaget.
Definition at line 24 of file jsil_language.cpp.
|
overridevirtual |
Formats the given expression in a language-specific way.
expr | the expression to format |
code | the formatted expression |
ns | a namespace |
Reimplemented from languaget.
Definition at line 107 of file jsil_language.cpp.
References expr2jsil().
|
overridevirtual |
Formats the given type in a language-specific way.
type | the type to format |
code | the formatted type |
ns | a namespace |
Reimplemented from languaget.
Definition at line 116 of file jsil_language.cpp.
References type2jsil().
|
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().
|
inlineoverridevirtual |
Reimplemented from languaget.
Definition at line 66 of file jsil_language.h.
|
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.
|
overridevirtual |
Reimplemented from languaget.
Definition at line 29 of file jsil_language.cpp.
References get_base_name(), and parse_path.
|
inlineoverridevirtual |
Implements languaget.
Definition at line 63 of file jsil_language.h.
|
overridevirtual |
Implements languaget.
Definition at line 53 of file jsil_language.cpp.
References jsil_parsert::clear(), messaget::get_message_handler(), parsert::in, jsil_parser, jsil_scanner_init(), jsil_parsert::parse(), parse_path, jsil_parsert::parse_tree, parse_tree, messaget::result(), parsert::set_file(), messaget::set_message_handler(), and jsil_parse_treet::swap().
|
overridevirtual |
Reimplemented from languaget.
Definition at line 44 of file jsil_language.cpp.
|
overridevirtual |
Implements languaget.
Definition at line 97 of file jsil_language.cpp.
References jsil_parse_treet::output(), and parse_tree.
|
overridevirtual |
Parses the given string into an expression.
code | the string to parse |
module | prefix to be used for identifiers |
expr | the parsed expression |
ns | a namespace |
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.
|
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().
|
protected |
Definition at line 76 of file jsil_language.h.
Referenced by modules_provided(), and parse().
|
protected |
Definition at line 75 of file jsil_language.h.
Referenced by interfaces(), parse(), show_parse(), and to_expr().