Skip to content

Commit 93c14fe

Browse files
tautschnigtautschnig
committed
Clean up ansi_c_convert_typet's interface
The need to invoke read() was only specified in a comment. Make the constructor take care of this. Also, make the constructor initialise all members rather than leaving this to clear(), which is thus no longer necessary. Finally, do not unnecessarily inherit from messaget (there is no is-a relationship).
1 parent d932d6f commit 93c14fe

File tree

4 files changed

+120
-106
lines changed

4 files changed

+120
-106
lines changed

‎src/ansi-c/ansi_c_convert_type.cpp

Lines changed: 48 additions & 48 deletions
Original file line numberDiff line numberDiff line change
@@ -13,18 +13,12 @@ Author: Daniel Kroening, [email protected]
1313

1414
#include <util/c_types.h>
1515
#include <util/config.h>
16+
#include <util/message.h>
1617
#include <util/std_types.h>
1718
#include <util/string_constant.h>
1819

1920
#include "gcc_types.h"
2021

21-
void ansi_c_convert_typet::read(const typet &type)
22-
{
23-
clear();
24-
source_location=type.source_location();
25-
read_rec(type);
26-
}
27-
2822
void ansi_c_convert_typet::read_rec(const typet &type)
2923
{
3024
if(type.id()==ID_merged_type)
@@ -298,6 +292,8 @@ void ansi_c_convert_typet::read_rec(const typet &type)
298292

299293
void ansi_c_convert_typet::write(typet &type)
300294
{
295+
messaget log{message_handler};
296+
301297
type.clear();
302298

303299
// first, do "other"
@@ -314,8 +310,8 @@ void ansi_c_convert_typet::write(typet &type)
314310
gcc_float128_cnt || gcc_float128x_cnt ||
315311
gcc_int128_cnt || bv_cnt)
316312
{
317-
error().source_location=source_location;
318-
error() << "illegal type modifier for defined type" << eom;
313+
log.error().source_location = source_location;
314+
log.error() << "illegal type modifier for defined type" << messaget::eom;
319315
throw 0;
320316
}
321317

@@ -330,8 +326,8 @@ void ansi_c_convert_typet::write(typet &type)
330326

331327
if(other.size()!=1)
332328
{
333-
error().source_location=source_location;
334-
error() << "illegal combination of defined types" << eom;
329+
log.error().source_location = source_location;
330+
log.error() << "illegal combination of defined types" << messaget::eom;
335331
throw 0;
336332
}
337333

@@ -362,9 +358,9 @@ void ansi_c_convert_typet::write(typet &type)
362358
{
363359
if(constructor && destructor)
364360
{
365-
error().source_location=source_location;
366-
error() << "combining constructor and destructor not supported"
367-
<< eom;
361+
log.error().source_location = source_location;
362+
log.error() << "combining constructor and destructor not supported"
363+
<< messaget::eom;
368364
throw 0;
369365
}
370366

@@ -374,9 +370,9 @@ void ansi_c_convert_typet::write(typet &type)
374370

375371
else if(type_p->id()!=ID_empty)
376372
{
377-
error().source_location=source_location;
378-
error() << "constructor and destructor required to be type void, "
379-
<< "found " << type_p->pretty() << eom;
373+
log.error().source_location = source_location;
374+
log.error() << "constructor and destructor required to be type void, "
375+
<< "found " << type_p->pretty() << messaget::eom;
380376
throw 0;
381377
}
382378

@@ -385,9 +381,9 @@ void ansi_c_convert_typet::write(typet &type)
385381
}
386382
else if(constructor || destructor)
387383
{
388-
error().source_location=source_location;
389-
error() << "constructor and destructor required to be type void, "
390-
<< "found " << type.pretty() << eom;
384+
log.error().source_location = source_location;
385+
log.error() << "constructor and destructor required to be type void, "
386+
<< "found " << type.pretty() << messaget::eom;
391387
throw 0;
392388
}
393389
else if(gcc_float16_cnt ||
@@ -400,8 +396,9 @@ void ansi_c_convert_typet::write(typet &type)
400396
gcc_int128_cnt || bv_cnt ||
401397
short_cnt || char_cnt)
402398
{
403-
error().source_location=source_location;
404-
error() << "cannot combine integer type with floating-point type" << eom;
399+
log.error().source_location = source_location;
400+
log.error() << "cannot combine integer type with floating-point type"
401+
<< messaget::eom;
405402
throw 0;
406403
}
407404

@@ -411,8 +408,8 @@ void ansi_c_convert_typet::write(typet &type)
411408
gcc_float64_cnt+gcc_float64x_cnt+
412409
gcc_float128_cnt+gcc_float128x_cnt>=2)
413410
{
414-
error().source_location=source_location;
415-
error() << "conflicting type modifiers" << eom;
411+
log.error().source_location = source_location;
412+
log.error() << "conflicting type modifiers" << messaget::eom;
416413
throw 0;
417414
}
418415

