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), irep_idt(), expr);
63 }
64 
65 std::string from_type(const typet &type)
66 {
67  symbol_tablet symbol_table;
68  return from_type(namespacet(symbol_table), irep_idt(), 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), irep_idt(), type);
95 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
type_to_name
std::string type_to_name(const namespacet &ns, const irep_idt &identifier, const typet &type)
Definition: language_util.cpp:46
typet
The type of an expression, extends irept.
Definition: type.h:29
to_expr
exprt to_expr(const namespacet &ns, const irep_idt &identifier, const std::string &src)
Definition: language_util.cpp:71
exprt
Base class for all expressions.
Definition: expr.h:53
mode.h
from_type
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
Definition: language_util.cpp:33
irep_idt
dstringt irep_idt
Definition: irep.h:32
namespace.h
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
languaget::from_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
language_util.h
languaget::from_expr
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
nil_exprt
The NIL expression.
Definition: std_expr.h:3973
language.h
Abstract interface to support a programming language.
messaget::set_message_handler
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:179
null_message_handlert
Definition: message.h:77
symbolt
Symbol table entry.
Definition: symbol.h:28
languaget::to_expr
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.
get_language_from_identifier
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
symbol_table.h
Author: Diffblue Ltd.
symbolt::module
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
std_expr.h
API to expression classes.
null_message_handler
null_message_handlert null_message_handler
Definition: message.cpp:14
from_expr
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Definition: language_util.cpp:20
languaget::type_to_name
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