Skip to content

Commit 2301de3

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 247380f commit 2301de3

File tree

5 files changed

+124
-106
lines changed

5 files changed

+124
-106
lines changed

‎scripts/expected_doxygen_warnings.txt

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,11 +5,11 @@ warning: Included by graph for 'c_types.h' not generated, too many nodes (128),
55
warning: Included by graph for 'config.h' not generated, too many nodes (78), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
66
warning: Included by graph for 'invariant.h' not generated, too many nodes (172), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
77
warning: Included by graph for 'irep.h' not generated, too many nodes (80), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
8-
warning: Included by graph for 'message.h' not generated, too many nodes (97), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
8+
warning: Included by graph for 'message.h' not generated, too many nodes (98), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
99
warning: Included by graph for 'namespace.h' not generated, too many nodes (88), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
1010
warning: Included by graph for 'pointer_expr.h' not generated, too many nodes (120), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
1111
warning: Included by graph for 'prefix.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
1212
warning: Included by graph for 'simplify_expr.h' not generated, too many nodes (67), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
1313
warning: Included by graph for 'std_code.h' not generated, too many nodes (71), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
14-
warning: Included by graph for 'std_expr.h' not generated, too many nodes (178), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
14+
warning: Included by graph for 'std_expr.h' not generated, too many nodes (179), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
1515
warning: Included by graph for 'symbol_table.h' not generated, too many nodes (71), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.

‎src/ansi-c/ansi_c_convert_type.cpp

Lines changed: 49 additions & 49 deletions
Original file line numberDiff line numberDiff line change
@@ -13,18 +13,12 @@ Author: Daniel Kroening, kroening@kroening.com
1313

1414
#include <util/c_types.h>
1515
#include <util/config.h>
16-
#include <util/std_types.h>
16+
#include <util/message.h>
17+
#include <util/pointer_expr.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)
@@ -266,6 +260,8 @@ void ansi_c_convert_typet::read_rec(const typet &type)
266260

267261
void ansi_c_convert_typet::write(typet &type)
268262
{
263+
messaget log{message_handler};
264+
269265
type.clear();
270266

271267
// first, do "other"
@@ -282,8 +278,8 @@ void ansi_c_convert_typet::write(typet &type)
282278
gcc_float128_cnt || gcc_float128x_cnt ||
283279
gcc_int128_cnt || bv_cnt)
284280
{
285-
error().source_location=source_location;
286-
error() << "illegal type modifier for defined type" << eom;
281+
log.error().source_location = source_location;
282+
log.error() << "illegal type modifier for defined type" << messaget::eom;
287283
throw 0;
288284
}
289285

@@ -298,8 +294,8 @@ void ansi_c_convert_typet::write(typet &type)
298294

299295
if(other.size()!=1)
300296
{
301-
error().source_location=source_location;
302-
error() << "illegal combination of defined types" << eom;
297+
log.error().source_location = source_location;
298+
log.error() << "illegal combination of defined types" << messaget::eom;
303299
throw 0;
304300
}
305301

@@ -319,9 +315,9 @@ void ansi_c_convert_typet::write(typet &type)
319315
{
320316
if(constructor && destructor)
321317
{
322-
error().source_location=source_location;
323-
error() << "combining constructor and destructor not supported"
324-
<< eom;
318+
log.error().source_location = source_location;
319+
log.error() << "combining constructor and destructor not supported"
320+
<< messaget::eom;
325321
throw 0;
326322
}
327323

@@ -331,9 +327,9 @@ void ansi_c_convert_typet::write(typet &type)
331327

332328
else if(type_p->id()!=ID_empty)
333329
{
334-
error().source_location=source_location;
335-
error() << "constructor and destructor required to be type void, "
336-
<< "found " << type_p->pretty() << eom;
330+
log.error().source_location = source_location;
331+
log.error() << "constructor and destructor required to be type void, "
332+
<< "found " << type_p->pretty() << messaget::eom;
337333
throw 0;
338334
}
339335

@@ -342,9 +338,9 @@ void ansi_c_convert_typet::write(typet &type)
342338
}
343339
else if(constructor || destructor)
344340
{
345-
error().source_location=source_location;
346-
error() << "constructor and destructor required to be type void, "
347-
<< "found " << type.pretty() << eom;
341+
log.error().source_location = source_location;
342+
log.error() << "constructor and destructor required to be type void, "
343+
<< "found " << type.pretty() << messaget::eom;
348344
throw 0;
349345
}
350346
else if(gcc_float16_cnt ||
@@ -357,8 +353,9 @@ void ansi_c_convert_typet::write(typet &type)
357353
gcc_int128_cnt || bv_cnt ||
358354
short_cnt || char_cnt)
359355
{
360-
error().source_location=source_location;
361-
error() << "cannot combine integer type with floating-point type" << eom;
356+
log.error().source_location = source_location;
357+
log.error() << "cannot combine integer type with floating-point type"
358+
<< messaget::eom;
362359
throw 0;
363360
}
364361

