Merge pull request #8419 from tautschnig/expr2c-no-dynamic_cast

Remove qualifierst

Author: tautschnig

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<qualifierst> clone = qualifiers.clone();
-  qualifierst &new_qualifiers = *clone;
+  std::unique_ptr<c_qualifierst> clone = qualifiers.clone();
+  c_qualifierst &new_qualifiers = *clone;
   new_qualifiers.read(src);
 
   const std::string d = declarator.empty() ? declarator : (" " + declarator);

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

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<qualifierst> java_qualifierst::clone() const
+std::unique_ptr<c_qualifierst> java_qualifierst::clone() const
 {
   auto other = std::make_unique<java_qualifierst>(ns);
   *other = *this;

jbmc/src/java_bytecode/java_qualifiers.h

@@ -23,20 +23,20 @@ class java_qualifierst : public c_qualifierst
 protected:
   java_qualifierst &operator=(const java_qualifierst &other);
 public:
-  virtual std::unique_ptr<qualifierst> clone() const override;
+  std::unique_ptr<c_qualifierst> clone() const override;
 
   java_qualifierst &operator+=(const java_qualifierst &other);
 
   const std::vector<java_annotationt> &get_annotations() const
   {
     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

src/ansi-c/c_qualifiers.cpp

@@ -24,11 +24,11 @@ c_qualifierst &c_qualifierst::operator=(const c_qualifierst &other)
   return *this;
 }
 
-std::unique_ptr<qualifierst> c_qualifierst::clone() const
+std::unique_ptr<c_qualifierst> c_qualifierst::clone() const
 {
   auto other = std::make_unique<c_qualifierst>();
   *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();
-}

src/ansi-c/c_qualifiers.h

@@ -10,45 +10,12 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_ANSI_C_C_QUALIFIERS_H
 #define CPROVER_ANSI_C_C_QUALIFIERS_H
 
-#include <iosfwd>
 #include <memory>
 #include <string>
 
 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<qualifierst> 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<qualifierst> clone() const override;
+  virtual std::unique_ptr<c_qualifierst> 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;

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<qualifierst> clone = qualifiers.clone();
-  c_qualifierst &new_qualifiers = dynamic_cast<c_qualifierst &>(*clone);
+  std::unique_ptr<c_qualifierst> 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());

src/ansi-c/expr2c_class.h

@@ -24,7 +24,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_code.h>
 
 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);
 

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<qualifierst> clone = qualifiers.clone();
-  qualifierst &new_qualifiers = *clone;
+  std::unique_ptr<c_qualifierst> clone = qualifiers.clone();
+  c_qualifierst &new_qualifiers = *clone;
   new_qualifiers.read(src);
 
   const std::string d = declarator.empty() ? declarator : (" " + declarator);
@@ -274,15 +274,15 @@ 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();
 
     if(base_type.id() == ID_code)
     {
       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;
   }