cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
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
22
std::string
from_expr_using_mode
(
23
const
namespacet
&ns,
24
const
irep_idt
&mode,
25
const
exprt
&expr)
26
{
27
std::unique_ptr<languaget> language = (mode == ID_unknown)
28
?
get_default_language
()
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
90
exprt
to_expr
(
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
101
null_message_handlert
null_message_handler
;
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
}
exprt
Base class for all expressions.
Definition
expr.h:57
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition
namespace.h:91
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition
namespace.cpp:134
nil_exprt
The NIL expression.
Definition
std_expr.h:3134
null_message_handlert
Definition
message.h:76
symbol_tablet
The symbol table.
Definition
symbol_table.h:14
symbolt
Symbol table entry.
Definition
symbol.h:28
symbolt::module
irep_idt module
Name of module the symbol belongs to.
Definition
symbol.h:43
typet
The type of an expression, extends irept.
Definition
type.h:29
id2string
const std::string & id2string(const irep_idt &d)
Definition
irep.h:44
language.h
Abstract interface to support a programming language.
from_expr
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Definition
language_util.cpp:39
to_expr
exprt to_expr(const namespacet &ns, const irep_idt &identifier, const std::string &src)
Definition
language_util.cpp:90
type_to_name
std::string type_to_name(const namespacet &ns, const irep_idt &identifier, const typet &type)
Definition
language_util.cpp:65
from_expr_using_mode
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...
Definition
language_util.cpp:22
from_type
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
Definition
language_util.cpp:52
language_util.h
get_language_from_mode
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Definition
mode.cpp:51
get_default_language
std::unique_ptr< languaget > get_default_language()
Returns the default language.
Definition
mode.cpp:139
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:84
mode.h
namespace.h
invariant.h
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition
invariant.h:423
message.h
std_expr.h
API to expression classes.
symbol_table.h
Author: Diffblue Ltd.
null_message_handler
null_message_handlert null_message_handler
Definition
message.cpp:14
irep_idt
dstringt irep_idt
Definition
verification_result.h:16
langapi
language_util.cpp
Generated by
1.17.0