Merge pull request diffblue#257 from diffblue/owen/precise-access-paths

Assorted small improvements to LVSA code

Author: smowton

src/pointer-analysis/local_value_set.cpp

@@ -336,15 +336,15 @@ void local_value_sett::assign(
     // initialiser from an external set that has been read from somewhere
     // and then written.
 
-    std::vector<std::pair<unsigned, exprt>> replacements;
+    std::vector<std::pair<object_numberingt::number_type, exprt>> replacements;
     for(const auto &obj : values_rhs.read())
     {
       const exprt &objexpr=object_numbering[obj.first];
       if(objexpr.id()==ID_external_value_set)
       {
-        external_value_set_exprt mod(
+        external_value_set_exprt evs_non_initializer(
           to_external_value_set(objexpr).as_non_initializer());
-        replacements.push_back({obj.first, mod});
+        replacements.emplace_back(obj.first, evs_non_initializer);
       }
     }
 
@@ -384,8 +384,6 @@ void local_value_sett::assign(
   }
 }
 
-// Note customised cases must return to avoid falling through to
-// value_sett's default behaviour.
 void local_value_sett::assign_rec(
   const exprt &lhs,
   const object_mapt &values_rhs,
@@ -414,7 +412,6 @@ void local_value_sett::assign_rec(
       make_union(e.object_map, values_rhs);
     else
       e.object_map=values_rhs;
-    return;
   }
   else if(lhs.id()==ID_dynamic_object)
   {
@@ -452,7 +449,6 @@ void local_value_sett::assign_rec(
       // Weak-update of the dynamic-object
       make_union(entry.object_map, values_rhs);
     }
-    return;
   }
   else if(lhs.id()==ID_external_value_set)
   {
@@ -467,9 +463,7 @@ void local_value_sett::assign_rec(
       declared_on_type,
       suffix_without_subtype);
     std::string access_path_suffix=
-      suffix_without_subtype == "" ?
-      "[]" :
-      suffix_without_subtype;
+      suffix_without_subtype.empty() ? "[]" : suffix_without_subtype;
     access_path_entry_exprt newentry(
       access_path_suffix,
       function,
@@ -496,11 +490,12 @@ void local_value_sett::assign_rec(
     }
 
     make_union(lhs_entry.object_map, values_rhs);
-    return;
   }
-
-  // For everything else, fall back on default behaviour:
-  baset::assign_rec(lhs, values_rhs, suffix, ns, add_to_sets);
+  else
+  {
+    // For everything else, fall back on default behaviour:
+    baset::assign_rec(lhs, values_rhs, suffix, ns, add_to_sets);
+  }
 }
 
 void local_value_sett::apply_code(