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 {
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 
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 }
c_qualifierst::read
virtual void read(const typet &src) override
Definition: c_qualifiers.cpp:62
java_qualifierst::read
virtual void read(const typet &src) override
Definition: java_qualifiers.cpp:43
c_qualifierst::operator+=
virtual qualifierst & operator+=(const qualifierst &other) override
Definition: c_qualifiers.h:136
typet
The type of an expression, extends irept.
Definition: type.h:29
java_qualifierst::write
virtual void write(typet &src) const override
Definition: java_qualifiers.cpp:50
java_qualifierst::is_subset_of
virtual bool is_subset_of(const qualifierst &other) const override
Definition: java_qualifiers.cpp:78
java_qualifierst::annotations
std::vector< java_annotationt > annotations
Definition: java_qualifiers.h:16
c_qualifierst::is_subset_of
virtual bool is_subset_of(const qualifierst &other) const override
Definition: c_qualifiers.h:107
qualifierst
Definition: c_qualifiers.h:19
c_qualifierst::clear
virtual void clear() override
Definition: c_qualifiers.h:79
java_qualifierst::as_string
virtual std::string as_string() const override
Definition: java_qualifiers.cpp:94
java_qualifierst::operator==
virtual bool operator==(const qualifierst &other) const override
Definition: java_qualifiers.cpp:70
make_unique.h
java_annotationt::valuet
Definition: java_types.h:27
c_qualifierst::operator==
virtual bool operator==(const qualifierst &other) const override
Definition: c_qualifiers.h:122
c_qualifierst::write
virtual void write(typet &src) const override
Definition: c_qualifiers.cpp:89
annotated_typet
Definition: java_types.h:69
java_qualifierst::count
virtual std::size_t count() const override
Definition: java_qualifiers.cpp:32
c_qualifierst::count
virtual std::size_t count() const override
Definition: c_qualifiers.h:150
java_qualifierst::clear
virtual void clear() override
Definition: java_qualifiers.cpp:37
java_qualifierst::ns
const namespacet & ns
Definition: java_qualifiers.h:15
c_qualifierst::operator=
c_qualifierst & operator=(const c_qualifierst &other)
Definition: c_qualifiers.cpp:14
java_qualifierst::clone
virtual std::unique_ptr< qualifierst > clone() const override
Definition: java_qualifiers.cpp:25
java_qualifierst
Definition: java_qualifiers.h:13
java_qualifierst::operator=
java_qualifierst & operator=(const java_qualifierst &other)
Definition: java_qualifiers.cpp:15
java_qualifierst::operator+=
virtual qualifierst & operator+=(const qualifierst &other) override
Definition: java_qualifiers.cpp:56
expr2java
std::string expr2java(const exprt &expr, const namespacet &ns)
Definition: expr2java.cpp:455
expr2java.h
c_qualifierst::as_string
virtual std::string as_string() const override
Definition: c_qualifiers.cpp:34
java_annotationt
Definition: java_types.h:24
java_qualifiers.h
Java-specific type qualifiers.
validation_modet::INVARIANT
@ INVARIANT