17 "Can only assign from a java_qualifierst using the same namespace");
25 auto other = std::make_unique<java_qualifierst>(
ns);
27 return std::move(other);
84 std::stringstream out;
92 if(!annotation.get_values().empty())
104 out <<
'"' << value.get_name() <<
'"' <<
'=';
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
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 std::size_t count() const
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
std::size_t count() const override
java_qualifierst & operator=(const java_qualifierst &other)
std::vector< java_annotationt > annotations
bool operator==(const java_qualifierst &other) const
The type of an expression, extends irept.
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'.