CBMC: /home/runner/work/cbmc/cbmc/src/langapi/language.h Source File

CBMC
Loading...
Searching...
No Matches
language.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Abstract interface to support a programming language
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_LANGAPI_LANGUAGE_H
13#define CPROVER_LANGAPI_LANGUAGE_H
14
15#include <util/invariant.h>
16#include <util/irep.h>
17
18#include <iosfwd>
19#include <memory> // unique_ptr
20#include <set>
21#include <string>
22#include <unordered_set>
23
24class exprt;
25class message_handlert;
26class namespacet;
27class optionst;
28class symbol_table_baset;
29class typet;
30
31 #define OPT_FUNCTIONS \
32 "(function):"
33
34 #define HELP_FUNCTIONS " {y--function} {uname} \t set main function name\n"
35
36 class languaget
37{
38public:
41 {
42 }
43
44 // parse file
45
46 virtual bool preprocess(
47 std::istream &instream,
48 const std::string &path,
49 std::ostream &outstream,
51 {
52 // unused parameters
54 (void)path;
56 return false;
57 }
58
59 virtual bool parse(
60 std::istream &instream,
61 const std::string &path,
62 message_handlert &message_handler) = 0;
63
73 symbol_table_baset &symbol_table,
74 message_handlert &message_handler) = 0;
75
76 // add external dependencies of a given module to set
77
78 virtual void dependencies(
79 const std::string &module,
80 std::set<std::string> &modules);
81
82 // add modules provided by currently parsed file to set
83
84 virtual void modules_provided(std::set<std::string> &modules)
85 {
86 (void)modules; // unused parameter
87 }
88
94 virtual void methods_provided(std::unordered_set<irep_idt> &methods) const
95{
96 (void)methods; // unused parameter
97 }
98
104 const irep_idt &function_id,
105 symbol_table_baset &symbol_table,
106 message_handlert &message_handler)
107 {
108 // unused parameters
109 (void)function_id;
110 (void)symbol_table;
111 (void)message_handler;
112 }
113
116 virtual bool final(symbol_table_baset &symbol_table);
117
118 // type check interfaces of currently parsed file
119
120 virtual bool interfaces(
121 symbol_table_baset &symbol_table,
122 message_handlert &message_handler);
123
124 // type check a module in the currently parsed file
125
126 virtual bool typecheck(
127 symbol_table_baset &symbol_table,
128 const std::string &module,
129 message_handlert &message_handler) = 0;
130
132 virtual bool can_keep_file_local()
133 {
134 return false;
135 }
136
146 virtual bool typecheck(
147 symbol_table_baset &symbol_table,
148 const std::string &module,
149 message_handlert &message_handler,
150 const bool keep_file_local)
151 {
152 INVARIANT(
153 false,
154 "three-argument typecheck should only be called for files written"
155 " in a language that allows file-local symbols, like C");
156 }
157
158 // language id / description
159
160 virtual std::string id() const = 0;
161 virtual std::string description() const = 0;
162 virtual std::set<std::string> extensions() const = 0;
163
164 // show parse tree
165
166 virtual void
167 show_parse(std::ostream &out, message_handlert &message_handler) = 0;
168
169 // conversion of expressions
170
176 virtual bool from_expr(
177 const exprt &expr,
178 std::string &code,
179 const namespacet &ns);
180
186 virtual bool from_type(
187 const typet &type,
188 std::string &code,
189 const namespacet &ns);
190
196 virtual bool type_to_name(
197 const typet &type,
198 std::string &name,
199 const namespacet &ns);
200
208 virtual bool to_expr(
209 const std::string &code,
210 const std::string &module,
211 exprt &expr,
212 const namespacet &ns,
213 message_handlert &message_handler) = 0;
214
215 virtual std::unique_ptr<languaget> new_language()=0;
216
217 // constructor / destructor
218
220 virtual ~languaget() { }
221};
222
223#endif // CPROVER_UTIL_LANGUAGE_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:57
virtual void modules_provided(std::set< std::string > &modules)
Definition language.h:84
virtual std::string description() const =0
languaget()
Definition language.h:219
virtual bool can_keep_file_local()
Is it possible to call three-argument typecheck() on this object?
Definition language.h:132
virtual void dependencies(const std::string &module, std::set< std::string > &modules)
Definition language.cpp:26
virtual bool typecheck(symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler, const bool keep_file_local)
typecheck without removing specified entries from the symbol table
Definition language.h:146
virtual bool from_type(const typet &type, std::string &code, const namespacet &ns)
Formats the given type in a language-specific way.
Definition language.cpp:41
virtual bool parse(std::istream &instream, const std::string &path, message_handlert &message_handler)=0
virtual bool type_to_name(const typet &type, std::string &name, const namespacet &ns)
Encodes the given type in a language-specific way.
Definition language.cpp:50
virtual std::string id() const =0
virtual std::set< std::string > extensions() const =0
virtual bool from_expr(const exprt &expr, std::string &code, const namespacet &ns)
Formats the given expression in a language-specific way.
Definition language.cpp:32
virtual void convert_lazy_method(const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
Requests this languaget should populate the body of method function_id in symbol_table.
Definition language.h:103
virtual bool generate_support_functions(symbol_table_baset &symbol_table, message_handlert &message_handler)=0
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
virtual bool typecheck(symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler)=0
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream, message_handlert &)
Definition language.h:46
virtual std::unique_ptr< languaget > new_language()=0
virtual bool interfaces(symbol_table_baset &symbol_table, message_handlert &message_handler)
Definition language.cpp:21
virtual bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns, message_handlert &message_handler)=0
Parses the given string into an expression.
virtual void methods_provided(std::unordered_set< irep_idt > &methods) const
Should fill methods with the symbol identifiers of all methods this languaget can provide a body for,...
Definition language.h:94
virtual void set_language_options(const optionst &, message_handlert &)
Set language-specific options.
Definition language.h:40
virtual ~languaget()
Definition language.h:220
virtual void show_parse(std::ostream &out, message_handlert &message_handler)=0
Definition message.h:27
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The symbol table base class interface.
The type of an expression, extends irept.
Definition type.h:29
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423

AltStyle によって変換されたページ (->オリジナル) /