Skip to content

Commit be06467

Browse files
committed
goto_inlinet isn't a messaget
Use a messaget member instead as there is no is-a relationship between goto_inlinet and messaget.
1 parent 77a0496 commit be06467

File tree

2 files changed

+35
-30
lines changed

2 files changed

+35
-30
lines changed

src/goto-programs/goto_inline_class.cpp

Lines changed: 27 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -64,10 +64,10 @@ void goto_inlinet::parameter_assignments(
6464
// if you run out of actual arguments there was a mismatch
6565
if(it1==arguments.end())
6666
{
67-
warning().source_location=source_location;
68-
warning() << "call to '" << function_name << "': "
69-
<< "not enough arguments, "
70-
<< "inserting non-deterministic value" << eom;
67+
log.warning().source_location = source_location;
68+
log.warning() << "call to '" << function_name << "': "
69+
<< "not enough arguments, "
70+
<< "inserting non-deterministic value" << messaget::eom;
7171

7272
actual = side_effect_expr_nondett(parameter_type, source_location);
7373
}
@@ -171,9 +171,9 @@ void goto_inlinet::replace_return(
171171
{
172172
if(!code_return.has_return_value())
173173
{
174-
warning().source_location=it->code.find_source_location();
175-
warning() << "return expects one operand!\n"
176-
<< it->code.pretty() << eom;
174+
log.warning().source_location = it->code.find_source_location();
175+
log.warning() << "return expects one operand!\n"
176+
<< it->code.pretty() << messaget::eom;
177177
continue;
178178
}
179179

@@ -355,9 +355,9 @@ void goto_inlinet::expand_function_call(
355355
{
356356
// it's recursive.
357357
// Uh. Buh. Give up.
358-
warning().source_location=function.find_source_location();
359-
warning() << "recursion is ignored on call to '" << identifier << "'"
360-
<< eom;
358+
log.warning().source_location = function.find_source_location();
359+
log.warning() << "recursion is ignored on call to '" << identifier << "'"
360+
<< messaget::eom;
361361

362362
if(force_full)
363363
target->turn_into_skip();
@@ -370,8 +370,9 @@ void goto_inlinet::expand_function_call(
370370

371371
if(f_it==goto_functions.function_map.end())
372372
{
373-
warning().source_location=function.find_source_location();
374-
warning() << "missing function '" << identifier << "' is ignored" << eom;
373+
log.warning().source_location = function.find_source_location();
374+
log.warning() << "missing function '" << identifier << "' is ignored"
375+
<< messaget::eom;
375376

376377
if(force_full)
377378
target->turn_into_skip();
@@ -401,15 +402,17 @@ void goto_inlinet::expand_function_call(
401402
function,
402403
arguments);
403404

404-
progress() << "Inserting " << identifier << " into caller" << eom;
405-
progress() << "Number of instructions: "
406-
<< cached.body.instructions.size() << eom;
405+
log.progress() << "Inserting " << identifier << " into caller"
406+
<< messaget::eom;
407+
log.progress() << "Number of instructions: "
408+
<< cached.body.instructions.size() << messaget::eom;
407409

408410
if(!caching)
409411
{
410-
progress() << "Removing " << identifier << " from cache" << eom;
411-
progress() << "Number of instructions: "
412-
<< cached.body.instructions.size() << eom;
412+
log.progress() << "Removing " << identifier << " from cache"
413+
<< messaget::eom;
414+
log.progress() << "Number of instructions: "
415+
<< cached.body.instructions.size() << messaget::eom;
413416

414417
inline_log.cleanup(cached.body);
415418
cache.erase(identifier);
@@ -438,8 +441,9 @@ void goto_inlinet::expand_function_call(
438441
{
439442
if(no_body_set.insert(identifier).second) // newly inserted
440443
{
441-
warning().source_location = function.find_source_location();
442-
warning() << "no body for function '" << identifier << "'" << eom;
444+
log.warning().source_location = function.find_source_location();
445+
log.warning() << "no body for function '" << identifier << "'"
446+
<< messaget::eom;
443447
}
444448
}
445449
}
@@ -567,9 +571,9 @@ const goto_inlinet::goto_functiont &goto_inlinet::goto_inline_transitive(
567571
DATA_INVARIANT(
568572
cached.body.empty(), "body of new function in cache must be empty");
569573

570-
progress() << "Creating copy of " << identifier << eom;
571-
progress() << "Number of instructions: "
572-
<< goto_function.body.instructions.size() << eom;
574+
log.progress() << "Creating copy of " << identifier << messaget::eom;
575+
log.progress() << "Number of instructions: "
576+
<< goto_function.body.instructions.size() << messaget::eom;
573577

574578
cached.copy_from(goto_function); // location numbers not changed
575579
inline_log.copy_from(goto_function.body, cached.body);

src/goto-programs/goto_inline_class.h

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -17,20 +17,20 @@ Author: Daniel Kroening, [email protected]
1717

1818
#include "goto_functions.h"
1919

20-
class goto_inlinet:public messaget
20+
class goto_inlinet
2121
{
2222
public:
2323
goto_inlinet(
2424
goto_functionst &goto_functions,
2525
const namespacet &ns,
2626
message_handlert &message_handler,
2727
bool adjust_function,
28-
bool caching=true):
29-
messaget(message_handler),
30-
goto_functions(goto_functions),
31-
ns(ns),
32-
adjust_function(adjust_function),
33-
caching(caching)
28+
bool caching = true)
29+
: log(message_handler),
30+
goto_functions(goto_functions),
31+
ns(ns),
32+
adjust_function(adjust_function),
33+
caching(caching)
3434
{
3535
}
3636

@@ -122,6 +122,7 @@ class goto_inlinet:public messaget
122122
};
123123

124124
protected:
125+
messaget log;
125126
goto_functionst &goto_functions;
126127
const namespacet &ns;
127128

0 commit comments

Comments
 (0)