cprover
languaget Class Referenceabstract

#include <language.h>

+ Inheritance diagram for languaget:
+ Collaboration diagram for languaget:

Public Member Functions

virtual void set_language_options (const optionst &)
 Set language-specific options. More...
 
virtual bool preprocess (std::istream &instream, const std::string &path, std::ostream &outstream)
 
virtual bool parse (std::istream &instream, const std::string &path)=0
 
virtual bool generate_support_functions (symbol_tablet &symbol_table)=0
 Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and language-specific library functions. More...
 
virtual void dependencies (const std::string &module, std::set< std::string > &modules)
 
virtual void modules_provided (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)
 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_tablet &symbol_table)
 
virtual bool typecheck (symbol_tablet &symbol_table, const std::string &module)=0
 
virtual std::string id () const
 
virtual std::string description () const
 
virtual std::set< std::string > extensions () const
 
virtual void show_parse (std::ostream &out)=0
 
virtual bool from_expr (const exprt &expr, std::string &code, const namespacet &ns)
 Formats the given expression in a language-specific way. More...
 
virtual bool from_type (const typet &type, std::string &code, const namespacet &ns)
 Formats the given type in a language-specific way. More...
 
virtual bool type_to_name (const typet &type, std::string &name, const namespacet &ns)
 Encodes the given type in a language-specific way. More...
 
virtual bool to_expr (const std::string &code, const std::string &module, exprt &expr, const namespacet &ns)=0
 Parses the given string into an expression. More...
 
virtual std::unique_ptr< languagetnew_language ()=0
 
 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 message_stream using output_generator if the configured verbosity is at least as high as that of message_stream. More...
 

Protected Attributes

bool language_options_initialized =false
 
system_library_symbolst system_symbols
 
- 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 commandt command (unsigned c)
 Create an ECMA-48 SGR (Select Graphic Rendition) command. More...
 
- Static Public Attributes inherited from messaget
static eomt eom
 
static const commandt reset
 return to default formatting, as defined by the terminal More...
 
static const commandt red
 render text with red foreground color More...
 
static const commandt green
 render text with green foreground color More...
 
static const commandt yellow
 render text with yellow foreground color More...
 
static const commandt blue
 render text with blue foreground color More...
 
static const commandt magenta
 render text with magenta foreground color More...
 
static const commandt cyan
 render text with cyan foreground color More...
 
static const commandt bright_red
 render text with bright red foreground color More...
 
static const commandt bright_green
 render text with bright green foreground color More...
 
static const commandt bright_yellow
 render text with bright yellow foreground color More...
 
static const commandt bright_blue
 render text with bright blue foreground color More...
 
static const commandt bright_magenta
 render text with bright magenta foreground color More...
 
static const commandt bright_cyan
 render text with bright cyan foreground color More...
 
static const commandt bold
 render text with bold font More...
 
static const commandt faint
 render text with faint font More...
 
static const commandt italic
 render italic text More...
 
static const commandt underline
 render underlined text More...
 

Detailed Description

Definition at line 39 of file language.h.

Constructor & Destructor Documentation

◆ languaget()

languaget::languaget ( )
inline

Definition at line 186 of file language.h.

◆ ~languaget()

virtual languaget::~languaget ( )
inlinevirtual

Definition at line 187 of file language.h.

Member Function Documentation

◆ convert_lazy_method()

virtual void languaget::convert_lazy_method ( const irep_idt function_id,
symbol_table_baset symbol_table 
)
inlinevirtual

Requests this languaget should populate the body of method function_id in symbol_table.

This will only be called if methods_provided advertised the given function_id could be provided by this languaget instance.

Reimplemented in java_bytecode_languaget.

Definition at line 104 of file language.h.

◆ dependencies()

void languaget::dependencies ( const std::string &  module,
std::set< std::string > &  modules 
)
virtual

Definition at line 31 of file language.cpp.

◆ description()

virtual std::string languaget::description ( ) const
inlinevirtual

Reimplemented in java_bytecode_languaget, cpp_languaget, ansi_c_languaget, and jsil_languaget.

