cprover
ansi_c_languaget Class Reference

#include <ansi_c_language.h>

Inheritance diagram for ansi_c_languaget:
[legend]
Collaboration diagram for ansi_c_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
 
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< 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 Attributes

ansi_c_parse_treet 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)
 
- 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...
 
- 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 21 of file ansi_c_language.h.

Constructor & Destructor Documentation

◆ ~ansi_c_languaget()

ansi_c_languaget::~ansi_c_languaget ( )
override

Definition at line 228 of file ansi_c_language.cpp.

◆ ansi_c_languaget()

ansi_c_languaget::ansi_c_languaget ( )
inline

Definition at line 43 of file ansi_c_language.h.

Member Function Documentation

◆ description()

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

Reimplemented from languaget.

Definition at line 70 of file ansi_c_language.h.

◆ extensions()

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

Reimplemented from languaget.

Definition at line 29 of file ansi_c_language.cpp.

◆ from_expr()

bool ansi_c_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 154 of file ansi_c_language.cpp.

References expr2c().

◆ from_type()

bool ansi_c_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 163 of file ansi_c_language.cpp.

References type2c().

◆ generate_support_functions()

bool ansi_c_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 129 of file ansi_c_language.cpp.

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

◆ id()

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

Reimplemented from languaget.

Definition at line 69 of file ansi_c_language.h.

◆ modules_provided()

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

Reimplemented from languaget.

Definition at line 34 of file ansi_c_language.cpp.

References get_base_name(), and parse_path.

◆ new_language()

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

Implements languaget.

Definition at line 66 of file ansi_c_language.h.

◆ parse()

◆ preprocess()

bool ansi_c_languaget::preprocess ( std::istream &  instream,
const std::string &  path,
std::ostream &  outstream 
)
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().

◆ show_parse()

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

Implements languaget.

Definition at line 144 of file ansi_c_language.cpp.

References ansi_c_parse_treet::output(), and parse_tree.

◆ to_expr()

bool ansi_c_languaget::to_expr ( const std::string &  code,
const std::string &  module,
exprt expr,
const namespacet ns 
)
overridevirtual

◆ type_to_name()

bool ansi_c_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 172 of file ansi_c_language.cpp.

References type2name().

◆ typecheck()

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

Member Data Documentation

◆ parse_path

std::string ansi_c_languaget::parse_path
protected

Definition at line 77 of file ansi_c_language.h.

Referenced by modules_provided(), and parse().

◆ parse_tree

ansi_c_parse_treet ansi_c_languaget::parse_tree
protected

Definition at line 76 of file ansi_c_language.h.

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


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