goto-analyzer: default result report now uses messaget

Splitting 'report into text file' and 'report onto console' enables tweaking
the latter, e.g., by adding colors.

Author: Daniel Kroening

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -178,11 +178,6 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("dot", true);
     options.set_option("outfile", cmdline.get_value("dot"));
   }
-  else
-  {
-    options.set_option("text", true);
-    options.set_option("outfile", "-");
-  }
 
   // The use should either select:
   //  1. a specific analysis, or
@@ -589,11 +584,13 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
 
     // Output file factory
     const std::string outfile=options.get_option("outfile");
+
     std::ofstream output_stream;
-    if(!(outfile=="-"))
+    if(outfile != "-" && outfile != "")
       output_stream.open(outfile);
 
-    std::ostream &out((outfile=="-") ? std::cout : output_stream);
+    std::ostream &out(
+      (outfile == "-" || outfile == "") ? std::cout : output_stream);
 
     if(!out)
     {

src/goto-analyzer/static_verifier.cpp

@@ -143,10 +143,8 @@ bool static_verifier(
     m.status() << "Writing XML report" << messaget::eom;
     out << xml_result;
   }
-  else
+  else if(options.get_bool_option("text"))
   {
-    INVARIANT(options.get_bool_option("text"), "Other output formats handled");
-
     forall_goto_functions(f_it, goto_model.goto_functions)
     {
       m.progress() << "Checking " << f_it->first << messaget::eom;
@@ -203,6 +201,62 @@ bool static_verifier(
       out << '\n';
     }
   }
+  else
+  {
+    forall_goto_functions(f_it, goto_model.goto_functions)
+    {
+      if(!f_it->second.body.has_assertion())
+        continue;
+
+      m.result() << "******** Function " << f_it->first << messaget::eom;
+
+      forall_goto_program_instructions(i_it, f_it->second.body)
+      {
+        if(!i_it->is_assert())
+          continue;
+
+        exprt e(i_it->guard);
+        auto dp = ai.abstract_state_before(i_it);
+        const ai_domain_baset &domain(*dp);
+        domain.ai_simplify(e, ns);
+
+        m.result() << '[' << i_it->source_location.get_property_id() << ']'
+                   << ' ';
+
+        out << i_it->source_location;
+
+        if(!i_it->source_location.get_comment().empty())
+          m.result() << ", " << i_it->source_location.get_comment();
+
+        m.result() << ": ";
+
+        if(e.is_true())
+        {
+          m.result() << "Success";
+          pass++;
+        }
+        else if(e.is_false())
+        {
+          m.result() << "Failure (if reachable)";
+          fail++;
+        }
+        else if(domain.is_bottom())
+        {
+          m.result() << "Success (unreachable)";
+          pass++;
+        }
+        else
+        {
+          m.result() << "Unknown";
+          unknown++;
+        }
+
+        m.result() << messaget::eom;
+      }
+
+      m.result() << messaget::eom;
+    }
+  }
 
   m.status() << "Summary: "
              << pass << " pass, "