Skip to content

Commit 35e31f7

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 0a09814 commit 35e31f7

File tree

4 files changed

+119
-106
lines changed

4 files changed

+119
-106
lines changed

‎src/ansi-c/ansi_c_convert_type.cpp

Lines changed: 47 additions & 48 deletions
Original file line numberDiff line numberDiff line change
@@ -19,13 +19,6 @@ Author: Daniel Kroening, kroening@kroening.com
1919

2020
#include "gcc_types.h"
2121

22-
void ansi_c_convert_typet::read(const typet &type)
23-
{
24-
clear();
25-
source_location=type.source_location();
26-
read_rec(type);
27-
}
28-
2922
void ansi_c_convert_typet::read_rec(const typet &type)
3023
{
3124
if(type.id()==ID_merged_type)
@@ -299,6 +292,8 @@ void ansi_c_convert_typet::read_rec(const typet &type)
299292

300293
void ansi_c_convert_typet::write(typet &type)
301294
{
295+
messaget log{message_handler};
296+
302297
type.clear();
303298

304299
// first, do "other"
@@ -315,8 +310,8 @@ void ansi_c_convert_typet::write(typet &type)
315310
gcc_float128_cnt || gcc_float128x_cnt ||
316311
gcc_int128_cnt || bv_cnt)
317312
{
318-
error().source_location=source_location;
319-
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;
320315
throw 0;
321316
}
322317

@@ -331,8 +326,8 @@ void ansi_c_convert_typet::write(typet &type)
331326

332327
if(other.size()!=1)
333328
{
334-
error().source_location=source_location;
335-
error() << "illegal combination of defined types" << eom;
329+
log.error().source_location = source_location;
330+
log.error() << "illegal combination of defined types" << messaget::eom;
336331
throw 0;
337332
}
338333

@@ -363,9 +358,9 @@ void ansi_c_convert_typet::write(typet &type)
363358
{
364359
if(constructor && destructor)
365360
{
366-
error().source_location=source_location;
367-
error() << "combining constructor and destructor not supported"
368-
<< eom;
361+
log.error().source_location = source_location;
362+
log.error() << "combining constructor and destructor not supported"
363+
<< messaget::eom;
369364
throw 0;
370365
}
371366

@@ -375,9 +370,9 @@ void ansi_c_convert_typet::write(typet &type)
375370

376371
else if(type_p->id()!=ID_empty)
377372
{
378-
error().source_location=source_location;
379-
error() << "constructor and destructor required to be type void, "
380-
<< "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;
381376
throw 0;
382377
}
383378

@@ -386,9 +381,9 @@ void ansi_c_convert_typet::write(typet &type)
386381
}
387382
else if(constructor || destructor)
388383
{
389-
error().source_location=source_location;
390-
error() << "constructor and destructor required to be type void, "
391-
<< "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;
392387
throw 0;
393388
}
394389
else if(gcc_float16_cnt ||
@@ -401,8 +396,9 @@ void ansi_c_convert_typet::write(typet &type)
401396
gcc_int128_cnt || bv_cnt ||
402397
short_cnt || char_cnt)
403398
{
404-
error().source_location=source_location;
405-
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;
406402
throw 0;
407403
}
408404

@@ -412,8 +408,8 @@ void ansi_c_convert_typet::write(typet &type)
412408
gcc_float64_cnt+gcc_float64x_cnt+
413409
gcc_float128_cnt+gcc_float128x_cnt>=2)
414410
{
415-
error().source_location=source_location;
416-
error() << "conflicting type modifiers" << eom;
411+
log.error().source_location = source_location;
412+
log.error() << "conflicting type modifiers" << messaget::eom;
417413
throw 0;
418414
}
419415

@@ -442,15 +438,16 @@ void ansi_c_convert_typet::write(typet &type)
442438
gcc_int128_cnt|| bv_cnt ||
443439
short_cnt || char_cnt)
444440
{
445-
error().source_location=source_location;
446-
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;
447444
throw 0;
448445
}
449446

450447
if(double_cnt && float_cnt)
451448
{
452-
error().source_location=source_location;
453-
error() << "conflicting type modifiers" << eom;
449+
log.error().source_location = source_location;
450+
log.error() << "conflicting type modifiers" << messaget::eom;
454451
throw 0;
455452
}
456453

