CBMC
java_qualifiers.h
Go to the documentation of this file.
1 // Author: Diffblue Ltd.
2 
5 
6 #ifndef CPROVER_JAVA_BYTECODE_JAVA_QUALIFIERS_H
7 #define CPROVER_JAVA_BYTECODE_JAVA_QUALIFIERS_H
8 
9 #include "java_types.h"
10 #include <ansi-c/c_qualifiers.h>
11 
13 {
14 private:
15  const namespacet &ns;
16  std::vector<java_annotationt> annotations;
17 
18 public:
19  explicit java_qualifierst(const namespacet &ns)
20  : ns(ns)
21  {}
22 
23 protected:
25 public:
26  std::unique_ptr<c_qualifierst> clone() const override;
27 
29 
30  const std::vector<java_annotationt> &get_annotations() const
31  {
32  return annotations;
33  }
34  std::size_t count() const override;
35 
36  void clear() override;
37 
38  void read(const typet &src) override;
39  void write(typet &src) const override;
40 
41  bool is_subset_of(const java_qualifierst &other) const;
42  bool operator==(const java_qualifierst &other) const;
43  bool operator!=(const java_qualifierst &other) const
44  {
45  return !(*this == other);
46  }
47 
48  std::string as_string() const override;
49 };
50 
51 #endif // CPROVER_JAVA_BYTECODE_JAVA_QUALIFIERS_H
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 operator!=(const java_qualifierst &other) const
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)
java_qualifierst(const namespacet &ns)
std::vector< java_annotationt > annotations
bool operator==(const java_qualifierst &other) const
const std::vector< java_annotationt > & get_annotations() const
const namespacet & ns
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
The type of an expression, extends irept.
Definition: type.h:29