Definition at line 130 of file language.h.

◆ extensions()

virtual std::set<std::string> languaget::extensions ( ) const
inlinevirtual

◆ final()

bool languaget::final ( symbol_table_baset symbol_table)
virtual

Final adjustments, e.g.

initializing stub functions and globals that were discovered during function loading

Reimplemented in java_bytecode_languaget.

Definition at line 21 of file language.cpp.

◆ from_expr()

bool languaget::from_expr ( const exprt expr,
std::string &  code,
const namespacet ns 
)
virtual

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 in java_bytecode_languaget, ansi_c_languaget, cpp_languaget, and jsil_languaget.

Definition at line 37 of file language.cpp.

◆ from_type()

bool languaget::from_type ( const typet type,
std::string &  code,
const namespacet ns 
)
virtual

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 in java_bytecode_languaget, ansi_c_languaget, cpp_languaget, and jsil_languaget.

Definition at line 46 of file language.cpp.

◆ generate_support_functions()

virtual bool languaget::generate_support_functions ( symbol_tablet symbol_table)
pure virtual

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.

Implemented in java_bytecode_languaget, ansi_c_languaget, json_symtab_languaget, cpp_languaget, and jsil_languaget.

◆ id()

virtual std::string languaget::id ( ) const
inlinevirtual

Reimplemented in java_bytecode_languaget, cpp_languaget, ansi_c_languaget, and jsil_languaget.

Definition at line 129 of file language.h.

◆ interfaces()

bool languaget::interfaces ( symbol_tablet symbol_table)
virtual

Reimplemented in jsil_languaget.

Definition at line 26 of file language.cpp.

◆ methods_provided()

virtual void languaget::methods_provided ( std::unordered_set< irep_idt > &  methods) const
inlinevirtual

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.

there is no need to mention methods whose bodies are eagerly generated). It should be prepared to handle a convert_lazy_method call for any symbol added to methods.

Reimplemented in java_bytecode_languaget.

Definition at line 94 of file language.h.

◆ modules_provided()

virtual void languaget::modules_provided ( std::set< std::string > &  modules)
inlinevirtual

Reimplemented in java_bytecode_languaget, cpp_languaget, ansi_c_languaget, and jsil_languaget.

Definition at line 84 of file language.h.

◆ new_language()

virtual std::unique_ptr<languaget> languaget::new_language ( )
pure virtual

◆ parse()

virtual bool languaget::parse ( std::istream &  instream,
const std::string &  path 
)
pure virtual

◆ preprocess()

virtual bool languaget::preprocess ( std::istream &  instream,
const std::string &  path,
std::ostream &  outstream 
)
inlinevirtual

Reimplemented in java_bytecode_languaget, ansi_c_languaget, cpp_languaget, and jsil_languaget.

Definition at line 49 of file language.h.

◆ set_language_options()

virtual void languaget::set_language_options ( const optionst )
inlinevirtual

Set language-specific options.

Reimplemented in java_bytecode_languaget, ansi_c_languaget, and cpp_languaget.

Definition at line 43 of file language.h.

◆ show_parse()

virtual void languaget::show_parse ( std::ostream &  out)
pure virtual

◆ to_expr()

virtual bool languaget::to_expr ( const std::string &  code,
const std::string &  module,
exprt expr,
const namespacet ns 
)
pure virtual

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

Implemented in java_bytecode_languaget, cpp_languaget, ansi_c_languaget, jsil_languaget, and json_symtab_languaget.

◆ type_to_name()

bool languaget::type_to_name ( const typet type,
std::string &  name,
const namespacet ns 
)
virtual

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 in ansi_c_languaget, and cpp_languaget.

Definition at line 55 of file language.cpp.

◆ typecheck()

virtual bool languaget::typecheck ( symbol_tablet symbol_table,
const std::string &  module 
)
pure virtual

Member Data Documentation

◆ language_options_initialized

bool languaget::language_options_initialized =false
protected

Definition at line 190 of file language.h.

◆ system_symbols

system_library_symbolst languaget::system_symbols
protected

Definition at line 191 of file language.h.


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