CBMC
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 <util/invariant.h>
12 #include <util/message.h>
13 #include <util/namespace.h>
14 #include <util/std_expr.h>
15 #include <util/symbol_table.h>
16 
17 #include "language.h"
18 #include "mode.h"
19 
20 #include <memory>
21 
23  const namespacet &ns,
24  const irep_idt &mode,
25  const exprt &expr)
26 {
27  std::unique_ptr<languaget> language = (mode == ID_unknown)
29  : get_language_from_mode(mode);
30  INVARIANT(
31  language, "could not retrieve language for mode '" + id2string(mode) + "'");
32 
33  std::string result;
34  language->from_expr(expr, result, ns);
35 
36  return result;
37 }
38 
39 std::string from_expr(
40  const namespacet &ns,
41  const irep_idt &identifier,
42  const exprt &expr)
43 {
44  std::unique_ptr<languaget> p(get_language_from_identifier(ns, identifier));
45 
46  std::string result;
47  p->from_expr(expr, result, ns);
48 
49  return result;
50 }
51 
52 std::string from_type(
53  const namespacet &ns,
54  const irep_idt &identifier,
55  const typet &type)
56 {
57  std::unique_ptr<languaget> p(get_language_from_identifier(ns, identifier));
58 
59  std::string result;
60  p->from_type(type, result, ns);
61 
62  return result;
63 }
64 
65 std::string type_to_name(
66  const namespacet &ns,
67  const irep_idt &identifier,
68  const typet &type)
69 {
70  std::unique_ptr<languaget> p(get_language_from_identifier(ns, identifier));
71 
72  std::string result;
73  p->type_to_name(type, result, ns);
74 
75  return result;
76 }
77 
78 std::string from_expr(const exprt &expr)
79 {
80  symbol_tablet symbol_table;
81  return from_expr(namespacet(symbol_table), irep_idt(), expr);
82 }
83 
84 std::string from_type(const typet &type)
85 {
86  symbol_tablet symbol_table;
87  return from_type(namespacet(symbol_table), irep_idt(), type);
88 }
89 
91  const namespacet &ns,
92  const irep_idt &identifier,
93  const std::string &src)
94 {
95  std::unique_ptr<languaget> p(get_language_from_identifier(ns, identifier));
96 
97  const symbolt &symbol=ns.lookup(identifier);
98 
99  exprt expr;
100 
102 
103  if(p->to_expr(src, id2string(symbol.module), expr, ns, null_message_handler))
104  return nil_exprt();
105 
106  return expr;
107 }
108 
109 std::string type_to_name(const typet &type)
110 {
111  symbol_tablet symbol_table;
112  return type_to_name(namespacet(symbol_table), irep_idt(), type);
113 }
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:56
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:148
The NIL expression.
Definition: std_expr.h:3073
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
const std::string & id2string(const irep_idt &d)
Definition: irep.h:40
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_expr_using_mode(const namespacet &ns, const irep_idt &mode, const exprt &expr)
Formats an expression using the given namespace, using the given mode to retrieve the language printe...
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
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Definition: mode.cpp:51
std::unique_ptr< languaget > get_default_language()
Returns the default language.
Definition: mode.cpp:139
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
API to expression classes.
Author: Diffblue Ltd.
null_message_handlert null_message_handler
Definition: message.cpp:14
dstringt irep_idt