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/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 }
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:13
statement_list_parser.h
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
linking
bool linking(symbol_tablet &dest_symbol_table, const symbol_tablet &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:1475
statement_list_typecheck.h
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
statement_list_parser
statement_list_parsert statement_list_parser
Instance of the parser, used by other modules.
Definition: statement_list_parser.cpp:21
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_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:335
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: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
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:111
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:56
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:357
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_parse_tree_io.h
messaget::result
mstreamt & result() const
Definition: message.h:409
make_unique.h
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:117
statement_list_scanner_init
void statement_list_scanner_init()
Defined in scanner.l.
type2stl
std::string type2stl(const typet &type, const namespacet &ns)
Converts a given type to human-readable STL code.
Definition: expr2statement_list.cpp:115
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:81
statement_list_languaget::description
std::string description() const override
Definition: statement_list_language.cpp:160
statement_list_entry_point.h
statement_list_languaget::new_language
std::unique_ptr< languaget > new_language() override
Definition: statement_list_language.cpp:150
linking.h
get_base_name.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_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:346
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:155
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:145
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
remove_internal_symbols.h
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:198
statement_list_languaget::statement_list_languaget
statement_list_languaget()
Definition: statement_list_language.cpp:126
expr2stl
std::string expr2stl(const exprt &expr, const namespacet &ns)
Converts a given expression to human-readable STL code.
Definition: expr2statement_list.cpp:108
symbol_table.h
Author: Diffblue Ltd.
statement_list_language.h
statement_list_languaget::set_language_options
void set_language_options(const optionst &options) override
Sets language specific options.
Definition: statement_list_language.cpp:25
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