Skip to content

Clean up ansi_c_convert_typet's interface #5599

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.

Sign up for GitHub

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 2 commits into from
Dec 1, 2022
Merged

Clean up ansi_c_convert_typet's interface #5599

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
957f87c
ansi_c_convert_typet is not a messaget
tautschnig Dec 1, 2022
794f6f7
Clean up ansi_c_convert_typet's interface
tautschnig Dec 1, 2022
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
96 changes: 48 additions & 48 deletions src/ansi-c/ansi_c_convert_type.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,18 +13,12 @@ Author: Daniel Kroening, [email protected]

#include <util/c_types.h>
#include <util/config.h>
#include <util/message.h>
#include <util/std_types.h>
#include <util/string_constant.h>

#include "gcc_types.h"

void ansi_c_convert_typet::read(const typet &type)
{
clear();
source_location=type.source_location();
read_rec(type);
}

void ansi_c_convert_typet::read_rec(const typet &type)
{
if(type.id()==ID_merged_type)
Expand Down Expand Up @@ -286,6 +280,8 @@ void ansi_c_convert_typet::read_rec(const typet &type)

void ansi_c_convert_typet::write(typet &type)
{
messaget log{message_handler};

type.clear();

// first, do "other"
Expand All @@ -302,8 +298,8 @@ void ansi_c_convert_typet::write(typet &type)
gcc_float128_cnt || gcc_float128x_cnt ||
gcc_int128_cnt || bv_cnt)
{
error().source_location=source_location;
error() << "illegal type modifier for defined type" << eom;
log.error().source_location = source_location;
log.error() << "illegal type modifier for defined type" << messaget::eom;
throw 0;
}

Expand All @@ -318,8 +314,8 @@ void ansi_c_convert_typet::write(typet &type)

if(other.size()!=1)
{
error().source_location=source_location;
error() << "illegal combination of defined types" << eom;
log.error().source_location = source_location;
log.error() << "illegal combination of defined types" << messaget::eom;
throw 0;
}

Expand All @@ -342,9 +338,9 @@ void ansi_c_convert_typet::write(typet &type)
{
if(constructor && destructor)
{
error().source_location=source_location;
error() << "combining constructor and destructor not supported"
<< eom;
log.error().source_location = source_location;
log.error() << "combining constructor and destructor not supported"
<< messaget::eom;
throw 0;
}

Expand All @@ -354,9 +350,9 @@ void ansi_c_convert_typet::write(typet &type)

else if(type_p->id()!=ID_empty)
{
error().source_location=source_location;
error() << "constructor and destructor required to be type void, "
<< "found " << type_p->pretty() << eom;
log.error().source_location = source_location;
log.error() << "constructor and destructor required to be type void, "
<< "found " << type_p->pretty() << messaget::eom;
throw 0;
}

Expand All @@ -365,9 +361,9 @@ void ansi_c_convert_typet::write(typet &type)
}
else if(constructor || destructor)
{
error().source_location=source_location;
error() << "constructor and destructor required to be type void, "
<< "found " << type.pretty() << eom;
log.error().source_location = source_location;
log.error() << "constructor and destructor required to be type void, "
<< "found " << type.pretty() << messaget::eom;
throw 0;
}
else if(gcc_float16_cnt ||
Expand All @@ -380,8 +376,9 @@ void ansi_c_convert_typet::write(typet &type)
gcc_int128_cnt || bv_cnt ||
short_cnt || char_cnt)
{
error().source_location=source_location;
error() << "cannot combine integer type with floating-point type" << eom;
log.error().source_location = source_location;
log.error() << "cannot combine integer type with floating-point type"
<< messaget::eom;
throw 0;
}

Expand All @@ -391,8 +388,8 @@ void ansi_c_convert_typet::write(typet &type)
gcc_float64_cnt+gcc_float64x_cnt+
gcc_float128_cnt+gcc_float128x_cnt>=2)
{
error().source_location=source_location;
error() << "conflicting type modifiers" << eom;
log.error().source_location = source_location;
log.error() << "conflicting type modifiers" << messaget::eom;
throw 0;
}

