cprover
language.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Abstract interface to support a programming language
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_UTIL_LANGUAGE_H
13 #define CPROVER_UTIL_LANGUAGE_H
14 
15 #include <set>
16 #include <iosfwd>
17 #include <string>
18 
19 #include "message.h"
20 
21 class symbol_tablet;
22 class exprt;
23 class namespacet;
24 class typet;
25 class cmdlinet;
26 
27 class languaget:public messaget
28 {
29 public:
30  // Parse language-specific options
31  virtual void get_language_options(const cmdlinet &) {}
32 
33  // parse file
34 
35  virtual bool preprocess(
36  std::istream &instream,
37  const std::string &path,
38  std::ostream &outstream) { return false; }
39 
40  virtual bool parse(
41  std::istream &instream,
42  const std::string &path)=0;
43 
44  // add external dependencies of a given module to set
45 
46  virtual void dependencies(
47  const std::string &module,
48  std::set<std::string> &modules);
49 
50  // add modules provided by currently parsed file to set
51 
52  virtual void modules_provided(std::set<std::string> &modules)
53  { }
54 
55  // add lazy functions provided to set
56 
57  virtual void lazy_methods_provided(std::set<irep_idt> &methods) const
58  { }
59 
60  // populate a lazy method
61  virtual void convert_lazy_method(const irep_idt &id, symbol_tablet &)
62  { }
63 
64  // final adjustments, e.g., initialization and call to main()
65 
66  virtual bool final(
67  symbol_tablet &symbol_table);
68 
69  // type check interfaces of currently parsed file
70 
71  virtual bool interfaces(
72  symbol_tablet &symbol_table);
73 
74  // type check a module in the currently parsed file
75 
76  virtual bool typecheck(
77  symbol_tablet &symbol_table,
78  const std::string &module)=0;
79 
80  // language id / description
81 
82  virtual std::string id() const { return ""; }
83  virtual std::string description() const { return ""; }
84  virtual std::set<std::string> extensions() const
85  { return std::set<std::string>(); }
86 
87  // show parse tree
88 
89  virtual void show_parse(std::ostream &out)=0;
90 
91  // conversion of expressions
92 
93  virtual bool from_expr(
94  const exprt &expr,
95  std::string &code,
96  const namespacet &ns);
97 
98  virtual bool from_type(
99  const typet &type,
100  std::string &code,
101  const namespacet &ns);
102 
103  virtual bool type_to_name(
104  const typet &type,
105  std::string &name,
106  const namespacet &ns);
107 
108  virtual bool to_expr(
109  const std::string &code,
110  const std::string &module,
111  exprt &expr,
112  const namespacet &ns)=0;
113 
114  virtual languaget *new_language()=0;
115 
116  // constructor / destructor
117 
118  languaget() { }
119  virtual ~languaget() { }
120 };
121 #endif // CPROVER_UTIL_LANGUAGE_H
The type of an expression.
Definition: type.h:20
languaget()
Definition: language.h:118
virtual std::set< std::string > extensions() const
Definition: language.h:84
virtual std::string description() const
Definition: language.h:83
virtual ~languaget()
Definition: language.h:119
virtual void get_language_options(const cmdlinet &)
Definition: language.h:31
virtual bool type_to_name(const typet &type, std::string &name, const namespacet &ns)
Definition: language.cpp:50
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream)
Definition: language.h:35
virtual void modules_provided(std::set< std::string > &modules)
Definition: language.h:52
virtual bool typecheck(symbol_tablet &symbol_table, const std::string &module)=0
virtual bool interfaces(symbol_tablet &symbol_table)
Definition: language.cpp:21
virtual std::string id() const
Definition: language.h:82
virtual void lazy_methods_provided(std::set< irep_idt > &methods) const
Definition: language.h:57
virtual bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns)=0
The symbol table.
Definition: symbol_table.h:52
TO_BE_DOCUMENTED.
Definition: namespace.h:62
virtual bool from_type(const typet &type, std::string &code, const namespacet &ns)
Definition: language.cpp:41
virtual void show_parse(std::ostream &out)=0
virtual languaget * new_language()=0
Base class for all expressions.
Definition: expr.h:46
virtual void dependencies(const std::string &module, std::set< std::string > &modules)
Definition: language.cpp:26
virtual void convert_lazy_method(const irep_idt &id, symbol_tablet &)
Definition: language.h:61
virtual bool from_expr(const exprt &expr, std::string &code, const namespacet &ns)
Definition: language.cpp:32
virtual bool parse(std::istream &instream, const std::string &path)=0