implement get_coverage method

Signed-off-by: Lucas Cordeiro <[email protected]>

Author: lucasccordeiro

src/goto-instrument/Makefile

@@ -37,6 +37,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../langapi/langapi$(LIBEXT) \
       ../xmllang/xmllang$(LIBEXT) \
       ../util/util$(LIBEXT) \
+      ../json/json$(LIBEXT) \
       ../solvers/solvers$(LIBEXT)
 
 INCLUDES= -I ..

src/goto-instrument/cover.cpp

@@ -16,6 +16,8 @@ Date: May 2016
 #include <util/prefix.h>
 #include <util/string2int.h>
 
+#include <json/json_parser.h>
+
 #include "cover.h"
 
 class basic_blockst
@@ -98,6 +100,62 @@ class basic_blockst
 
 /*******************************************************************\
 
+Function: coverage_goalst::get_coverage
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void coverage_goalst::get_coverage(const std::string &coverage,
+                                   message_handlert &message_handler)
+{
+  jsont json;
+
+  //check coverage file
+  if(parse_json(coverage, message_handler, json))
+  {
+    messaget message(message_handler);
+    message.error() << coverage << " file is not a valid json file"
+                    << messaget::eom;
+    exit(0);
+  }
+
+  //make sure that we have an array of elements
+  if(!json.is_array())
+  {
+    messaget message(message_handler);
+    message.error() << "expecting an array in the " <<  coverage << " file, but got "
+                    << json << messaget::eom;
+    exit(0);
+  }
+
+  for(jsont::arrayt::const_iterator
+      it=json.array.begin();
+      it!=json.array.end();
+      it++)
+  {
+    //get the goals array
+    if ((*it)["goals"].is_array())
+	{
+	  for(jsont::arrayt::const_iterator
+	      itg=(*it)["goals"].array.begin();
+	      itg!=(*it)["goals"].array.end();
+	      itg++)
+	  {
+        //get the line of each existing goal
+	    const std::string line=(*itg)["sourceLocation"]["line"].value;
+	    set_goals(line);
+	  }
+	}
+  }
+}
+
+/*******************************************************************\
+
 Function: coverage_goalst::set_goals
 
   Inputs:

src/goto-instrument/cover.h

@@ -16,6 +16,8 @@ Date: May 2016
 class coverage_goalst
 {
 public:
+  void get_coverage(const std::string &coverage,
+                    message_handlert &message_handler);
   void set_goals(std::string goal);
   bool is_existing_goal(source_locationt source_location);
 

src/symex/Makefile

@@ -16,6 +16,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
        ../goto-symex/rewrite_union$(OBJEXT) \
        ../pointer-analysis/dereference$(OBJEXT) \
        ../goto-instrument/cover$(OBJEXT) \
+       ../json/json$(LIBEXT) \
        ../path-symex/path-symex$(LIBEXT)
 
 INCLUDES= -I ..