cprover
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 {
17  INVARIANT(
18  &other.ns == &ns,
19  "Can only assign from a java_qualifierst using the same namespace");
20  annotations = other.annotations;
22  return *this;
23 }
24 
25 std::unique_ptr<qualifierst> java_qualifierst::clone() const
26 {
27  auto other = util_make_unique<java_qualifierst>(ns);
28  *other = *this;
29  return std::move(other);
30 }
31 
32 std::size_t java_qualifierst::count() const
33 {
34  return c_qualifierst::count() + annotations.size();
35 }
36 
38 {
40  annotations.clear();
41 }
42 
43 void java_qualifierst::read(const typet &src)
44 {
46  auto &annotated_type = static_cast<const annotated_typet &>(src);
47  annotations = annotated_type.get_annotations();
48 }
49 
51 {
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 
70 bool java_qualifierst::operator==(const qualifierst &other) const
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 {
80  if(!c_qualifierst::is_subset_of(other))
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 
94 std::string java_qualifierst::as_string() const
95 {
96  std::stringstream out;
97  for(const java_annotationt &annotation : annotations)
98  {
99  out << '@';
100  out << annotation.get_type().subtype().get(ID_identifier);
101 
102  if(!annotation.get_values().empty())
103  {
104  out << '(';
105 
106  bool first = true;
107  for(const java_annotationt::valuet &value : annotation.get_values())
108  {
109  if(first)
110  first = false;
111  else
112  out << ", ";
113 
114  out << '"' << value.get_name() << '"' << '=';
115  out << expr2java(value.get_value(), ns);
116  }
117 
118  out << ')';
119  }
120  out << ' ';
121  }
122  out << c_qualifierst::as_string();
123  return out.str();
124 }
Java-specific type qualifiers.
The type of an expression, extends irept.
Definition: type.h:27
virtual bool operator==(const qualifierst &other) const override
Definition: c_qualifiers.h:122
virtual void write(typet &src) const override
virtual std::unique_ptr< qualifierst > clone() const override
virtual std::string as_string() const override
virtual std::size_t count() const override
c_qualifierst & operator=(const c_qualifierst &other)
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:198
virtual void read(const typet &src) override
const std::vector< java_annotationt > & get_annotations() const
virtual bool operator==(const qualifierst &other) const override
virtual void clear() override
Definition: c_qualifiers.h:79
virtual void clear() override
virtual void read(const typet &src) override
virtual std::size_t count() const override
Definition: c_qualifiers.h:150
java_qualifierst & operator=(const java_qualifierst &other)
virtual std::string as_string() const override
virtual bool is_subset_of(const qualifierst &other) const override
Definition: c_qualifiers.h:107
virtual bool is_subset_of(const qualifierst &other) const override
virtual qualifierst & operator+=(const qualifierst &other) override
Definition: c_qualifiers.h:136
std::vector< java_annotationt > annotations
virtual qualifierst & operator+=(const qualifierst &other) override
virtual void write(typet &src) const override
const namespacet & ns
std::string expr2java(const exprt &expr, const namespacet &ns)
Definition: expr2java.cpp:441