diff --git a/jbmc/src/java_bytecode/expr2java.cpp b/jbmc/src/java_bytecode/expr2java.cpp index 223988d10f6..376b331a573 100644 --- a/jbmc/src/java_bytecode/expr2java.cpp +++ b/jbmc/src/java_bytecode/expr2java.cpp @@ -242,11 +242,11 @@ std::string expr2javat::convert_constant( std::string expr2javat::convert_rec( const typet &src, - const qualifierst &qualifiers, + const c_qualifierst &qualifiers, const std::string &declarator) { - std::unique_ptr clone = qualifiers.clone(); - qualifierst &new_qualifiers = *clone; + std::unique_ptr clone = qualifiers.clone(); + c_qualifierst &new_qualifiers = *clone; new_qualifiers.read(src); const std::string d = declarator.empty() ? declarator : (" " + declarator); diff --git a/jbmc/src/java_bytecode/expr2java.h b/jbmc/src/java_bytecode/expr2java.h index 152eab1bab7..427568dd33b 100644 --- a/jbmc/src/java_bytecode/expr2java.h +++ b/jbmc/src/java_bytecode/expr2java.h @@ -42,7 +42,7 @@ class expr2javat:public expr2ct virtual std::string convert_rec( const typet &src, - const qualifierst &qualifiers, + const c_qualifierst &qualifiers, const std::string &declarator) override; // length of string representation of Java Char diff --git a/jbmc/src/java_bytecode/java_qualifiers.cpp b/jbmc/src/java_bytecode/java_qualifiers.cpp index acff3ae93ab..d146580cc91 100644 --- a/jbmc/src/java_bytecode/java_qualifiers.cpp +++ b/jbmc/src/java_bytecode/java_qualifiers.cpp @@ -20,7 +20,7 @@ java_qualifierst &java_qualifierst::operator=(const java_qualifierst &other) return *this; } -std::unique_ptr java_qualifierst::clone() const +std::unique_ptr java_qualifierst::clone() const { auto other = std::make_unique(ns); *other = *this; diff --git a/jbmc/src/java_bytecode/java_qualifiers.h b/jbmc/src/java_bytecode/java_qualifiers.h index 3a235f64778..8e61ad187e6 100644 --- a/jbmc/src/java_bytecode/java_qualifiers.h +++ b/jbmc/src/java_bytecode/java_qualifiers.h @@ -23,7 +23,7 @@ class java_qualifierst : public c_qualifierst protected: java_qualifierst &operator=(const java_qualifierst &other); public: - virtual std::unique_ptr clone() const override; + std::unique_ptr clone() const override; java_qualifierst &operator+=(const java_qualifierst &other); @@ -31,12 +31,12 @@ class java_qualifierst : public c_qualifierst { return annotations; } - virtual std::size_t count() const override; + std::size_t count() const override; - virtual void clear() override; + void clear() override; - virtual void read(const typet &src) override; - virtual void write(typet &src) const override; + void read(const typet &src) override; + void write(typet &src) const override; bool is_subset_of(const java_qualifierst &other) const; bool operator==(const java_qualifierst &other) const; @@ -45,7 +45,7 @@ class java_qualifierst : public c_qualifierst return !(*this == other); } - virtual std::string as_string() const override; + std::string as_string() const override; }; #endif // CPROVER_JAVA_BYTECODE_JAVA_QUALIFIERS_H diff --git a/src/ansi-c/c_qualifiers.cpp b/src/ansi-c/c_qualifiers.cpp index 36d64fb6433..02604390d32 100644 --- a/src/ansi-c/c_qualifiers.cpp +++ b/src/ansi-c/c_qualifiers.cpp @@ -24,11 +24,11 @@ c_qualifierst &c_qualifierst::operator=(const c_qualifierst &other) return *this; } -std::unique_ptr c_qualifierst::clone() const +std::unique_ptr c_qualifierst::clone() const { auto other = std::make_unique(); *other = *this; - return std::move(other); + return other; } std::string c_qualifierst::as_string() const @@ -151,9 +151,3 @@ void c_qualifierst::clear(typet &dest) dest.remove(ID_C_nodiscard); dest.remove(ID_C_noreturn); } - -/// pretty-print the qualifiers -std::ostream &operator<<(std::ostream &out, const qualifierst &qualifiers) -{ - return out << qualifiers.as_string(); -} diff --git a/src/ansi-c/c_qualifiers.h b/src/ansi-c/c_qualifiers.h index 052cf17f824..3c403dcadb3 100644 --- a/src/ansi-c/c_qualifiers.h +++ b/src/ansi-c/c_qualifiers.h @@ -10,45 +10,12 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_ANSI_C_C_QUALIFIERS_H #define CPROVER_ANSI_C_C_QUALIFIERS_H -#include #include #include class typet; -class qualifierst -{ -protected: - // Only derived classes can construct - qualifierst() = default; - -public: - // Copy/move construction/assignment is deleted here and in derived classes - qualifierst(const qualifierst &) = delete; - qualifierst(qualifierst &&) = delete; - qualifierst &operator=(const qualifierst &) = delete; - qualifierst &operator=(qualifierst &&) = delete; - - // Destruction is virtual - virtual ~qualifierst() = default; - -public: - virtual std::unique_ptr clone() const = 0; - - virtual std::size_t count() const = 0; - - virtual void clear() = 0; - - virtual void read(const typet &src) = 0; - virtual void write(typet &src) const = 0; - - // String conversion - virtual std::string as_string() const = 0; - friend std::ostream &operator<<(std::ostream &, const qualifierst &); -}; - - -class c_qualifierst : public qualifierst +class c_qualifierst { public: c_qualifierst() @@ -62,12 +29,14 @@ class c_qualifierst : public qualifierst read(src); } + virtual ~c_qualifierst() = default; + protected: c_qualifierst &operator=(const c_qualifierst &other); public: - virtual std::unique_ptr clone() const override; + virtual std::unique_ptr clone() const; - virtual void clear() override + virtual void clear() { is_constant=false; is_volatile=false; @@ -91,9 +60,9 @@ class c_qualifierst : public qualifierst // will likely add alignment here as well - virtual std::string as_string() const override; - virtual void read(const typet &src) override; - virtual void write(typet &src) const override; + virtual std::string as_string() const; + virtual void read(const typet &src); + virtual void write(typet &src) const; static void clear(typet &dest); @@ -141,7 +110,7 @@ class c_qualifierst : public qualifierst return *this; } - virtual std::size_t count() const override + virtual std::size_t count() const { return is_constant + is_volatile + is_restricted + is_atomic + is_ptr32 + is_ptr64 + is_nodiscard + is_noreturn; diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index ae1ec2b98dc..3257a74f270 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -213,16 +213,16 @@ void expr2ct::get_shorthands(const exprt &expr) std::string expr2ct::convert(const typet &src) { - return convert_rec(src, c_qualifierst(), ""); + return convert_with_identifier(src, ""); } std::string expr2ct::convert_rec( const typet &src, - const qualifierst &qualifiers, + const c_qualifierst &qualifiers, const std::string &declarator) { - std::unique_ptr clone = qualifiers.clone(); - c_qualifierst &new_qualifiers = dynamic_cast(*clone); + std::unique_ptr clone = qualifiers.clone(); + c_qualifierst &new_qualifiers = *clone; new_qualifiers.read(src); std::string q=new_qualifiers.as_string(); @@ -379,7 +379,7 @@ std::string expr2ct::convert_rec( for(const auto &c : union_type.components()) { dest += ' '; - dest += convert_rec(c.type(), c_qualifierst(), id2string(c.get_name())); + dest += convert_with_identifier(c.type(), id2string(c.get_name())); dest += ';'; } @@ -538,7 +538,7 @@ std::string expr2ct::convert_rec( { std::string arg_declarator= convert(symbol_exprt(it->get_identifier(), it->type())); - dest+=convert_rec(it->type(), c_qualifierst(), arg_declarator); + dest += convert_with_identifier(it->type(), arg_declarator); } } @@ -692,10 +692,8 @@ std::string expr2ct::convert_struct_type( } dest+=' '; - dest+=convert_rec( - component.type(), - c_qualifierst(), - id2string(component.get_name())); + dest += convert_with_identifier( + component.type(), id2string(component.get_name())); dest+=';'; } @@ -715,7 +713,7 @@ std::string expr2ct::convert_struct_type( /// \return A C-like type declaration of an array std::string expr2ct::convert_array_type( const typet &src, - const qualifierst &qualifiers, + const c_qualifierst &qualifiers, const std::string &declarator_str) { return convert_array_type( @@ -732,7 +730,7 @@ std::string expr2ct::convert_array_type( /// \return A C-like type declaration of an array std::string expr2ct::convert_array_type( const typet &src, - const qualifierst &qualifiers, + const c_qualifierst &qualifiers, const std::string &declarator_str, bool inc_size_if_possible) { @@ -2850,7 +2848,7 @@ expr2ct::convert_code_frontend_decl(const codet &src, unsigned indent) dest+="inline "; } - dest+=convert_rec(src.op0().type(), c_qualifierst(), declarator); + dest += convert_with_identifier(src.op0().type(), declarator); if(src.operands().size()==2) dest+="="+convert(src.op1()); diff --git a/src/ansi-c/expr2c_class.h b/src/ansi-c/expr2c_class.h index 6ede63b7c2b..e60af80fa33 100644 --- a/src/ansi-c/expr2c_class.h +++ b/src/ansi-c/expr2c_class.h @@ -24,7 +24,7 @@ Author: Daniel Kroening, kroening@kroening.com #include class annotated_pointer_constant_exprt; -class qualifierst; +class c_qualifierst; class namespacet; class r_or_w_ok_exprt; class pointer_in_range_exprt; @@ -57,7 +57,7 @@ class expr2ct virtual std::string convert_rec( const typet &src, - const qualifierst &qualifiers, + const c_qualifierst &qualifiers, const std::string &declarator); virtual std::string convert_struct_type( @@ -74,12 +74,12 @@ class expr2ct virtual std::string convert_array_type( const typet &src, - const qualifierst &qualifiers, + const c_qualifierst &qualifiers, const std::string &declarator_str); std::string convert_array_type( const typet &src, - const qualifierst &qualifiers, + const c_qualifierst &qualifiers, const std::string &declarator_str, bool inc_size_if_possible); diff --git a/src/cpp/expr2cpp.cpp b/src/cpp/expr2cpp.cpp index 1144b0fb0ce..f562d5fe4ca 100644 --- a/src/cpp/expr2cpp.cpp +++ b/src/cpp/expr2cpp.cpp @@ -42,7 +42,7 @@ class expr2cppt:public expr2ct std::string convert_rec( const typet &src, - const qualifierst &qualifiers, + const c_qualifierst &qualifiers, const std::string &declarator) override; }; @@ -130,11 +130,11 @@ std::string expr2cppt::convert_constant( std::string expr2cppt::convert_rec( const typet &src, - const qualifierst &qualifiers, + const c_qualifierst &qualifiers, const std::string &declarator) { - std::unique_ptr clone = qualifiers.clone(); - qualifierst &new_qualifiers = *clone; + std::unique_ptr clone = qualifiers.clone(); + c_qualifierst &new_qualifiers = *clone; new_qualifiers.read(src); const std::string d = declarator.empty() ? declarator : (" " + declarator); @@ -274,7 +274,7 @@ std::string expr2cppt::convert_rec( typet member; member.swap(tmp.add(ID_to_member)); - std::string dest="("+convert_rec(member, c_qualifierst(), "")+":: *)"; + std::string dest = "(" + convert(member) + ":: *)"; const auto &base_type = to_pointer_type(src).base_type(); @@ -282,7 +282,7 @@ std::string expr2cppt::convert_rec( { const code_typet &code_type = to_code_type(base_type); const typet &return_type = code_type.return_type(); - dest=convert_rec(return_type, c_qualifierst(), "")+" "+dest; + dest = convert(return_type) + " " + dest; const code_typet::parameterst &args = code_type.parameters(); dest+="("; @@ -293,14 +293,14 @@ std::string expr2cppt::convert_rec( { if(it!=args.begin()) dest+=", "; - dest+=convert_rec(it->type(), c_qualifierst(), ""); + dest += convert(it->type()); } dest+=")"; dest+=d; } else - dest = convert_rec(base_type, c_qualifierst(), "") + " " + dest + d; + dest = convert(base_type) + " " + dest + d; return dest; }