@@ -368,8 +365,8 @@ void ansi_c_convert_typet::write(typet &type)
368365
gcc_float64_cnt+gcc_float64x_cnt+
369366
gcc_float128_cnt+gcc_float128x_cnt>=2)
370367
{
371-
error().source_location=source_location;
372-
error() << "conflicting type modifiers" << eom;
368+
log.error().source_location = source_location;
369+
log.error() << "conflicting type modifiers" << messaget::eom;
373370
throw 0;
374371
}
375372

@@ -398,15 +395,16 @@ void ansi_c_convert_typet::write(typet &type)
398395
gcc_int128_cnt|| bv_cnt ||
399396
short_cnt || char_cnt)
400397
{
401-
error().source_location=source_location;
402-
error() << "cannot combine integer type with floating-point type" << eom;
398+
log.error().source_location = source_location;
399+
log.error() << "cannot combine integer type with floating-point type"
400+
<< messaget::eom;
403401
throw 0;
404402
}
405403

406404
if(double_cnt && float_cnt)
407405
{
408-
error().source_location=source_location;
409-
error() << "conflicting type modifiers" << eom;
406+
log.error().source_location = source_location;
407+
log.error() << "conflicting type modifiers" << messaget::eom;
410408
throw 0;
411409
}
412410

@@ -423,15 +421,15 @@ void ansi_c_convert_typet::write(typet &type)
423421
type=long_double_type();
424422
else
425423
{
426-
error().source_location=source_location;
427-
error() << "conflicting type modifiers" << eom;
424+
log.error().source_location = source_location;
425+
log.error() << "conflicting type modifiers" << messaget::eom;
428426
throw 0;
429427
}
430428
}
431429
else
432430
{
433-
error().source_location=source_location;
434-
error() << "illegal type modifier for float" << eom;
431+
log.error().source_location = source_location;
432+
log.error() << "illegal type modifier for float" << messaget::eom;
435433
throw 0;
436434
}
437435
}
@@ -442,8 +440,9 @@ void ansi_c_convert_typet::write(typet &type)
442440
gcc_float128_cnt || bv_cnt || proper_bool_cnt ||
443441
char_cnt || long_cnt)
444442
{
445-
error().source_location=source_location;
446-
error() << "illegal type modifier for C boolean type" << eom;
443+
log.error().source_location = source_location;
444+
log.error() << "illegal type modifier for C boolean type"
445+
<< messaget::eom;
447446
throw 0;
448447
}
449448

@@ -456,8 +455,9 @@ void ansi_c_convert_typet::write(typet &type)
456455
gcc_float128_cnt || bv_cnt ||
457456
char_cnt || long_cnt)
458457
{
459-
error().source_location=source_location;
460-
error() << "illegal type modifier for proper boolean type" << eom;
458+
log.error().source_location = source_location;
459+
log.error() << "illegal type modifier for proper boolean type"
460+
<< messaget::eom;
461461
throw 0;
462462
}
463463

@@ -475,15 +475,15 @@ void ansi_c_convert_typet::write(typet &type)
475475
int8_cnt || int16_cnt || int32_cnt || int64_cnt ||
476476
gcc_float128_cnt || bv_cnt || proper_bool_cnt)
477477
{
478-
error().source_location=source_location;
479-
error() << "illegal type modifier for char type" << eom;
478+
log.error().source_location = source_location;
479+
log.error() << "illegal type modifier for char type" << messaget::eom;
480480
throw 0;
481481
}
482482

483483
if(signed_cnt && unsigned_cnt)
484484
{
485-
error().source_location=source_location;
486-
error() << "conflicting type modifiers" << eom;
485+
log.error().source_location = source_location;
486+
log.error() << "conflicting type modifiers" << messaget::eom;
487487
throw 0;
488488
}
489489
else if(unsigned_cnt)
@@ -501,8 +501,8 @@ void ansi_c_convert_typet::write(typet &type)
501501

