CBMC
language_filest Class Reference

#include <language_file.h>

+ Inheritance diagram for language_filest:
+ Collaboration diagram for language_filest:

Public Member Functions

language_filetadd_file (const std::string &filename)
 
void remove_file (const std::string &filename)
 
void clear_files ()
 
bool parse ()
 
void show_parse (std::ostream &out)
 
bool generate_support_functions (symbol_tablet &symbol_table)
 
bool typecheck (symbol_tablet &symbol_table, const bool keep_file_local=false)
 
bool final (symbol_table_baset &symbol_table)
 
bool interfaces (symbol_tablet &symbol_table)
 
void convert_lazy_method (const irep_idt &id, symbol_table_baset &symbol_table)
 
bool can_convert_lazy_method (const irep_idt &id) const
 
void clear ()
 
- 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 Member Functions

bool typecheck_module (symbol_tablet &symbol_table, language_modulet &module, const bool keep_file_local)
 
bool typecheck_module (symbol_tablet &symbol_table, const std::string &module, const bool keep_file_local)
 

Private Types

typedef std::map< std::string, language_filetfile_mapt
 
typedef std::map< std::string, language_moduletmodule_mapt
 
typedef std::map< irep_idt, language_filet * > lazy_method_mapt
 

Private Attributes

file_mapt file_map
 
module_mapt module_map
 
lazy_method_mapt lazy_method_map
 

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...
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

Detailed Description

Definition at line 62 of file language_file.h.

Member Typedef Documentation

◆ file_mapt

typedef std::map<std::string, language_filet> language_filest::file_mapt
private

Definition at line 65 of file language_file.h.

◆ lazy_method_mapt

Definition at line 73 of file language_file.h.

◆ module_mapt

typedef std::map<std::string, language_modulet> language_filest::module_mapt
private

Definition at line 68 of file language_file.h.

Member Function Documentation

◆ add_file()

language_filet& language_filest::add_file ( const std::string &  filename)
inline

Definition at line 77 of file language_file.h.

◆ can_convert_lazy_method()

bool language_filest::can_convert_lazy_method ( const irep_idt id) const
inline

Definition at line 131 of file language_file.h.

◆ clear()

void language_filest::clear ( )
inline

Definition at line 136 of file language_file.h.

◆ clear_files()

void language_filest::clear_files ( )
inline

Definition at line 99 of file language_file.h.

◆ convert_lazy_method()

void language_filest::convert_lazy_method ( const irep_idt id,
symbol_table_baset symbol_table 
)
inline

Definition at line 121 of file language_file.h.

◆ final()

bool language_filest::final ( symbol_table_baset symbol_table)

Definition at line 178 of file language_file.cpp.

◆ generate_support_functions()

bool language_filest::generate_support_functions ( symbol_tablet symbol_table)

Definition at line 163 of file language_file.cpp.

◆ interfaces()

bool language_filest::interfaces ( symbol_tablet symbol_table)

Definition at line 192 of file language_file.cpp.

◆ parse()

bool language_filest::parse ( )

Definition at line 51 of file language_file.cpp.

◆ remove_file()

void language_filest::remove_file ( const std::string &  filename)
inline

Definition at line 83 of file language_file.h.

◆ show_parse()

void language_filest::show_parse ( std::ostream &  out)

Definition at line 45 of file language_file.cpp.

◆ typecheck()

bool language_filest::typecheck ( symbol_tablet symbol_table,
const bool  keep_file_local = false 
)

Definition at line 83 of file language_file.cpp.

◆ typecheck_module() [1/2]

bool language_filest::typecheck_module ( symbol_tablet symbol_table,
const std::string &  module,
const bool  keep_file_local 
)
protected

Definition at line 204 of file language_file.cpp.

◆ typecheck_module() [2/2]

bool language_filest::typecheck_module ( symbol_tablet symbol_table,
language_modulet module,
const bool  keep_file_local 
)
protected

Definition at line 222 of file language_file.cpp.

Member Data Documentation

◆ file_map

file_mapt language_filest::file_map
private

Definition at line 66 of file language_file.h.

◆ lazy_method_map

lazy_method_mapt language_filest::lazy_method_map
private

Definition at line 74 of file language_file.h.

◆ module_map

module_mapt language_filest::module_map
private

Definition at line 69 of file language_file.h.


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