CBMC
statement_list_language.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Statement List Language Interface
4 
5 Author: Matthias Weiss, matthias.weiss@diffblue.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_STATEMENT_LIST_STATEMENT_LIST_LANGUAGE_H
13 #define CPROVER_STATEMENT_LIST_STATEMENT_LIST_LANGUAGE_H
14 
16 #include <langapi/language.h>
17 
19 
24 {
25 public:
29  void set_language_options(const optionst &options) override;
30 
36  bool parse(std::istream &instream, const std::string &path) override;
37 
39  bool generate_support_functions(symbol_tablet &symbol_table) override;
40 
49  bool typecheck(
50  symbol_tablet &symbol_table,
51  const std::string &module,
52  const bool keep_file_local) override;
53 
54  bool
55  typecheck(symbol_tablet &symbol_table, const std::string &module) override;
56 
57  bool can_keep_file_local() override;
58 
60  void show_parse(std::ostream &out) override;
61 
62  // Constructor and destructor.
63  ~statement_list_languaget() override;
65 
71  bool from_expr(const exprt &expr, std::string &code, const namespacet &ns)
72  override;
73 
79  bool from_type(const typet &type, std::string &code, const namespacet &ns)
80  override;
81 
87  bool type_to_name(const typet &type, std::string &name, const namespacet &ns)
88  override;
89 
96  bool to_expr(
97  const std::string &code,
98  const std::string &module,
99  exprt &expr,
100  const namespacet &ns) override;
101 
102  std::unique_ptr<languaget> new_language() override;
103 
104  // ID, description, extensions, modules.
105  std::string id() const override;
106  std::string description() const override;
107  std::set<std::string> extensions() const override;
108  void modules_provided(std::set<std::string> &modules) override;
109 
110 private:
112  std::string parse_path;
114 };
115 
116 std::unique_ptr<languaget> new_statement_list_language();
117 
118 #endif // CPROVER_STATEMENT_LIST_STATEMENT_LIST_LANGUAGE_H
symbol_tablet
The symbol table.
Definition: symbol_table.h:13
statement_list_languaget::type_to_name
bool type_to_name(const typet &type, std::string &name, const namespacet &ns) override
Encodes the given type in a language-specific way.
Definition: statement_list_language.cpp:109
statement_list_languaget::generate_support_functions
bool generate_support_functions(symbol_tablet &symbol_table) override
Currently unused.
Definition: statement_list_language.cpp:30
optionst
Definition: options.h:22
typet
The type of an expression, extends irept.
Definition: type.h:28
statement_list_languaget::can_keep_file_local
bool can_keep_file_local() override
Is it possible to call three-argument typecheck() on this object?
Definition: statement_list_language.cpp:79
statement_list_languaget::params
object_factory_parameterst params
Definition: statement_list_language.h:113
new_statement_list_language
std::unique_ptr< languaget > new_statement_list_language()
Definition: statement_list_language.cpp:145
statement_list_languaget::extensions
std::set< std::string > extensions() const override
Definition: statement_list_language.cpp:140
exprt
Base class for all expressions.
Definition: expr.h:55
object_factory_parameterst
Definition: object_factory_parameters.h:20
statement_list_languaget::parse
bool parse(std::istream &instream, const std::string &path) override
Parses input given by instream and saves this result to this instance's parse tree.
Definition: statement_list_language.cpp:56
statement_list_languaget::from_type
bool from_type(const typet &type, std::string &code, const namespacet &ns) override
Formats the given type in a language-specific way.
Definition: statement_list_language.cpp:100
statement_list_languaget::show_parse
void show_parse(std::ostream &out) override
Prints the parse tree to the given output stream.
Definition: statement_list_language.cpp:74
statement_list_languaget
Implements the language interface for the Statement List language.
Definition: statement_list_language.h:23
statement_list_languaget::parse_tree
statement_list_parse_treet parse_tree
Definition: statement_list_language.h:111
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:90
statement_list_languaget::parse_path
std::string parse_path
Definition: statement_list_language.h:112
statement_list_languaget::to_expr
bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns) override
Parses the given string into an expression.
Definition: statement_list_language.cpp:117
statement_list_parse_tree.h
statement_list_languaget::description
std::string description() const override
Definition: statement_list_language.cpp:160
statement_list_languaget::new_language
std::unique_ptr< languaget > new_language() override
Definition: statement_list_language.cpp:150
language.h
object_factory_parameters.h
statement_list_languaget::~statement_list_languaget
~statement_list_languaget() override
Definition: statement_list_language.cpp:130
statement_list_languaget::modules_provided
void modules_provided(std::set< std::string > &modules) override
Definition: statement_list_language.cpp:135
statement_list_languaget::from_expr
bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) override
Formats the given expression in a language-specific way.
Definition: statement_list_language.cpp:91
statement_list_parse_treet
Intermediate representation of a parsed Statement List file before converting it into a goto program.
Definition: statement_list_parse_tree.h:20
statement_list_languaget::id
std::string id() const override
Definition: statement_list_language.cpp:155
statement_list_languaget::typecheck
bool typecheck(symbol_tablet &symbol_table, const std::string &module, const bool keep_file_local) override
Converts the current parse tree into a symbol table.
Definition: statement_list_language.cpp:36
languaget
Definition: language.h:37
statement_list_languaget::statement_list_languaget
statement_list_languaget()
Definition: statement_list_language.cpp:126
statement_list_languaget::set_language_options
void set_language_options(const optionst &options) override
Sets language specific options.
Definition: statement_list_language.cpp:25