diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp index 6adf2e3da2b..d7b40b7030e 100644 --- a/src/goto-programs/interpreter.cpp +++ b/src/goto-programs/interpreter.cpp @@ -39,20 +39,20 @@ const std::size_t interpretert::npos=std::numeric_limits::max(); void interpretert::operator()() { - status() << "0- Initialize:" << eom; + output.status() << "0- Initialize:" << messaget::eom; initialize(true); try { - status() << "Type h for help\n" << eom; + output.status() << "Type h for help\n" << messaget::eom; while(!done) command(); - status() << total_steps << "- Program End.\n" << eom; + output.status() << total_steps << "- Program End.\n" << messaget::eom; } catch (const char *e) { - error() << e << "\n" << eom; + output.error() << e << "\n" << messaget::eom; } while(!done) @@ -113,22 +113,19 @@ void interpretert::show_state() { if(!show) return; - status() << "\n" - << total_steps+1 - << " ----------------------------------------------------\n"; + output.status() << "\n" + << total_steps + 1 + << " ----------------------------------------------------\n"; if(pc==function->second.body.instructions.end()) { - status() << "End of function '" << function->first << "'\n"; + output.status() << "End of function '" << function->first << "'\n"; } else function->second.body.output_instruction( - ns, - function->first, - status(), - *pc); + ns, function->first, output.status(), *pc); - status() << eom; + output.status() << messaget::eom; } /// reads a user command and executes it. @@ -147,18 +144,18 @@ void interpretert::command() done=true; else if(ch=='h') { - status() << "Interpreter help\n" - << "h: display this menu\n" - << "j: output json trace\n" - << "m: output memory dump\n" - << "o: output goto trace\n" - << "q: quit\n" - << "r: run up to entry point\n" - << "s#: step a number of instructions\n" - << "sa: step across a function\n" - << "so: step out of a function\n" - << "se: step until end of program\n" - << eom; + output.status() << "Interpreter help\n" + << "h: display this menu\n" + << "j: output json trace\n" + << "m: output memory dump\n" + << "o: output goto trace\n" + << "q: quit\n" + << "r: run up to entry point\n" + << "s#: step a number of instructions\n" + << "sa: step across a function\n" + << "so: step out of a function\n" + << "se: step until end of program\n" + << messaget::eom; } else if(ch=='j') { @@ -176,7 +173,7 @@ void interpretert::command() return; } } - json_steps.output(result()); + json_steps.output(output.result()); } else if(ch=='m') { @@ -197,7 +194,7 @@ void interpretert::command() return; } } - steps.output(ns, result()); + steps.output(ns, output.result()); } else if(ch=='r') { @@ -408,8 +405,9 @@ void interpretert::execute_other() mp_integer size=get_size(pc->code.op0().type()); while(rhs.size()(offset)] << " > object count " - << memory.size() << eom; + output.error() << "interpreter: invalid pointer " + << rhs[numeric_cast_v(offset)] + << " > object count " << memory.size() << messaget::eom; throw "interpreter: reading from invalid pointer"; } @@ -671,10 +669,9 @@ void interpretert::execute_assign() mp_integer size=get_size(code_assign.lhs().type()); if(size!=rhs.size()) - error() << "!! failed to obtain rhs (" - << rhs.size() << " vs. " - << size << ")\n" - << eom; + output.error() << "!! failed to obtain rhs (" << rhs.size() << " vs. " + << size << ")\n" + << messaget::eom; else { goto_trace_stept &trace_step=steps.get_last_step(); @@ -716,11 +713,11 @@ void interpretert::assign( memory_cellt &cell = memory[numeric_cast_v(address_val)]; if(show) { - status() << total_steps << " ** assigning " - << address_to_symbol(address_val).get_identifier() << "[" - << address_to_offset(address_val) - << "]:=" << rhs[numeric_cast_v(i)] << "\n" - << eom; + output.status() << total_steps << " ** assigning " + << address_to_symbol(address_val).get_identifier() + << "[" << address_to_offset(address_val) + << "]:=" << rhs[numeric_cast_v(i)] << "\n" + << messaget::eom; } cell.value = rhs[numeric_cast_v(i)]; if(cell.initialized==memory_cellt::initializedt::UNKNOWN) @@ -740,8 +737,8 @@ void interpretert::execute_assert() if(!evaluate_boolean(pc->get_condition())) { if(show) - error() << "assertion failed at " << pc->location_number - << "\n" << eom; + output.error() << "assertion failed at " << pc->location_number << "\n" + << messaget::eom; } } @@ -847,7 +844,7 @@ void interpretert::execute_function_call() } if(show) - error() << "no body for "+id2string(identifier) << eom; + output.error() << "no body for " << identifier << messaget::eom; } } @@ -903,8 +900,8 @@ typet interpretert::concretize_type(const typet &type) if(computed_size.size()==1 && computed_size[0]>=0) { - result() << "Concretized array with size " << computed_size[0] - << eom; + output.result() << "Concretized array with size " << computed_size[0] + << messaget::eom; return array_typet( type.subtype(), @@ -912,7 +909,8 @@ typet interpretert::concretize_type(const typet &type) } else { - warning() << "Failed to concretize variable array" << eom; + output.warning() << "Failed to concretize variable array" + << messaget::eom; } } return type; @@ -1067,11 +1065,12 @@ void interpretert::print_memory(bool input_flags) const memory_cellt &cell=cell_address.second; const auto identifier = address_to_symbol(i).get_identifier(); const auto offset=address_to_offset(i); - status() << identifier << "[" << offset << "]" - << "=" << cell.value << eom; + output.status() << identifier << "[" << offset << "]" + << "=" << cell.value << messaget::eom; if(input_flags) - status() << "(" << static_cast(cell.initialized) << ")" << eom; - status() << eom; + output.status() << "(" << static_cast(cell.initialized) << ")" + << messaget::eom; + output.status() << messaget::eom; } } diff --git a/src/goto-programs/interpreter.h b/src/goto-programs/interpreter.h index c4b84863bc7..bd74d05b7ba 100644 --- a/src/goto-programs/interpreter.h +++ b/src/goto-programs/interpreter.h @@ -12,10 +12,10 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_PROGRAMS_INTERPRETER_H #define CPROVER_GOTO_PROGRAMS_INTERPRETER_H -#include - #include "goto_model.h" +class message_handlert; + void interpreter( const goto_modelt &, message_handlert &); diff --git a/src/goto-programs/interpreter_class.h b/src/goto-programs/interpreter_class.h index 96f051853a3..58dac3a193a 100644 --- a/src/goto-programs/interpreter_class.h +++ b/src/goto-programs/interpreter_class.h @@ -24,14 +24,14 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_trace.h" #include "json_goto_trace.h" -class interpretert:public messaget +class interpretert { public: interpretert( const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions, message_handlert &_message_handler) - : messaget(_message_handler), + : output(_message_handler), symbol_table(_symbol_table), ns(_symbol_table), goto_functions(_goto_functions), @@ -97,6 +97,7 @@ class interpretert:public messaget const dynamic_typest &get_dynamic_types() { return dynamic_types; } protected: + messaget output; const symbol_tablet &symbol_table; // This is a cache so that we don't have to create it when a call needs it diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp index c9c97084ad9..7302b52e018 100644 --- a/src/goto-programs/interpreter_evaluate.cpp +++ b/src/goto-programs/interpreter_evaluate.cpp @@ -404,8 +404,8 @@ void interpretert::evaluate( { const std::string &value = id2string(to_constant_expr(expr).get_value()); if(show) - warning() << "string decoding not fully implemented " - << value.size() + 1 << eom; + output.warning() << "string decoding not fully implemented " + << value.size() + 1 << messaget::eom; dest.push_back(get_string_container()[value]); return; } @@ -457,15 +457,14 @@ void interpretert::evaluate( if(side_effect.get_statement()==ID_nondet) { if(show) - error() << "nondet not implemented" << eom; + output.error() << "nondet not implemented" << messaget::eom; return; } else if(side_effect.get_statement()==ID_allocate) { if(show) - error() << "heap memory allocation not fully implemented " - << expr.type().subtype().pretty() - << eom; + output.error() << "heap memory allocation not fully implemented " + << expr.type().subtype().pretty() << messaget::eom; std::stringstream buffer; num_dynamic_objects++; buffer << "interpreter::dynamic_object" << num_dynamic_objects; @@ -478,9 +477,8 @@ void interpretert::evaluate( return; } if(show) - error() << "side effect not implemented " - << side_effect.get_statement() - << eom; + output.error() << "side effect not implemented " + << side_effect.get_statement() << messaget::eom; } else if(expr.id()==ID_bitor) { @@ -1041,14 +1039,14 @@ void interpretert::evaluate( { if(expr.type().id()==ID_signedbv) { - warning() << "Infinite size arrays not supported" << eom; + output.warning() << "Infinite size arrays not supported" << messaget::eom; return; } } - error() << "!! failed to evaluate expression: " - << from_expr(ns, function->first, expr) << "\n" - << expr.id() << "[" << expr.type().id() << "]" - << eom; + output.error() << "!! failed to evaluate expression: " + << from_expr(ns, function->first, expr) << "\n" + << expr.id() << "[" << expr.type().id() << "]" + << messaget::eom; } mp_integer interpretert::evaluate_address( @@ -1157,9 +1155,8 @@ mp_integer interpretert::evaluate_address( if(!fail_quietly) { - error() << "!! failed to evaluate address: " - << from_expr(ns, function->first, expr) - << eom; + output.error() << "!! failed to evaluate address: " + << from_expr(ns, function->first, expr) << messaget::eom; } return 0;