cprover
language_file.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_UTIL_LANGUAGE_FILE_H
11 #define CPROVER_UTIL_LANGUAGE_FILE_H
12 
13 #include <iosfwd>
14 #include <set>
15 #include <map>
16 #include <string>
17 
18 #include "message.h"
19 
20 class symbol_tablet;
21 class language_filet;
22 class languaget;
23 
25 {
26 public:
27  std::string name;
30 
32  { type_checked=in_progress=false; }
33 };
34 
36 {
37 public:
38  typedef std::set<std::string> modulest;
39  modulest modules;
40 
42  std::string filename;
43 
44  void get_modules();
45 
46  void convert_lazy_method(
47  const irep_idt &id,
48  symbol_tablet &symbol_table);
49 
50  language_filet(const language_filet &rhs);
51 
52  language_filet():language(nullptr)
53  {
54  }
55 
56  ~language_filet();
57 };
58 
60 {
61 public:
62  typedef std::map<std::string, language_filet> file_mapt;
63  file_mapt file_map;
64 
65  // Contains pointers into file_mapt!
66  typedef std::map<std::string, language_modulet> module_mapt;
67  module_mapt module_map;
68 
69  // Contains pointers into filemapt!
70  // This is safe-ish as long as this is std::map.
71  typedef std::map<irep_idt, language_filet *> lazy_method_mapt;
72  lazy_method_mapt lazy_method_map;
73 
74  void clear_files()
75  {
76  file_map.clear();
77  }
78 
79  bool parse();
80 
81  void show_parse(std::ostream &out);
82 
83  bool typecheck(symbol_tablet &symbol_table);
84 
85  bool final(symbol_tablet &symbol_table);
86 
87  bool interfaces(symbol_tablet &symbol_table);
88 
89  bool has_lazy_method(const irep_idt &id)
90  {
91  return lazy_method_map.count(id)!=0;
92  }
93 
94  // The method must have been added to the symbol table and registered
95  // in lazy_method_map (currently always in language_filest::typecheck)
96  // for this to be legal.
98  const irep_idt &id,
99  symbol_tablet &symbol_table)
100  {
101  return lazy_method_map.at(id)->convert_lazy_method(id, symbol_table);
102  }
103 
104  void clear()
105  {
106  file_map.clear();
107  module_map.clear();
108  lazy_method_map.clear();
109  }
110 
111 protected:
112  bool typecheck_module(
113  symbol_tablet &symbol_table,
114  language_modulet &module);
115 
116  bool typecheck_module(
117  symbol_tablet &symbol_table,
118  const std::string &module);
119 };
120 
121 #endif // CPROVER_UTIL_LANGUAGE_FILE_H
languaget * language
Definition: language_file.h:41
std::set< std::string > modulest
Definition: language_file.h:38
void convert_lazy_method(const irep_idt &id, symbol_tablet &symbol_table)
Definition: language_file.h:97
The symbol table.
Definition: symbol_table.h:52
std::map< std::string, language_filet > file_mapt
Definition: language_file.h:62
std::map< irep_idt, language_filet * > lazy_method_mapt
Definition: language_file.h:71
lazy_method_mapt lazy_method_map
Definition: language_file.h:72
std::map< std::string, language_modulet > module_mapt
Definition: language_file.h:66
std::string name
Definition: language_file.h:27
modulest modules
Definition: language_file.h:39
bool has_lazy_method(const irep_idt &id)
Definition: language_file.h:89
file_mapt file_map
Definition: language_file.h:63
std::string filename
Definition: language_file.h:42
module_mapt module_map
Definition: language_file.h:67
language_filet * file
Definition: language_file.h:29