CBMC
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 << 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  }
124  out << c_qualifierst::as_string();
125  return out.str();
126 }
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:137
typet
The type of an expression, extends irept.
Definition: type.h:28
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:108
qualifierst
Definition: c_qualifiers.h:19
c_qualifierst::clear
virtual void clear() override
Definition: c_qualifiers.h:80
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
irept::get
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
make_unique.h
java_annotationt::valuet
Definition: java_types.h:24
c_qualifierst::operator==
virtual bool operator==(const qualifierst &other) const override
Definition: c_qualifiers.h:123
c_qualifierst::write
virtual void write(typet &src) const override
Definition: c_qualifiers.cpp:89
annotated_typet
Definition: java_types.h:66
java_qualifierst::count
virtual std::size_t count() const override
Definition: java_qualifiers.cpp:32
to_reference_type
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
Definition: pointer_expr.h:148
c_qualifierst::count
virtual std::size_t count() const override
Definition: c_qualifiers.h:151
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:12
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
pointer_typet::base_type
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
expr2java
std::string expr2java(const exprt &expr, const namespacet &ns)
Definition: expr2java.cpp:450
expr2java.h
c_qualifierst::as_string
virtual std::string as_string() const override
Definition: c_qualifiers.cpp:34
java_annotationt
Definition: java_types.h:21
java_qualifiers.h
validation_modet::INVARIANT
@ INVARIANT