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
@@ -586,14 +581,15 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
 
   if(options.get_bool_option("general-analysis"))
   {
-
     // Output file factory
     const std::string outfile=options.get_option("outfile");
+
     std::ofstream output_stream;
-    if(!(outfile=="-"))
+    if(outfile != "-" && !outfile.empty())
       output_stream.open(outfile);
 
-    std::ostream &out((outfile=="-") ? std::cout : output_stream);
+    std::ostream &out(
+      (outfile == "-" || outfile.empty()) ? std::cout : output_stream);
 
     if(!out)
     {
@@ -614,7 +610,6 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
       return CPROVER_EXIT_INTERNAL_ERROR;
     }
 
-
     // Run
     status() << "Computing abstract states" << eom;
     (*analyzer)(goto_model);

src/goto-analyzer/static_show_domain.cpp

@@ -45,7 +45,7 @@ bool static_show_domain(
   }
   else
   {
-    INVARIANT(options.get_bool_option("text"), "Other output formats handled");
+    // 'text' or console output
     ai.output(goto_model, 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() << ']'
+                   << ' ';
+
+        m.result() << 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, "

src/goto-analyzer/unreachable_instructions.cpp

@@ -233,8 +233,7 @@ bool static_unreachable_instructions(
       }
       else
       {
-        INVARIANT(options.get_bool_option("text"),
-                  "Other output formats handled");
+        // text or console
         output_dead_plain(ns, f_it->second.body, dead_map, out);
       }
     }
@@ -342,14 +341,13 @@ static void list_functions(
       // this to macros/asm renaming
       continue;
 
-    if(options.get_bool_option("text"))
+    if(options.get_bool_option("json"))
     {
-      os << concat_dir_file(
-              id2string(first_location.get_working_directory()),
-              id2string(first_location.get_file())) << " "
-         << decl.base_name << " "
-         << first_location.get_line() << " "
-         << last_location.get_line() << "\n";
+      json_output_function(
+        decl.base_name,
+        first_location,
+        last_location,
+        json_result);
     }
     else if(options.get_bool_option("xml"))
     {
@@ -360,11 +358,15 @@ static void list_functions(
         xml_result);
     }
     else
-      json_output_function(
-        decl.base_name,
-        first_location,
-        last_location,
-        json_result);
+    {
+      // text or console
+      os << concat_dir_file(
+              id2string(first_location.get_working_directory()),
+              id2string(first_location.get_file())) << " "
+         << decl.base_name << " "
+         << first_location.get_line() << " "
+         << last_location.get_line() << "\n";
+    }
   }
 
   if(options.get_bool_option("json") && !json_result.array.empty())
@@ -381,8 +383,6 @@ void unreachable_functions(
   optionst options;
   if(json)
     options.set_option("json", true);
-  else
-    options.set_option("text", true);
 
   std::unordered_set<irep_idt> called = compute_called_functions(goto_model);
 
@@ -397,8 +397,6 @@ void reachable_functions(
   optionst options;
   if(json)
     options.set_option("json", true);
-  else
-    options.set_option("text", true);
 
   std::unordered_set<irep_idt> called = compute_called_functions(goto_model);