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 <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
20std::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
33std::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
46std::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
59std::string from_expr(const exprt &expr)
60{
61 symbol_tablet symbol_table;
62 return from_expr(namespacet(symbol_table), irep_idt(), expr);
63}
64
65std::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
91std::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().
The NIL expression.
Definition std_expr.h:2874
The symbol table.
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