cprover
cpp_languaget Class Reference

#include <cpp_language.h>

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

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
 
bool merge_symbol_table (symbol_tablet &dest, symbol_tablet &src, const std::string &module, class replace_symbolt &replace_symbol) const
 
void show_parse (std::ostream &out) override
 
 ~cpp_languaget () override
 
 cpp_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< languagetnew_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 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 ()
 
- 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 Member Functions

void show_parse (std::ostream &out, const cpp_itemt &item)
 
std::string main_symbol ()
 
- 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...
 

Protected Attributes

cpp_parse_treet cpp_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)
 
- 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 cpp_language.h.

Constructor & Destructor Documentation

◆ ~cpp_languaget()

cpp_languaget::~cpp_languaget ( )
override

Definition at line 276 of file cpp_language.cpp.

◆ cpp_languaget()

cpp_languaget::cpp_languaget ( )
inline

Definition at line 52 of file cpp_language.h.

Member Function Documentation

◆ description()

std::string cpp_languaget::description ( ) const
inlineoverridevirtual

Reimplemented from languaget.

Definition at line 82 of file cpp_language.h.

◆ extensions()

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

Reimplemented from languaget.

Definition at line 33 of file cpp_language.cpp.

◆ from_expr()

bool cpp_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 211 of file cpp_language.cpp.

References expr2cpp().

◆ from_type()

bool cpp_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 220 of file cpp_language.cpp.

References type2cpp().

◆ generate_support_functions()

bool cpp_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 137 of file cpp_language.cpp.

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

◆ id()

std::string cpp_languaget::id ( ) const
inlineoverridevirtual

Reimplemented from languaget.

Definition at line 81 of file cpp_language.h.

◆ main_symbol()

std::string cpp_languaget::main_symbol ( )
inlineprotected

Definition at line 93 of file cpp_language.h.

◆ merge_symbol_table()

bool cpp_languaget::merge_symbol_table ( symbol_tablet dest,
symbol_tablet src,
const std::string &  module,
class replace_symbolt replace_symbol 
) const

◆ modules_provided()

void cpp_languaget::modules_provided ( std::set< std::string > &  modules)
overridevirtual

Reimplemented from languaget.

Definition at line 51 of file cpp_language.cpp.

References get_base_name(), and parse_path.

◆ new_language()

std::unique_ptr<languaget> cpp_languaget::new_language ( )
inlineoverridevirtual

Implements languaget.

Definition at line 78 of file cpp_language.h.

◆ parse()

◆ preprocess()

bool cpp_languaget::preprocess ( std::istream &  instream,
const std::string &  path,
std::ostream &  outstream 
)
overridevirtual

ANSI-C preprocessing.

Reimplemented from languaget.

Definition at line 57 of file cpp_language.cpp.

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

Referenced by parse().

◆ show_parse() [1/2]

void cpp_languaget::show_parse ( std::ostream &  out)
overridevirtual

Implements languaget.

Definition at line 143 of file cpp_language.cpp.

References cpp_parse_tree, and cpp_parse_treet::items.

Referenced by show_parse().

◆ show_parse() [2/2]

◆ to_expr()

bool cpp_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 238 of file cpp_language.cpp.

References cpp_parsert::clear(), cpp_parser, cpp_typecheck(), messaget::get_message_handler(), parsert::in, cpp_parse_treet::items, irept::make_nil(), cpp_parsert::parse(), cpp_parsert::parse_tree, messaget::result(), parsert::set_file(), and messaget::set_message_handler().

◆ type_to_name()

bool cpp_languaget::type_to_name ( const typet type,
std::string &  name,
const namespacet ns 
)
overridevirtual

Encodes the given type in a language-specific way.

Parameters
typethe type to encode
namethe encoded type
nsa namespace
Returns
false if the conversion succeeds

Reimplemented from languaget.

Definition at line 229 of file cpp_language.cpp.

References cpp_type2name().

◆ typecheck()

bool cpp_languaget::typecheck ( symbol_tablet symbol_table,
const std::string &  module 
)
overridevirtual

Implements languaget.

Definition at line 121 of file cpp_language.cpp.

References cpp_parse_tree, cpp_typecheck(), messaget::get_message_handler(), and linking().

Member Data Documentation

◆ cpp_parse_tree

cpp_parse_treet cpp_languaget::cpp_parse_tree
protected

Definition at line 88 of file cpp_language.h.

Referenced by parse(), show_parse(), and typecheck().

◆ parse_path

std::string cpp_languaget::parse_path
protected

Definition at line 89 of file cpp_language.h.

Referenced by modules_provided(), and parse().


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