Add clear() to path exploration worklist

Subclasses of path_storaget are now required to implement a clear()
method. This is so that if we terminate path exploration early, the
worklist can be cleared.

This commit facilitates writing tests that ensure that the worklist is
empty iff symbolic execution has finished; this should happen naturally
if symex runs its course over the entire program, but might not happen
if we terminate symex early.

This commit is in preparation for a future commit that makes the
--stop-on-fail flag terminate symbolic execution early.

Author: karkhaz

src/goto-symex/path_storage.cpp

@@ -43,6 +43,11 @@ std::size_t path_lifot::size() const
   return paths.size();
 }
 
+void path_lifot::clear()
+{
+  paths.clear();
+}
+
 // _____________________________________________________________________________
 // path_fifot
 
@@ -69,6 +74,11 @@ std::size_t path_fifot::size() const
   return paths.size();
 }
 
+void path_fifot::clear()
+{
+  paths.clear();
+}
+
 // _____________________________________________________________________________
 // path_strategy_choosert
 

src/goto-symex/path_storage.h

@@ -50,6 +50,14 @@ class path_storaget
     return private_peek();
   }
 
+  /// \brief Clear all saved paths
+  ///
+  /// This is typically used because we want to terminate symbolic execution
+  /// early. It doesn't matter too much in terms of memory usage since CBMC
+  /// typically exits soon after we do that, however it's nice to have tests
+  /// that check that the worklist is always empty when symex finishes.
+  virtual void clear() = 0;
+
   /// \brief Add paths to resume to the storage
   ///
   /// Symbolic execution is suspended when we reach a conditional goto
@@ -90,6 +98,7 @@ class path_lifot : public path_storaget
 public:
   void push(const patht &, const patht &) override;
   std::size_t size() const override;
+  void clear() override;
 
 protected:
   std::list<path_storaget::patht>::iterator last_peeked;
@@ -106,6 +115,7 @@ class path_fifot : public path_storaget
 public:
   void push(const patht &, const patht &) override;
   std::size_t size() const override;
+  void clear() override;
 
 protected:
   std::list<patht> paths;