cprover
Loading...
Searching...
No Matches
statement_list_language.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Statement List Language Interface
4
5Author: Matthias Weiss, matthias.weiss@diffblue.com
6
7\*******************************************************************/
8
11
18
19#include <linking/linking.h>
21#include <util/get_base_name.h>
22#include <util/symbol_table.h>
23
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
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
133
138
139void statement_list_languaget::modules_provided(std::set<std::string> &modules)
140{
141 modules.insert(get_base_name(parse_path, true));
142}
143
144std::set<std::string> statement_list_languaget::extensions() const
145{
146 return {"awl"};
147}
148
149std::unique_ptr<languaget> new_statement_list_language()
150{
151 return std::make_unique<statement_list_languaget>();
152}
153
154std::unique_ptr<languaget> statement_list_languaget::new_language()
155{
156 return std::make_unique<statement_list_languaget>();
157}
158
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.
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.
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:1130
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.