cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
java_qualifiers.cpp
Go to the documentation of this file.
1
// Author: Diffblue Ltd.
2
5
6
#include "
java_qualifiers.h
"
7
8
#include <sstream>
9
#include <iterator>
10
11
#include "
expr2java.h
"
12
13
java_qualifierst
&
java_qualifierst::operator=
(
const
java_qualifierst
&other)
14
{
15
INVARIANT
(
16
&other.
ns
== &
ns
,
17
"Can only assign from a java_qualifierst using the same namespace"
);
18
annotations
= other.
annotations
;
19
c_qualifierst::operator=
(other);
20
return
*
this
;
21
}
22
23
std::unique_ptr<c_qualifierst>
java_qualifierst::clone
()
const
24
{
25
auto
other = std::make_unique<java_qualifierst>(
ns
);
26
*other = *
this
;
27
return
std::move(other);
28
}
29
30
void
java_qualifierst::clear
()
31
{
32
c_qualifierst::clear
();
33
annotations
.clear();
34
}
35
36
void
java_qualifierst::read
(
const
typet
&src)
37
{
38
c_qualifierst::read
(src);
39
auto
&annotated_type =
static_cast<
const
annotated_typet
&
>
(src);
40
annotations
= annotated_type.get_annotations();
41
}
42
43
void
java_qualifierst::write
(
typet
&src)
const
44
{
45
c_qualifierst::write
(src);
46
type_checked_cast<annotated_typet>
(src).get_annotations() =
annotations
;
47
}
48
49
java_qualifierst
&
java_qualifierst::operator+=
(
const
java_qualifierst
&other)
50
{
51
c_qualifierst::operator+=
(other);
52
std::copy(
53
other.
annotations
.begin(),
54
other.
annotations
.end(),
55
std::back_inserter(
annotations
));
56
return
*
this
;
57
}
58
59
bool
java_qualifierst::operator==
(
const
java_qualifierst
&other)
const
60
{
61
return
c_qualifierst::operator==
(other) &&
annotations
== other.
annotations
;
62
}
63
64
bool
java_qualifierst::is_subset_of
(
const
java_qualifierst
&other)
const
65
{
66
if
(!
c_qualifierst::is_subset_of
(other))
67
return
false
;
68
auto
&other_a = other.
annotations
;
69
for
(
const
auto
&annotation :
annotations
)
70
{
71
if
(std::find(other_a.begin(), other_a.end(), annotation) == other_a.end())
72
return
false
;
73
}
74
return
true
;
75
}
76
77
std::string
java_qualifierst::as_string
()
const
78
{
79
std::stringstream out;
80
for
(
const
java_annotationt
&annotation :
annotations
)
81
{
82
out <<
'@'
;
83
out <<
to_reference_type
(annotation.get_type())
84
.
base_type
()
85
.
get
(ID_identifier);
86
87
if
(!annotation.get_values().empty())
88
{
89
out <<
'('
;
90
91
bool
first =
true
;
92
for
(
const
java_annotationt::valuet
&value : annotation.get_values())
93
{
94
if
(first)
95
first =
false
;
96
else
97
out <<
", "
;
98
99
out <<
'"'
<< value.get_name() <<
'"'
<<
'='
;
100
out <<
expr2java
(value.get_value(),
ns
);
101
}
102
103
out <<
')'
;
104
}
105
out <<
' '
;
106
}
107
out <<
c_qualifierst::as_string
();
108
return
out.str();
109
}
annotated_typet
Definition
java_types.h:66
c_qualifierst::write
virtual void write(typet &src) const
Definition
c_qualifiers.cpp:95
c_qualifierst::read
virtual void read(const typet &src)
Definition
c_qualifiers.cpp:65
c_qualifierst::operator+=
c_qualifierst & operator+=(const c_qualifierst &other)
Definition
c_qualifiers.h:99
c_qualifierst::is_subset_of
bool is_subset_of(const c_qualifierst &other) const
Definition
c_qualifiers.h:69
c_qualifierst::clear
virtual void clear()
Definition
c_qualifiers.h:39
c_qualifierst::as_string
virtual std::string as_string() const
Definition
c_qualifiers.cpp:34
c_qualifierst::operator=
c_qualifierst & operator=(const c_qualifierst &other)
Definition
c_qualifiers.cpp:13
c_qualifierst::operator==
bool operator==(const c_qualifierst &other) const
Definition
c_qualifiers.h:82
irept::get
const irep_idt & get(const irep_idt &name) const
Definition
irep.cpp:44
java_annotationt::valuet
Definition
java_types.h:24
java_annotationt
Definition
java_types.h:21
java_qualifierst::read
void read(const typet &src) override
Definition
java_qualifiers.cpp:36
java_qualifierst::operator+=
java_qualifierst & operator+=(const java_qualifierst &other)
Definition
java_qualifiers.cpp:49
java_qualifierst::write
void write(typet &src) const override
Definition
java_qualifiers.cpp:43
java_qualifierst::as_string
std::string as_string() const override
Definition
java_qualifiers.cpp:77
java_qualifierst::is_subset_of
bool is_subset_of(const java_qualifierst &other) const
Definition
java_qualifiers.cpp:64
java_qualifierst::clone
std::unique_ptr< c_qualifierst > clone() const override
Definition
java_qualifiers.cpp:23
java_qualifierst::clear
void clear() override
Definition
java_qualifiers.cpp:30
java_qualifierst::operator=
java_qualifierst & operator=(const java_qualifierst &other)
Definition
java_qualifiers.cpp:13
java_qualifierst::java_qualifierst
java_qualifierst(const namespacet &ns)
Definition
java_qualifiers.h:19
java_qualifierst::annotations
std::vector< java_annotationt > annotations
Definition
java_qualifiers.h:16
java_qualifierst::operator==
bool operator==(const java_qualifierst &other) const
Definition
java_qualifiers.cpp:59
java_qualifierst::ns
const namespacet & ns
Definition
java_qualifiers.h:15
pointer_typet::base_type
const typet & base_type() const
The type of the data what we point to.
Definition
pointer_expr.h:35
typet
The type of an expression, extends irept.
Definition
type.h:29
expr2java
std::string expr2java(const exprt &expr, const namespacet &ns)
Definition
expr2java.cpp:454
expr2java.h
type_checked_cast
auto type_checked_cast(TType &base) -> typename detail::expr_dynamic_cast_return_typet< T, TType >::type
Cast a reference to a generic typet to a specific derived class and checks that the type could be con...
Definition
expr_cast.h:242
java_qualifiers.h
Java-specific type qualifiers.
to_reference_type
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
Definition
pointer_expr.h:162
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition
invariant.h:423
jbmc
src
java_bytecode
java_qualifiers.cpp
Generated by
1.17.0