Skip to content

Commit 33de0af

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 99f1a2e commit 33de0af

File tree

4 files changed

+121
-102
lines changed

4 files changed

+121
-102
lines changed

‎src/ansi-c/ansi_c_convert_type.cpp

Lines changed: 48 additions & 48 deletions
Original file line numberDiff line numberDiff line change
@@ -14,20 +14,14 @@ Author: Daniel Kroening, kroening@kroening.com
1414
#include <util/arith_tools.h>
1515
#include <util/c_types.h>
1616
#include <util/config.h>
17+
#include <util/message.h>
1718
#include <util/namespace.h>
1819
#include <util/simplify_expr.h>
1920
#include <util/std_types.h>
2021
#include <util/string_constant.h>
2122

2223
#include "gcc_types.h"
2324

24-
void ansi_c_convert_typet::read(const typet &type)
25-
{
26-
clear();
27-
source_location=type.source_location();
28-
read_rec(type);
29-
}
30-
3125
void ansi_c_convert_typet::read_rec(const typet &type)
3226
{
3327
if(type.id()==ID_merged_type)
@@ -269,6 +263,8 @@ void ansi_c_convert_typet::read_rec(const typet &type)
269263

270264
void ansi_c_convert_typet::write(typet &type)
271265
{
266+
messaget log{message_handler};
267+
272268
type.clear();
273269

274270
// first, do "other"
@@ -285,8 +281,8 @@ void ansi_c_convert_typet::write(typet &type)
285281
gcc_float128_cnt || gcc_float128x_cnt ||
286282
gcc_int128_cnt || bv_cnt)
287283
{
288-
error().source_location=source_location;
289-
error() << "illegal type modifier for defined type" << eom;
284+
log.error().source_location = source_location;
285+
log.error() << "illegal type modifier for defined type" << messaget::eom;
290286
throw 0;
291287
}
292288

@@ -301,8 +297,8 @@ void ansi_c_convert_typet::write(typet &type)
301297

302298
if(other.size()!=1)
303299
{
304-
error().source_location=source_location;
305-
error() << "illegal combination of defined types" << eom;
300+
log.error().source_location = source_location;
301+
log.error() << "illegal combination of defined types" << messaget::eom;
306302
throw 0;
307303
}
308304

@@ -322,9 +318,9 @@ void ansi_c_convert_typet::write(typet &type)
322318
{
323319
if(constructor && destructor)
324320
{
325-
error().source_location=source_location;
326-
error() << "combining constructor and destructor not supported"
327-
<< eom;
321+
log.error().source_location = source_location;
322+
log.error() << "combining constructor and destructor not supported"
323+
<< messaget::eom;
328324
throw 0;
329325
}
330326

@@ -334,9 +330,9 @@ void ansi_c_convert_typet::write(typet &type)
334330

335331
else if(type_p->id()!=ID_empty)
336332
{
337-
error().source_location=source_location;
338-
error() << "constructor and destructor required to be type void, "
339-
<< "found " << type_p->pretty() << eom;
333+
log.error().source_location = source_location;
334+
log.error() << "constructor and destructor required to be type void, "
335+
<< "found " << type_p->pretty() << messaget::eom;
340336
throw 0;
341337
}
342338

@@ -345,9 +341,9 @@ void ansi_c_convert_typet::write(typet &type)
345341
}
346342
else if(constructor || destructor)
347343
{
348-
error().source_location=source_location;
349-
error() << "constructor and destructor required to be type void, "
350-
<< "found " << type.pretty() << eom;
344+
log.error().source_location = source_location;
345+
log.error() << "constructor and destructor required to be type void, "
346+
<< "found " << type.pretty() << messaget::eom;
351347
throw 0;
352348
}
353349
else if(gcc_float16_cnt ||
@@ -360,8 +356,9 @@ void ansi_c_convert_typet::write(typet &type)
360356
gcc_int128_cnt || bv_cnt ||
361357
short_cnt || char_cnt)
362358
{
363-
error().source_location=source_location;
364-
error() << "cannot combine integer type with floating-point type" << eom;
359+
log.error().source_location = source_location;
360+
log.error() << "cannot combine integer type with floating-point type"
361+
<< messaget::eom;
365362
throw 0;
366363
}
367364

@@ -371,8 +368,8 @@ void ansi_c_convert_typet::write(typet &type)
371368
gcc_float64_cnt+gcc_float64x_cnt+
372369
gcc_float128_cnt+gcc_float128x_cnt>=2)
373370
{
374-
error().source_location=source_location;
375-
error() << "conflicting type modifiers" << eom;
371+
log.error().source_location = source_location;
372+
log.error() << "conflicting type modifiers" << messaget::eom;
376373
throw 0;
377374
}
378375

