Skip to content

Commit b01b9b7

Browse files
tautschnigtautschnig
authored
Merge pull request #5599 from tautschnig/cleanup-ansi_c_convert_type
Clean up ansi_c_convert_typet's interface
2 parents eb0472e + 794f6f7 commit b01b9b7

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)
@@ -286,6 +280,8 @@ void ansi_c_convert_typet::read_rec(const typet &type)
286280

287281
void ansi_c_convert_typet::write(typet &type)
288282
{
283+
messaget log{message_handler};
284+
289285
type.clear();
290286

291287
// first, do "other"
@@ -302,8 +298,8 @@ void ansi_c_convert_typet::write(typet &type)
302298
gcc_float128_cnt || gcc_float128x_cnt ||
303299
gcc_int128_cnt || bv_cnt)
304300
{
305-
error().source_location=source_location;
306-
error() << "illegal type modifier for defined type" << eom;
301+
log.error().source_location = source_location;
302+
log.error() << "illegal type modifier for defined type" << messaget::eom;
307303
throw 0;
308304
}
309305

@@ -318,8 +314,8 @@ void ansi_c_convert_typet::write(typet &type)
318314

319315
if(other.size()!=1)
320316
{
321-
error().source_location=source_location;
322-
error() << "illegal combination of defined types" << eom;
317+
log.error().source_location = source_location;
318+
log.error() << "illegal combination of defined types" << messaget::eom;
323319
throw 0;
324320
}
325321

@@ -342,9 +338,9 @@ void ansi_c_convert_typet::write(typet &type)
342338
{
343339
if(constructor && destructor)
344340
{
345-
error().source_location=source_location;
346-
error() << "combining constructor and destructor not supported"
347-
<< eom;
341+
log.error().source_location = source_location;
342+
log.error() << "combining constructor and destructor not supported"
343+
<< messaget::eom;
348344
throw 0;
349345
}
350346

@@ -354,9 +350,9 @@ void ansi_c_convert_typet::write(typet &type)
354350

355351
else if(type_p->id()!=ID_empty)
356352
{
357-
error().source_location=source_location;
358-
error() << "constructor and destructor required to be type void, "
359-
<< "found " << type_p->pretty() << eom;
353+
log.error().source_location = source_location;
354+
log.error() << "constructor and destructor required to be type void, "
355+
<< "found " << type_p->pretty() << messaget::eom;
360356
throw 0;
361357
}
362358

@@ -365,9 +361,9 @@ void ansi_c_convert_typet::write(typet &type)
365361
}
366362
else if(constructor || destructor)
367363
{
368-
error().source_location=source_location;
369-
error() << "constructor and destructor required to be type void, "
370-
<< "found " << type.pretty() << eom;
364+
log.error().source_location = source_location;
365+
log.error() << "constructor and destructor required to be type void, "
366+
<< "found " << type.pretty() << messaget::eom;
371367
throw 0;
372368
}
373369
else if(gcc_float16_cnt ||
@@ -380,8 +376,9 @@ void ansi_c_convert_typet::write(typet &type)
380376
gcc_int128_cnt || bv_cnt ||
381377
short_cnt || char_cnt)
382378
{
383-
error().source_location=source_location;
384-
error() << "cannot combine integer type with floating-point type" << eom;
379+
log.error().source_location = source_location;
380+
log.error() << "cannot combine integer type with floating-point type"
381+
<< messaget::eom;
385382
throw 0;
386383
}
387384

@@ -391,8 +388,8 @@ void ansi_c_convert_typet::write(typet &type)
391388
gcc_float64_cnt+gcc_float64x_cnt+
392389
gcc_float128_cnt+gcc_float128x_cnt>=2)
393390
{
394-
error().source_location=source_location;
395-
error() << "conflicting type modifiers" << eom;
391+
log.error().source_location = source_location;
392+
log.error() << "conflicting type modifiers" << messaget::eom;
396393
throw 0;
397394
}
398395

@@ -421,15 +418,16 @@ void ansi_c_convert_typet::write(typet &type)
421418
gcc_int128_cnt|| bv_cnt ||
422419
short_cnt || char_cnt)
423420
{
424-
error().source_location=source_location;
425-
error() << "cannot combine integer type with floating-point type" << eom;
421+
log.error().source_location = source_location;
422+
log.error() << "cannot combine integer type with floating-point type"
423+
<< messaget::eom;
426424
throw 0;
427425
}
428426

429427
if(double_cnt && float_cnt)
430428
{
431-
error().source_location=source_location;
432-
error() << "conflicting type modifiers" << eom;
429+
log.error().source_location = source_location;
430+
log.error() << "conflicting type modifiers" << messaget::eom;
433431
throw 0;
434432
}
435433

