CBMC
|
#include <ansi_c_language.h>
Public Member Functions | |
void | set_language_options (const optionst &options, message_handlert &) override |
Set language-specific options. More... | |
bool | preprocess (std::istream &instream, const std::string &path, std::ostream &outstream, message_handlert &message_handler) override |
ANSI-C preprocessing. More... | |
bool | parse (std::istream &instream, const std::string &path, message_handlert &message_handler) override |
bool | generate_support_functions (symbol_table_baset &symbol_table, message_handlert &message_handler) override |
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and language-specific library functions. More... | |
bool | typecheck (symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler, const bool keep_file_local) override |
typecheck without removing specified entries from the symbol table More... | |
bool | typecheck (symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler, const bool keep_file_local, const std::set< irep_idt > &keep) |
bool | can_keep_file_local () override |
Is it possible to call three-argument typecheck() on this object? More... | |
bool | typecheck (symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler) override |
void | show_parse (std::ostream &out, message_handlert &) 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, message_handlert &message_handler) 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 |
Public Member Functions inherited from languaget | |
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, message_handlert &message_handler) |
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 | interfaces (symbol_table_baset &symbol_table, message_handlert &message_handler) |
languaget () | |
virtual | ~languaget () |
Protected Attributes | |
ansi_c_parse_treet | parse_tree |
std::string | parse_path |
c_object_factory_parameterst | object_factory_params |
Definition at line 34 of file ansi_c_language.h.
|
override |
Definition at line 237 of file ansi_c_language.cpp.
|
inline |
Definition at line 87 of file ansi_c_language.h.
|
inlineoverridevirtual |
Is it possible to call three-argument typecheck() on this object?
Reimplemented from languaget.
Definition at line 71 of file ansi_c_language.h.
|
inlineoverridevirtual |
Implements languaget.
Definition at line 117 of file ansi_c_language.h.
|
overridevirtual |
Implements languaget.
Definition at line 28 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 157 of file ansi_c_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 166 of file ansi_c_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 138 of file ansi_c_language.cpp.
|
inlineoverridevirtual |
Implements languaget.
Definition at line 116 of file ansi_c_language.h.
|
overridevirtual |
Reimplemented from languaget.
Definition at line 33 of file ansi_c_language.cpp.
|
inlineoverridevirtual |
Implements languaget.
Definition at line 111 of file ansi_c_language.h.
|
overridevirtual |
Implements languaget.
Definition at line 52 of file ansi_c_language.cpp.
|
overridevirtual |
ANSI-C preprocessing.
Reimplemented from languaget.
Definition at line 39 of file ansi_c_language.cpp.
|
inlineoverridevirtual |
Set language-specific options.
Reimplemented from languaget.
Definition at line 38 of file ansi_c_language.h.
|
overridevirtual |
Implements languaget.
Definition at line 147 of file ansi_c_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 |
message_handler | a message handler |
Implements languaget.
Definition at line 184 of file ansi_c_language.cpp.
|
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 175 of file ansi_c_language.cpp.
|
inlineoverridevirtual |
Implements languaget.
Definition at line 76 of file ansi_c_language.h.
|
overridevirtual |
typecheck without removing specified entries from the symbol table
Some concrete subclasses of languaget discard unused symbols from a goto binary as part of typechecking it. This function allows the caller to specify a list of symbols that should be kept, even if that language's typecheck() implementation would normally discard those symbols.
This function should only be called on objects for which a call to can_keep_symbols() returns true
.
Reimplemented from languaget.
Definition at line 106 of file ansi_c_language.cpp.
bool ansi_c_languaget::typecheck | ( | symbol_table_baset & | symbol_table, |
const std::string & | module, | ||
message_handlert & | message_handler, | ||
const bool | keep_file_local, | ||
const std::set< irep_idt > & | keep | ||
) |
Definition at line 115 of file ansi_c_language.cpp.
|
protected |
Definition at line 126 of file ansi_c_language.h.
|
protected |
Definition at line 124 of file ansi_c_language.h.
|
protected |
Definition at line 123 of file ansi_c_language.h.