@@ -467,15 +464,15 @@ void ansi_c_convert_typet::write(typet &type)
467464
type=long_double_type();
468465
else
469466
{
470-
error().source_location=source_location;
471-
error() << "conflicting type modifiers" << eom;
467+
log.error().source_location = source_location;
468+
log.error() << "conflicting type modifiers" << messaget::eom;
472469
throw 0;
473470
}
474471
}
475472
else
476473
{
477-
error().source_location=source_location;
478-
error() << "illegal type modifier for float" << eom;
474+
log.error().source_location = source_location;
475+
log.error() << "illegal type modifier for float" << messaget::eom;
479476
throw 0;
480477
}
481478
}
@@ -486,8 +483,9 @@ void ansi_c_convert_typet::write(typet &type)
486483
gcc_float128_cnt || bv_cnt || proper_bool_cnt ||
487484
char_cnt || long_cnt)
488485
{
489-
error().source_location=source_location;
490-
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;
491489
throw 0;
492490
}
493491

@@ -500,8 +498,9 @@ void ansi_c_convert_typet::write(typet &type)
500498
gcc_float128_cnt || bv_cnt ||
501499
char_cnt || long_cnt)
502500
{
503-
error().source_location=source_location;
504-
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;
505504
throw 0;
506505
}
507506

@@ -519,15 +518,15 @@ void ansi_c_convert_typet::write(typet &type)
519518
int8_cnt || int16_cnt || int32_cnt || int64_cnt ||
520519
gcc_float128_cnt || bv_cnt || proper_bool_cnt)
521520
{
522-
error().source_location=source_location;
523-
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;
524523
throw 0;
525524
}
526525

527526
if(signed_cnt && unsigned_cnt)
528527
{
529-
error().source_location=source_location;
530-
error() << "conflicting type modifiers" << eom;
528+
log.error().source_location = source_location;
529+
log.error() << "conflicting type modifiers" << messaget::eom;
531530
throw 0;
532531
}
533532
else if(unsigned_cnt)
@@ -545,8 +544,8 @@ void ansi_c_convert_typet::write(typet &type)
545544

546545
if(signed_cnt && unsigned_cnt)
547546
{
548-
error().source_location=source_location;
549-
error() << "conflicting type modifiers" << eom;
547+
log.error().source_location = source_location;
548+
log.error() << "conflicting type modifiers" << messaget::eom;
550549
throw 0;
551550
}
552551
else if(unsigned_cnt)
@@ -558,8 +557,8 @@ void ansi_c_convert_typet::write(typet &type)
558557
{
559558
if(long_cnt || char_cnt || short_cnt || gcc_int128_cnt || bv_cnt)
560559
{
561-
error().source_location=source_location;
562-
error() << "conflicting type modifiers" << eom;
560+
log.error().source_location = source_location;
561+
log.error() << "conflicting type modifiers" << messaget::eom;
563562
throw 0;
564563
}
565564

@@ -615,8 +614,8 @@ void ansi_c_convert_typet::write(typet &type)
615614
{
616615
if(long_cnt || char_cnt)
617616
{
618-
error().source_location=source_location;
619-
error() << "conflicting type modifiers" << eom;
617+
log.error().source_location = source_location;
618+
log.error() << "conflicting type modifiers" << messaget::eom;
620619
throw 0;
621620
}
622621

@@ -648,8 +647,8 @@ void ansi_c_convert_typet::write(typet &type)
648647
}
649648
else
650649
{
651-
error().source_location=source_location;
652-
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;
653652
throw 0;
654653
}
655654
}

‎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, kroening@kroening.com
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
@@ -36,9 +36,7 @@ void c_typecheck_baset::typecheck_type(typet &type)
3636
{
3737
// we first convert, and then check
3838
{
39-
ansi_c_convert_typet ansi_c_convert_type(get_message_handler());
40-
41-
ansi_c_convert_type.read(type);
39+
ansi_c_convert_typet ansi_c_convert_type{get_message_handler(), type};
4240
ansi_c_convert_type.write(type);
4341
}
4442

0 commit comments

Comments
 (0)