cprover
Loading...
Searching...
No Matches
language_util.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@cs.cmu.edu
6
7\*******************************************************************/
8
9#include "language_util.h"
10
11#include <util/invariant.h>
12#include <util/namespace.h>
13#include <util/std_expr.h>
14#include <util/symbol_table.h>
15
16#include "language.h"
17#include "mode.h"
18
19#include <memory>
20
22 const namespacet &ns,
23 const irep_idt &mode,
24 const exprt &expr)
25{
26 std::unique_ptr<languaget> language = (mode == ID_unknown)
30 language, "could not retrieve language for mode '" + id2string(mode) + "'");
31
32 std::string result;
33 language->from_expr(expr, result, ns);
34
35 return result;
36}
37
38std::string from_expr(
39 const namespacet &ns,
40 const irep_idt &identifier,
41 const exprt &expr)
42{
43 std::unique_ptr<languaget> p(get_language_from_identifier(ns, identifier));
44
45 std::string result;
46 p->from_expr(expr, result, ns);
47
48 return result;
49}
50
51std::string from_type(
52 const namespacet &ns,
53 const irep_idt &identifier,
54 const typet &type)
55{
56 std::unique_ptr<languaget> p(get_language_from_identifier(ns, identifier));
57
58 std::string result;
59 p->from_type(type, result, ns);
60
61 return result;
62}
63
64std::string type_to_name(
65 const namespacet &ns,
66 const irep_idt &identifier,
67 const typet &type)
68{
69 std::unique_ptr<languaget> p(get_language_from_identifier(ns, identifier));
70
71 std::string result;
72 p->type_to_name(type, result, ns);
73
74 return result;
75}
76
77std::string from_expr(const exprt &expr)
78{
79 symbol_tablet symbol_table;
80 return from_expr(namespacet(symbol_table), irep_idt(), expr);
81}
82
83std::string from_type(const typet &type)
84{
85 symbol_tablet symbol_table;
86 return from_type(namespacet(symbol_table), irep_idt(), type);
87}
88
90 const namespacet &ns,
91 const irep_idt &identifier,
92 const std::string &src)
93{
94 std::unique_ptr<languaget> p(get_language_from_identifier(ns, identifier));
95
97 p->set_message_handler(null_message_handler);
98
99 const symbolt &symbol=ns.lookup(identifier);
100
101 exprt expr;
102
103 if(p->to_expr(src, id2string(symbol.module), expr, ns))
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:563
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
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:3026
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: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_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