Expand Down Expand Up @@ -421,15 +418,16 @@ void ansi_c_convert_typet::write(typet &type)
gcc_int128_cnt|| bv_cnt ||
short_cnt || char_cnt)
{
error().source_location=source_location;
error() << "cannot combine integer type with floating-point type" << eom;
log.error().source_location = source_location;
log.error() << "cannot combine integer type with floating-point type"
<< messaget::eom;
throw 0;
}

if(double_cnt && float_cnt)
{
error().source_location=source_location;
error() << "conflicting type modifiers" << eom;
log.error().source_location = source_location;
log.error() << "conflicting type modifiers" << messaget::eom;
throw 0;
}

Expand All @@ -446,15 +444,15 @@ void ansi_c_convert_typet::write(typet &type)
type=long_double_type();
else
{
error().source_location=source_location;
error() << "conflicting type modifiers" << eom;
log.error().source_location = source_location;
log.error() << "conflicting type modifiers" << messaget::eom;
throw 0;
}
}
else
{
error().source_location=source_location;
error() << "illegal type modifier for float" << eom;
log.error().source_location = source_location;
log.error() << "illegal type modifier for float" << messaget::eom;
throw 0;
}
}
Expand All @@ -465,8 +463,9 @@ void ansi_c_convert_typet::write(typet &type)
gcc_float128_cnt || bv_cnt || proper_bool_cnt ||
char_cnt || long_cnt)
{
error().source_location=source_location;
error() << "illegal type modifier for C boolean type" << eom;
log.error().source_location = source_location;
log.error() << "illegal type modifier for C boolean type"
<< messaget::eom;
throw 0;
}

Expand All @@ -479,8 +478,9 @@ void ansi_c_convert_typet::write(typet &type)
gcc_float128_cnt || bv_cnt ||
char_cnt || long_cnt)
{
error().source_location=source_location;
error() << "illegal type modifier for proper boolean type" << eom;
log.error().source_location = source_location;
log.error() << "illegal type modifier for proper boolean type"
<< messaget::eom;
throw 0;
}

Expand All @@ -498,15 +498,15 @@ void ansi_c_convert_typet::write(typet &type)
int8_cnt || int16_cnt || int32_cnt || int64_cnt ||
gcc_float128_cnt || bv_cnt || proper_bool_cnt)
{
error().source_location=source_location;
error() << "illegal type modifier for char type" << eom;
log.error().source_location = source_location;
log.error() << "illegal type modifier for char type" << messaget::eom;
throw 0;
}

if(signed_cnt && unsigned_cnt)
{
error().source_location=source_location;
error() << "conflicting type modifiers" << eom;
log.error().source_location = source_location;
log.error() << "conflicting type modifiers" << messaget::eom;
throw 0;
}
else if(unsigned_cnt)
Expand All @@ -524,8 +524,8 @@ void ansi_c_convert_typet::write(typet &type)

if(signed_cnt && unsigned_cnt)
{
error().source_location=source_location;
error() << "conflicting type modifiers" << eom;
log.error().source_location = source_location;
log.error() << "conflicting type modifiers" << messaget::eom;
throw 0;
}
else if(unsigned_cnt)
Expand All @@ -537,8 +537,8 @@ void ansi_c_convert_typet::write(typet &type)
{
if(long_cnt || char_cnt || short_cnt || gcc_int128_cnt || bv_cnt)
{
error().source_location=source_location;
error() << "conflicting type modifiers" << eom;
log.error().source_location = source_location;
log.error() << "conflicting type modifiers" << messaget::eom;
throw 0;
}

Expand Down Expand Up @@ -594,8 +594,8 @@ void ansi_c_convert_typet::write(typet &type)
{
if(long_cnt || char_cnt)
{
error().source_location=source_location;
error() << "conflicting type modifiers" << eom;
log.error().source_location = source_location;
log.error() << "conflicting type modifiers" << messaget::eom;
throw 0;
}

Expand Down Expand Up @@ -627,8 +627,8 @@ void ansi_c_convert_typet::write(typet &type)
}
else
{
error().source_location=source_location;
error() << "illegal type modifier for integer type" << eom;
log.error().source_location = source_location;
log.error() << "illegal type modifier for integer type" << messaget::eom;
throw 0;
}
}
Expand Down
92 changes: 56 additions & 36 deletions src/ansi-c/ansi_c_convert_type.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,15 +12,16 @@ Author: Daniel Kroening, [email protected]
#ifndef CPROVER_ANSI_C_ANSI_C_CONVERT_TYPE_H
#define CPROVER_ANSI_C_ANSI_C_CONVERT_TYPE_H

