CBMC
Loading...
Searching...
No Matches
language_util.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, [email protected]
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)
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
39std::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
52std::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
65std::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
78std::string from_expr(const exprt &expr)
79{
80 symbol_tablet symbol_table;
81 return from_expr(namespacet(symbol_table), irep_idt(), expr);
82}
83
84std::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
109std::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}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The NIL expression.
Definition std_expr.h:3208
The symbol table.
Symbol table entry.
Definition symbol.h:28
The type of an expression, extends irept.
Definition type.h:29
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
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_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
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
#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