502502
if(signed_cnt && unsigned_cnt)
503503
{
504-
error().source_location=source_location;
505-
error() << "conflicting type modifiers" << eom;
504+
log.error().source_location = source_location;
505+
log.error() << "conflicting type modifiers" << messaget::eom;
506506
throw 0;
507507
}
508508
else if(unsigned_cnt)
@@ -514,8 +514,8 @@ void ansi_c_convert_typet::write(typet &type)
514514
{
515515
if(long_cnt || char_cnt || short_cnt || gcc_int128_cnt || bv_cnt)
516516
{
517-
error().source_location=source_location;
518-
error() << "conflicting type modifiers" << eom;
517+
log.error().source_location = source_location;
518+
log.error() << "conflicting type modifiers" << messaget::eom;
519519
throw 0;
520520
}
521521

@@ -571,8 +571,8 @@ void ansi_c_convert_typet::write(typet &type)
571571
{
572572
if(long_cnt || char_cnt)
573573
{
574-
error().source_location=source_location;
575-
error() << "conflicting type modifiers" << eom;
574+
log.error().source_location = source_location;
575+
log.error() << "conflicting type modifiers" << messaget::eom;
576576
throw 0;
577577
}
578578

@@ -604,8 +604,8 @@ void ansi_c_convert_typet::write(typet &type)
604604
}
605605
else
606606
{
607-
error().source_location=source_location;
608-
error() << "illegal type modifier for integer type" << eom;
607+
log.error().source_location = source_location;
608+
log.error() << "illegal type modifier for integer type" << messaget::eom;
609609
throw 0;
610610
}
611611
}

‎src/ansi-c/ansi_c_convert_type.h

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

1515
#include <list>
1616

17-
#include <util/expr.h>
18-
#include <util/message.h>
17+
#include <util/std_expr.h>
1918

2019
#include "c_qualifiers.h"
2120
#include "c_storage_spec.h"
2221

23-
class ansi_c_convert_typet:public messaget
22+
class message_handlert;
23+
24+
class ansi_c_convert_typet
2425
{
2526
public:
2627
unsigned unsigned_cnt, signed_cnt, char_cnt,
@@ -55,49 +56,71 @@ class ansi_c_convert_typet:public messaget
5556
// qualifiers
5657
c_qualifierst c_qualifiers;
5758

58-
virtual void read(const typet &type);
5959
virtual void write(typet &type);
6060

6161
source_locationt source_location;
6262

6363
std::list<typet> other;
6464

65-
explicit ansi_c_convert_typet(message_handlert &_message_handler):
66-
messaget(_message_handler)
67-
// 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)
6867
{
68+
source_location = type.source_location();
69+
read_rec(type);
6970
}
7071

71-
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+
constructor(false),
116+
destructor(false),
117+
requires(nil_exprt{}),
118+
assigns(nil_exprt{}),
119+
ensures(nil_exprt{}),
120+
message_handler(_message_handler)
72121
{
73-
unsigned_cnt=signed_cnt=char_cnt=int_cnt=short_cnt=
74-
long_cnt=double_cnt=float_cnt=c_bool_cnt=proper_bool_cnt=complex_cnt=
75-
int8_cnt=int16_cnt=int32_cnt=int64_cnt=
76-
ptr32_cnt=ptr64_cnt=
77-
gcc_float16_cnt=
78-
gcc_float32_cnt=gcc_float32x_cnt=
79-
gcc_float64_cnt=gcc_float64x_cnt=
80-
gcc_float128_cnt=gcc_float128x_cnt=
81-
gcc_int128_cnt=bv_cnt=floatbv_cnt=fixedbv_cnt=0;
82-
vector_size.make_nil();
83-
alignment.make_nil();
84-
bv_width.make_nil();
85-
fraction_width.make_nil();
86-
msc_based.make_nil();
87-
gcc_attribute_mode.make_nil();
88-
89-
requires.make_nil();
90-
assigns.make_nil();
91-
ensures.make_nil();
92-
93-
packed=aligned=constructor=destructor=false;
94-
95-
other.clear();
96-
c_storage_spec.clear();
97-
c_qualifiers.clear();
98122
}
99123

100-
protected:
101124
virtual void read_rec(const typet &type);
102125
virtual void build_type_with_subtype(typet &type) const;
103126
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
@@ -34,9 +34,7 @@ void c_typecheck_baset::typecheck_type(typet &type)
3434
{
3535
// we first convert, and then check
3636
{
37-
ansi_c_convert_typet ansi_c_convert_type(get_message_handler());
38-
39-
ansi_c_convert_type.read(type);
37+
ansi_c_convert_typet ansi_c_convert_type{get_message_handler(), type};
4038
ansi_c_convert_type.write(type);
4139
}
4240

0 commit comments

Comments
 (0)