cprover
|
#include <jsil_language.h>
Public Member Functions | |
bool | preprocess (std::istream &instream, const std::string &path, std::ostream &outstream) override |
bool | parse (std::istream &instream, const std::string &path) override |
bool | generate_support_functions (symbol_table_baset &symbol_table) override |
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and language-specific library functions. | |
bool | typecheck (symbol_table_baset &context, const std::string &module) override |
Converting from parse tree and type checking. | |
void | show_parse (std::ostream &out) override |
virtual | ~jsil_languaget () |
jsil_languaget () | |
bool | from_expr (const exprt &expr, std::string &code, const namespacet &ns) override |
Formats the given expression in a language-specific way. | |
bool | from_type (const typet &type, std::string &code, const namespacet &ns) override |
Formats the given type in a language-specific way. | |
bool | to_expr (const std::string &code, const std::string &module, exprt &expr, const namespacet &ns) override |
Parses the given string into an expression. | |
std::unique_ptr< languaget > | new_language () override |
std::string | id () const override |
std::string | description () const override |
std::set< std::string > | extensions () const override |
void | modules_provided (std::set< std::string > &modules) override |
bool | interfaces (symbol_table_baset &symbol_table) override |
Adding symbols for all procedure declarations. | |
![]() | |
virtual void | set_language_options (const optionst &) |
Set language-specific options. | |
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. | |
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 . | |
virtual bool | final (symbol_table_baset &symbol_table) |
Final adjustments, e.g. | |
virtual bool | can_keep_file_local () |
Is it possible to call three-argument typecheck() on this object? | |
virtual bool | typecheck (symbol_table_baset &symbol_table, const std::string &module, const bool keep_file_local) |
typecheck without removing specified entries from the symbol table | |
virtual bool | type_to_name (const typet &type, std::string &name, const namespacet &ns) |
Encodes the given type in a language-specific way. | |
languaget () | |
virtual | ~languaget () |
Protected Attributes | |
jsil_parse_treet | parse_tree |
std::string | parse_path |
Additional Inherited Members |
Definition at line 23 of file jsil_language.h.
|
virtual |
Definition at line 169 of file jsil_language.cpp.
|
inline |
Definition at line 41 of file jsil_language.h.
|
inlineoverridevirtual |
Implements languaget.
Definition at line 62 of file jsil_language.h.
|
overridevirtual |
Implements 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.
|
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.
|
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.
|
inlineoverridevirtual |
Implements languaget.
Definition at line 58 of file jsil_language.h.
|
overridevirtual |
Adding symbols for all procedure declarations.
Reimplemented from languaget.
Definition at line 35 of file jsil_language.cpp.
|
overridevirtual |
Reimplemented from languaget.
Definition at line 29 of file jsil_language.cpp.
|
inlineoverridevirtual |
Implements languaget.
Definition at line 55 of file jsil_language.h.
Implements languaget.
Definition at line 53 of file jsil_language.cpp.
|
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.
|
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.
|
overridevirtual |
Converting from parse tree and type checking.
Implements languaget.
Definition at line 79 of file jsil_language.cpp.
|
protected |
Definition at line 71 of file jsil_language.h.
|
protected |
Definition at line 70 of file jsil_language.h.