new help formatter and console API

This commit adds a new help formatter, which supports a limited form of
markup to visually distinguish different syntactic elements of the command
line arguments.

Rendering of the syntax highlighting is done via a new console API.

Author: kroening

Diff for: src/cprover/Makefile

@@ -2,7 +2,6 @@ SRC = address_taken.cpp \
       axioms.cpp \
       bv_pointers_wide.cpp \
       c_safety_checks.cpp \
-      console.cpp \
       cprover_main.cpp \
       cprover_parse_options.cpp \
       counterexample_found.cpp \
@@ -13,7 +12,6 @@ SRC = address_taken.cpp \
       format_hooks.cpp \
       free_symbols.cpp \
       generalization.cpp \
-      help_formatter.cpp \
       inductiveness.cpp \
       instrument_contracts.cpp \
       instrument_given_invariants.cpp \

Diff for: src/cprover/cprover_parse_options.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/config.h>
 #include <util/cout_message.h>
 #include <util/exit_codes.h>
+#include <util/help_formatter.h>
 #include <util/options.h>
 #include <util/signal_catcher.h>
 #include <util/ui_message.h>
@@ -35,7 +36,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "c_safety_checks.h"
 #include "format_hooks.h"
-#include "help_formatter.h"
 #include "instrument_contracts.h"
 #include "instrument_given_invariants.h"
 #include "state_encoding.h"

Diff for: src/cprover/generalization.cpp

@@ -11,9 +11,9 @@ Author: Daniel Kroening, [email protected]
 
 #include "generalization.h"
 
+#include <util/console.h>
 #include <util/format_expr.h>
 
-#include "console.h"
 #include "solver.h"
 
 #include <iostream>

Diff for: src/cprover/inductiveness.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 #include "inductiveness.h"
 
 #include <util/arith_tools.h>
+#include <util/console.h>
 #include <util/cout_message.h>
 #include <util/format_expr.h>
 #include <util/simplify_expr.h>
@@ -20,7 +21,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "axioms.h"
 #include "bv_pointers_wide.h"
-#include "console.h"
 #include "counterexample_found.h"
 #include "propagate.h"
 #include "solver.h"

Diff for: src/cprover/propagate.cpp

@@ -11,10 +11,10 @@ Author: Daniel Kroening, [email protected]
 
 #include "propagate.h"
 
+#include <util/console.h>
 #include <util/format_expr.h>
 #include <util/simplify_expr.h>
 
-#include "console.h"
 #include "simplify_state_expr.h"
 #include "state.h"
 

Diff for: src/cprover/report_properties.cpp

@@ -11,10 +11,9 @@ Author: Daniel Kroening, [email protected]
 
 #include "report_properties.h"
 
+#include <util/console.h>
 #include <util/cout_message.h>
 
-#include "console.h"
-
 #include <iomanip>
 
 void report_properties(const std::vector<propertyt> &properties)

Diff for: src/cprover/report_traces.cpp

@@ -11,9 +11,9 @@ Author: Daniel Kroening, [email protected]
 
 #include "report_traces.h"
 
+#include <util/console.h>
 #include <util/format_expr.h>
 
-#include "console.h"
 #include "state.h"
 
 #include <iomanip>

Diff for: src/cprover/solver.cpp

@@ -11,12 +11,12 @@ Author: Daniel Kroening, [email protected]
 
 #include "solver.h"
 
+#include <util/console.h>
 #include <util/cout_message.h>
 #include <util/format_expr.h>
 #include <util/std_expr.h>
 
 #include "address_taken.h"
-#include "console.h"
 #include "counterexample_found.h"
 #include "generalization.h"
 #include "inductiveness.h"

Diff for: src/cprover/solver_progress.cpp

@@ -11,7 +11,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "solver_progress.h"
 
-#include "console.h"
+#include <util/console.h>
 
 #include <iostream>
 

Diff for: src/util/Makefile

@@ -8,6 +8,7 @@ SRC = arith_tools.cpp \
       c_types.cpp \
       cmdline.cpp \
       config.cpp \
+      console.cpp \
       cout_message.cpp \
       dstring.cpp \
       endianness_map.cpp \
@@ -28,6 +29,7 @@ SRC = arith_tools.cpp \
       fresh_symbol.cpp \
       get_base_name.cpp \
       get_module.cpp \
+      help_formatter.cpp \
       identifier.cpp \
       ieee_float.cpp \
       interval_union.cpp \

Diff for: src/cprover/console.cpp renamed to src/util/console.cpp

@@ -227,13 +227,6 @@ std::size_t consolet::width()
   return _width;
 }
 
-extern "C" int mk_wcwidth(wchar_t ucs);
-
-int consolet::wcwidth(wchar_t ucs)
-{
-  return mk_wcwidth(ucs);
-}
-
 consolet::redirectt::redirectt(
   std::ostream &__console_out,
   std::ostream &__console_err)

Diff for: src/cprover/console.h renamed to src/util/console.h

@@ -9,8 +9,8 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Console
 
-#ifndef CPROVER_CPROVER_CONSOLE_H
-#define CPROVER_CPROVER_CONSOLE_H
+#ifndef CPROVER_UTIL_CONSOLE_H
+#define CPROVER_UTIL_CONSOLE_H
 
 #include <cstddef>
 #include <iosfwd>
@@ -66,12 +66,6 @@ class consolet
 
   static std::size_t width();
 
-  // -1: not printable
-  //  0: no width
-  //  1: usual single width
-  //  2: double width
-  static int wcwidth(wchar_t);
-
   // redirection
   class redirectt
   {
@@ -95,4 +89,4 @@ class consolet
   static std::ostream *_err;
 };
 
-#endif // CPROVER_CPROVER_CONSOLE_H
+#endif // CPROVER_UTIL_CONSOLE_H

Diff for: src/cprover/help_formatter.cpp renamed to src/util/help_formatter.cpp

@@ -9,8 +9,8 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Help Formatter
 
-#ifndef CPROVER_CPROVER_HELP_FORMATTER_H
-#define CPROVER_CPROVER_HELP_FORMATTER_H
+#ifndef CPROVER_UTIL_HELP_FORMATTER_H
+#define CPROVER_UTIL_HELP_FORMATTER_H
 
 #include <iosfwd>
 #include <string>
@@ -49,4 +49,4 @@ operator<<(std::ostream &out, const help_formattert &h)
   return out;
 }
 
-#endif // CPROVER_CPROVER_HELP_FORMATTER_H
+#endif // CPROVER_UTIL_HELP_FORMATTER_H