Pass widening_mode into abstract_environment::merge

Author: jezhiggins

src/analyses/variable-sensitivity/abstract_environment.cpp

@@ -329,7 +329,9 @@ abstract_object_pointert abstract_environmentt::add_object_context(
   return object_factory->wrap_with_context(abstract_object);
 }
 
-bool abstract_environmentt::merge(const abstract_environmentt &env)
+bool abstract_environmentt::merge(
+  const abstract_environmentt &env,
+  wident widen_mode)
 {
   // for each entry in the incoming environment we need to either add it
   // if it is new, or merge with the existing key if it is not present

src/analyses/variable-sensitivity/abstract_environment.h

@@ -32,6 +32,12 @@ class variable_sensitivity_object_factoryt;
 using variable_sensitivity_object_factory_ptrt =
   std::shared_ptr<variable_sensitivity_object_factoryt>;
 
+enum class wident
+{
+  no,
+  should_widen
+};
+
 class abstract_environmentt
 {
 public:
@@ -187,9 +193,10 @@ class abstract_environmentt
   /// Computes the join between "this" and "b"
   ///
   /// \param env: the other environment
+  /// \param widen_mode: indicates if this is a widening merge
   ///
   /// \return A Boolean, true when the merge has changed something
-  virtual bool merge(const abstract_environmentt &env);
+  virtual bool merge(const abstract_environmentt &env, wident widen_mode);
 
   /// This should be used as a default case / everything else has failed
   /// The string is so that I can easily find and diagnose cases where this

src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp

@@ -204,9 +204,9 @@ bool variable_sensitivity_domaint::merge(
   std::cout << "Merging from/to:\n " << from->location_number << " --> "
             << to->location_number << '\n';
 #endif
-
+  auto widen_mode = from->should_widen(*to) ? wident::should_widen : wident::no;
   // Use the abstract_environment merge
-  bool any_changes = abstract_state.merge(b.abstract_state);
+  bool any_changes = abstract_state.merge(b.abstract_state, widen_mode);
 
   DATA_INVARIANT(abstract_state.verify(), "Structural invariant");
   return any_changes;