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 
24 {
26 }
27 
29  symbol_tablet &symbol_table)
30 {
31  return statement_list_entry_point(symbol_table, get_message_handler());
32 }
33 
35  symbol_tablet &symbol_table,
36  const std::string &module,
37  const bool keep_file_local)
38 {
39  symbol_tablet new_symbol_table;
40 
42  parse_tree, new_symbol_table, module, get_message_handler()))
43  return true;
44 
46  new_symbol_table, get_message_handler(), keep_file_local);
47 
48  if(linking(symbol_table, new_symbol_table, get_message_handler()))
49  return true;
50 
51  return false;
52 }
53 
55  std::istream &instream,
56  const std::string &path)
57 {
59  parse_path = path;
62  statement_list_parser.in = &instream;
65 
66  // store result
68 
69  return result;
70 }
71 
72 void statement_list_languaget::show_parse(std::ostream &out)
73 {
75 }
76 
78 {
79  return true;
80 }
81 
83  symbol_tablet &symbol_table,
84  const std::string &module)
85 {
86  return typecheck(symbol_table, module, true);
87 }
88 
90  const exprt &expr,
91  std::string &code,
92  const namespacet &ns)
93 {
94  code = expr2stl(expr, ns);
95  return false;
96 }
97 
99  const typet &type,
100  std::string &code,
101  const namespacet &ns)
102 {
103  code = type2stl(type, ns);
104  return false;
105 }
106 
108  const typet &type,
109  std::string &name,
110  const namespacet &ns)
111 {
112  return from_type(type, name, ns);
113 }
114 
116  const std::string &,
117  const std::string &,
118  exprt &,
119  const namespacet &)
120 {
121  return true;
122 }
123 
125 {
126 }
127 
129 {
130  parse_tree.clear();
131 }
132 
133 void statement_list_languaget::modules_provided(std::set<std::string> &modules)
134 {
135  modules.insert(get_base_name(parse_path, true));
136 }
137 
138 std::set<std::string> statement_list_languaget::extensions() const
139 {
140  return {"awl"};
141 }
142 
143 std::unique_ptr<languaget> new_statement_list_language()
144 {
145  return util_make_unique<statement_list_languaget>();
146 }
147 
148 std::unique_ptr<languaget> statement_list_languaget::new_language()
149 {
150  return util_make_unique<statement_list_languaget>();
151 }
152 
153 std::string statement_list_languaget::id() const
154 {
155  return "Statement List";
156 }
157 
159 {
160  return "Statement List Language by Siemens";
161 }
get_base_name
std::string get_base_name(const std::string &in, bool strip_suffix)
cleans a filename from path and extension
Definition: get_base_name.cpp:16
expr2statement_list.h
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
statement_list_parser.h
Statement List Language Parser.
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:107
statement_list_typecheck.h
Statement List Language Type Checking.
statement_list_languaget::generate_support_functions
bool generate_support_functions(symbol_tablet &symbol_table) override
Currently unused.
Definition: statement_list_language.cpp:28
optionst
Definition: options.h:23
statement_list_parser
statement_list_parsert statement_list_parser
Instance of the parser, used by other modules.
Definition: statement_list_parser.cpp:23
typet
The type of an expression, extends irept.
Definition: type.h:29
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:77
statement_list_parsert::parse
bool parse() override
Starts the parsing process and saves the result inside of this instance's parse tree.
Definition: statement_list_parser.cpp:326
statement_list_languaget::params
object_factory_parameterst params
Definition: statement_list_language.h:113
statement_list_languaget::extensions
std::set< std::string > extensions() const override
Definition: statement_list_language.cpp:138
exprt
Base class for all expressions.
Definition: expr.h:53
object_factory_parameterst
Definition: object_factory_parameters.h:24
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:54
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:98
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:72
remove_internal_symbols
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.
Definition: remove_internal_symbols.cpp:77
output_parse_tree
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.
Definition: statement_list_parse_tree_io.cpp:54
statement_list_parsert::swap_tree
void swap_tree(statement_list_parse_treet &other)
Swaps the contents of the parse tree of this instance with other.
Definition: statement_list_parser.cpp:348
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:92
statement_list_parse_tree_io.h
Statement List Language Parse Tree Output.
messaget::result
mstreamt & result() const
Definition: message.h:409
statement_list_languaget::parse_path
std::string parse_path
Definition: statement_list_language.h:112
parsert::in
std::istream * in
Definition: parser.h:26
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:115
statement_list_scanner_init
void statement_list_scanner_init()
Defined in scanner.l.
linking
bool linking(symbol_tablet &dest_symbol_table, symbol_tablet &new_symbol_table, message_handlert &message_handler)
Definition: linking.cpp:1441
type2stl
std::string type2stl(const typet &type, const namespacet &ns)
Converts a given type to human-readable STL code.
Definition: expr2statement_list.cpp:114
statement_list_typecheck
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.
Definition: statement_list_typecheck.cpp:57
statement_list_languaget::description
std::string description() const override
Definition: statement_list_language.cpp:158
statement_list_entry_point.h
Statement List Language Entry Point.
statement_list_languaget::new_language
std::unique_ptr< languaget > new_language() override
Definition: statement_list_language.cpp:148
linking.h
ANSI-C Linking.
get_base_name.h
statement_list_languaget::~statement_list_languaget
~statement_list_languaget() override
Definition: statement_list_language.cpp:128
statement_list_languaget::modules_provided
void modules_provided(std::set< std::string > &modules) override
Definition: statement_list_language.cpp:133
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:89
statement_list_parsert::clear
void clear() override
Removes all functions and function blocks from the parse tree and clears the internal state of the pa...
Definition: statement_list_parser.cpp:337
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:184
statement_list_languaget::id
std::string id() const override
Definition: statement_list_language.cpp:153
statement_list_parse_treet::clear
void clear()
Removes all functions and function blocks from the parse tree.
Definition: statement_list_parse_tree.cpp:98
new_statement_list_language
std::unique_ptr< languaget > new_statement_list_language()
Definition: statement_list_language.cpp:143
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:34
remove_internal_symbols.h
Remove symbols that are internal only.
statement_list_entry_point
bool statement_list_entry_point(symbol_tablet &symbol_table, message_handlert &message_handler)
Creates a new entry point for the Statement List language.
Definition: statement_list_entry_point.cpp:196
statement_list_languaget::statement_list_languaget
statement_list_languaget()
Definition: statement_list_language.cpp:124
expr2stl
std::string expr2stl(const exprt &expr, const namespacet &ns)
Converts a given expression to human-readable STL code.
Definition: expr2statement_list.cpp:107
statement_list_language.h
Statement List Language Interface.
statement_list_languaget::set_language_options
void set_language_options(const optionst &options) override
Sets language specific options.
Definition: statement_list_language.cpp:23
parsert::set_file
void set_file(const irep_idt &file)
Definition: parser.h:85
parsert::set_line_no
void set_line_no(unsigned _line_no)
Definition: parser.h:80