@@ -401,15 +398,16 @@ void ansi_c_convert_typet::write(typet &type)
401398
gcc_int128_cnt|| bv_cnt ||
402399
short_cnt || char_cnt)
403400
{
404-
error().source_location=source_location;
405-
error() << "cannot combine integer type with floating-point type" << eom;
401+
log.error().source_location = source_location;
402+
log.error() << "cannot combine integer type with floating-point type"
403+
<< messaget::eom;
406404
throw 0;
407405
}
408406

409407
if(double_cnt && float_cnt)
410408
{
411-
error().source_location=source_location;
412-
error() << "conflicting type modifiers" << eom;
409+
log.error().source_location = source_location;
410+
log.error() << "conflicting type modifiers" << messaget::eom;
413411
throw 0;
414412
}
415413

@@ -426,15 +424,15 @@ void ansi_c_convert_typet::write(typet &type)
426424
type=long_double_type();
427425
else
428426
{
429-
error().source_location=source_location;
430-
error() << "conflicting type modifiers" << eom;
427+
log.error().source_location = source_location;
428+
log.error() << "conflicting type modifiers" << messaget::eom;
431429
throw 0;
432430
}
433431
}
434432
else
435433
{
436-
error().source_location=source_location;
437-
error() << "illegal type modifier for float" << eom;
434+
log.error().source_location = source_location;
435+
log.error() << "illegal type modifier for float" << messaget::eom;
438436
throw 0;
439437
}
440438
}
@@ -445,8 +443,9 @@ void ansi_c_convert_typet::write(typet &type)
445443
gcc_float128_cnt || bv_cnt || proper_bool_cnt ||
446444
char_cnt || long_cnt)
447445
{
448-
error().source_location=source_location;
449-
error() << "illegal type modifier for C boolean type" << eom;
446+
log.error().source_location = source_location;
447+
log.error() << "illegal type modifier for C boolean type"
448+
<< messaget::eom;
450449
throw 0;
451450
}
452451

@@ -459,8 +458,9 @@ void ansi_c_convert_typet::write(typet &type)
459458
gcc_float128_cnt || bv_cnt ||
460459
char_cnt || long_cnt)
461460
{
462-
error().source_location=source_location;
463-
error() << "illegal type modifier for proper boolean type" << eom;
461+
log.error().source_location = source_location;
462+
log.error() << "illegal type modifier for proper boolean type"
463+
<< messaget::eom;
464464
throw 0;
465465
}
466466

@@ -478,15 +478,15 @@ void ansi_c_convert_typet::write(typet &type)
478478
int8_cnt || int16_cnt || int32_cnt || int64_cnt ||
479479
gcc_float128_cnt || bv_cnt || proper_bool_cnt)
480480
{
481-
error().source_location=source_location;
482-
error() << "illegal type modifier for char type" << eom;
481+
log.error().source_location = source_location;
482+
log.error() << "illegal type modifier for char type" << messaget::eom;
483483
throw 0;
484484
}
485485

