CBMC
statement_list_language.cpp
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 
16 #include "statement_list_parser.h"
18 
19 #include <linking/linking.h>
21 #include <util/get_base_name.h>
22 #include <util/symbol_table.h>
23 
25  const optionst &options,
27 {
29 }
30 
32  symbol_table_baset &symbol_table,
33  message_handlert &message_handler)
34 {
35  return statement_list_entry_point(symbol_table, message_handler);
36 }
37 
39  symbol_table_baset &symbol_table,
40  const std::string &module,
41  message_handlert &message_handler,
42  const bool keep_file_local)
43 {
44  symbol_tablet new_symbol_table;
45 
47  parse_tree, new_symbol_table, module, message_handler))
48  return true;
49 
50  remove_internal_symbols(new_symbol_table, message_handler, keep_file_local);
51 
52  if(linking(symbol_table, new_symbol_table, message_handler))
53  return true;
54 
55  return false;
56 }
57 
59  std::istream &instream,
60  const std::string &path,
61  message_handlert &message_handler)
62 {
63  statement_list_parsert statement_list_parser{message_handler};
64  parse_path = path;
65  statement_list_parser.set_line_no(0);
66  statement_list_parser.set_file(path);
67  statement_list_parser.in = &instream;
68  bool result = statement_list_parser.parse();
69 
70  // store result
71  statement_list_parser.swap_tree(parse_tree);
72 
73  return result;
74 }
75 
77 {
79 }
80 
82 {
83  return true;
84 }
85 
87  symbol_table_baset &symbol_table,
88  const std::string &module,
89  message_handlert &message_handler)
90 {
91  return typecheck(symbol_table, module, message_handler, true);
92 }
93 
95  const exprt &expr,
96  std::string &code,
97  const namespacet &ns)
98 {
99  code = expr2stl(expr, ns);
100  return false;
101 }
102 
104  const typet &type,
105  std::string &code,
106  const namespacet &ns)
107 {
108  code = type2stl(type, ns);
109  return false;
110 }
111 
113  const typet &type,
114  std::string &name,
115  const namespacet &ns)
116 {
117  return from_type(type, name, ns);
118 }
119 
121  const std::string &,
122  const std::string &,
123  exprt &,
124  const namespacet &,
126 {
127  return true;
128 }
129 
131 {
132 }
133 
135 {
136  parse_tree.clear();
137 }
138 
139 void statement_list_languaget::modules_provided(std::set<std::string> &modules)
140 {
141  modules.insert(get_base_name(parse_path, true));
142 }
143 
144 std::set<std::string> statement_list_languaget::extensions() const
145 {
146  return {"awl"};
147 }
148 
149 std::unique_ptr<languaget> new_statement_list_language()
150 {
151  return std::make_unique<statement_list_languaget>();
152 }
153 
154 std::unique_ptr<languaget> statement_list_languaget::new_language()
155 {
156  return std::make_unique<statement_list_languaget>();
157 }
158 
159 std::string statement_list_languaget::id() const
160 {
161  return "Statement List";
162 }
163 
165 {
166  return "Statement List Language by Siemens";
167 }
Base class for all expressions.
Definition: expr.h:56
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
void modules_provided(std::set< std::string > &modules) override
object_factory_parameterst params
void set_language_options(const optionst &options, message_handlert &message_handler) override
Sets language specific options.
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.
std::set< std::string > extensions() const override
void show_parse(std::ostream &out, message_handlert &) override
Prints the parse tree to the given output stream.
bool typecheck(symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler, const bool keep_file_local) override
Converts the current parse tree into a symbol table.
std::unique_ptr< languaget > new_language() override
std::string id() const override
bool generate_support_functions(symbol_table_baset &symbol_table, message_handlert &) override
Currently unused.
bool from_type(const typet &type, std::string &code, const namespacet &ns) override
Formats the given type in a language-specific way.
statement_list_parse_treet parse_tree
bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) override
Formats the given expression in a language-specific way.
std::string description() const override
bool can_keep_file_local() override
Is it possible to call three-argument typecheck() on this object?
bool type_to_name(const typet &type, std::string &name, const namespacet &ns) override
Encodes the given type in a language-specific way.
bool parse(std::istream &instream, const std::string &path, message_handlert &message_handler) override
Parses input given by instream and saves this result to this instance's parse tree.
void clear()
Removes all functions and function blocks from the parse tree.
Responsible for starting the parse process and to translate the result into a statement_list_parse_tr...
The symbol table base class interface.
The symbol table.
Definition: symbol_table.h:14
The type of an expression, extends irept.
Definition: type.h:29
std::string expr2stl(const exprt &expr, const namespacet &ns)
Converts a given expression to human-readable STL code.
std::string type2stl(const typet &type, const namespacet &ns)
Converts a given type to human-readable STL code.
std::string get_base_name(const std::string &in, bool strip_suffix)
cleans a filename from path and extension
bool linking(symbol_table_baset &dest_symbol_table, const symbol_table_baset &new_symbol_table, message_handlert &message_handler)
Merges the symbol table new_symbol_table into dest_symbol_table, renaming symbols from new_symbol_tab...
Definition: linking.cpp:1618
ANSI-C Linking.
void remove_internal_symbols(symbol_table_baset &symbol_table, message_handlert &mh, const bool keep_file_local)
Removes internal symbols from a symbol table A symbol is EXPORTED if it is a.
Remove symbols that are internal only.
bool statement_list_entry_point(symbol_table_baset &symbol_table, message_handlert &message_handler)
Creates a new entry point for the Statement List language.
Statement List Language Entry Point.
std::unique_ptr< languaget > new_statement_list_language()
Statement List Language Interface.
void output_parse_tree(std::ostream &out, const statement_list_parse_treet &parse_tree)
Prints the given Statement List parse tree in a human-readable form to the given output stream.
Statement List Language Parse Tree Output.
Statement List Language Parser.
bool statement_list_typecheck(const statement_list_parse_treet &parse_tree, symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler)
Create a new statement_list_typecheckt object and perform a type check to fill the symbol table.
Statement List Language Type Checking.
Author: Diffblue Ltd.