From 9cb2c2a1e44f78935f92ccb94501f45ffb3865b0 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 16 May 2018 18:52:34 +0100 Subject: [PATCH 1/6] functor for language-specific expression formatting --- src/util/Makefile | 1 + src/util/formatter.cpp | 38 +++++++++++++++ src/util/formatter.h | 104 +++++++++++++++++++++++++++++++++++++++++ 3 files changed, 143 insertions(+) create mode 100644 src/util/formatter.cpp create mode 100644 src/util/formatter.h diff --git a/src/util/Makefile b/src/util/Makefile index 74fc5aec412..d3551dc4dc3 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -18,6 +18,7 @@ SRC = arith_tools.cpp \ fixedbv.cpp \ format_constant.cpp \ format_expr.cpp \ + formatter.cpp \ format_number_range.cpp \ format_type.cpp \ fresh_symbol.cpp \ diff --git a/src/util/formatter.cpp b/src/util/formatter.cpp new file mode 100644 index 00000000000..3d1575cec9a --- /dev/null +++ b/src/util/formatter.cpp @@ -0,0 +1,38 @@ +/*******************************************************************\ + +Module: Expression Pretty Printing + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +/// \file +/// Expression Pretty Printing + +#include "formatter.h" +#include "format_expr.h" +#include "format_type.h" + +debug_formattert debug_formatter; +default_debug_formattert default_debug_formatter; + +std::ostream &default_debug_formattert::format( + std::ostream &out, + const exprt &src) +{ + return out << ::format(src); +} + +std::ostream &default_debug_formattert::format( + std::ostream &out, + const typet &src) +{ + return out << ::format(src); +} + +std::ostream &default_debug_formattert::format( + std::ostream &out, + const source_locationt &src) +{ + return out << src; +} diff --git a/src/util/formatter.h b/src/util/formatter.h new file mode 100644 index 00000000000..cfb82a06f46 --- /dev/null +++ b/src/util/formatter.h @@ -0,0 +1,104 @@ +/*******************************************************************\ + +Module: + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#ifndef CPROVER_UTIL_FORMATTER_H +#define CPROVER_UTIL_FORMATTER_H + +#include "expr.h" + +class formattert; + +//! The below enables convenient syntax for feeding +//! formatters and objects into streams, via stream << formatter(o) +template +class formatter_containert +{ +public: + explicit formatter_containert( + formattert &_formatter, + const T &_o) : formatter(_formatter), o(_o) + { + } + + class formattert &formatter; + const T &o; +}; + +//! This is an abstract interface for a expr/type formatter +class formattert +{ +public: + // use these + formatter_containert operator()(const exprt &o) + { + return formatter_containert(*this, o); + } + + formatter_containert operator()(const typet &o) + { + return formatter_containert(*this, o); + } + + formatter_containert operator()(const source_locationt &o) + { + return formatter_containert(*this, o); + } + + // overload those + virtual std::ostream &format(std::ostream &, const exprt &) = 0; + virtual std::ostream &format(std::ostream &, const typet &) = 0; + virtual std::ostream &format(std::ostream &, const source_locationt &) = 0; +}; + +//! enable feeding into output streams +template +inline std::ostream & +operator<<(std::ostream &os, formatter_containert c) +{ + return c.formatter.format(os, c.o); +} + +//! this is the default debug formatter +class default_debug_formattert:public formattert +{ + std::ostream &format(std::ostream &, const exprt &) override; + std::ostream &format(std::ostream &, const typet &) override; + std::ostream &format(std::ostream &, const source_locationt &) override; +}; + +extern default_debug_formattert default_debug_formatter; + +//! this is the debug formatter, defaulting to the above +class debug_formattert:public formattert +{ +public: + debug_formattert():formatter(&default_debug_formatter) + { + } + + std::ostream &format(std::ostream &os, const exprt &o) override + { + return formatter->format(os, o); + } + + std::ostream &format(std::ostream &os, const typet &o) override + { + return formatter->format(os, o); + } + + std::ostream &format(std::ostream &os, const source_locationt &o) override + { + return formatter->format(os, o); + } + + formattert *formatter; +}; + +extern debug_formattert debug_formatter; + +#endif // CPROVER_UTIL_FORMATTER_H From 677ea949801b84b46ce7f1f8eabfeab7154ade69 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 17 May 2018 11:57:14 +0100 Subject: [PATCH 2/6] replace usage of format() by debug_formatter() --- src/analyses/constant_propagator.cpp | 4 +- .../generate_function_bodies.cpp | 10 +- src/goto-programs/goto_trace.cpp | 8 +- .../equation_conversion_exceptions.h | 4 +- src/goto-symex/slice_by_trace.cpp | 6 +- src/goto-symex/symex_target_equation.cpp | 16 +-- src/pointer-analysis/dereference.cpp | 4 +- src/pointer-analysis/value_set.cpp | 25 ++--- .../value_set_dereference.cpp | 19 ++-- src/solvers/refinement/string_constraint.h | 19 ++-- src/solvers/refinement/string_refinement.cpp | 103 +++++++++--------- .../refinement/string_refinement_util.cpp | 17 +-- 12 files changed, 119 insertions(+), 116 deletions(-) diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index 452e8355a93..855cfe23f8d 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -13,7 +13,7 @@ Author: Peter Schrammel #ifdef DEBUG #include -#include +#include #endif #include @@ -223,7 +223,7 @@ bool constant_propagator_domaint::two_way_propagate_rec( const namespacet &ns) { #ifdef DEBUG - std::cout << "two_way_propagate_rec: " << format(expr) << '\n'; + std::cout << "two_way_propagate_rec: " << debug_formatter(expr) << '\n'; #endif bool change=false; diff --git a/src/goto-programs/generate_function_bodies.cpp b/src/goto-programs/generate_function_bodies.cpp index aca0ed19aba..f21a3c23c89 100644 --- a/src/goto-programs/generate_function_bodies.cpp +++ b/src/goto-programs/generate_function_bodies.cpp @@ -9,7 +9,7 @@ Author: Diffblue Ltd. #include "generate_function_bodies.h" #include -#include +#include #include #include @@ -102,7 +102,7 @@ class assert_false_generate_function_bodiest : public generate_function_bodiest const namespacet ns(symbol_table); std::ostringstream comment_stream; comment_stream << id2string(ID_assertion) << " " - << format(assert_instruction->guard); + << debug_formatter(assert_instruction->guard); assert_instruction->source_location.set_comment(comment_stream.str()); assert_instruction->source_location.set_property_class(ID_assertion); auto end_instruction = add_instruction(); @@ -134,7 +134,7 @@ class assert_false_then_assume_false_generate_function_bodiest const namespacet ns(symbol_table); std::ostringstream comment_stream; comment_stream << id2string(ID_assertion) << " " - << format(assert_instruction->guard); + << debug_formatter(assert_instruction->guard); assert_instruction->source_location.set_comment(comment_stream.str()); assert_instruction->source_location.set_property_class(ID_assertion); auto assume_instruction = add_instruction(); @@ -203,7 +203,7 @@ class havoc_generate_function_bodiest : public generate_function_bodiest, bool constant_known_array_size = lhs_array_type.size().is_constant(); if(!constant_known_array_size) { - warning() << "Cannot havoc non-const array " << format(lhs) + warning() << "Cannot havoc non-const array " << debug_formatter(lhs) << " in function " << function_name << ": Unknown array size" << eom; } @@ -219,7 +219,7 @@ class havoc_generate_function_bodiest : public generate_function_bodiest, // Pretty much the same thing as a unknown size array // Technically not allowed by the C standard, but we model // unknown size arrays in structs this way - warning() << "Cannot havoc non-const array " << format(lhs) + warning() << "Cannot havoc non-const array " << debug_formatter(lhs) << " in function " << function_name << ": Array size 0" << eom; } diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp index e7f05e09e96..a6c6cd6319c 100644 --- a/src/goto-programs/goto_trace.cpp +++ b/src/goto-programs/goto_trace.cpp @@ -17,7 +17,7 @@ Author: Daniel Kroening #include #include -#include +#include #include #include @@ -74,8 +74,8 @@ void goto_trace_stept::output( if(is_assignment()) { - out << " " << format(full_lhs) - << " = " << format(full_lhs_value) + out << " " << debug_formatter(full_lhs) + << " = " << debug_formatter(full_lhs_value) << '\n'; } @@ -95,7 +95,7 @@ void goto_trace_stept::output( if(!comment.empty()) out << " " << comment << '\n'; - out << " " << format(pc->guard) << '\n'; + out << " " << debug_formatter(pc->guard) << '\n'; out << '\n'; } } diff --git a/src/goto-symex/equation_conversion_exceptions.h b/src/goto-symex/equation_conversion_exceptions.h index ffa57abefe0..76f8a455f4f 100644 --- a/src/goto-symex/equation_conversion_exceptions.h +++ b/src/goto-symex/equation_conversion_exceptions.h @@ -14,7 +14,7 @@ Author: Diffblue Ltd. #include -#include +#include #include "symex_target_equation.h" @@ -28,7 +28,7 @@ class equation_conversion_exceptiont : public std::runtime_error { std::ostringstream error_msg; error_msg << runtime_error::what(); - error_msg << "\nSource GOTO statement: " << format(step.source.pc->code); + error_msg << "\nSource GOTO statement: " << debug_formatter(step.source.pc->code); error_msg << "\nStep:\n"; step.output(error_msg); error_message = error_msg.str(); diff --git a/src/goto-symex/slice_by_trace.cpp b/src/goto-symex/slice_by_trace.cpp index 9fe0036911d..9dfb6572abd 100644 --- a/src/goto-symex/slice_by_trace.cpp +++ b/src/goto-symex/slice_by_trace.cpp @@ -21,7 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include +#include void symex_slice_by_tracet::slice_by_trace( std::string trace_files, @@ -257,10 +257,10 @@ void symex_slice_by_tracet::compute_ts_back( #if 0 std::cout << "EVENT: " << event << '\n'; - std::cout << "GUARD: " << format(guard) << '\n'; + std::cout << "GUARD: " << debug_formatter(guard) << '\n'; for(size_t j=0; j < t.size(); j++) { - std::cout << "t[" << j << "]=" << format(t[j]) << + std::cout << "t[" << j << "]=" << debug_formatter(t[j]) << '\n'; } #endif diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index 9554f1fd3a0..2573d41054a 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -11,7 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "symex_target_equation.h" -#include +#include #include #include #include @@ -795,10 +795,10 @@ void symex_target_equationt::SSA_stept::output(std::ostream &out) const switch(type) { case goto_trace_stept::typet::ASSERT: - out << "ASSERT " << format(cond_expr) << '\n'; + out << "ASSERT " << debug_formatter(cond_expr) << '\n'; break; case goto_trace_stept::typet::ASSUME: - out << "ASSUME " << format(cond_expr) << '\n'; + out << "ASSUME " << debug_formatter(cond_expr) << '\n'; break; case goto_trace_stept::typet::LOCATION: out << "LOCATION" << '\n'; @@ -812,7 +812,7 @@ void symex_target_equationt::SSA_stept::output(std::ostream &out) const case goto_trace_stept::typet::DECL: out << "DECL" << '\n'; - out << format(ssa_lhs) << '\n'; + out << debug_formatter(ssa_lhs) << '\n'; break; case goto_trace_stept::typet::ASSIGNMENT: @@ -876,7 +876,7 @@ void symex_target_equationt::SSA_stept::output(std::ostream &out) const out << "MEMORY_BARRIER\n"; break; case goto_trace_stept::typet::GOTO: - out << "IF " << format(cond_expr) << " GOTO\n"; + out << "IF " << debug_formatter(cond_expr) << " GOTO\n"; break; default: @@ -884,13 +884,13 @@ void symex_target_equationt::SSA_stept::output(std::ostream &out) const } if(is_assert() || is_assume() || is_assignment() || is_constraint()) - out << format(cond_expr) << '\n'; + out << debug_formatter(cond_expr) << '\n'; if(is_assert() || is_constraint()) out << comment << '\n'; if(is_shared_read() || is_shared_write()) - out << format(ssa_lhs) << '\n'; + out << debug_formatter(ssa_lhs) << '\n'; - out << "Guard: " << format(guard) << '\n'; + out << "Guard: " << debug_formatter(guard) << '\n'; } diff --git a/src/pointer-analysis/dereference.cpp b/src/pointer-analysis/dereference.cpp index 863c44cffb7..45563dd7247 100644 --- a/src/pointer-analysis/dereference.cpp +++ b/src/pointer-analysis/dereference.cpp @@ -13,7 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #ifdef DEBUG #include -#include +#include #endif #include @@ -37,7 +37,7 @@ exprt dereferencet::operator()(const exprt &pointer) const typet &type=pointer.type().subtype(); #ifdef DEBUG - std::cout << "DEREF: " << format(pointer) << '\n'; + std::cout << "DEREF: " << debug_formatter(pointer) << '\n'; #endif return dereference_rec( diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index aea661e5b62..3a5a39dfc0a 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -24,8 +24,7 @@ Author: Daniel Kroening, kroening@kroening.com #ifdef DEBUG #include -#include -#include +#include #endif #include "add_failed_symbols.h" @@ -327,7 +326,7 @@ void value_sett::get_value_set( #if 0 for(value_setst::valuest::const_iterator it=dest.begin(); it!=dest.end(); it++) - std::cout << "GET_VALUE_SET: " << format(*it) << '\n'; + std::cout << "GET_VALUE_SET: " << debug_formatter(*it) << '\n'; #endif } @@ -352,7 +351,7 @@ void value_sett::get_value_set_rec( const namespacet &ns) const { #if 0 - std::cout << "GET_VALUE_SET_REC EXPR: " << format(expr) << "\n"; + std::cout << "GET_VALUE_SET_REC EXPR: " << debug_formatter(expr) << "\n"; std::cout << "GET_VALUE_SET_REC SUFFIX: " << suffix << '\n'; #endif @@ -884,7 +883,7 @@ void value_sett::get_value_set_rec( for(const auto &obj : dest.read()) { const exprt &e=to_expr(obj); - std::cout << " " << format(e) << "\n"; + std::cout << " " << debug_formatter(e) << "\n"; } std::cout << "\n"; #endif @@ -929,7 +928,7 @@ void value_sett::get_reference_set_rec( const namespacet &ns) const { #if 0 - std::cout << "GET_REFERENCE_SET_REC EXPR: " << format(expr) + std::cout << "GET_REFERENCE_SET_REC EXPR: " << debug_formatter(expr) << '\n'; #endif @@ -956,7 +955,7 @@ void value_sett::get_reference_set_rec( #if 0 for(expr_sett::const_iterator it=value_set.begin(); it!=value_set.end(); it++) - std::cout << "VALUE_SET: " << format(*it) << '\n'; + std::cout << "VALUE_SET: " << debug_formatter(*it) << '\n'; #endif return; @@ -1093,10 +1092,10 @@ void value_sett::assign( bool add_to_sets) { #if 0 - std::cout << "ASSIGN LHS: " << format(lhs) << " : " - << format(lhs.type()) << '\n'; - std::cout << "ASSIGN RHS: " << format(rhs) << " : " - << format(rhs.type()) << '\n'; + std::cout << "ASSIGN LHS: " << debug_formatter(lhs) << " : " + << debug_formatter(lhs.type()) << '\n'; + std::cout << "ASSIGN RHS: " << debug_formatter(rhs) << " : " + << debug_formatter(rhs.type()) << '\n'; std::cout << "--------------------------------------------\n"; output(ns, std::cout); #endif @@ -1301,7 +1300,7 @@ void value_sett::assign_rec( bool add_to_sets) { #if 0 - std::cout << "ASSIGN_REC LHS: " << format(lhs) << '\n'; + std::cout << "ASSIGN_REC LHS: " << debug_formatter(lhs) << '\n'; std::cout << "ASSIGN_REC LHS ID: " << lhs.id() << '\n'; std::cout << "ASSIGN_REC SUFFIX: " << suffix << '\n'; @@ -1309,7 +1308,7 @@ void value_sett::assign_rec( it!=values_rhs.read().end(); it++) std::cout << "ASSIGN_REC RHS: " << - format(object_numbering[it->first]) << '\n'; + debug_formatter(object_numbering[it->first]) << '\n'; std::cout << '\n'; #endif diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index 8b2ed99baab..90374651385 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -13,7 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #ifdef DEBUG #include -#include #endif #include @@ -23,7 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include +#include #include #include #include @@ -77,7 +76,7 @@ exprt value_set_dereferencet::dereference( const typet &type=pointer.type().subtype(); #if 0 - std::cout << "DEREF: " << format(pointer) << '\n'; + std::cout << "DEREF: " << debug_formatter(pointer) << '\n'; #endif // collect objects the pointer may point to @@ -90,7 +89,7 @@ exprt value_set_dereferencet::dereference( it=points_to_set.begin(); it!=points_to_set.end(); it++) - std::cout << "P: " << format(*it) << '\n'; + std::cout << "P: " << debug_formatter(*it) << '\n'; #endif // get the values of these @@ -105,8 +104,8 @@ exprt value_set_dereferencet::dereference( valuet value=build_reference_to(*it, mode, pointer, guard); #if 0 - std::cout << "V: " << format(value.pointer_guard) << " --> "; - std::cout << format(value.value) << '\n'; + std::cout << "V: " << debug_formatter(value.pointer_guard) << " --> "; + std::cout << debug_formatter(value.value) << '\n'; #endif values.push_back(value); @@ -191,7 +190,7 @@ exprt value_set_dereferencet::dereference( } #if 0 - std::cout << "R: " << format(value) << "\n\n"; + std::cout << "R: " << debug_formatter(value) << "\n\n"; #endif return value; @@ -281,7 +280,7 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to( const exprt &object=o.object(); #if 0 - std::cout << "O: " << format(root_object) << '\n'; + std::cout << "O: " << debug_formatter(root_object) << '\n'; #endif valuet result; @@ -561,8 +560,8 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to( { std::ostringstream msg; msg << "memory model not applicable (got `" - << format(result.value.type()) << "', expected `" - << format(dereference_type) << "')"; + << debug_formatter(result.value.type()) << "', expected `" + << debug_formatter(dereference_type) << "')"; dereference_callback.dereference_failure( "pointer dereference", msg.str(), tmp_guard); diff --git a/src/solvers/refinement/string_constraint.h b/src/solvers/refinement/string_constraint.h index e72ead2495d..21b19cea2b8 100644 --- a/src/solvers/refinement/string_constraint.h +++ b/src/solvers/refinement/string_constraint.h @@ -23,8 +23,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include "bv_refinement.h" #include "string_refinement_invariant.h" -#include -#include +#include #include #include @@ -140,9 +139,9 @@ extern inline string_constraintt &to_string_constraint(exprt &expr) inline std::string to_string(const string_constraintt &expr) { std::ostringstream out; - out << "forall " << format(expr.univ_var()) << " in [" - << format(expr.lower_bound()) << ", " << format(expr.upper_bound()) - << "). " << format(expr.premise()) << " => " << format(expr.body()); + out << "forall " << debug_formatter(expr.univ_var()) << " in [" + << debug_formatter(expr.lower_bound()) << ", " << debug_formatter(expr.upper_bound()) + << "). " << debug_formatter(expr.premise()) << " => " << debug_formatter(expr.body()); return out.str(); } @@ -212,12 +211,12 @@ class string_not_contains_constraintt : public exprt inline std::string to_string(const string_not_contains_constraintt &expr) { std::ostringstream out; - out << "forall x in [" << format(expr.univ_lower_bound()) << ", " - << format(expr.univ_upper_bound()) << "). " << format(expr.premise()) + out << "forall x in [" << debug_formatter(expr.univ_lower_bound()) << ", " + << debug_formatter(expr.univ_upper_bound()) << "). " << debug_formatter(expr.premise()) << " => (" - << "exists y in [" << format(expr.exists_lower_bound()) << ", " - << format(expr.exists_upper_bound()) << "). " << format(expr.s0()) - << "[x+y] != " << format(expr.s1()) << "[y])"; + << "exists y in [" << debug_formatter(expr.exists_lower_bound()) << ", " + << debug_formatter(expr.exists_upper_bound()) << "). " << debug_formatter(expr.s0()) + << "[x+y] != " << debug_formatter(expr.s1()) << "[y])"; return out.str(); } diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 4fe87dfc7cb..74baaee7ff5 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -19,16 +19,19 @@ Author: Alberto Griggio, alberto.griggio@gmail.com #include -#include -#include -#include #include #include +#include +#include #include + #include #include + +#include +#include +#include #include -#include static bool is_valid_string_constraint( messaget::mstreamt &stream, @@ -190,7 +193,7 @@ static void display_index_set( for(const auto &i : index_set.cumulative) { const exprt &s=i.first; - stream << "IS(" << format(s) << ")=={" << eom; + stream << "IS(" << debug_formatter(s) << ")=={" << eom; for(const auto &j : i.second) { @@ -200,7 +203,7 @@ static void display_index_set( count_current++; stream << "**"; } - stream << " " << format(j) << ";" << eom; + stream << " " << debug_formatter(j) << ";" << eom; count++; } stream << "}" << eom; @@ -324,15 +327,15 @@ static union_find_replacet generate_symbol_resolution_from_equations( const exprt &rhs = eq.rhs(); if(lhs.id()!=ID_symbol) { - stream << log_message << "non symbol lhs: " << format(lhs) - << " with rhs: " << format(rhs) << eom; + stream << log_message << "non symbol lhs: " << debug_formatter(lhs) + << " with rhs: " << debug_formatter(rhs) << eom; continue; } if(lhs.type()!=rhs.type()) { - stream << log_message << "non equal types lhs: " << format(lhs) - << "\n####################### rhs: " << format(rhs) << eom; + stream << log_message << "non equal types lhs: " << debug_formatter(lhs) + << "\n####################### rhs: " << debug_formatter(rhs) << eom; continue; } @@ -365,7 +368,7 @@ static union_find_replacet generate_symbol_resolution_from_equations( else { stream << log_message << "non struct with char pointer subexpr " - << format(rhs) << "\n * of type " << format(rhs.type()) << eom; + << debug_formatter(rhs) << "\n * of type " << debug_formatter(rhs.type()) << eom; } } } @@ -501,8 +504,8 @@ union_find_replacet string_identifiers_resolution_from_equations( if(lhs_strings.empty()) { stream << log_message << "non struct with string subtype " - << format(eq.lhs()) << "\n * of type " - << format(eq.lhs().type()) << eom; + << debug_formatter(eq.lhs()) << "\n * of type " + << debug_formatter(eq.lhs().type()) << eom; } for(const exprt &expr : extract_strings(eq.rhs())) @@ -539,8 +542,8 @@ void output_equations( const namespacet &ns) { for(std::size_t i = 0; i < equations.size(); ++i) - output << " [" << i << "] " << format(equations[i].lhs()) - << " == " << format(equations[i].rhs()) << std::endl; + output << " [" << i << "] " << debug_formatter(equations[i].lhs()) + << " == " << debug_formatter(equations[i].rhs()) << std::endl; } /// Main decision procedure of the solver. Looks for a valuation of variables @@ -621,7 +624,7 @@ decision_proceduret::resultt string_refinementt::dec_solve() #ifdef DEBUG debug() << "symbol resolve:" << eom; for(const auto &pair : symbol_resolve.to_vector()) - debug() << format(pair.first) << " --> " << format(pair.second) << eom; + debug() << debug_formatter(pair.first) << " --> " << debug_formatter(pair.second) << eom; #endif const union_find_replacet string_id_symbol_resolve = @@ -630,7 +633,7 @@ decision_proceduret::resultt string_refinementt::dec_solve() debug() << "symbol resolve string:" << eom; for(const auto &pair : string_id_symbol_resolve.to_vector()) { - debug() << format(pair.first) << " --> " << format(pair.second) << eom; + debug() << debug_formatter(pair.first) << " --> " << debug_formatter(pair.second) << eom; } #endif @@ -678,15 +681,15 @@ decision_proceduret::resultt string_refinementt::dec_solve() debug() << "dec_solve: arrays_of_pointers:" << eom; for(auto pair : generator.array_pool.get_arrays_of_pointers()) { - debug() << " * " << format(pair.first) << "\t--> " << format(pair.second) - << " : " << format(pair.second.type()) << eom; + debug() << " * " << debug_formatter(pair.first) << "\t--> " << debug_formatter(pair.second) + << " : " << debug_formatter(pair.second.type()) << eom; } #endif for(const auto &eq : local_equations) { #ifdef DEBUG - debug() << "dec_solve: set_to " << format(eq) << eom; + debug() << "dec_solve: set_to " << debug_formatter(eq) << eom; #endif supert::set_to(eq, true); } @@ -889,7 +892,7 @@ void string_refinementt::add_lemma( ++it; } - debug() << "adding lemma " << format(simple_lemma) << eom; + debug() << "adding lemma " << debug_formatter(simple_lemma) << eom; prop.l_set_to_true(convert(simple_lemma)); } @@ -922,7 +925,7 @@ static optionalt get_array( if(size_val.id()!=ID_constant) { - stream << "(sr::get_array) string of unknown size: " << format(size_val) + stream << "(sr::get_array) string of unknown size: " << debug_formatter(size_val) << eom; return {}; } @@ -937,8 +940,8 @@ static optionalt get_array( if(n > MAX_CONCRETE_STRING_SIZE) { - stream << "(sr::get_array) long string (size " << format(arr.length()) - << " = " << n << ") " << format(arr) << eom; + stream << "(sr::get_array) long string (size " << debug_formatter(arr.length()) + << " = " << n << ") " << debug_formatter(arr) << eom; stream << "(sr::get_array) consider reducing string-max-input-length so " "that no string exceeds " << MAX_CONCRETE_STRING_SIZE @@ -988,25 +991,25 @@ static exprt get_char_array_and_concretize( { const auto &eom = messaget::eom; static const std::string indent(" "); - stream << "- " << format(arr) << ":\n"; - stream << indent << indent << "- type: " << format(arr.type()) << eom; + stream << "- " << debug_formatter(arr) << ":\n"; + stream << indent << indent << "- type: " << debug_formatter(arr.type()) << eom; const auto arr_model_opt = get_array(super_get, ns, max_string_length, stream, arr); if(arr_model_opt) { - stream << indent << indent << "- char_array: " << format(*arr_model_opt) + stream << indent << indent << "- char_array: " << debug_formatter(*arr_model_opt) << '\n'; - stream << indent << indent << "- type : " << format(arr_model_opt->type()) + stream << indent << indent << "- type : " << debug_formatter(arr_model_opt->type()) << eom; const exprt simple = simplify_expr(*arr_model_opt, ns); - stream << indent << indent << "- simplified_char_array: " << format(simple) + stream << indent << indent << "- simplified_char_array: " << debug_formatter(simple) << eom; if( const auto concretized_array = get_array( super_get, ns, max_string_length, stream, to_array_string_expr(simple))) { stream << indent << indent - << "- concretized_char_array: " << format(*concretized_array) + << "- concretized_char_array: " << debug_formatter(*concretized_array) << eom; if( @@ -1046,21 +1049,21 @@ void debug_model( const exprt model = get_char_array_and_concretize( super_get, ns, max_string_length, stream, arr); - stream << "- " << format(arr) << ":\n" - << indent << "- pointer: " << format(pointer_array.first) << "\n" - << indent << "- model: " << format(model) << messaget::eom; + stream << "- " << debug_formatter(arr) << ":\n" + << indent << "- pointer: " << debug_formatter(pointer_array.first) << "\n" + << indent << "- model: " << debug_formatter(model) << messaget::eom; } for(const auto &symbol : boolean_symbols) { stream << " - " << symbol.get_identifier() << ": " - << format(super_get(symbol)) << '\n'; + << debug_formatter(super_get(symbol)) << '\n'; } for(const auto &symbol : index_symbols) { stream << " - " << symbol.get_identifier() << ": " - << format(super_get(symbol)) << '\n'; + << debug_formatter(super_get(symbol)) << '\n'; } stream << messaget::eom; } @@ -1300,7 +1303,7 @@ static void debug_check_axioms_step( else if(axiom.id() == ID_string_not_contains_constraint) stream << to_string(to_string_not_contains_constraint(axiom)); else - stream << format(axiom); + stream << debug_formatter(axiom); stream << '\n' << indent2 << "- axiom_in_model:\n" << indent2 << indent; if(axiom_in_model.id() == ID_string_constraint) @@ -1308,13 +1311,13 @@ static void debug_check_axioms_step( else if(axiom_in_model.id() == ID_string_not_contains_constraint) stream << to_string(to_string_not_contains_constraint(axiom_in_model)); else - stream << format(axiom_in_model); + stream << debug_formatter(axiom_in_model); stream << '\n' << indent2 << "- negated_axiom:\n" - << indent2 << indent << format(negaxiom) << '\n'; + << indent2 << indent << debug_formatter(negaxiom) << '\n'; stream << indent2 << "- negated_axiom_with_concretized_arrays:\n" - << indent2 << indent << format(with_concretized_arrays) << '\n'; + << indent2 << indent << debug_formatter(with_concretized_arrays) << '\n'; } /// \return true if the current model satisfies all the axioms @@ -1345,7 +1348,7 @@ static std::pair> check_axioms( stream << "symbol_resolve:" << eom; auto pairs = symbol_resolve.to_vector(); for(const auto &pair : pairs) - stream << " - " << format(pair.first) << " --> " << format(pair.second) + stream << " - " << debug_formatter(pair.first) << " --> " << debug_formatter(pair.second) << eom; #ifdef DEBUG @@ -1391,7 +1394,7 @@ static std::pair> check_axioms( find_counter_example(ns, ui, with_concretized_arrays, univ_var)) { stream << indent2 << "- violated_for: " << univ_var.get_identifier() - << "=" << format(*witness) << eom; + << "=" << debug_formatter(*witness) << eom; violated[i]=*witness; } else @@ -1444,7 +1447,7 @@ static std::pair> check_axioms( if(const auto witness = find_counter_example(ns, ui, negaxiom, univ_var)) { stream << indent2 << "- violated_for: " << univ_var.get_identifier() - << "=" << format(*witness) << eom; + << "=" << debug_formatter(*witness) << eom; violated_not_contains[i]=*witness; } } @@ -2273,12 +2276,12 @@ static bool is_valid_string_constraint( const array_index_mapt premise_indices=gather_indices(expr.premise()); if(!premise_indices.empty()) { - stream << "Premise has indices: " << format(expr) << ", map: {"; + stream << "Premise has indices: " << debug_formatter(expr) << ", map: {"; for(const auto &pair : premise_indices) { - stream << format(pair.first) << ": {"; + stream << debug_formatter(pair.first) << ": {"; for(const auto &i : pair.second) - stream << format(i) << ", "; + stream << debug_formatter(i) << ", "; } stream << "}}" << eom; return false; @@ -2298,8 +2301,8 @@ static bool is_valid_string_constraint( const exprt result=simplify_expr(equals, ns); if(result.is_false()) { - stream << "Indices not equal: " << format(expr) - << ", str: " << format(pair.first) << eom; + stream << "Indices not equal: " << debug_formatter(expr) + << ", str: " << debug_formatter(pair.first) << eom; return false; } } @@ -2307,8 +2310,8 @@ static bool is_valid_string_constraint( // Condition 3: f must be linear in the quantified variable if(!is_linear_arithmetic_expr(rep, expr.univ_var())) { - stream << "f is not linear: " << format(expr) - << ", str: " << format(pair.first) << eom; + stream << "f is not linear: " << debug_formatter(expr) + << ", str: " << debug_formatter(pair.first) << eom; return false; } @@ -2316,7 +2319,7 @@ static bool is_valid_string_constraint( // body if(!universal_only_in_index(expr)) { - stream << "Universal variable outside of index:" << format(expr) << eom; + stream << "Universal variable outside of index:" << debug_formatter(expr) << eom; return false; } } diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp index a93df7b75ef..33bca97c660 100644 --- a/src/solvers/refinement/string_refinement_util.cpp +++ b/src/solvers/refinement/string_refinement_util.cpp @@ -6,19 +6,22 @@ \*******************************************************************/ -#include -#include -#include -#include #include #include -#include -#include #include +#include #include #include #include +#include +#include + +#include +#include +#include +#include #include + #include "string_refinement_util.h" /// Applies `f` on all strings contained in `e` that are not if-expressions. @@ -474,7 +477,7 @@ void string_dependenciest::output_dot(std::ostream &stream) const ostream << '"' << builtin_function_nodes[n.index].data->name() << '_' << n.index << '"'; else - ostream << '"' << format(string_nodes[n.index].expr) << '"'; + ostream << '"' << debug_formatter(string_nodes[n.index].expr) << '"'; return ostream.str(); }; stream << "digraph dependencies {\n"; From fdf802ac59203f6298a7fa732e48cff8f02c4f37 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 18 May 2018 12:44:23 +0100 Subject: [PATCH 3/6] formatter for ANSI-C --- src/ansi-c/Makefile | 1 + src/ansi-c/ansi_c_formatter.cpp | 29 +++++++++++++++++++++++++++++ src/ansi-c/ansi_c_formatter.h | 28 ++++++++++++++++++++++++++++ 3 files changed, 58 insertions(+) create mode 100644 src/ansi-c/ansi_c_formatter.cpp create mode 100644 src/ansi-c/ansi_c_formatter.h diff --git a/src/ansi-c/Makefile b/src/ansi-c/Makefile index d57c0934a7d..629233f792a 100644 --- a/src/ansi-c/Makefile +++ b/src/ansi-c/Makefile @@ -2,6 +2,7 @@ SRC = anonymous_member.cpp \ ansi_c_convert_type.cpp \ ansi_c_declaration.cpp \ ansi_c_entry_point.cpp \ + ansi_c_formatter.cpp \ ansi_c_internal_additions.cpp \ ansi_c_language.cpp \ ansi_c_lex.yy.cpp \ diff --git a/src/ansi-c/ansi_c_formatter.cpp b/src/ansi-c/ansi_c_formatter.cpp new file mode 100644 index 00000000000..d564f64d197 --- /dev/null +++ b/src/ansi-c/ansi_c_formatter.cpp @@ -0,0 +1,29 @@ +/*******************************************************************\ + +Module: + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#include "ansi_c_formatter.h" + +#include "expr2c.h" + +#include + +std::ostream &ansi_c_formattert::format(std::ostream &os, const exprt &expr) +{ + return os << expr2c(expr, ns); +} + +std::ostream &ansi_c_formattert::format(std::ostream &os, const typet &type) +{ + return os << type2c(type, ns); +} + +std::ostream & +ansi_c_formattert::format(std::ostream &os, const source_locationt &loc) +{ + return os << loc; +} diff --git a/src/ansi-c/ansi_c_formatter.h b/src/ansi-c/ansi_c_formatter.h new file mode 100644 index 00000000000..e9472e54553 --- /dev/null +++ b/src/ansi-c/ansi_c_formatter.h @@ -0,0 +1,28 @@ +/*******************************************************************\ + +Module: + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#ifndef CPROVER_ANSI_C_FORMATTER_H +#define CPROVER_ANSI_C_FORMATTER_H + +#include + +class ansi_c_formattert : public formattert +{ +public: + explicit ansi_c_formattert(const namespacet &_ns) : ns(_ns) + { + } + + std::ostream &format(std::ostream &, const exprt &) override; + std::ostream &format(std::ostream &, const typet &) override; + std::ostream &format(std::ostream &, const source_locationt &) override; + + const namespacet &ns; +}; + +#endif // CPROVER_ANSI_C_FORMATTER_H From 841d4070ffd735a98cc81d93dba41a7585124f28 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 18 May 2018 13:09:10 +0100 Subject: [PATCH 4/6] formatter for Java --- src/java_bytecode/Makefile | 1 + src/java_bytecode/java_formatter.cpp | 29 ++++++++++++++++++++++++++++ src/java_bytecode/java_formatter.h | 28 +++++++++++++++++++++++++++ 3 files changed, 58 insertions(+) create mode 100644 src/java_bytecode/java_formatter.cpp create mode 100644 src/java_bytecode/java_formatter.h diff --git a/src/java_bytecode/Makefile b/src/java_bytecode/Makefile index 6cb0f1e84b7..d30ff950f8d 100644 --- a/src/java_bytecode/Makefile +++ b/src/java_bytecode/Makefile @@ -22,6 +22,7 @@ SRC = bytecode_info.cpp \ java_class_loader_limit.cpp \ java_enum_static_init_unwind_handler.cpp \ java_entry_point.cpp \ + java_formatter.cpp \ java_local_variable_table.cpp \ java_object_factory.cpp \ java_pointer_casts.cpp \ diff --git a/src/java_bytecode/java_formatter.cpp b/src/java_bytecode/java_formatter.cpp new file mode 100644 index 00000000000..dd20ca939fe --- /dev/null +++ b/src/java_bytecode/java_formatter.cpp @@ -0,0 +1,29 @@ +/*******************************************************************\ + +Module: + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#include "java_formatter.h" + +#include "expr2java.h" + +#include + +std::ostream &java_formattert::format(std::ostream &os, const exprt &expr) +{ + return os << expr2java(expr, ns); +} + +std::ostream &java_formattert::format(std::ostream &os, const typet &type) +{ + return os << type2java(type, ns); +} + +std::ostream & +java_formattert::format(std::ostream &os, const source_locationt &loc) +{ + return os << loc; +} diff --git a/src/java_bytecode/java_formatter.h b/src/java_bytecode/java_formatter.h new file mode 100644 index 00000000000..6106da46ffa --- /dev/null +++ b/src/java_bytecode/java_formatter.h @@ -0,0 +1,28 @@ +/*******************************************************************\ + +Module: + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#ifndef CPROVER_JAVA_FORMATTER_H +#define CPROVER_JAVA_FORMATTER_H + +#include + +class java_formattert : public formattert +{ +public: + explicit java_formattert(const namespacet &_ns) : ns(_ns) + { + } + + std::ostream &format(std::ostream &, const exprt &) override; + std::ostream &format(std::ostream &, const typet &) override; + std::ostream &format(std::ostream &, const source_locationt &) override; + + const namespacet &ns; +}; + +#endif // CPROVER_JAVA_FORMATTER_H From 1e7fb0adbda45ab4b87be4d17a48b832aad1cda0 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 18 May 2018 14:29:59 +0100 Subject: [PATCH 5/6] C++ formatter --- src/cpp/Makefile | 1 + src/cpp/cpp_formatter.cpp | 29 +++++++++++++++++++++++++++++ src/cpp/cpp_formatter.h | 28 ++++++++++++++++++++++++++++ 3 files changed, 58 insertions(+) create mode 100644 src/cpp/cpp_formatter.cpp create mode 100644 src/cpp/cpp_formatter.h diff --git a/src/cpp/Makefile b/src/cpp/Makefile index b98e4766b42..d3a8428449e 100644 --- a/src/cpp/Makefile +++ b/src/cpp/Makefile @@ -6,6 +6,7 @@ SRC = cpp_constructor.cpp \ cpp_destructor.cpp \ cpp_enum_type.cpp \ cpp_exception_id.cpp \ + cpp_formatter.cpp \ cpp_id.cpp \ cpp_instantiate_template.cpp \ cpp_internal_additions.cpp \ diff --git a/src/cpp/cpp_formatter.cpp b/src/cpp/cpp_formatter.cpp new file mode 100644 index 00000000000..e1b58c6d0ca --- /dev/null +++ b/src/cpp/cpp_formatter.cpp @@ -0,0 +1,29 @@ +/*******************************************************************\ + +Module: + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#include "cpp_formatter.h" + +#include "expr2cpp.h" + +#include + +std::ostream &cpp_formattert::format(std::ostream &os, const exprt &expr) +{ + return os << expr2cpp(expr, ns); +} + +std::ostream &cpp_formattert::format(std::ostream &os, const typet &type) +{ + return os << type2cpp(type, ns); +} + +std::ostream & +cpp_formattert::format(std::ostream &os, const source_locationt &loc) +{ + return os << loc; +} diff --git a/src/cpp/cpp_formatter.h b/src/cpp/cpp_formatter.h new file mode 100644 index 00000000000..cc78b1d79d9 --- /dev/null +++ b/src/cpp/cpp_formatter.h @@ -0,0 +1,28 @@ +/*******************************************************************\ + +Module: + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#ifndef CPROVER_CPP_FORMATTER_H +#define CPROVER_CPP_FORMATTER_H + +#include + +class cpp_formattert : public formattert +{ +public: + explicit cpp_formattert(const namespacet &_ns) : ns(_ns) + { + } + + std::ostream &format(std::ostream &, const exprt &) override; + std::ostream &format(std::ostream &, const typet &) override; + std::ostream &format(std::ostream &, const source_locationt &) override; + + const namespacet &ns; +}; + +#endif // CPROVER_CPP_FORMATTER_H From f93fb2cde2498483e17af72703e554dda7af2d5f Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 17 May 2018 10:53:07 +0100 Subject: [PATCH 6/6] use formatter in show_symbol_table --- src/cbmc/cbmc_parse_options.cpp | 5 +- .../goto_instrument_parse_options.cpp | 6 +- src/goto-programs/show_symbol_table.cpp | 86 ++++++++----------- src/goto-programs/show_symbol_table.h | 13 ++- src/jbmc/jbmc_parse_options.cpp | 9 +- 5 files changed, 59 insertions(+), 60 deletions(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 35069fc9665..d4fcf5ac47f 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -25,6 +25,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include @@ -595,7 +596,9 @@ int cbmc_parse_optionst::get_goto_program( if(cmdline.isset("show-symbol-table")) { - show_symbol_table(goto_model, ui_message_handler.get_ui()); + namespacet ns(goto_model.symbol_table); + ansi_c_formattert formatter(ns); + show_symbol_table(goto_model, ui_message_handler.get_ui(), formatter); return CPROVER_EXIT_SUCCESS; } diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index cdfa46f45d9..d44750ddbee 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -21,6 +21,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + #include #include #include @@ -463,7 +465,9 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("show-symbol-table")) { - ::show_symbol_table(goto_model, get_ui()); + namespacet ns(goto_model.symbol_table); + ansi_c_formattert formatter(ns); + ::show_symbol_table(goto_model, get_ui(), formatter); return CPROVER_EXIT_SUCCESS; } diff --git a/src/goto-programs/show_symbol_table.cpp b/src/goto-programs/show_symbol_table.cpp index 771bc88da00..7a8479cf347 100644 --- a/src/goto-programs/show_symbol_table.cpp +++ b/src/goto-programs/show_symbol_table.cpp @@ -19,13 +19,14 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_model.h" -void show_symbol_table_xml_ui() +void show_symbol_table_xml_ui(formattert &) { } void show_symbol_table_brief_plain( const symbol_tablet &symbol_table, - std::ostream &out) + std::ostream &out, + formattert &formatter) { // we want to sort alphabetically std::set symbols; @@ -41,29 +42,17 @@ void show_symbol_table_brief_plain( { const symbolt &symbol=ns.lookup(id); - std::unique_ptr ptr; - - if(symbol.mode=="") - ptr=get_default_language(); - else - { - ptr=get_language_from_mode(symbol.mode); - if(ptr==nullptr) - throw "symbol "+id2string(symbol.name)+" has unknown mode"; - } - - std::string type_str; - if(symbol.type.is_not_nil()) - ptr->from_type(symbol.type, type_str, ns); - - out << symbol.name << " " << type_str << '\n'; + out << symbol.name << " " << formatter(symbol.type) << '\n'; + else + out << symbol.name << '\n'; } } void show_symbol_table_plain( const symbol_tablet &symbol_table, - std::ostream &out) + std::ostream &out, + formattert &formatter) { out << '\n' << "Symbols:" << '\n' << '\n'; @@ -81,35 +70,24 @@ void show_symbol_table_plain( { const symbolt &symbol=ns.lookup(id); - std::unique_ptr ptr; - - if(symbol.mode=="") - { - ptr=get_default_language(); - } - else - { - ptr=get_language_from_mode(symbol.mode); - } - - if(!ptr) - throw "symbol "+id2string(symbol.name)+" has unknown mode"; - std::string type_str, value_str; - if(symbol.type.is_not_nil()) - ptr->from_type(symbol.type, type_str, ns); - - if(symbol.value.is_not_nil()) - ptr->from_expr(symbol.value, value_str, ns); - out << "Symbol......: " << symbol.name << '\n' << std::flush; out << "Pretty name.: " << symbol.pretty_name << '\n'; out << "Module......: " << symbol.module << '\n'; out << "Base name...: " << symbol.base_name << '\n'; out << "Mode........: " << symbol.mode << '\n'; - out << "Type........: " << type_str << '\n'; - out << "Value.......: " << value_str << '\n'; + + out << "Type........: "; + if(symbol.type.is_not_nil()) + out << formatter(symbol.type); + out << '\n'; + + out << "Value.......: "; + if(symbol.value.is_not_nil()) + out << formatter(symbol.value); + out << '\n'; + out << "Flags.......:"; if(symbol.is_lvalue) @@ -146,7 +124,7 @@ void show_symbol_table_plain( out << " volatile"; out << '\n'; - out << "Location....: " << symbol.location << '\n'; + out << "Location....: " << formatter(symbol.location) << '\n'; out << '\n' << std::flush; } @@ -154,16 +132,17 @@ void show_symbol_table_plain( void show_symbol_table( const symbol_tablet &symbol_table, - ui_message_handlert::uit ui) + ui_message_handlert::uit ui, + formattert &formatter) { switch(ui) { case ui_message_handlert::uit::PLAIN: - show_symbol_table_plain(symbol_table, std::cout); + show_symbol_table_plain(symbol_table, std::cout, formatter); break; case ui_message_handlert::uit::XML_UI: - show_symbol_table_xml_ui(); + show_symbol_table_xml_ui(formatter); break; default: @@ -173,23 +152,25 @@ void show_symbol_table( void show_symbol_table( const goto_modelt &goto_model, - ui_message_handlert::uit ui) + ui_message_handlert::uit ui, + formattert &formatter) { - show_symbol_table(goto_model.symbol_table, ui); + show_symbol_table(goto_model.symbol_table, ui, formatter); } void show_symbol_table_brief( const symbol_tablet &symbol_table, - ui_message_handlert::uit ui) + ui_message_handlert::uit ui, + formattert &formatter) { switch(ui) { case ui_message_handlert::uit::PLAIN: - show_symbol_table_brief_plain(symbol_table, std::cout); + show_symbol_table_brief_plain(symbol_table, std::cout, formatter); break; case ui_message_handlert::uit::XML_UI: - show_symbol_table_xml_ui(); + show_symbol_table_xml_ui(formatter); break; default: @@ -199,7 +180,8 @@ void show_symbol_table_brief( void show_symbol_table_brief( const goto_modelt &goto_model, - ui_message_handlert::uit ui) + ui_message_handlert::uit ui, + formattert &formatter) { - show_symbol_table_brief(goto_model.symbol_table, ui); + show_symbol_table_brief(goto_model.symbol_table, ui, formatter); } diff --git a/src/goto-programs/show_symbol_table.h b/src/goto-programs/show_symbol_table.h index 82e49128967..9fcfc546bac 100644 --- a/src/goto-programs/show_symbol_table.h +++ b/src/goto-programs/show_symbol_table.h @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_PROGRAMS_SHOW_SYMBOL_TABLE_H #define CPROVER_GOTO_PROGRAMS_SHOW_SYMBOL_TABLE_H +#include #include class symbol_tablet; @@ -19,18 +20,22 @@ class goto_modelt; void show_symbol_table( const symbol_tablet &, - ui_message_handlert::uit ui); + ui_message_handlert::uit ui, + formattert & = debug_formatter); void show_symbol_table_brief( const symbol_tablet &, - ui_message_handlert::uit ui); + ui_message_handlert::uit ui, + formattert & = debug_formatter); void show_symbol_table( const goto_modelt &, - ui_message_handlert::uit ui); + ui_message_handlert::uit ui, + formattert & = debug_formatter); void show_symbol_table_brief( const goto_modelt &, - ui_message_handlert::uit ui); + ui_message_handlert::uit ui, + formattert & = debug_formatter); #endif // CPROVER_GOTO_PROGRAMS_SHOW_SYMBOL_TABLE_H diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp index 328dc639156..edf92cfb182 100644 --- a/src/jbmc/jbmc_parse_options.cpp +++ b/src/jbmc/jbmc_parse_options.cpp @@ -55,6 +55,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -671,8 +672,10 @@ int jbmc_parse_optionst::get_goto_program( // values, etc if(cmdline.isset("show-symbol-table")) { + const namespacet ns(lazy_goto_model.symbol_table); + java_formattert formatter(ns); show_symbol_table( - lazy_goto_model.symbol_table, ui_message_handler.get_ui()); + lazy_goto_model.symbol_table, ui_message_handler.get_ui(), formatter); return 0; } @@ -850,8 +853,10 @@ bool jbmc_parse_optionst::show_loaded_functions( { if(cmdline.isset("show-symbol-table")) { + namespacet ns(goto_model.get_symbol_table()); + java_formattert formatter(ns); show_symbol_table( - goto_model.get_symbol_table(), ui_message_handler.get_ui()); + goto_model.get_symbol_table(), ui_message_handler.get_ui(), formatter); return true; }