486486
if(signed_cnt && unsigned_cnt)
487487
{
488-
error().source_location=source_location;
489-
error() << "conflicting type modifiers" << eom;
488+
log.error().source_location = source_location;
489+
log.error() << "conflicting type modifiers" << messaget::eom;
490490
throw 0;
491491
}
492492
else if(unsigned_cnt)
@@ -504,8 +504,8 @@ void ansi_c_convert_typet::write(typet &type)
504504

505505
if(signed_cnt && unsigned_cnt)
506506
{
507-
error().source_location=source_location;
508-
error() << "conflicting type modifiers" << eom;
507+
log.error().source_location = source_location;
508+
log.error() << "conflicting type modifiers" << messaget::eom;
509509
throw 0;
510510
}
511511
else if(unsigned_cnt)
@@ -517,8 +517,8 @@ void ansi_c_convert_typet::write(typet &type)
517517
{
518518
if(long_cnt || char_cnt || short_cnt || gcc_int128_cnt || bv_cnt)
519519
{
520-
error().source_location=source_location;
521-
error() << "conflicting type modifiers" << eom;
520+
log.error().source_location = source_location;
521+
log.error() << "conflicting type modifiers" << messaget::eom;
522522
throw 0;
523523
}
524524

@@ -574,8 +574,8 @@ void ansi_c_convert_typet::write(typet &type)
574574
{
575575
if(long_cnt || char_cnt)
576576
{
577-
error().source_location=source_location;
578-
error() << "conflicting type modifiers" << eom;
577+
log.error().source_location = source_location;
578+
log.error() << "conflicting type modifiers" << messaget::eom;
579579
throw 0;
580580
}
581581

@@ -607,8 +607,8 @@ void ansi_c_convert_typet::write(typet &type)
607607
}
608608
else
609609
{
610-
error().source_location=source_location;
611-
error() << "illegal type modifier for integer type" << eom;
610+
log.error().source_location = source_location;
611+
log.error() << "illegal type modifier for integer type" << messaget::eom;
612612
throw 0;
613613
}
614614
}

‎src/ansi-c/ansi_c_convert_type.h

Lines changed: 57 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -14,12 +14,14 @@ Author: Daniel Kroening, kroening@kroening.com
1414

1515
#include <list>
1616

17-
#include <util/message.h>
17+
#include <util/std_expr.h>
1818

1919
#include "c_qualifiers.h"
2020
#include "c_storage_spec.h"
2121

22-
class ansi_c_convert_typet:public messaget
22+
class message_handlert;
23+
24+
class ansi_c_convert_typet
2325
{
2426
public:
2527
unsigned unsigned_cnt, signed_cnt, char_cnt,
@@ -54,49 +56,71 @@ class ansi_c_convert_typet:public messaget
5456
// qualifiers
5557
c_qualifierst c_qualifiers;
5658

57-
virtual void read(const typet &type);
5859
virtual void write(typet &type);
5960

6061
source_locationt source_location;
6162

6263
std::list<typet> other;
6364

64-
explicit ansi_c_convert_typet(message_handlert &_message_handler):
65-
messaget(_message_handler)
66-
// class members are initialized by calling read()
65+
ansi_c_convert_typet(message_handlert &_message_handler, const typet &type)
66+
: ansi_c_convert_typet(_message_handler)
6767
{
68+
source_location = type.source_location();
69+
read_rec(type);
6870
}
6971

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

99-
protected:
100124
virtual void read_rec(const typet &type);
101125
virtual void build_type_with_subtype(typet &type) const;
102126
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
@@ -33,9 +33,7 @@ void c_typecheck_baset::typecheck_type(typet &type)
3333
{
3434
// we first convert, and then check
3535
{
36-
ansi_c_convert_typet ansi_c_convert_type(get_message_handler());
37-
38-
ansi_c_convert_type.read(type);
36+
ansi_c_convert_typet ansi_c_convert_type{get_message_handler(), type};
3937
ansi_c_convert_type.write(type);
4038
}
4139

0 commit comments

Comments
 (0)