cprover
|
#include <ansi_c_language.h>
Public Member Functions | |
bool | preprocess (std::istream &instream, const std::string &path, std::ostream &outstream) override |
ANSI-C preprocessing. More... | |
bool | parse (std::istream &instream, const std::string &path) override |
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... | |
bool | typecheck (symbol_tablet &symbol_table, const std::string &module) override |
void | show_parse (std::ostream &out) override |
~ansi_c_languaget () override | |
ansi_c_languaget () | |
bool | from_expr (const exprt &expr, std::string &code, const namespacet &ns) override |
Formats the given expression in a language-specific way. More... | |
bool | from_type (const typet &type, std::string &code, const namespacet &ns) override |
Formats the given type in a language-specific way. More... | |
bool | type_to_name (const typet &type, std::string &name, const namespacet &ns) override |
Encodes the given type in a language-specific way. More... | |
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... | |
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 |
![]() | |
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 | interfaces (symbol_tablet &symbol_table) |
void | set_should_generate_opaque_method_stubs (bool should_generate_stubs) |
Turn on or off stub generation. More... | |
languaget () | |
virtual | ~languaget () |
Protected Attributes | |
ansi_c_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 21 of file ansi_c_language.h.
|
override |
Definition at line 228 of file ansi_c_language.cpp.
|
inline |
Definition at line 43 of file ansi_c_language.h.
|
inlineoverridevirtual |
Reimplemented from languaget.
Definition at line 70 of file ansi_c_language.h.
|
overridevirtual |
Reimplemented from languaget.
Definition at line 29 of file ansi_c_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 154 of file ansi_c_language.cpp.
References expr2c().
|
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 163 of file ansi_c_language.cpp.
References type2c().
|
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 129 of file ansi_c_language.cpp.
References ansi_c_entry_point(), languaget::generate_opaque_method_stubs(), and messaget::get_message_handler().
|
inlineoverridevirtual |
Reimplemented from languaget.
Definition at line 69 of file ansi_c_language.h.
|
overridevirtual |
Reimplemented from languaget.
Definition at line 34 of file ansi_c_language.cpp.
References get_base_name(), and parse_path.
|
inlineoverridevirtual |
Implements languaget.
Definition at line 66 of file ansi_c_language.h.
|
overridevirtual |
Implements languaget.
Definition at line 52 of file ansi_c_language.cpp.
References configt::ansi_c, ansi_c_internal_additions(), ansi_c_parser, ansi_c_scanner_init(), ansi_c_parsert::clear(), config, ansi_c_parsert::cpp11, ansi_c_parsert::cpp98, configt::ansi_ct::Float128_type, ansi_c_parsert::Float128_type, configt::ansi_ct::for_has_scope, ansi_c_parsert::for_has_scope, messaget::get_message_handler(), parsert::in, ansi_c_parsert::mode, configt::ansi_ct::mode, ansi_c_parsert::parse(), parse_path, ansi_c_parsert::parse_tree, parse_tree, preprocess(), messaget::result(), parsert::set_file(), parsert::set_line_no(), messaget::set_message_handler(), ansi_c_parse_treet::swap(), configt::ansi_ct::ts_18661_3_Floatn_types, and ansi_c_parsert::ts_18661_3_Floatn_types.
Referenced by add_library(), and compilet::parse_stdin().
|
overridevirtual |
ANSI-C preprocessing.
Reimplemented from languaget.
Definition at line 40 of file ansi_c_language.cpp.
References c_preprocess(), and messaget::get_message_handler().
Referenced by parse(), and compilet::parse_stdin().
|
overridevirtual |
Implements languaget.
Definition at line 144 of file ansi_c_language.cpp.
References ansi_c_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 181 of file ansi_c_language.cpp.
References configt::ansi_c, ansi_c_parser, ansi_c_scanner_init(), ansi_c_typecheck(), ansi_c_parsert::clear(), config, messaget::get_message_handler(), irept::id(), parsert::in, ansi_c_parse_treet::items, irept::make_nil(), ansi_c_parsert::mode, configt::ansi_ct::mode, exprt::op0(), exprt::operands(), ansi_c_parsert::parse(), ansi_c_parsert::parse_tree, messaget::result(), parsert::set_file(), messaget::set_message_handler(), configt::ansi_ct::ts_18661_3_Floatn_types, ansi_c_parsert::ts_18661_3_Floatn_types, and exprt::type().
|
overridevirtual |
Encodes the given type in a language-specific way.
type | the type to encode |
name | the encoded type |
ns | a namespace |
Reimplemented from languaget.
Definition at line 172 of file ansi_c_language.cpp.
References type2name().
|
overridevirtual |
Implements languaget.
Definition at line 106 of file ansi_c_language.cpp.
References ansi_c_typecheck(), messaget::get_message_handler(), linking(), parse_tree, and remove_internal_symbols().
Referenced by add_library().
|
protected |
Definition at line 77 of file ansi_c_language.h.
Referenced by modules_provided(), and parse().
|
protected |
Definition at line 76 of file ansi_c_language.h.
Referenced by parse(), show_parse(), and typecheck().