CBMC
Loading...
Searching...
No Matches
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{
16 &other.ns == &ns,
17 "Can only assign from a java_qualifierst using the same namespace");
20 return *this;
21}
22
23std::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
35
37{
39 auto &annotated_type = static_cast<const annotated_typet &>(src);
40 annotations = annotated_type.get_annotations();
41}
42
44{
46 type_checked_cast<annotated_typet>(src).get_annotations() = annotations;
47}
48
50{
52 std::copy(
53 other.annotations.begin(),
54 other.annotations.end(),
55 std::back_inserter(annotations));
56 return *this;
57}
58
60{
61 return c_qualifierst::operator==(other) && annotations == other.annotations;
62}
63
65{
67 return false;
68 auto &other_a = other.annotations;
69 for(const auto &annotation : annotations)
70 {
71 if(std::find(other_a.begin(), other_a.end(), annotation) == other_a.end())
72 return false;
73 }
74 return true;
75}
76
77std::string java_qualifierst::as_string() const
78{
79 std::stringstream out;
80 for(const java_annotationt &annotation : annotations)
81 {
82 out << '@';
83 out << to_reference_type(annotation.get_type())
84 .base_type()
85 .get(ID_identifier);
86
87 if(!annotation.get_values().empty())
88 {
89 out << '(';
90
91 bool first = true;
92 for(const java_annotationt::valuet &value : annotation.get_values())
93 {
94 if(first)
95 first = false;
96 else
97 out << ", ";
98
99 out << '"' << value.get_name() << '"' << '=';
100 out << expr2java(value.get_value(), ns);
101 }
102
103 out << ')';
104 }
105 out << ' ';
106 }
108 return out.str();
109}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
virtual void write(typet &src) const
virtual void read(const typet &src)
c_qualifierst & operator+=(const c_qualifierst &other)
bool is_subset_of(const c_qualifierst &other) const
virtual void clear()
virtual std::string as_string() const
c_qualifierst & operator=(const c_qualifierst &other)
bool operator==(const c_qualifierst &other) const
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
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
The type of an expression, extends irept.
Definition type.h:29
std::string expr2java(const exprt &expr, const namespacet &ns)
Java-specific type qualifiers.
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423