* src/misc/freelist.cc (free_list::remove): Work around

invalidated iterators.
* tgba/bdddict.cc (unregister_variable): New methods,
extracted from ...
(bdd_dict::unregister_all_my_variables): ... here.
* tgba/bdddict.hh (unregister_variable): Declare them.

ChangeLog

@@ -1,3 +1,12 @@
+2004-03-25  Alexandre Duret-Lutz  <adl@src.lip6.fr>
+
+	* src/misc/freelist.cc (free_list::remove): Work around
+	invalidated iterators.
+	* tgba/bdddict.cc (unregister_variable): New methods,
+	extracted from ...
+	(bdd_dict::unregister_all_my_variables): ... here.
+	* tgba/bdddict.hh (unregister_variable): Declare them.
+
 2004-03-23  Alexandre DURET-LUTZ  <adl@src.lip6.fr>
 
 	* src/misc/freelist.hh (free_list::remove, free_list::insert): New

src/misc/freelist.cc

@@ -131,13 +131,15 @@ namespace spot
   void
   free_list::remove(int base, int n)
   {
-    free_list_type::iterator cur;
+    free_list_type::iterator cur = fl.begin();
     int end = base + n;
-    for (cur = fl.begin(); cur != fl.end() && cur->first <= end; ++cur)
+    while (cur != fl.end() && cur->first <= end)
       {
 	int cend = cur->first + cur->second;
+	// Remove may invalidate the current iterator, so advance it first.
+	free_list_type::iterator old = cur++;
 	if (cend >= end)
-	  remove(cur, base, std::max(n, cend - base));
+	  remove(old, base, std::max(n, cend - base));
       }
   }
 

src/tgba/bdddict.cc

@@ -172,6 +172,76 @@ namespace spot
     free_annonymous_list_of[for_me] = free_annonymous_list_of[from_other];
   }
 
+  void
+  bdd_dict::unregister_variable(int var, const void* me)
+  {
+    vr_map::iterator i = var_refs.find(var);
+    assert(i != var_refs.end());
+    unregister_variable(i, me);
+  }
+
+  void
+  bdd_dict::unregister_variable(vr_map::iterator& cur, const void* me)
+  {
+    ref_set& s = cur->second;
+    ref_set::iterator si = s.find(me);
+    if (si == s.end())
+      return;
+    s.erase(si);
+    if (! s.empty())
+      return;
+
+    // ME was the last user of this variable.
+    // Let's free it.  First, we need to find
+    // if this is a Now, a Var, or an Acc variable.
+    int var = cur->first;
+    int n = 1;
+    const ltl::formula* f = 0;
+    vf_map::iterator vi = var_formula_map.find(var);
+    if (vi != var_formula_map.end())
+      {
+	f = vi->second;
+	var_map.erase(f);
+	var_formula_map.erase(vi);
+      }
+    else
+      {
+	vi = now_formula_map.find(var);
+	if (vi != now_formula_map.end())
+	  {
+	    f = vi->second;
+	    now_map.erase(f);
+	    now_formula_map.erase(vi);
+	    n = 2;
+	    bdd_setpair(next_to_now, var + 1, var + 1);
+	    bdd_setpair(now_to_next, var, var);
+	  }
+	else
+	  {
+	    vi = acc_formula_map.find(var);
+	    if (vi != acc_formula_map.end())
+	      {
+		f = vi->second;
+		acc_map.erase(f);
+		acc_formula_map.erase(vi);
+	      }
+	    else
+	      {
+		free_annonymous_list_of_type::iterator i;
+		for (i = free_annonymous_list_of.begin();
+		     i != free_annonymous_list_of.end(); ++i)
+		  i->second.remove(var, n);
+	      }
+	  }
+      }
+    // Actually release the associated BDD variables, and the
+    // formula itself.
+    release_variables(var, n);
+    if (f)
+      ltl::destroy(f);
+    var_refs.erase(cur);
+  }
+
   void
   bdd_dict::unregister_all_my_variables(const void* me)
   {
@@ -181,62 +251,7 @@ namespace spot
 	// Increment i++ now, we will possibly erase
 	// the current node (which would invalidate the iterator).
 	vr_map::iterator cur = i++;
-
+	unregister_variable(cur, me);
-	ref_set& s = cur->second;
-	ref_set::iterator si = s.find(me);
-	if (si == s.end())
-	  continue;
-	s.erase(si);
-	if (! s.empty())
-	  continue;
-	// ME was the last user of this variable.
-	// Let's free it.  First, we need to find
-	// if this is a Now, a Var, or an Acc variable.
-	int var = cur->first;
-	int n = 1;
-	const ltl::formula* f;
-	vf_map::iterator vi = var_formula_map.find(var);
-	if (vi != var_formula_map.end())
-	  {
-	    f = vi->second;
-	    var_map.erase(f);
-	    var_formula_map.erase(vi);
-	  }
-	else
-	  {
-	    vi = now_formula_map.find(var);
-	    if (vi != now_formula_map.end())
-	      {
-		f = vi->second;
-		now_map.erase(f);
-		now_formula_map.erase(vi);
-		n = 2;
-		bdd_setpair(next_to_now, var + 1, var + 1);
-		bdd_setpair(now_to_next, var, var);
-	      }
-	    else
-	      {
-		vi = acc_formula_map.find(var);
-		if (vi != acc_formula_map.end())
-		  {
-		    f = vi->second;
-		    acc_map.erase(f);
-		    acc_formula_map.erase(vi);
-		  }
-		else
-		  {
-		    free_annonymous_list_of_type::iterator i;
-		    for (i = free_annonymous_list_of.begin();
-			 i != free_annonymous_list_of.end(); ++i)
-		      i->second.remove(var, n);
-		  }
-	      }
-	  }
-	// Actually release the associated BDD variables, and the
-	// formula itself.
-	release_variables(var, n);
-	ltl::destroy(f);
-	var_refs.erase(cur);
       }
     free_annonymous_list_of.erase(me);
   }

src/tgba/bdddict.hh

@@ -135,11 +135,14 @@ namespace spot
     /// is deleted if \a from_other is still alive.
     void register_all_variables_of(const void* from_other, const void* for_me);
 
-    /// \brief Release the variables used by object.
+    /// \brief Release all variables used by an object.
     ///
     /// Usually called in the destructor if \a me.
     void unregister_all_my_variables(const void* me);
 
+    /// \brief Release a variable used by \a me.
+    void unregister_variable(int var, const void* me);
+
     /// @{
     /// Check whether formula \a f has already been registered by \a by_me.
     bool is_registered_proposition(const ltl::formula* f, const void* by_me);
@@ -164,6 +167,7 @@ namespace spot
     typedef Sgi::hash_map<int, ref_set> vr_map;
     vr_map var_refs;
 
+    void unregister_variable(vr_map::iterator& cur, const void* me);
 
     class annon_free_list : public spot::free_list
     {