@@ -441,15 +438,16 @@ void ansi_c_convert_typet::write(typet &type)
441438
gcc_int128_cnt|| bv_cnt ||
442439
short_cnt || char_cnt)
443440
{
444-
error().source_location=source_location;
445-
error() << "cannot combine integer type with floating-point type" << eom;
441+
log.error().source_location = source_location;
442+
log.error() << "cannot combine integer type with floating-point type"
443+
<< messaget::eom;
446444
throw 0;
447445
}
448446

449447
if(double_cnt && float_cnt)
450448
{
451-
error().source_location=source_location;
452-
error() << "conflicting type modifiers" << eom;
449+
log.error().source_location = source_location;
450+
log.error() << "conflicting type modifiers" << messaget::eom;
453451
throw 0;
454452
}
455453

@@ -466,15 +464,15 @@ void ansi_c_convert_typet::write(typet &type)
466464
type=long_double_type();
467465
else
468466
{
469-
error().source_location=source_location;
470-
error() << "conflicting type modifiers" << eom;
467+
log.error().source_location = source_location;
468+
log.error() << "conflicting type modifiers" << messaget::eom;
471469
throw 0;
472470
}
473471
}
474472
else
475473
{
476-
error().source_location=source_location;
477-
error() << "illegal type modifier for float" << eom;
474+
log.error().source_location = source_location;
475+
log.error() << "illegal type modifier for float" << messaget::eom;
478476
throw 0;
479477
}
480478
}
@@ -485,8 +483,9 @@ void ansi_c_convert_typet::write(typet &type)
485483
gcc_float128_cnt || bv_cnt || proper_bool_cnt ||
486484
char_cnt || long_cnt)
487485
{
488-
error().source_location=source_location;
489-
error() << "illegal type modifier for C boolean type" << eom;
486+
log.error().source_location = source_location;
487+
log.error() << "illegal type modifier for C boolean type"
488+
<< messaget::eom;
490489
throw 0;
491490
}
492491

@@ -499,8 +498,9 @@ void ansi_c_convert_typet::write(typet &type)
499498
gcc_float128_cnt || bv_cnt ||
500499
char_cnt || long_cnt)
501500
{
502-
error().source_location=source_location;
503-
error() << "illegal type modifier for proper boolean type" << eom;
501+
log.error().source_location = source_location;
502+
log.error() << "illegal type modifier for proper boolean type"
503+
<< messaget::eom;
504504
throw 0;
505505
}
506506

@@ -518,15 +518,15 @@ void ansi_c_convert_typet::write(typet &type)
518518
int8_cnt || int16_cnt || int32_cnt || int64_cnt ||
519519
gcc_float128_cnt || bv_cnt || proper_bool_cnt)
520520
{
521-
error().source_location=source_location;
522-
error() << "illegal type modifier for char type" << eom;
521+
log.error().source_location = source_location;
522+
log.error() << "illegal type modifier for char type" << messaget::eom;
523523
throw 0;
524524
}
525525

526526
if(signed_cnt && unsigned_cnt)
527527
{
528-
error().source_location=source_location;
529-
error() << "conflicting type modifiers" << eom;
528+
log.error().source_location = source_location;
529+
log.error() << "conflicting type modifiers" << messaget::eom;
530530
throw 0;
531531
}
532532
else if(unsigned_cnt)
@@ -544,8 +544,8 @@ void ansi_c_convert_typet::write(typet &type)
544544

545545
if(signed_cnt && unsigned_cnt)
546546
{
547-
error().source_location=source_location;
548-
error() << "conflicting type modifiers" << eom;
547+
log.error().source_location = source_location;
548+
log.error() << "conflicting type modifiers" << messaget::eom;
549549
throw 0;
550550
}
551551
else if(unsigned_cnt)
@@ -557,8 +557,8 @@ void ansi_c_convert_typet::write(typet &type)
557557
{
558558
if(long_cnt || char_cnt || short_cnt || gcc_int128_cnt || bv_cnt)
559559
{
560-
error().source_location=source_location;
561-
error() << "conflicting type modifiers" << eom;
560+
log.error().source_location = source_location;
561+
log.error() << "conflicting type modifiers" << messaget::eom;
562562
throw 0;
563563
}
564564

@@ -614,8 +614,8 @@ void ansi_c_convert_typet::write(typet &type)
614614
{
615615
if(long_cnt || char_cnt)
616616
{
617-
error().source_location=source_location;
618-
error() << "conflicting type modifiers" << eom;
617+
log.error().source_location = source_location;
618+
log.error() << "conflicting type modifiers" << messaget::eom;
619619
throw 0;
620620
}
621621

@@ -647,8 +647,8 @@ void ansi_c_convert_typet::write(typet &type)
647647
}
648648
else
649649
{
650-
error().source_location=source_location;
651-
error() << "illegal type modifier for integer type" << eom;
650+
log.error().source_location = source_location;
651+
log.error() << "illegal type modifier for integer type" << messaget::eom;
652652
throw 0;
653653
}
654654
}

‎src/ansi-c/ansi_c_convert_type.h

Lines changed: 56 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -12,15 +12,16 @@ Author: Daniel Kroening, [email protected]
1212
#ifndef CPROVER_ANSI_C_ANSI_C_CONVERT_TYPE_H
1313
#define CPROVER_ANSI_C_ANSI_C_CONVERT_TYPE_H
1414

