Skip to content

Commit 957f87c

Browse files
tautschnigtautschnig
committed
ansi_c_convert_typet is not a messaget
Use a message handler instead.
1 parent 69fbd6e commit 957f87c

File tree

3 files changed

+68
-57
lines changed

3 files changed

+68
-57
lines changed

‎src/ansi-c/ansi_c_convert_type.cpp

Lines changed: 48 additions & 41 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ 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

@@ -286,6 +287,8 @@ void ansi_c_convert_typet::read_rec(const typet &type)
286287

287288
void ansi_c_convert_typet::write(typet &type)
288289
{
290+
messaget log{message_handler};
291+
289292
type.clear();
290293

291294
// first, do "other"
@@ -302,8 +305,8 @@ void ansi_c_convert_typet::write(typet &type)
302305
gcc_float128_cnt || gcc_float128x_cnt ||
303306
gcc_int128_cnt || bv_cnt)
304307
{
305-
error().source_location=source_location;
306-
error() << "illegal type modifier for defined type" << eom;
308+
log.error().source_location = source_location;
309+
log.error() << "illegal type modifier for defined type" << messaget::eom;
307310
throw 0;
308311
}
309312

@@ -318,8 +321,8 @@ void ansi_c_convert_typet::write(typet &type)
318321

319322
if(other.size()!=1)
320323
{
321-
error().source_location=source_location;
322-
error() << "illegal combination of defined types" << eom;
324+
log.error().source_location = source_location;
325+
log.error() << "illegal combination of defined types" << messaget::eom;
323326
throw 0;
324327
}
325328

@@ -342,9 +345,9 @@ void ansi_c_convert_typet::write(typet &type)
342345
{
343346
if(constructor && destructor)
344347
{
345-
error().source_location=source_location;
346-
error() << "combining constructor and destructor not supported"
347-
<< eom;
348+
log.error().source_location = source_location;
349+
log.error() << "combining constructor and destructor not supported"
350+
<< messaget::eom;
348351
throw 0;
349352
}
350353

@@ -354,9 +357,9 @@ void ansi_c_convert_typet::write(typet &type)
354357

355358
else if(type_p->id()!=ID_empty)
356359
{
357-
error().source_location=source_location;
358-
error() << "constructor and destructor required to be type void, "
359-
<< "found " << type_p->pretty() << eom;
360+
log.error().source_location = source_location;
361+
log.error() << "constructor and destructor required to be type void, "
362+
<< "found " << type_p->pretty() << messaget::eom;
360363
throw 0;
361364
}
362365

@@ -365,9 +368,9 @@ void ansi_c_convert_typet::write(typet &type)
365368
}
366369
else if(constructor || destructor)
367370
{
368-
error().source_location=source_location;
369-
error() << "constructor and destructor required to be type void, "
370-
<< "found " << type.pretty() << eom;
371+
log.error().source_location = source_location;
372+
log.error() << "constructor and destructor required to be type void, "
373+
<< "found " << type.pretty() << messaget::eom;
371374
throw 0;
372375
}
373376
else if(gcc_float16_cnt ||
@@ -380,8 +383,9 @@ void ansi_c_convert_typet::write(typet &type)
380383
gcc_int128_cnt || bv_cnt ||
381384
short_cnt || char_cnt)
382385
{
383-
error().source_location=source_location;
384-
error() << "cannot combine integer type with floating-point type" << eom;
386+
log.error().source_location = source_location;
387+
log.error() << "cannot combine integer type with floating-point type"
388+
<< messaget::eom;
385389
throw 0;
386390
}
387391

@@ -391,8 +395,8 @@ void ansi_c_convert_typet::write(typet &type)
391395
gcc_float64_cnt+gcc_float64x_cnt+
392396
gcc_float128_cnt+gcc_float128x_cnt>=2)
393397
{
394-
error().source_location=source_location;
395-
error() << "conflicting type modifiers" << eom;
398+
log.error().source_location = source_location;
399+
log.error() << "conflicting type modifiers" << messaget::eom;
396400
throw 0;
397401
}
398402