@@ -446,15 +444,15 @@ void ansi_c_convert_typet::write(typet &type)
446444
type=long_double_type();
447445
else
448446
{
449-
error().source_location=source_location;
450-
error() << "conflicting type modifiers" << eom;
447+
log.error().source_location = source_location;
448+
log.error() << "conflicting type modifiers" << messaget::eom;
451449
throw 0;
452450
}
453451
}
454452
else
455453
{
456-
error().source_location=source_location;
457-
error() << "illegal type modifier for float" << eom;
454+
log.error().source_location = source_location;
455+
log.error() << "illegal type modifier for float" << messaget::eom;
458456
throw 0;
459457
}
460458
}
@@ -465,8 +463,9 @@ void ansi_c_convert_typet::write(typet &type)
465463
gcc_float128_cnt || bv_cnt || proper_bool_cnt ||
466464
char_cnt || long_cnt)
467465
{
468-
error().source_location=source_location;
469-
error() << "illegal type modifier for C boolean type" << eom;
466+
log.error().source_location = source_location;
467+
log.error() << "illegal type modifier for C boolean type"
468+
<< messaget::eom;
470469
throw 0;
471470
}
472471

@@ -479,8 +478,9 @@ void ansi_c_convert_typet::write(typet &type)
479478
gcc_float128_cnt || bv_cnt ||
480479
char_cnt || long_cnt)
481480
{
482-
error().source_location=source_location;
483-
error() << "illegal type modifier for proper boolean type" << eom;
481+
log.error().source_location = source_location;
482+
log.error() << "illegal type modifier for proper boolean type"
483+
<< messaget::eom;
484484
throw 0;
485485
}
486486

@@ -498,15 +498,15 @@ void ansi_c_convert_typet::write(typet &type)
498498
int8_cnt || int16_cnt || int32_cnt || int64_cnt ||
499499
gcc_float128_cnt || bv_cnt || proper_bool_cnt)
500500
{
501-
error().source_location=source_location;
502-
error() << "illegal type modifier for char type" << eom;
501+
log.error().source_location = source_location;
502+
log.error() << "illegal type modifier for char type" << messaget::eom;
503503
throw 0;
504504
}
505505

506506
if(signed_cnt && unsigned_cnt)
507507
{
508-
error().source_location=source_location;
509-
error() << "conflicting type modifiers" << eom;
508+
log.error().source_location = source_location;
509+
log.error() << "conflicting type modifiers" << messaget::eom;
510510
throw 0;
511511
}
512512
else if(unsigned_cnt)
@@ -524,8 +524,8 @@ void ansi_c_convert_typet::write(typet &type)
524524

525525
if(signed_cnt && unsigned_cnt)
526526
{
527-
error().source_location=source_location;
528-
error() << "conflicting type modifiers" << eom;
527+
log.error().source_location = source_location;
528+
log.error() << "conflicting type modifiers" << messaget::eom;
529529
throw 0;
530530
}
531531
else if(unsigned_cnt)
@@ -537,8 +537,8 @@ void ansi_c_convert_typet::write(typet &type)
537537
{
538538
if(long_cnt || char_cnt || short_cnt || gcc_int128_cnt || bv_cnt)
539539
{
540-
error().source_location=source_location;
541-
error() << "conflicting type modifiers" << eom;
540+
log.error().source_location = source_location;
541+
log.error() << "conflicting type modifiers" << messaget::eom;
542542
throw 0;
543543
}
544544

@@ -594,8 +594,8 @@ void ansi_c_convert_typet::write(typet &type)
594594
{
595595
if(long_cnt || char_cnt)
596596
{
597-
error().source_location=source_location;
598-
error() << "conflicting type modifiers" << eom;
597+
log.error().source_location = source_location;
598+
log.error() << "conflicting type modifiers" << messaget::eom;
599599
throw 0;
600600
}
601601

@@ -627,8 +627,8 @@ void ansi_c_convert_typet::write(typet &type)
627627
}
628628
else
629629
{
630-
error().source_location=source_location;
631-
error() << "illegal type modifier for integer type" << eom;
630+
log.error().source_location = source_location;
631+
log.error() << "illegal type modifier for integer type" << messaget::eom;
632632
throw 0;
633633
}
634634
}

‎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,
@@ -55,49 +56,68 @@ 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+
message_handler(_message_handler)
72118
{
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-
assigns.clear();
90-
requires.clear();
91-
ensures.clear();
92-
93-
packed=aligned=constructor=destructor=false;
94-
95-
other.clear();
96-
c_storage_spec.clear();
97-
c_qualifiers.clear();
98119
}
99120

100-
protected:
101121
virtual void read_rec(const typet &type);
102122
virtual void build_type_with_subtype(typet &type) const;
103123
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)