cprover
Loading...
Searching...
No Matches
language_file.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9
10#ifndef CPROVER_LANGAPI_LANGUAGE_FILE_H
11#define CPROVER_LANGAPI_LANGUAGE_FILE_H
12
13#include <iosfwd>
14#include <map>
15#include <memory> // unique_ptr
16#include <set>
17#include <string>
18#include <unordered_set>
19
21
23class language_filet;
24class languaget;
25
27{
28public:
29 std::string name;
32
38};
39
40class language_filet final
41{
42public:
43 typedef std::set<std::string> modulest;
45
46 std::unique_ptr<languaget> language;
47 std::string filename;
48
49 void get_modules();
50
52 const irep_idt &id,
53 symbol_table_baset &symbol_table);
54
55 explicit language_filet(const std::string &filename);
57
59};
60
62{
63private:
64 typedef std::map<std::string, language_filet> file_mapt;
66
67 typedef std::map<std::string, language_modulet> module_mapt;
69
70 // Contains pointers into file_map!
71 // This is safe-ish as long as this is std::map.
72 typedef std::map<irep_idt, language_filet *> lazy_method_mapt;
74
75public:
76 language_filet &add_file(const std::string &filename)
77 {
79 return file_map.emplace(filename, std::move(language_file)).first->second;
80 }
81
82 void remove_file(const std::string &filename)
83 {
84 // Clear relevant entries from lazy_method_map
85 language_filet *language_file = &file_map.at(filename);
86 std::unordered_set<irep_idt> files_methods;
87 for(auto const &method : lazy_method_map)
88 {
89 if(method.second == language_file)
90 files_methods.insert(method.first);
91 }
94
95 file_map.erase(filename);
96 }
97
99 {
101 file_map.clear();
102 }
103
104 bool parse(message_handlert &message_handler);
105
106 void show_parse(std::ostream &out);
107
109
110 bool
111
112 typecheck(
113 symbol_table_baset &symbol_table,
114 const bool keep_file_local,
115 message_handlert &message_handler);
116 bool
117 typecheck(symbol_table_baset &symbol_table, message_handlert &message_handler)
118 {
119 return typecheck(symbol_table, false, message_handler);
120 }
121
122 bool final(symbol_table_baset &symbol_table);
123
124 bool interfaces(symbol_table_baset &symbol_table);
125
126 // The method must have been added to the symbol table and registered
127 // in lazy_method_map (currently always in language_filest::typecheck)
128 // for this to be legal.
130 const irep_idt &id,
131 symbol_table_baset &symbol_table,
132 message_handlert &message_handler)
133 {
134 PRECONDITION(symbol_table.has_symbol(id));
135 lazy_method_mapt::iterator it=lazy_method_map.find(id);
136 if(it!=lazy_method_map.end())
137 it->second->convert_lazy_method(id, symbol_table);
138 }
139
140 bool can_convert_lazy_method(const irep_idt &id) const
141 {
142 return lazy_method_map.count(id) != 0;
143 }
144
145 void clear()
146 {
147 file_map.clear();
150 }
151
152protected:
153 bool typecheck_module(
154 symbol_table_baset &symbol_table,
156 const bool keep_file_local,
157 message_handlert &message_handler);
158
159 bool typecheck_module(
160 symbol_table_baset &symbol_table,
161 const std::string &module,
162 const bool keep_file_local,
163 message_handlert &message_handler);
164};
165
166#endif // CPROVER_UTIL_LANGUAGE_FILE_H
virtual void clear()
Reset the abstract state.
Definition ai.h:266
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
bool parse(message_handlert &message_handler)
bool typecheck_module(symbol_table_baset &symbol_table, language_modulet &module, const bool keep_file_local, message_handlert &message_handler)
std::map< std::string, language_modulet > module_mapt
void convert_lazy_method(const irep_idt &id, symbol_table_baset &symbol_table, message_handlert &message_handler)
bool typecheck(symbol_table_baset &symbol_table, const bool keep_file_local, message_handlert &message_handler)
file_mapt file_map
void show_parse(std::ostream &out)
std::map< std::string, language_filet > file_mapt
bool interfaces(symbol_table_baset &symbol_table)
bool typecheck(symbol_table_baset &symbol_table, message_handlert &message_handler)
lazy_method_mapt lazy_method_map
language_filet & add_file(const std::string &filename)
bool can_convert_lazy_method(const irep_idt &id) const
std::map< irep_idt, language_filet * > lazy_method_mapt
void remove_file(const std::string &filename)
bool generate_support_functions(symbol_table_baset &symbol_table)
module_mapt module_map
std::string filename
~language_filet()
To avoid compiler errors, the complete definition of a pointed-to type must be visible at the point a...
void convert_lazy_method(const irep_idt &id, symbol_table_baset &symbol_table)
std::set< std::string > modulest
std::unique_ptr< languaget > language
std::string name
language_filet * file
The symbol table base class interface.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
#define PRECONDITION(CONDITION)
Definition invariant.h:463
Definition kdev_t.h:19
Author: Diffblue Ltd.