cprover
language_util.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@cs.cmu.edu
6 
7 \*******************************************************************/
8 
9 #include "language_util.h"
10 
11 #include <memory>
12 
13 #include <util/symbol_table.h>
14 #include <util/namespace.h>
15 #include <util/std_expr.h>
16 
17 #include "language.h"
18 #include "mode.h"
19 
20 std::string from_expr(
21  const namespacet &ns,
22  const irep_idt &identifier,
23  const exprt &expr)
24 {
25  std::unique_ptr<languaget> p(get_language_from_identifier(ns, identifier));
26 
27  std::string result;
28  p->from_expr(expr, result, ns);
29 
30  return result;
31 }
32 
33 std::string from_type(
34  const namespacet &ns,
35  const irep_idt &identifier,
36  const typet &type)
37 {
38  std::unique_ptr<languaget> p(get_language_from_identifier(ns, identifier));
39 
40  std::string result;
41  p->from_type(type, result, ns);
42 
43  return result;
44 }
45 
46 std::string type_to_name(
47  const namespacet &ns,
48  const irep_idt &identifier,
49  const typet &type)
50 {
51  std::unique_ptr<languaget> p(get_language_from_identifier(ns, identifier));
52 
53  std::string result;
54  p->type_to_name(type, result, ns);
55 
56  return result;
57 }
58 
59 std::string from_expr(const exprt &expr)
60 {
61  symbol_tablet symbol_table;
62  return from_expr(namespacet(symbol_table), "", expr);
63 }
64 
65 std::string from_type(const typet &type)
66 {
67  symbol_tablet symbol_table;
68  return from_type(namespacet(symbol_table), "", type);
69 }
70 
72  const namespacet &ns,
73  const irep_idt &identifier,
74  const std::string &src)
75 {
76  std::unique_ptr<languaget> p(get_language_from_identifier(ns, identifier));
77 
80 
81  const symbolt &symbol=ns.lookup(identifier);
82 
83  exprt expr;
84 
85  if(p->to_expr(src, id2string(symbol.module), expr, ns))
86  return nil_exprt();
87 
88  return expr;
89 }
90 
91 std::string type_to_name(const typet &type)
92 {
93  symbol_tablet symbol_table;
94  return type_to_name(namespacet(symbol_table), "", type);
95 }
The type of an expression, extends irept.
Definition: type.h:27
exprt to_expr(const namespacet &ns, const irep_idt &identifier, const std::string &src)
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
null_message_handlert null_message_handler
Definition: message.cpp:14
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:55
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
Symbol table entry.
Definition: symbol.h:27
std::string type_to_name(const namespacet &ns, const irep_idt &identifier, const typet &type)
The NIL expression.
Definition: std_expr.h:4461
virtual bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns)=0
Parses the given string into an expression.
API to expression classes.
The symbol table.
Definition: symbol_table.h:19
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
Abstract interface to support a programming language.
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:169
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
Author: Diffblue Ltd.
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
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:46
std::unique_ptr< languaget > get_language_from_identifier(const namespacet &ns, const irep_idt &identifier)
Get the language corresponding to the mode of the given identifier's symbol.
Definition: mode.cpp:83
Base class for all expressions.
Definition: expr.h:54
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:37
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166