From 963b866f3a934b8cb32782b42367b36f7377245b Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 15 Aug 2018 14:58:10 +0100 Subject: [PATCH 1/3] format_expr now produces unicode --- src/util/format_expr.cpp | 31 ++++++++++++++++++++++++++++--- 1 file changed, 28 insertions(+), 3 deletions(-) diff --git a/src/util/format_expr.cpp b/src/util/format_expr.cpp index 0007306c264..7b087990324 100644 --- a/src/util/format_expr.cpp +++ b/src/util/format_expr.cpp @@ -62,6 +62,27 @@ static std::ostream &format_rec(std::ostream &os, const multi_ary_exprt &src) { bool first = true; + std::string operator_str; + + if(src.id() == ID_and) + operator_str = u8"\u2227"; // wedge, U+2227 + else if(src.id() == ID_or) + operator_str = u8"\u2228"; // vee, U+2228 + else if(src.id() == ID_xor) + operator_str = u8"\u2295"; // + in circle, U+2295 + else if(src.id() == ID_le) + operator_str = u8"\u2264"; // <=, U+2264 + else if(src.id() == ID_ge) + operator_str = u8"\u2265"; // >=, U+2265 + else if(src.id() == ID_notequal) + operator_str = u8"\u2260"; // /=, U+2260 + else if(src.id() == ID_implies) + operator_str = u8"\u21d2"; // =>, U+21D2 + else if(src.id() == ID_iff) + operator_str = u8"\u21d4"; // <=>, U+21D4 + else + operator_str = id2string(src.id()); + for(const auto &op : src.operands()) { if(first) @@ -95,7 +116,7 @@ static std::ostream &format_rec(std::ostream &os, const binary_exprt &src) static std::ostream &format_rec(std::ostream &os, const unary_exprt &src) { if(src.id() == ID_not) - os << '!'; + os << u8"\u00ac"; // neg, U+00AC else if(src.id() == ID_unary_minus) os << '-'; else @@ -197,8 +218,12 @@ std::ostream &format_rec(std::ostream &os, const exprt &expr) } else if(id == ID_type) return format_rec(os, expr.type()); - else if(id == ID_forall || id == ID_exists) - return os << id << ' ' << format(to_quantifier_expr(expr).symbol()) << " : " + else if(id == ID_forall) + return os << id << u8" \u2200 : " + << format(to_quantifier_expr(expr).symbol().type()) << " . " + << format(to_quantifier_expr(expr).where()); + else if(id == ID_exists) + return os << id << u8" \u2203 : " << format(to_quantifier_expr(expr).symbol().type()) << " . " << format(to_quantifier_expr(expr).where()); else if(id == ID_let) From f2fa169b73b8de938cd55b7fd0492a66f0467fd4 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 28 Aug 2018 16:22:34 +0100 Subject: [PATCH 2/3] draw Gentzen turnstile using Unicode --- src/cbmc/show_vcc.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/cbmc/show_vcc.cpp b/src/cbmc/show_vcc.cpp index 6a5b051cff9..4f1d699433f 100644 --- a/src/cbmc/show_vcc.cpp +++ b/src/cbmc/show_vcc.cpp @@ -66,7 +66,10 @@ void bmct::show_vcc_plain(std::ostream &out) } } - out << "|--------------------------" << "\n"; + // Unicode equivalent of "|--------------------------" + out << u8"\u251c"; + for(unsigned i=0; i<26; i++) out << u8"\u2500"; + out << '\n'; std::string string_value= from_expr(ns, s_it->source.pc->function, s_it->cond_expr); From 86aea9bc3f0bc2b32d0e07aec549643e3acf0081 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 28 Aug 2018 17:20:12 +0100 Subject: [PATCH 3/3] use status() to output VCCs --- src/cbmc/show_vcc.cpp | 19 ++++++++++++++----- 1 file changed, 14 insertions(+), 5 deletions(-) diff --git a/src/cbmc/show_vcc.cpp b/src/cbmc/show_vcc.cpp index 4f1d699433f..b50eb3df2f6 100644 --- a/src/cbmc/show_vcc.cpp +++ b/src/cbmc/show_vcc.cpp @@ -22,9 +22,8 @@ Author: Daniel Kroening, kroening@kroening.com void bmct::show_vcc_plain(std::ostream &out) { - out << "\n" << "VERIFICATION CONDITIONS:" << "\n" << "\n"; - bool has_threads=equation.has_threads(); + bool first=true; for(symex_target_equationt::SSA_stepst::iterator s_it=equation.SSA_steps.begin(); @@ -34,6 +33,11 @@ void bmct::show_vcc_plain(std::ostream &out) if(!s_it->is_assert()) continue; + if(first) + first=false; + else + out << '\n'; + if(s_it->source.pc->source_location.is_not_nil()) out << s_it->source.pc->source_location << "\n"; @@ -74,8 +78,6 @@ void bmct::show_vcc_plain(std::ostream &out) std::string string_value= from_expr(ns, s_it->source.pc->function, s_it->cond_expr); out << "{" << 1 << "} " << string_value << "\n"; - - out << "\n"; } } @@ -162,7 +164,14 @@ void bmct::show_vcc() break; case ui_message_handlert::uit::PLAIN: - show_vcc_plain(out); + status() << "VERIFICATION CONDITIONS:\n" << eom; + if(have_file) + show_vcc_plain(out); + else + { + show_vcc_plain(status()); + status() << eom; + } break; }