@@ -421,15 +425,16 @@ void ansi_c_convert_typet::write(typet &type)
421425
gcc_int128_cnt|| bv_cnt ||
422426
short_cnt || char_cnt)
423427
{
424-
error().source_location=source_location;
425-
error() << "cannot combine integer type with floating-point type" << eom;
428+
log.error().source_location = source_location;
429+
log.error() << "cannot combine integer type with floating-point type"
430+
<< messaget::eom;
426431
throw 0;
427432
}
428433

429434
if(double_cnt && float_cnt)
430435
{
431-
error().source_location=source_location;
432-
error() << "conflicting type modifiers" << eom;
436+
log.error().source_location = source_location;
437+
log.error() << "conflicting type modifiers" << messaget::eom;
433438
throw 0;
434439
}
435440

@@ -446,15 +451,15 @@ void ansi_c_convert_typet::write(typet &type)
446451
type=long_double_type();
447452
else
448453
{
449-
error().source_location=source_location;
450-
error() << "conflicting type modifiers" << eom;
454+
log.error().source_location = source_location;
455+
log.error() << "conflicting type modifiers" << messaget::eom;
451456
throw 0;
452457
}
453458
}
454459
else
455460
{
456-
error().source_location=source_location;
457-
error() << "illegal type modifier for float" << eom;
461+
log.error().source_location = source_location;
462+
log.error() << "illegal type modifier for float" << messaget::eom;
458463
throw 0;
459464
}
460465
}
@@ -465,8 +470,9 @@ void ansi_c_convert_typet::write(typet &type)
465470
gcc_float128_cnt || bv_cnt || proper_bool_cnt ||
466471
char_cnt || long_cnt)
467472
{
468-
error().source_location=source_location;
469-
error() << "illegal type modifier for C boolean type" << eom;
473+
log.error().source_location = source_location;
474+
log.error() << "illegal type modifier for C boolean type"
475+
<< messaget::eom;
470476
throw 0;
471477
}
472478

@@ -479,8 +485,9 @@ void ansi_c_convert_typet::write(typet &type)
479485
gcc_float128_cnt || bv_cnt ||
480486
char_cnt || long_cnt)
481487
{
482-
error().source_location=source_location;
483-
error() << "illegal type modifier for proper boolean type" << eom;
488+
log.error().source_location = source_location;
489+
log.error() << "illegal type modifier for proper boolean type"
490+
<< messaget::eom;
484491
throw 0;
485492
}
486493

@@ -498,15 +505,15 @@ void ansi_c_convert_typet::write(typet &type)
498505
int8_cnt || int16_cnt || int32_cnt || int64_cnt ||
499506
gcc_float128_cnt || bv_cnt || proper_bool_cnt)
500507
{
501-
error().source_location=source_location;
502-
error() << "illegal type modifier for char type" << eom;
508+
log.error().source_location = source_location;
509+
log.error() << "illegal type modifier for char type" << messaget::eom;
503510
throw 0;
504511
}
505512

506513
if(signed_cnt && unsigned_cnt)
507514
{
508-
error().source_location=source_location;
509-
error() << "conflicting type modifiers" << eom;
515+
log.error().source_location = source_location;
516+
log.error() << "conflicting type modifiers" << messaget::eom;
510517
throw 0;
511518
}
512519
else if(unsigned_cnt)
@@ -524,8 +531,8 @@ void ansi_c_convert_typet::write(typet &type)
524531

525532
if(signed_cnt && unsigned_cnt)
526533
{
527-
error().source_location=source_location;
528-
error() << "conflicting type modifiers" << eom;
534+
log.error().source_location = source_location;
535+
log.error() << "conflicting type modifiers" << messaget::eom;
529536
throw 0;
530537
}
531538
else if(unsigned_cnt)
@@ -537,8 +544,8 @@ void ansi_c_convert_typet::write(typet &type)
537544
{
538545
if(long_cnt || char_cnt || short_cnt || gcc_int128_cnt || bv_cnt)
539546
{
540-
error().source_location=source_location;
541-
error() << "conflicting type modifiers" << eom;
547+
log.error().source_location = source_location;
548+
log.error() << "conflicting type modifiers" << messaget::eom;
542549
throw 0;
543550
}
544551

@@ -594,8 +601,8 @@ void ansi_c_convert_typet::write(typet &type)
594601
{
595602
if(long_cnt || char_cnt)
596603
{
597-
error().source_location=source_location;
598-
error() << "conflicting type modifiers" << eom;
604+
log.error().source_location = source_location;
605+
log.error() << "conflicting type modifiers" << messaget::eom;
599606
throw 0;
600607
}
601608

@@ -627,8 +634,8 @@ void ansi_c_convert_typet::write(typet &type)
627634
}
628635
else
629636
{
630-
error().source_location=source_location;
631-
error() << "illegal type modifier for integer type" << eom;
637+
log.error().source_location = source_location;
638+
log.error() << "illegal type modifier for integer type" << messaget::eom;
632639
throw 0;
633640
}
634641
}

