cprover
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 <util/make_unique.h>
12
13#include "expr2java.h"
14
16{
18 &other.ns == &ns,
19 "Can only assign from a java_qualifierst using the same namespace");
22 return *this;
23}
24
25std::unique_ptr<qualifierst> java_qualifierst::clone() const
26{
28 *other = *this;
29 return std::move(other);
30}
31
32std::size_t java_qualifierst::count() const
33{
34 return c_qualifierst::count() + annotations.size();
35}
36
42
44{
46 auto &annotated_type = static_cast<const annotated_typet &>(src);
47 annotations = annotated_type.get_annotations();
48}
49
51{
53 type_checked_cast<annotated_typet>(src).get_annotations() = annotations;
54}
55
57{
59 auto jq = dynamic_cast<const java_qualifierst *>(&other);
60 if(jq != nullptr)
61 {
62 std::copy(
63 jq->annotations.begin(),
64 jq->annotations.end(),
65 std::back_inserter(annotations));
66 }
67 return *this;
68}
69
71{
72 auto jq = dynamic_cast<const java_qualifierst *>(&other);
73 if(jq == nullptr)
74 return false;
75 return c_qualifierst::operator==(other) && annotations == jq->annotations;
76}
77
79{
81 return false;
82 auto jq = dynamic_cast<const java_qualifierst *>(&other);
83 if(jq == nullptr)
84 return annotations.empty();
85 auto &other_a = jq->annotations;
86 for(const auto &annotation : annotations)
87 {
88 if(std::find(other_a.begin(), other_a.end(), annotation) == other_a.end())
89 return false;
90 }
91 return true;
92}
93
94std::string java_qualifierst::as_string() const
95{
96 std::stringstream out;
97 for(const java_annotationt &annotation : annotations)
98 {
99 out << '@';
100 out << to_reference_type(annotation.get_type())
101 .base_type()
102 .get(ID_identifier);
103
104 if(!annotation.get_values().empty())
105 {
106 out << '(';
107
108 bool first = true;
109 for(const java_annotationt::valuet &value : annotation.get_values())
110 {
111 if(first)
112 first = false;
113 else
114 out << ", ";
115
116 out << '"' << value.get_name() << '"' << '=';
117 out << expr2java(value.get_value(), ns);
118 }
119
120 out << ')';
121 }
122 out << ' ';
123 }
125 return out.str();
126}
virtual void clear() override
virtual qualifierst & operator+=(const qualifierst &other) override
virtual std::string as_string() const override
virtual void write(typet &src) const override
virtual bool operator==(const qualifierst &other) const override
virtual std::size_t count() const override
virtual void read(const typet &src) override
c_qualifierst & operator=(const c_qualifierst &other)
virtual bool is_subset_of(const qualifierst &other) const override
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
virtual std::unique_ptr< qualifierst > clone() const override
virtual void read(const typet &src) override
virtual bool is_subset_of(const qualifierst &other) const override
virtual void write(typet &src) const override
virtual std::string as_string() const override
virtual bool operator==(const qualifierst &other) const override
virtual qualifierst & operator+=(const qualifierst &other) override
virtual std::size_t count() const override
virtual void clear() override
java_qualifierst & operator=(const java_qualifierst &other)
std::vector< java_annotationt > annotations
const namespacet & ns
const typet & base_type() const
The type of the data what we point to.
The type of an expression, extends irept.
Definition type.h:29
std::string expr2java(const exprt &expr, const namespacet &ns)
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-specific type qualifiers.
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition make_unique.h:19
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