check whether a given state exists before adding dependencies

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

Author: lucasccordeiro

src/analyses/ai.h

@@ -274,6 +274,14 @@ class ait:public ai_baset
     ai_baset::clear();
   }
 
+  // this one just finds states
+  virtual const bool state_exist(locationt l) const
+  {
+    typename state_mapt::const_iterator it=state_map.find(l);
+    if(it==state_map.end()) return false;
+    return true;
+  }
+
 protected:
   typedef hash_map_cont<locationt, domainT, const_target_hash> state_mapt;
   state_mapt state_map;

src/goto-instrument/full_slicer.cpp

@@ -41,14 +41,17 @@ void full_slicert::add_dependencies(
   const dependence_grapht &dep_graph,
   const dep_node_to_cfgt &dep_node_to_cfg)
 {
-  const dependence_grapht::nodet &d_node=
-    dep_graph[dep_graph[node.PC].get_node_id()];
-
-  for(dependence_grapht::edgest::const_iterator
-      it=d_node.in.begin();
-      it!=d_node.in.end();
-      ++it)
-    add_to_queue(queue, dep_node_to_cfg[it->first], node.PC);
+  if (dep_graph.state_exist(node.PC))
+  {
+    const dependence_grapht::nodet &d_node=
+      dep_graph[dep_graph[node.PC].get_node_id()];
+
+    for(dependence_grapht::edgest::const_iterator
+        it=d_node.in.begin();
+        it!=d_node.in.end();
+        ++it)
+      add_to_queue(queue, dep_node_to_cfg[it->first], node.PC);
+  }
 }
 
 /*******************************************************************\