cprover
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/make_unique.h>
23 #include <util/symbol_table.h>
24 
26 {
28 }
29 
31  symbol_tablet &symbol_table)
32 {
33  return statement_list_entry_point(symbol_table, get_message_handler());
34 }
35 
37  symbol_tablet &symbol_table,
38  const std::string &module,
39  const bool keep_file_local)
40 {
41  symbol_tablet new_symbol_table;
42 
44  parse_tree, new_symbol_table, module, get_message_handler()))
45  return true;
46 
48  new_symbol_table, get_message_handler(), keep_file_local);
49 
50  if(linking(symbol_table, new_symbol_table, get_message_handler()))
51  return true;
52 
53  return false;
54 }
55 
57  std::istream &instream,
58  const std::string &path)
59 {
61  parse_path = path;
64  statement_list_parser.in = &instream;
67 
68  // store result
70 
71  return result;
72 }
73 
74 void statement_list_languaget::show_parse(std::ostream &out)
75 {
77 }
78 
80 {
81  return true;
82 }
83 
85  symbol_tablet &symbol_table,
86  const std::string &module)
87 {
88  return typecheck(symbol_table, module, true);
89 }
90 
92  const exprt &expr,
93  std::string &code,
94  const namespacet &ns)
95 {
96  code = expr2stl(expr, ns);
97  return false;
98 }
99 
101  const typet &type,
102  std::string &code,
103  const namespacet &ns)
104 {
105  code = type2stl(type, ns);
106  return false;
107 }
108 
110  const typet &type,
111  std::string &name,
112  const namespacet &ns)
113 {
114  return from_type(type, name, ns);
115 }
116 
118  const std::string &,
119  const std::string &,
120  exprt &,
121  const namespacet &)
122 {
123  return true;
124 }
125 
127 {
128 }
129 
131 {
132  parse_tree.clear();
133 }
134 
135 void statement_list_languaget::modules_provided(std::set<std::string> &modules)
136 {
137  modules.insert(get_base_name(parse_path, true));
138 }
139 
140 std::set<std::string> statement_list_languaget::extensions() const
141 {
142  return {"awl"};
143 }
144 
145 std::unique_ptr<languaget> new_statement_list_language()
146 {
147  return util_make_unique<statement_list_languaget>();
148 }
149 
150 std::unique_ptr<languaget> statement_list_languaget::new_language()
151 {
152  return util_make_unique<statement_list_languaget>();
153 }
154 
155 std::string statement_list_languaget::id() const
156 {
157  return "Statement List";
158 }
159 
161 {
162  return "Statement List Language by Siemens";
163 }
Base class for all expressions.
Definition: expr.h:54
mstreamt & result() const
Definition: message.h:409
message_handlert & get_message_handler()
Definition: message.h:184
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
std::istream * in
Definition: parser.h:26
void set_file(const irep_idt &file)
Definition: parser.h:85
void set_line_no(unsigned _line_no)
Definition: parser.h:80
bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns) override
Parses the given string into an expression.
void modules_provided(std::set< std::string > &modules) override
void show_parse(std::ostream &out) override
Prints the parse tree to the given output stream.
object_factory_parameterst params
std::set< std::string > extensions() const override
std::unique_ptr< languaget > new_language() override
bool generate_support_functions(symbol_tablet &symbol_table) override
Currently unused.
std::string id() const override
bool from_type(const typet &type, std::string &code, const namespacet &ns) override
Formats the given type in a language-specific way.
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.
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 typecheck(symbol_tablet &symbol_table, const std::string &module, const bool keep_file_local) override
Converts the current parse tree into a symbol table.
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.
void set_language_options(const optionst &options) override
Sets language specific options.
void clear()
Removes all functions and function blocks from the parse tree.
void clear() override
Removes all functions and function blocks from the parse tree and clears the internal state of the pa...
void swap_tree(statement_list_parse_treet &other)
Swaps the contents of the parse tree of this instance with other.
bool parse() override
Starts the parsing process and saves the result inside of this instance's parse tree.
The symbol table.
Definition: symbol_table.h:14
The type of an expression, extends irept.
Definition: type.h:28
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_tablet &dest_symbol_table, symbol_tablet &new_symbol_table, message_handlert &message_handler)
Definition: linking.cpp:1444
ANSI-C Linking.
void remove_internal_symbols(symbol_tablet &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_tablet &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_parsert statement_list_parser
Instance of the parser, used by other modules.
Statement List Language Parser.
void statement_list_scanner_init()
Defined in scanner.l.
bool statement_list_typecheck(const statement_list_parse_treet &parse_tree, symbol_tablet &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.