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<c_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  std::copy(
58  other.annotations.begin(),
59  other.annotations.end(),
60  std::back_inserter(annotations));
61  return *this;
62 }
63 
65 {
66  return c_qualifierst::operator==(other) && annotations == other.annotations;
67 }
68 
70 {
71  if(!c_qualifierst::is_subset_of(other))
72  return false;
73  auto &other_a = other.annotations;
74  for(const auto &annotation : annotations)
75  {
76  if(std::find(other_a.begin(), other_a.end(), annotation) == other_a.end())
77  return false;
78  }
79  return true;
80 }
81 
82 std::string java_qualifierst::as_string() const
83 {
84  std::stringstream out;
85  for(const java_annotationt &annotation : annotations)
86  {
87  out << '@';
88  out << to_reference_type(annotation.get_type())
89  .base_type()
90  .get(ID_identifier);
91 
92  if(!annotation.get_values().empty())
93  {
94  out << '(';
95 
96  bool first = true;
97  for(const java_annotationt::valuet &value : annotation.get_values())
98  {
99  if(first)
100  first = false;
101  else
102  out << ", ";
103 
104  out << '"' << value.get_name() << '"' << '=';
105  out << expr2java(value.get_value(), ns);
106  }
107 
108  out << ')';
109  }
110  out << ' ';
111  }
112  out << c_qualifierst::as_string();
113  return out.str();
114 }
c_qualifierst & operator+=(const c_qualifierst &other)
Definition: c_qualifiers.h:99
virtual void write(typet &src) const
virtual void read(const typet &src)
bool is_subset_of(const c_qualifierst &other) const
Definition: c_qualifiers.h:69
virtual std::size_t count() const
Definition: c_qualifiers.h:113
virtual void clear()
Definition: c_qualifiers.h:39
virtual std::string as_string() const
c_qualifierst & operator=(const c_qualifierst &other)
bool operator==(const c_qualifierst &other) const
Definition: c_qualifiers.h:82
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:44
void read(const typet &src) override
java_qualifierst & operator+=(const java_qualifierst &other)
void write(typet &src) const override
std::string as_string() const override
bool is_subset_of(const java_qualifierst &other) const
std::unique_ptr< c_qualifierst > clone() const override
std::size_t count() const override
void clear() override
java_qualifierst & operator=(const java_qualifierst &other)
std::vector< java_annotationt > annotations
bool operator==(const java_qualifierst &other) const
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:454
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