#include <list>

#include <util/expr.h>
#include <util/message.h>
#include <util/std_expr.h>

#include "c_qualifiers.h"
#include "c_storage_spec.h"

class ansi_c_convert_typet:public messaget
#include <list>

class message_handlert;

class ansi_c_convert_typet
{
public:
unsigned unsigned_cnt, signed_cnt, char_cnt,
Expand Down Expand Up @@ -55,49 +56,68 @@ class ansi_c_convert_typet:public messaget
// qualifiers
c_qualifierst c_qualifiers;

virtual void read(const typet &type);
virtual void write(typet &type);

source_locationt source_location;

std::list<typet> other;

explicit ansi_c_convert_typet(message_handlert &_message_handler):
messaget(_message_handler)
// class members are initialized by calling read()
ansi_c_convert_typet(message_handlert &_message_handler, const typet &type)
: ansi_c_convert_typet(_message_handler)
{
source_location = type.source_location();
read_rec(type);
}

virtual void clear()
protected:
message_handlert &message_handler;

// Default-initialize all members. To be used by classes deriving from this
// one to make sure additional members can be initialized before invoking
// read_rec.
explicit ansi_c_convert_typet(message_handlert &_message_handler)
: unsigned_cnt(0),
signed_cnt(0),
char_cnt(0),
int_cnt(0),
short_cnt(0),
long_cnt(0),
double_cnt(0),
float_cnt(0),
c_bool_cnt(0),
proper_bool_cnt(0),
complex_cnt(0),
int8_cnt(0),
int16_cnt(0),
int32_cnt(0),
int64_cnt(0),
ptr32_cnt(0),
ptr64_cnt(0),
gcc_float16_cnt(0),
gcc_float32_cnt(0),
gcc_float32x_cnt(0),
gcc_float64_cnt(0),
gcc_float64x_cnt(0),
gcc_float128_cnt(0),
gcc_float128x_cnt(0),
gcc_int128_cnt(0),
bv_cnt(0),
floatbv_cnt(0),
fixedbv_cnt(0),
gcc_attribute_mode(static_cast<const typet &>(get_nil_irep())),
packed(false),
aligned(false),
vector_size(nil_exprt{}),
alignment(nil_exprt{}),
bv_width(nil_exprt{}),
fraction_width(nil_exprt{}),
msc_based(nil_exprt{}),
constructor(false),
destructor(false),
message_handler(_message_handler)
{
unsigned_cnt=signed_cnt=char_cnt=int_cnt=short_cnt=
long_cnt=double_cnt=float_cnt=c_bool_cnt=proper_bool_cnt=complex_cnt=
int8_cnt=int16_cnt=int32_cnt=int64_cnt=
ptr32_cnt=ptr64_cnt=
gcc_float16_cnt=
gcc_float32_cnt=gcc_float32x_cnt=
gcc_float64_cnt=gcc_float64x_cnt=
gcc_float128_cnt=gcc_float128x_cnt=
gcc_int128_cnt=bv_cnt=floatbv_cnt=fixedbv_cnt=0;
vector_size.make_nil();
alignment.make_nil();
bv_width.make_nil();
fraction_width.make_nil();
msc_based.make_nil();
gcc_attribute_mode.make_nil();

assigns.clear();
requires.clear();
ensures.clear();

packed=aligned=constructor=destructor=false;

other.clear();
c_storage_spec.clear();
c_qualifiers.clear();
}

protected:
virtual void read_rec(const typet &type);
virtual void build_type_with_subtype(typet &type) const;
virtual void set_attributes(typet &type) const;
Expand Down
4 changes: 1 addition & 3 deletions src/ansi-c/c_typecheck_type.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,9 +35,7 @@ void c_typecheck_baset::typecheck_type(typet &type)
{
// we first convert, and then check
{
ansi_c_convert_typet ansi_c_convert_type(get_message_handler());

ansi_c_convert_type.read(type);
ansi_c_convert_typet ansi_c_convert_type{get_message_handler(), type};
ansi_c_convert_type.write(type);
}

Expand Down
Loading