Skip to content

Remove qualifierst #8419

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Aug 20, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions jbmc/src/java_bytecode/expr2java.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
2 changes: 1 addition & 1 deletion jbmc/src/java_bytecode/expr2java.h
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion jbmc/src/java_bytecode/java_qualifiers.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
12 changes: 6 additions & 6 deletions jbmc/src/java_bytecode/java_qualifiers.h
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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
10 changes: 2 additions & 8 deletions src/ansi-c/c_qualifiers.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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();
}
49 changes: 9 additions & 40 deletions src/ansi-c/c_qualifiers.h
Original file line number Diff line number Diff line change
Expand Up @@ -10,45 +10,12 @@
#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()
Expand All @@ -62,12 +29,14 @@
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;
Expand All @@ -91,9 +60,9 @@

// 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;

Check warning on line 65 in src/ansi-c/c_qualifiers.h

View check run for this annotation

Codecov / codecov/patch

src/ansi-c/c_qualifiers.h#L63-L65

Added lines #L63 - L65 were not covered by tests

static void clear(typet &dest);

Expand Down Expand Up @@ -141,7 +110,7 @@
return *this;
}

virtual std::size_t count() const override
virtual std::size_t count() const

Check warning on line 113 in src/ansi-c/c_qualifiers.h

View check run for this annotation

Codecov / codecov/patch

src/ansi-c/c_qualifiers.h#L113

Added line #L113 was not covered by tests
{
return is_constant + is_volatile + is_restricted + is_atomic + is_ptr32 +
is_ptr64 + is_nodiscard + is_noreturn;
Expand Down
24 changes: 11 additions & 13 deletions src/ansi-c/expr2c.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -213,16 +213,16 @@

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();
Expand Down Expand Up @@ -379,7 +379,7 @@
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 += ';';
}

Expand Down Expand Up @@ -538,7 +538,7 @@
{
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);
}
}

Expand Down Expand Up @@ -692,10 +692,8 @@
}

dest+=' ';
dest+=convert_rec(
component.type(),
c_qualifierst(),
id2string(component.get_name()));
dest += convert_with_identifier(
component.type(), id2string(component.get_name()));
dest+=';';
}

Expand All @@ -715,7 +713,7 @@
/// \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,

Check warning on line 716 in src/ansi-c/expr2c.cpp

View check run for this annotation

Codecov / codecov/patch

src/ansi-c/expr2c.cpp#L716

Added line #L716 was not covered by tests
const std::string &declarator_str)
{
return convert_array_type(
Expand All @@ -732,7 +730,7 @@
/// \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,

Check warning on line 733 in src/ansi-c/expr2c.cpp

View check run for this annotation

Codecov / codecov/patch

src/ansi-c/expr2c.cpp#L733

Added line #L733 was not covered by tests
const std::string &declarator_str,
bool inc_size_if_possible)
{
Expand Down Expand Up @@ -2850,7 +2848,7 @@
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());
Expand Down
8 changes: 4 additions & 4 deletions src/ansi-c/expr2c_class.h
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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(
Expand All @@ -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);

Expand Down
16 changes: 8 additions & 8 deletions src/cpp/expr2cpp.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@

std::string convert_rec(
const typet &src,
const qualifierst &qualifiers,
const c_qualifierst &qualifiers,
const std::string &declarator) override;
};

Expand Down Expand Up @@ -130,11 +130,11 @@

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);
Expand Down Expand Up @@ -274,15 +274,15 @@
typet member;
member.swap(tmp.add(ID_to_member));

std::string dest="("+convert_rec(member, c_qualifierst(), "")+":: *)";
std::string dest = "(" + convert(member) + ":: *)";

Check warning on line 277 in src/cpp/expr2cpp.cpp

View check run for this annotation

Codecov / codecov/patch

src/cpp/expr2cpp.cpp#L277

Added line #L277 was not covered by tests

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;

Check warning on line 285 in src/cpp/expr2cpp.cpp

View check run for this annotation

Codecov / codecov/patch

src/cpp/expr2cpp.cpp#L285

Added line #L285 was not covered by tests

const code_typet::parameterst &args = code_type.parameters();
dest+="(";
Expand All @@ -293,14 +293,14 @@
{
if(it!=args.begin())
dest+=", ";
dest+=convert_rec(it->type(), c_qualifierst(), "");
dest += convert(it->type());

Check warning on line 296 in src/cpp/expr2cpp.cpp

View check run for this annotation

Codecov / codecov/patch

src/cpp/expr2cpp.cpp#L296

Added line #L296 was not covered by tests
}

dest+=")";
dest+=d;
}
else
dest = convert_rec(base_type, c_qualifierst(), "") + " " + dest + d;
dest = convert(base_type) + " " + dest + d;

Check warning on line 303 in src/cpp/expr2cpp.cpp

View check run for this annotation

Codecov / codecov/patch

src/cpp/expr2cpp.cpp#L303

Added line #L303 was not covered by tests

return dest;
}
Expand Down
Loading