19 "Can only assign from a java_qualifierst using the same namespace");
29 return std::move(other);
63 jq->annotations.begin(),
64 jq->annotations.end(),
85 auto &other_a = jq->annotations;
88 if(std::find(other_a.begin(), other_a.end(), annotation) == other_a.end())
96 std::stringstream out;
104 if(!annotation.get_values().empty())
116 out <<
'"' << value.get_name() <<
'"' <<
'=';
virtual void clear() override
virtual qualifierst & operator+=(const qualifierst &other) override
virtual std::string as_string() const override
virtual void write(typet &src) const override
virtual bool operator==(const qualifierst &other) const override
virtual std::size_t count() const override
virtual void read(const typet &src) override
c_qualifierst & operator=(const c_qualifierst &other)
virtual bool is_subset_of(const qualifierst &other) const override
const irep_idt & get(const irep_idt &name) const
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 typet & base_type() const
The type of the data what we point to.
The type of an expression, extends irept.
std::string expr2java(const exprt &expr, const namespacet &ns)
auto type_checked_cast(TType &base) -> typename detail::expr_dynamic_cast_return_typet< T, TType >::type
Cast a reference to a generic typet to a specific derived class and checks that the type could be con...
Java-specific type qualifiers.
std::unique_ptr< T > util_make_unique(Ts &&... ts)
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'.