Skip to content

Commit f668aac

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 f668aac

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
@@ -18,13 +18,6 @@ Author: Daniel Kroening, kroening@kroening.com
1818

1919
#include "gcc_types.h"
2020

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-
2821
void ansi_c_convert_typet::read_rec(const typet &type)
2922
{
3023
if(type.id()==ID_merged_type)
@@ -298,6 +291,8 @@ void ansi_c_convert_typet::read_rec(const typet &type)
298291

299292
void ansi_c_convert_typet::write(typet &type)
300293
{
294+
messaget log{message_handler};
295+
301296
type.clear();
302297

303298
// first, do "other"
@@ -314,8 +309,8 @@ void ansi_c_convert_typet::write(typet &type)
314309
gcc_float128_cnt || gcc_float128x_cnt ||
315310
gcc_int128_cnt || bv_cnt)
316311
{
317-
error().source_location=source_location;
318-
error() << "illegal type modifier for defined type" << eom;
312+
log.error().source_location = source_location;
313+
log.error() << "illegal type modifier for defined type" << messaget::eom;
319314
throw 0;
320315
}
321316

@@ -330,8 +325,8 @@ void ansi_c_convert_typet::write(typet &type)
330325

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

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

@@ -374,9 +369,9 @@ void ansi_c_convert_typet::write(typet &type)
374369

375370
else if(type_p->id()!=ID_empty)
376371
{
377-
error().source_location=source_location;
378-
error() << "constructor and destructor required to be type void, "
379-
<< "found " << type_p->pretty() << eom;
372+
log.error().source_location = source_location;
373+
log.error() << "constructor and destructor required to be type void, "
374+
<< "found " << type_p->pretty() << messaget::eom;
380375
throw 0;
381376
}
382377

@@ -385,9 +380,9 @@ void ansi_c_convert_typet::write(typet &type)
385380
}
386381
else if(constructor || destructor)
387382
{
388-
error().source_location=source_location;
389-
error() << "constructor and destructor required to be type void, "
390-
<< "found " << type.pretty() << eom;
383+
log.error().source_location = source_location;
384+
log.error() << "constructor and destructor required to be type void, "
385+
<< "found " << type.pretty() << messaget::eom;
391386
throw 0;
392387
}
393388
else if(gcc_float16_cnt ||
@@ -400,8 +395,9 @@ void ansi_c_convert_typet::write(typet &type)
400395
gcc_int128_cnt || bv_cnt ||
401396
short_cnt || char_cnt)
402397
{
403-
error().source_location=source_location;
404-
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;
405401
throw 0;
406402
}
407403

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

@@ -441,15 +437,16 @@ void ansi_c_convert_typet::write(typet &type)
441437
gcc_int128_cnt|| bv_cnt ||
442438
short_cnt || char_cnt)
443439
{
444-
error().source_location=source_location;
445-
error() << "cannot combine integer type with floating-point type" << eom;
440+
log.error().source_location = source_location;
441+
log.error() << "cannot combine integer type with floating-point type"
442+
<< messaget::eom;
446443
throw 0;
447444
}
448445

449446
if(double_cnt && float_cnt)
450447
{
451-
error().source_location=source_location;
452-
error() << "conflicting type modifiers" << eom;
448+
log.error().source_location = source_location;
449+
log.error() << "conflicting type modifiers" << messaget::eom;
453450
throw 0;
454451
}
455452

@@ -466,15 +463,15 @@ void ansi_c_convert_typet::write(typet &type)
466463
type=long_double_type();
467464
else
468465
{
469-
error().source_location=source_location;
470-
error() << "conflicting type modifiers" << eom;
466+
log.error().source_location = source_location;
467+
log.error() << "conflicting type modifiers" << messaget::eom;
471468
throw 0;
472469
}
473470
}
474471
else
475472
{
476-
error().source_location=source_location;
477-
error() << "illegal type modifier for float" << eom;
473+
log.error().source_location = source_location;
474+
log.error() << "illegal type modifier for float" << messaget::eom;
478475
throw 0;
479476
}
480477
}
@@ -485,8 +482,9 @@ void ansi_c_convert_typet::write(typet &type)
485482
gcc_float128_cnt || bv_cnt || proper_bool_cnt ||
486483
char_cnt || long_cnt)
487484
{
488-
error().source_location=source_location;
489-
error() << "illegal type modifier for C boolean type" << eom;
485+
log.error().source_location = source_location;
486+
log.error() << "illegal type modifier for C boolean type"
487+
<< messaget::eom;
490488
throw 0;
491489
}
492490

@@ -499,8 +497,9 @@ void ansi_c_convert_typet::write(typet &type)
499497
gcc_float128_cnt || bv_cnt ||
500498
char_cnt || long_cnt)
501499
{
502-
error().source_location=source_location;
503-
error() << "illegal type modifier for proper boolean type" << eom;
500+
log.error().source_location = source_location;
501+
log.error() << "illegal type modifier for proper boolean type"
502+
<< messaget::eom;
504503
throw 0;
505504
}
506505

@@ -518,15 +517,15 @@ void ansi_c_convert_typet::write(typet &type)
518517
int8_cnt || int16_cnt || int32_cnt || int64_cnt ||
519518
gcc_float128_cnt || bv_cnt || proper_bool_cnt)
520519
{
521-
error().source_location=source_location;
522-
error() << "illegal type modifier for char type" << eom;
520+
log.error().source_location = source_location;
521+
log.error() << "illegal type modifier for char type" << messaget::eom;
523522
throw 0;
524523
}
525524

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

545544
if(signed_cnt && unsigned_cnt)
546545
{
547-
error().source_location=source_location;
548-
error() << "conflicting type modifiers" << eom;
546+
log.error().source_location = source_location;
547+
log.error() << "conflicting type modifiers" << messaget::eom;
549548
throw 0;
550549
}
551550
else if(unsigned_cnt)
@@ -557,8 +556,8 @@ void ansi_c_convert_typet::write(typet &type)
557556
{
558557
if(long_cnt || char_cnt || short_cnt || gcc_int128_cnt || bv_cnt)
559558
{
560-
error().source_location=source_location;
561-
error() << "conflicting type modifiers" << eom;
559+
log.error().source_location = source_location;
560+
log.error() << "conflicting type modifiers" << messaget::eom;
562561
throw 0;
563562
}
564563

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

@@ -647,8 +646,8 @@ void ansi_c_convert_typet::write(typet &type)
647646
}
648647
else
649648
{
650-
error().source_location=source_location;
651-
error() << "illegal type modifier for integer type" << eom;
649+
log.error().source_location = source_location;
650+
log.error() << "illegal type modifier for integer type" << messaget::eom;
652651
throw 0;
653652
}
654653
}

‎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
@@ -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)