variable_sensitivity_domaint::to_predicate

Wrapper that calls down into abstract_environmentt::to_predicate

Author: jezhiggins

src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp

@@ -176,6 +176,11 @@ void variable_sensitivity_domaint::output(
   abstract_state.output(out, ai, ns);
 }
 
+exprt variable_sensitivity_domaint::to_predicate() const
+{
+  return abstract_state.to_predicate();
+}
+
 void variable_sensitivity_domaint::make_bottom()
 {
   abstract_state.make_bottom();

src/analyses/variable-sensitivity/variable_sensitivity_domain.h

@@ -146,7 +146,11 @@ class variable_sensitivity_domaint : public ai_domain_baset
   void output(std::ostream &out, const ai_baset &ai, const namespacet &ns)
     const override;
 
-  void output(std::ostream &out) const;
+  /// Gives a Boolean condition that is true for all values represented by the
+  /// domain.  This allows domains to be converted into program invariants.
+  ///
+  /// \return exprt describing the domain
+  exprt to_predicate() const override;
 
   /// Computes the join between "this" and "b".
   ///