Merge pull request diffblue#414 from diffblue/owen-jones-diffblue/remove-old-command-line-argument

Remove --lvsa-function command line argument

Author: owen-jones-diffblue

src/driver/sec_driver_parse_options.cpp

@@ -241,100 +241,69 @@ int sec_driver_parse_optionst::doit()
       serializer(dbpath, id2string, get_message_handler());
     local_value_set_analysist::dbt summarydb(serializer, 30);
     namespacet ns(goto_model.symbol_table);
-    if(cmdline.isset("lvsa-function"))
+
+    const std::string function_name = cmdline.get_value("function");
+    const bool print_function_summary = cmdline.isset("show-value-sets");
+    const bool print_all_summaries = cmdline.isset("show-value-sets-all");
+
+    irep_idt fully_qualified_name =
+      get_cprover_start_main_callee(goto_model);
+
+    call_grapht const call_graph(goto_model.goto_functions);
+    std::vector<irep_idt> process_order =
+      get_inverse_topological_order(call_graph.get_directed_graph());
+    size_t total_funcs=process_order.size();
+    size_t processed=0;
+    json_objectt json_function_descriptions;
+    for(const auto& fname : process_order)
     {
-      const auto& fname=cmdline.get_value("lvsa-function");
-      if(goto_model.goto_functions.function_map.count(fname) == 0)
-      {
-        error()
-          << "Function '" << fname
-          << "' specified as lvsa-function could not be found" << eom;
-        debug() << "Available functions include:\n";
-        int fnCount = 10;
-        for(auto &f : goto_model.goto_functions.function_map)
-        {
-          if(fnCount-- == 0)
-            break;
-          debug() << " " << f.first.c_str() << "\n";
-        }
-        debug() << eom;
-        return CPROVER_EXIT_INCORRECT_TASK;
-      }
+      ++processed;
+      if(fname=="_start")
+        continue;
+      progress() << "LVSA: analysing " << fname
+                 << "[" << processed << "/" << total_funcs << "]" << eom;
       const auto& gf=goto_model.goto_functions.function_map.at(fname);
+      if(!gf.body_available())
+        continue;
       class_hierarchyt class_hierarchy;
       class_hierarchy(goto_model.symbol_table);
       local_value_set_analysist value_set_analysis(
-        ns, gf.type, fname, summarydb, class_hierarchy);
+        ns, gf.type, id2string(fname), summarydb, class_hierarchy);
       value_set_analysis.set_message_handler(get_message_handler());
       value_set_analysis(gf.body);
-      value_set_analysis.output(gf.body, std::cout);
-      if(dbpath.size()!=0)
-        value_set_analysis.save_summary(gf.body);
-    }
-    else {
-      const std::string function_name = cmdline.get_value("function");
-      const bool print_function_summary = cmdline.isset("show-value-sets");
-      const bool print_all_summaries = cmdline.isset("show-value-sets-all");
-
-      irep_idt fully_qualified_name =
-        get_cprover_start_main_callee(goto_model);
-
-      call_grapht const call_graph(goto_model.goto_functions);
-      std::vector<irep_idt> process_order =
-        get_inverse_topological_order(call_graph.get_directed_graph());
-      size_t total_funcs=process_order.size();
-      size_t processed=0;
-      json_objectt json_function_descriptions;
-      for(const auto& fname : process_order)
+
+      if((print_function_summary && fname == fully_qualified_name) || print_all_summaries)
       {
-        ++processed;
-        if(fname=="_start")
-          continue;
-        progress() << "LVSA: analysing " << fname
-                   << "[" << processed << "/" << total_funcs << "]" << eom;
-        const auto& gf=goto_model.goto_functions.function_map.at(fname);
-        if(!gf.body_available())
-          continue;
-        class_hierarchyt class_hierarchy;
-        class_hierarchy(goto_model.symbol_table);
-        local_value_set_analysist value_set_analysis(
-          ns, gf.type, id2string(fname), summarydb, class_hierarchy);
-        value_set_analysis.set_message_handler(get_message_handler());
-        value_set_analysis(gf.body);
-
-        if((print_function_summary && fname == fully_qualified_name) || print_all_summaries)
+        switch(get_ui())
         {
-          switch(get_ui())
+          case ui_message_handlert::uit::PLAIN:
+          {
+            status() << "*** function " << fname << '\n';
+            value_set_analysis.output(gf.body, status());
+            status() << eom;
+            break;
+          }
+          case ui_message_handlert::uit::JSON_UI:
           {
-            case ui_message_handlert::uit::PLAIN:
-            {
-              status() << "*** function " << fname << '\n';
-              value_set_analysis.output(gf.body, status());
-              status() << eom;
-              break;
-            }
-            case ui_message_handlert::uit::JSON_UI:
-            {
-              json_function_descriptions[id2string(fname)]=
-                value_set_analysis.output_json(gf.body);
-              break;
-            }
-          default:
-            INVARIANT(false, "LVSA summary dump: UI type not handled");
+            json_function_descriptions[id2string(fname)]=
+              value_set_analysis.output_json(gf.body);
+            break;
           }
+        default:
+          INVARIANT(false, "LVSA summary dump: UI type not handled");
         }
-        if(dbpath.size()!=0)
-          value_set_analysis.save_summary(gf.body);
       }
+      if(dbpath.size()!=0)
+        value_set_analysis.save_summary(gf.body);
+    }
 
-      if((print_function_summary || print_all_summaries) &&
-         get_ui()==ui_message_handlert::uit::JSON_UI)
-      {
-        json_objectt dump_message;
-        dump_message["messageType"]=json_stringt("LVSA-ALL-FUNCTIONS-DUMP");
-        dump_message["functions"]=json_function_descriptions;
-        status() << dump_message << eom;
-      }
+    if((print_function_summary || print_all_summaries) &&
+       get_ui()==ui_message_handlert::uit::JSON_UI)
+    {
+      json_objectt dump_message;
+      dump_message["messageType"]=json_stringt("LVSA-ALL-FUNCTIONS-DUMP");
+      dump_message["functions"]=json_function_descriptions;
+      status() << dump_message << eom;
     }
     return CPROVER_EXIT_SUCCESS;
   }
@@ -553,7 +522,6 @@ void sec_driver_parse_optionst::help()
     " --json file_name                 output results in JSON format to given file\n"
     " --xml file_name                  output results in XML format to given file\n"
     " --function                       set main function name\n"
-    " --lvsa-function                  set function to analyze with LVSA\n"
     " --lvsa-summary-directory         directory to store LVSA summaries\n"
     "\n"
     "Java Bytecode frontend options:\n"

src/driver/sec_driver_parse_options.h

@@ -40,7 +40,7 @@ class optionst;
   "(intervals)(show-intervals)" \
   "(non-null)(show-non-null)" \
   "(lvsa-summary-directory):" \
-  "(local-value-set-analysis)(show-value-sets-all)(show-value-sets)(lvsa-function):" \
+  "(local-value-set-analysis)(show-value-sets-all)(show-value-sets)" \
   "(security-scanner):" \
   "(do-not-use-precise-access-paths)" \
   "(rebuild-taint-cache)" \