Skip to content
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 @@ 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()
Expand All @@ -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;
Expand All @@ -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);

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

Expand Down Expand Up @@ -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);
}
}

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

Expand All @@ -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(
Expand All @@ -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)
{
Expand Down Expand Up @@ -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());
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 @@ class expr2cppt:public expr2ct

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_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);
Expand Down Expand Up @@ -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+="(";
Expand All @@ -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;
}
Expand Down