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 "expr2java.h"
12 
14 {
15  INVARIANT(
16  &other.ns == &ns,
17  "Can only assign from a java_qualifierst using the same namespace");
18  annotations = other.annotations;
20  return *this;
21 }
22 
23 std::unique_ptr<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 
30 std::size_t java_qualifierst::count() const
31 {
32  return c_qualifierst::count() + annotations.size();
33 }
34 
36 {
38  annotations.clear();
39 }
40 
41 void java_qualifierst::read(const typet &src)
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  auto jq = dynamic_cast<const java_qualifierst *>(&other);
58  if(jq != nullptr)
59  {
60  std::copy(
61  jq->annotations.begin(),
62  jq->annotations.end(),
63  std::back_inserter(annotations));
64  }
65  return *this;
66 }
67 
68 bool java_qualifierst::operator==(const qualifierst &other) const
69 {
70  auto jq = dynamic_cast<const java_qualifierst *>(&other);
71  if(jq == nullptr)
72  return false;
73  return c_qualifierst::operator==(other) && annotations == jq->annotations;
74 }
75 
77 {
78  if(!c_qualifierst::is_subset_of(other))
79  return false;
80  auto jq = dynamic_cast<const java_qualifierst *>(&other);
81  if(jq == nullptr)
82  return annotations.empty();
83  auto &other_a = jq->annotations;
84  for(const auto &annotation : annotations)
85  {
86  if(std::find(other_a.begin(), other_a.end(), annotation) == other_a.end())
87  return false;
88  }
89  return true;
90 }
91 
92 std::string java_qualifierst::as_string() const
93 {
94  std::stringstream out;
95  for(const java_annotationt &annotation : annotations)
96  {
97  out << '@';
98  out << to_reference_type(annotation.get_type())
99  .base_type()
100  .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 }
virtual void clear() override
Definition: c_qualifiers.h:80
virtual std::string as_string() const override
virtual void write(typet &src) const override
virtual bool operator==(const qualifierst &other) const override
Definition: c_qualifiers.h:123
virtual std::size_t count() const override
Definition: c_qualifiers.h:151
virtual void read(const typet &src) override
virtual qualifierst & operator+=(const qualifierst &other) override
Definition: c_qualifiers.h:137
c_qualifierst & operator=(const c_qualifierst &other)
virtual bool is_subset_of(const qualifierst &other) const override
Definition: c_qualifiers.h:108
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.
Definition: pointer_expr.h:35
The type of an expression, extends irept.
Definition: type.h:29
std::string expr2java(const exprt &expr, const namespacet &ns)
Definition: expr2java.cpp:452
Java-specific type qualifiers.
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
Definition: pointer_expr.h:162