CBMC
ansi_c_languaget Class Reference

#include <ansi_c_language.h>

+ Inheritance diagram for ansi_c_languaget:
+ Collaboration diagram for ansi_c_languaget:

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< 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 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
 

Detailed Description

Definition at line 34 of file ansi_c_language.h.

Constructor & Destructor Documentation

◆ ~ansi_c_languaget()

ansi_c_languaget::~ansi_c_languaget ( )
override

Definition at line 237 of file ansi_c_language.cpp.

◆ ansi_c_languaget()

ansi_c_languaget::ansi_c_languaget ( )
inline

Definition at line 87 of file ansi_c_language.h.

Member Function Documentation

◆ can_keep_file_local()

bool ansi_c_languaget::can_keep_file_local ( )
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.

◆ description()

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

Implements languaget.

Definition at line 117 of file ansi_c_language.h.

◆ extensions()

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

Implements languaget.

Definition at line 28 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 157 of file ansi_c_language.cpp.

◆ 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 166 of file ansi_c_language.cpp.

◆ generate_support_functions()

bool ansi_c_languaget::generate_support_functions ( symbol_table_baset symbol_table,
message_handlert message_handler 
)
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.

◆ id()

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

Implements languaget.

Definition at line 116 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 33 of file ansi_c_language.cpp.

◆ new_language()

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

Implements languaget.

Definition at line 111 of file ansi_c_language.h.

◆ parse()

bool ansi_c_languaget::parse ( std::istream &  instream,
const std::string &  path,
message_handlert message_handler 
)
overridevirtual

Implements languaget.

Definition at line 52 of file ansi_c_language.cpp.

◆ preprocess()

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

ANSI-C preprocessing.

Reimplemented from languaget.

Definition at line 39 of file ansi_c_language.cpp.

◆ set_language_options()

void ansi_c_languaget::set_language_options ( const optionst ,
message_handlert  
)
inlineoverridevirtual

Set language-specific options.

Reimplemented from languaget.

Definition at line 38 of file ansi_c_language.h.

◆ show_parse()

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

Implements languaget.

Definition at line 147 of file ansi_c_language.cpp.

◆ to_expr()

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

Parses the given string into an expression.

Parameters
codethe string to parse
moduleprefix to be used for identifiers
exprthe parsed expression
nsa namespace
message_handlera message handler
Returns
false if the conversion succeeds

Implements languaget.

Definition at line 184 of file ansi_c_language.cpp.

◆ 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 175 of file ansi_c_language.cpp.

◆ typecheck() [1/3]

bool ansi_c_languaget::typecheck ( symbol_table_baset symbol_table,
const std::string &  module,
message_handlert message_handler 
)
inlineoverridevirtual

Implements languaget.

Definition at line 76 of file ansi_c_language.h.

◆ typecheck() [2/3]

bool ansi_c_languaget::typecheck ( symbol_table_baset symbol_table,
const std::string &  module,
message_handlert message_handler,
const bool  keep_file_local 
)
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.

◆ typecheck() [3/3]

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.

Member Data Documentation

◆ object_factory_params

c_object_factory_parameterst ansi_c_languaget::object_factory_params
protected

Definition at line 126 of file ansi_c_language.h.

◆ parse_path

std::string ansi_c_languaget::parse_path
protected

Definition at line 124 of file ansi_c_language.h.

◆ parse_tree

ansi_c_parse_treet ansi_c_languaget::parse_tree
protected

Definition at line 123 of file ansi_c_language.h.


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