forked from diffblue/cbmc
-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathjava_qualifiers.cpp
109 lines (92 loc) · 2.46 KB
/
java_qualifiers.cpp
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
// Author: Diffblue Ltd.
/// \file
/// Java-specific type qualifiers
#include "java_qualifiers.h"
#include <sstream>
#include <iterator>
#include "expr2java.h"
java_qualifierst &java_qualifierst::operator=(const java_qualifierst &other)
{
INVARIANT(
&other.ns == &ns,
"Can only assign from a java_qualifierst using the same namespace");
annotations = other.annotations;
c_qualifierst::operator=(other);
return *this;
}
std::unique_ptr<c_qualifierst> java_qualifierst::clone() const
{
auto other = std::make_unique<java_qualifierst>(ns);
*other = *this;
return std::move(other);
}
void java_qualifierst::clear()
{
c_qualifierst::clear();
annotations.clear();
}
void java_qualifierst::read(const typet &src)
{
c_qualifierst::read(src);
auto &annotated_type = static_cast<const annotated_typet &>(src);
annotations = annotated_type.get_annotations();
}
void java_qualifierst::write(typet &src) const
{
c_qualifierst::write(src);
type_checked_cast<annotated_typet>(src).get_annotations() = annotations;
}
java_qualifierst &java_qualifierst::operator+=(const java_qualifierst &other)
{
c_qualifierst::operator+=(other);
std::copy(
other.annotations.begin(),
other.annotations.end(),
std::back_inserter(annotations));
return *this;
}
bool java_qualifierst::operator==(const java_qualifierst &other) const
{
return c_qualifierst::operator==(other) && annotations == other.annotations;
}
bool java_qualifierst::is_subset_of(const java_qualifierst &other) const
{
if(!c_qualifierst::is_subset_of(other))
return false;
auto &other_a = other.annotations;
for(const auto &annotation : annotations)
{
if(std::find(other_a.begin(), other_a.end(), annotation) == other_a.end())
return false;
}
return true;
}
std::string java_qualifierst::as_string() const
{
std::stringstream out;
for(const java_annotationt &annotation : annotations)
{
out << '@';
out << to_reference_type(annotation.get_type())
.base_type()
.get(ID_identifier);
if(!annotation.get_values().empty())
{
out << '(';
bool first = true;
for(const java_annotationt::valuet &value : annotation.get_values())
{
if(first)
first = false;
else
out << ", ";
out << '"' << value.get_name() << '"' << '=';
out << expr2java(value.get_value(), ns);
}
out << ')';
}
out << ' ';
}
out << c_qualifierst::as_string();
return out.str();
}