15-
#include <list>
16-
17-
#include <util/expr.h>
18-
#include <util/message.h>
15+
#include <util/std_expr.h>
1916

2017
#include "c_qualifiers.h"
2118
#include "c_storage_spec.h"
2219

23-
class ansi_c_convert_typet:public messaget
20+
#include <list>
21+
22+
class message_handlert;
23+
24+
class ansi_c_convert_typet
2425
{
2526
public:
2627
unsigned unsigned_cnt, signed_cnt, char_cnt,
@@ -56,49 +57,68 @@ class ansi_c_convert_typet:public messaget
5657
// qualifiers
5758
c_qualifierst c_qualifiers;
5859

59-
virtual void read(const typet &type);
6060
virtual void write(typet &type);
6161

6262
source_locationt source_location;
6363

6464
std::list<typet> other;
6565

66-
explicit ansi_c_convert_typet(message_handlert &_message_handler):
67-
messaget(_message_handler)
68-
// class members are initialized by calling read()
66+
ansi_c_convert_typet(message_handlert &_message_handler, const typet &type)
67+
: ansi_c_convert_typet(_message_handler)
6968
{
69+
source_location = type.source_location();
70+
read_rec(type);
7071
}
7172

72-
virtual void clear()
73+
protected:
74+
message_handlert &message_handler;
75+
76+
// Default-initialize all members. To be used by classes deriving from this
77+
// one to make sure additional members can be initialized before invoking
78+
// read_rec.
79+
explicit ansi_c_convert_typet(message_handlert &_message_handler)
80+
: unsigned_cnt(0),
81+
signed_cnt(0),
82+
char_cnt(0),
83+
int_cnt(0),
84+
short_cnt(0),
85+
long_cnt(0),
86+
double_cnt(0),
87+
float_cnt(0),
88+
c_bool_cnt(0),
89+
proper_bool_cnt(0),
90+
complex_cnt(0),
91+
int8_cnt(0),
92+
int16_cnt(0),
93+
int32_cnt(0),
94+
int64_cnt(0),
95+
ptr32_cnt(0),
96+
ptr64_cnt(0),
97+
gcc_float16_cnt(0),
98+
gcc_float32_cnt(0),
99+
gcc_float32x_cnt(0),
100+
gcc_float64_cnt(0),
101+
gcc_float64x_cnt(0),
102+
gcc_float128_cnt(0),
103+
gcc_float128x_cnt(0),
104+
gcc_int128_cnt(0),
105+
bv_cnt(0),
106+
floatbv_cnt(0),
107+
fixedbv_cnt(0),
108+
gcc_attribute_mode(static_cast<const typet &>(get_nil_irep())),
109+
packed(false),
110+
aligned(false),
111+
vector_size(nil_exprt{}),
112+
alignment(nil_exprt{}),
113+
bv_width(nil_exprt{}),
114+
fraction_width(nil_exprt{}),
115+
msc_based(nil_exprt{}),
116+
constructor(false),
117+
destructor(false),
118+
message_handler(_message_handler)
73119
{
74-
unsigned_cnt=signed_cnt=char_cnt=int_cnt=short_cnt=
75-
long_cnt=double_cnt=float_cnt=c_bool_cnt=proper_bool_cnt=complex_cnt=
76-
int8_cnt=int16_cnt=int32_cnt=int64_cnt=
77-
ptr32_cnt=ptr64_cnt=
78-
gcc_float16_cnt=
79-
gcc_float32_cnt=gcc_float32x_cnt=
80-
gcc_float64_cnt=gcc_float64x_cnt=
81-
gcc_float128_cnt=gcc_float128x_cnt=
82-
gcc_int128_cnt=bv_cnt=floatbv_cnt=fixedbv_cnt=0;
83-
vector_size.make_nil();
84-
alignment.make_nil();
85-
bv_width.make_nil();
86-
fraction_width.make_nil();
87-
msc_based.make_nil();
88-
gcc_attribute_mode.make_nil();
89-
90-
assigns.clear();
91-
requires.clear();
92-
ensures.clear();
93-
94-
packed=aligned=constructor=destructor=false;
95-
96-
other.clear();
97-
c_storage_spec.clear();
98-
c_qualifiers.clear();
99120
}
100121

101-
protected:
102122
virtual void read_rec(const typet &type);
103123
virtual void build_type_with_subtype(typet &type) const;
104124
virtual void set_attributes(typet &type) const;

‎src/ansi-c/c_typecheck_type.cpp

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -35,9 +35,7 @@ void c_typecheck_baset::typecheck_type(typet &type)
3535
{
3636
// we first convert, and then check
3737
{
38-
ansi_c_convert_typet ansi_c_convert_type(get_message_handler());
39-
40-
ansi_c_convert_type.read(type);
38+
ansi_c_convert_typet ansi_c_convert_type{get_message_handler(), type};
4139
ansi_c_convert_type.write(type);
4240
}
4341

0 commit comments

Comments
 (0)