‎src/ansi-c/ansi_c_convert_type.h

Lines changed: 11 additions & 8 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,
@@ -62,9 +63,9 @@ class ansi_c_convert_typet:public messaget
6263

6364
std::list<typet> other;
6465

65-
explicit ansi_c_convert_typet(message_handlert &_message_handler):
66-
messaget(_message_handler)
67-
// class members are initialized by calling read()
66+
explicit ansi_c_convert_typet(message_handlert &_message_handler)
67+
: message_handler(_message_handler)
68+
// class members are initialized by calling read()
6869
{
6970
}
7071

@@ -98,6 +99,8 @@ class ansi_c_convert_typet:public messaget
9899
}
99100

100101
protected:
102+
message_handlert &message_handler;
103+
101104
virtual void read_rec(const typet &type);
102105
virtual void build_type_with_subtype(typet &type) const;
103106
virtual void set_attributes(typet &type) const;

‎src/cpp/cpp_convert_type.cpp

Lines changed: 9 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
1414
#include <util/c_types.h>
1515
#include <util/config.h>
1616
#include <util/invariant.h>
17+
#include <util/message.h>
1718
#include <util/std_types.h>
1819

1920
#include <ansi-c/ansi_c_convert_type.h>
@@ -86,7 +87,7 @@ void cpp_convert_typet::read_rec(const typet &type)
8687
{
8788
other.push_back(type);
8889
cpp_convert_plain_type(
89-
to_array_type(other.back()).element_type(), get_message_handler());
90+
to_array_type(other.back()).element_type(), message_handler);
9091
}
9192
else if(type.id()==ID_template)
9293
{
@@ -125,8 +126,7 @@ void cpp_convert_typet::read_template(const typet &type)
125126
other.push_back(type);
126127
typet &t=other.back();
127128

128-
cpp_convert_plain_type(
129-
to_type_with_subtype(t).subtype(), get_message_handler());
129+
cpp_convert_plain_type(to_type_with_subtype(t).subtype(), message_handler);
130130

131131
irept &arguments=t.add(ID_arguments);
132132

@@ -142,7 +142,7 @@ void cpp_convert_typet::read_template(const typet &type)
142142
}
143143
else
144144
{
145-
cpp_convert_plain_type(decl.type(), get_message_handler());
145+
cpp_convert_plain_type(decl.type(), message_handler);
146146
}
147147

148148
// TODO: initializer
@@ -163,7 +163,7 @@ void cpp_convert_typet::read_function_type(const typet &type)
163163
t.remove_subtype();
164164

165165
if(return_type.is_not_nil())
166-
cpp_convert_plain_type(return_type, get_message_handler());
166+
cpp_convert_plain_type(return_type, message_handler);
167167

168168
// take care of parameter types
169169
code_typet::parameterst &parameters = t.parameters();
@@ -182,7 +182,7 @@ void cpp_convert_typet::read_function_type(const typet &type)
182182
cpp_declarationt &declaration=to_cpp_declaration(parameter_expr);
183183
source_locationt type_location=declaration.type().source_location();
184184

185-
cpp_convert_plain_type(declaration.type(), get_message_handler());
185+
cpp_convert_plain_type(declaration.type(), message_handler);
186186

187187
// there should be only one declarator
188188
assert(declaration.declarators().size()==1);
@@ -252,8 +252,9 @@ void cpp_convert_typet::write(typet &type)
252252
{
253253
if(wchar_t_count || char16_t_count || char32_t_count)
254254
{
255-
error().source_location = source_location;
256-
error() << "illegal type modifier for defined type" << eom;
255+
messaget log{message_handler};
256+
log.error().source_location = source_location;
257+
log.error() << "illegal type modifier for defined type" << messaget::eom;
257258
throw 0;
258259
}
259260

0 commit comments

Comments
 (0)