CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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
14{
16 &other.ns == &ns,
17 "Can only assign from a java_qualifierst using the same namespace");
20 return *this;
21}
22
23std::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
30std::size_t java_qualifierst::count() const
31{
32 return c_qualifierst::count() + annotations.size();
33}
34
40
42{
44 auto &annotated_type = static_cast<const annotated_typet &>(src);
45 annotations = annotated_type.get_annotations();
46}
47
49{
51 type_checked_cast<annotated_typet>(src).get_annotations() = annotations;
52}
53
55{
57 std::copy(
58 other.annotations.begin(),
59 other.annotations.end(),
60 std::back_inserter(annotations));
61 return *this;
62}
63
65{
66 return c_qualifierst::operator==(other) && annotations == other.annotations;
67}
68
70{
72 return false;
73 auto &other_a = other.annotations;
74 for(const auto &annotation : annotations)
75 {
76 if(std::find(other_a.begin(), other_a.end(), annotation) == other_a.end())
77 return false;
78 }
79 return true;
80}
81
82std::string java_qualifierst::as_string() const
83{
84 std::stringstream out;
85 for(const java_annotationt &annotation : annotations)
86 {
87 out << '@';
88 out << to_reference_type(annotation.get_type())
89 .base_type()
90 .get(ID_identifier);
91
92 if(!annotation.get_values().empty())
93 {
94 out << '(';
95
96 bool first = true;
97 for(const java_annotationt::valuet &value : annotation.get_values())
98 {
99 if(first)
100 first = false;
101 else
102 out << ", ";
103
104 out << '"' << value.get_name() << '"' << '=';
105 out << expr2java(value.get_value(), ns);
106 }
107
108 out << ')';
109 }
110 out << ' ';
111 }
113 return out.str();
114}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
virtual void write(typet &src) const
virtual void read(const typet &src)
c_qualifierst & operator+=(const c_qualifierst &other)
bool is_subset_of(const c_qualifierst &other) const
virtual std::size_t count() const
virtual void clear()
virtual std::string as_string() const
c_qualifierst & operator=(const c_qualifierst &other)
bool operator==(const c_qualifierst &other) const
void read(const typet &src) override
java_qualifierst & operator+=(const java_qualifierst &other)
void write(typet &src) const override
std::string as_string() const override
bool is_subset_of(const java_qualifierst &other) const
std::unique_ptr< c_qualifierst > clone() const override
std::size_t count() const override
void clear() override
java_qualifierst & operator=(const java_qualifierst &other)
std::vector< java_annotationt > annotations
bool operator==(const java_qualifierst &other) const
const namespacet & ns
The type of an expression, extends irept.
Definition type.h:29
std::string expr2java(const exprt &expr, const namespacet &ns)
Java-specific type qualifiers.
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423