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 
79  p->set_message_handler(null_message_handler);
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 has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
The NIL expression.
Definition: std_expr.h:2874
The symbol table.
Definition: symbol_table.h:14
Symbol table entry.
Definition: symbol.h:28
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
The type of an expression, extends irept.
Definition: type.h:29
dstringt irep_idt
Definition: irep.h:37
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
Abstract interface to support a programming language.
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
exprt to_expr(const namespacet &ns, const irep_idt &identifier, const std::string &src)
std::string type_to_name(const namespacet &ns, const irep_idt &identifier, const typet &type)
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
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:84
API to expression classes.
Author: Diffblue Ltd.
null_message_handlert null_message_handler
Definition: message.cpp:14