diff --git a/src/analyses/Makefile b/src/analyses/Makefile
index 7502f6a..70d78a1 100644
--- a/src/analyses/Makefile
+++ b/src/analyses/Makefile
@@ -2,7 +2,7 @@ SRC = natural_loops.cpp is_threaded.cpp dirty.cpp interval_analysis.cpp \
       invariant_set.cpp invariant_set_domain.cpp invariant_propagation.cpp \
       static_analysis.cpp uninitialized_domain.cpp local_may_alias.cpp \
       locals.cpp goto_check.cpp call_graph.cpp interval_domain.cpp \
-      reaching_definitions.cpp ai.cpp
+      goto_rw.cpp reaching_definitions.cpp ai.cpp may_alias.cpp
 
 INCLUDES= -I ..
 
diff --git a/src/analyses/cfg_dominators.h b/src/analyses/cfg_dominators.h
index c48d3cd..f297ac0 100644
--- a/src/analyses/cfg_dominators.h
+++ b/src/analyses/cfg_dominators.h
@@ -16,6 +16,7 @@ Author: Georg Weissenbacher, georg@weissenbacher.name
 
 #include <goto-programs/goto_functions.h>
 #include <goto-programs/goto_program.h>
+#include <goto-programs/cfg.h>
 
 template<class P, class T>
 class cfg_dominators_templatet
@@ -26,13 +27,10 @@ public:
   struct nodet
   {
     target_sett dominators;
-    std::list<T> successors, predecessors;
-
-    T PC;
   };
 
-  typedef std::map<T, nodet> node_mapt;
-  node_mapt node_map;
+  typedef procedure_local_cfg_baset<nodet, P, T> cfgt;
+  cfgt cfg;
 
   void operator()(P &program);
 
@@ -43,8 +41,6 @@ public:
 
 protected:
   void initialise(P &program);
-  void construct_cfg(P &program);
-  void construct_cfg(P &program, T PC);
   void fixedpoint(P &program);
 };
 
@@ -69,88 +65,47 @@ std::ostream &operator << (
   return out;
 }
 
-template<class P, class T>
-void cfg_dominators_templatet<P, T>::operator()(P &program)
-{
-  initialise(program);
-  fixedpoint(program);
-}
-
 /*******************************************************************\
 
-Function: cfg_dominators_templatet::initialise
+Function: operator ()
 
   Inputs:
 
  Outputs:
 
- Purpose: Initialises the elements of the fixed point analysis
+ Purpose: Compute dominators
 
 \*******************************************************************/
 
 template<class P, class T>
-void cfg_dominators_templatet<P, T>::initialise(P &program)
+void cfg_dominators_templatet<P, T>::operator()(P &program)
 {
-  construct_cfg(program);
-
-  // initialise top element
-  for(typename node_mapt::const_iterator e_it=node_map.begin();
-      e_it!=node_map.end(); ++e_it)
-    top.insert(e_it->first);
+  initialise(program);
+  fixedpoint(program);
 }
 
 /*******************************************************************\
 
-Function: cfg_dominators_templatet::construct_cfg
+Function: cfg_dominators_templatet::initialise
 
   Inputs:
 
  Outputs:
 
- Purpose: Initialises the predecessor and successor sets
+ Purpose: Initialises the elements of the fixed point analysis
 
 \*******************************************************************/
 
 template<class P, class T>
-void cfg_dominators_templatet<P, T>::construct_cfg(P &program)
-{
-  for(T it = program.instructions.begin();
-      it != program.instructions.end();
-      ++it)
-  {
-    construct_cfg(program, it);
-  }
-}
-
-/*******************************************************************\
-
-Function: cfg_dominators_templatet::construct_cfg
-
-  Inputs:
-
- Outputs:
-
- Purpose: Initialises the predecessor and successor sets
-
-\*******************************************************************/
-
-template <class P, class T>
-void cfg_dominators_templatet<P, T>::construct_cfg(P &program, T PC)
+void cfg_dominators_templatet<P, T>::initialise(P &program)
 {
-  nodet &node=node_map[PC];
-  node.PC=PC;
-  
-  program.get_successors(PC, node.successors);
-
-  // now do backward edges
-  for(typename std::list<T>::const_iterator
-      s_it=node.successors.begin();
-      s_it!=node.successors.end();
-      s_it++)
-  {
-    node_map[*s_it].predecessors.push_back(node.PC);
-  }
+  cfg(program);
 
+  // initialise top element
+  for(typename cfgt::entry_mapt::const_iterator
+      e_it=cfg.entry_map.begin();
+      e_it!=cfg.entry_map.end(); ++e_it)
+    top.insert(cfg[e_it->second].PC);
 }
 
 /*******************************************************************\
@@ -171,14 +126,14 @@ void cfg_dominators_templatet<P, T>::fixedpoint(P &program)
   std::list<T> worklist;
 
   entry_node = program.instructions.begin();
-  nodet &n=node_map[entry_node];
+  typename cfgt::nodet &n=cfg[cfg.entry_map[entry_node]];
   n.dominators.insert(entry_node);
 
-  for(typename std::list<T>::const_iterator 
-      s_it=n.successors.begin();
-      s_it!=n.successors.end();
+  for(typename cfgt::edgest::const_iterator 
+      s_it=n.out.begin();
+      s_it!=n.out.end();
       ++s_it)
-    worklist.push_back(*s_it);
+    worklist.push_back(cfg[s_it->first].PC);
 
   while(!worklist.empty())
   {
@@ -187,26 +142,26 @@ void cfg_dominators_templatet<P, T>::fixedpoint(P &program)
     worklist.pop_front();
 
     bool changed=false;
-    nodet &node=node_map[current];
+    typename cfgt::nodet &node=cfg[cfg.entry_map[current]];
     if(node.dominators.empty())
-      for(typename std::list<T>::const_iterator 
-          p_it=node.predecessors.begin();
-          !changed && p_it!=node.predecessors.end();
+      for(typename cfgt::edgest::const_iterator 
+          p_it=node.in.begin();
+          !changed && p_it!=node.in.end();
           ++p_it)
-        if(!node_map[*p_it].dominators.empty())
+        if(!cfg[p_it->first].dominators.empty())
         {
-          node.dominators=node_map[*p_it].dominators;
+          node.dominators=cfg[p_it->first].dominators;
           node.dominators.insert(current);
           changed=true;
         }
 
     // compute intersection of predecessors
-    for(typename std::list<T>::const_iterator 
-          p_it=node.predecessors.begin();
-        p_it!=node.predecessors.end();
+    for(typename cfgt::edgest::const_iterator 
+          p_it=node.in.begin();
+        p_it!=node.in.end();
         ++p_it)
     {   
-      const target_sett &other=node_map[*p_it].dominators;
+      const target_sett &other=cfg[p_it->first].dominators;
       if(other.empty())
         continue;
 
@@ -236,12 +191,12 @@ void cfg_dominators_templatet<P, T>::fixedpoint(P &program)
 
     if(changed) // fixed point for node reached?
     {
-      for(typename std::list<T>::const_iterator 
-            s_it=node.successors.begin();
-          s_it!=node.successors.end();
+      for(typename cfgt::edgest::const_iterator 
+            s_it=node.out.begin();
+          s_it!=node.out.end();
           ++s_it)
       {
-        worklist.push_back(*s_it);
+        worklist.push_back(cfg[s_it->first].PC);
       }
     }
   }
@@ -262,8 +217,9 @@ Function: cfg_dominators_templatet::output
 template <class P, class T>
 void cfg_dominators_templatet<P, T>::output(std::ostream &out) const
 {
-  for(typename node_mapt::const_iterator it=node_map.begin();
-      it!=node_map.end(); ++it)
+  for(typename cfgt::entry_mapt::const_iterator
+      it=cfg.entry_map.begin();
+      it!=cfg.entry_map.end(); ++it)
   {
     unsigned n=it->first->location_number;
     
diff --git a/src/analyses/dirty.h b/src/analyses/dirty.h
index 4b936b7..8be3f37 100644
--- a/src/analyses/dirty.h
+++ b/src/analyses/dirty.h
@@ -24,6 +24,12 @@ public:
     build(goto_function);
   }
 
+  explicit dirtyt(const goto_functionst &goto_functions)
+  {
+    forall_goto_functions(it, goto_functions)
+      build(it->second);
+  }
+
   void output(std::ostream &out) const;
 
   // will go away, use below  
diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index 97e6fb5..19e8646 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -1347,7 +1347,7 @@ void goto_checkt::goto_check(goto_functiont &goto_function)
 {
   assertions.clear();
   
-  local_may_aliast local_may_alias_obj(goto_function);
+  local_may_aliast local_may_alias_obj(goto_function, ns);
   local_may_alias=&local_may_alias_obj;
 
   goto_programt &goto_program=goto_function.body;
diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp
new file mode 100644
index 0000000..2f8e97f
--- /dev/null
+++ b/src/analyses/goto_rw.cpp
@@ -0,0 +1,1089 @@
+/*******************************************************************\
+
+Module: 
+
+Author: Daniel Kroening
+
+Date: April 2010
+
+\*******************************************************************/
+
+#include <limits>
+
+#include <util/std_code.h>
+#include <util/std_expr.h>
+#include <util/pointer_offset_size.h>
+#include <util/byte_operators.h>
+#include <util/arith_tools.h>
+
+#include <goto-programs/goto_functions.h>
+
+#include <analyses/may_alias.h>
+#include <pointer-analysis/goto_program_dereference.h>
+
+#include "goto_rw.h"
+
+/*******************************************************************\
+
+Function: range_domain_baset::~range_domain_baset
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+range_domain_baset::~range_domain_baset()
+{
+}
+
+/*******************************************************************\
+
+Function: range_domaint::output
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void range_domaint::output(
+  const namespacet &ns, std::ostream &out) const
+{
+  out << "[";
+  for(const_iterator itr=begin();
+      itr!=end();
+      ++itr)
+  {
+    if(itr!=begin()) out << ";";
+    out << itr->first << ":" << itr->second;
+  }
+  out << "]";
+}
+
+/*******************************************************************\
+
+Function: rw_range_sett::~rw_range_sett
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+rw_range_sett::~rw_range_sett()
+{
+  for(rw_range_sett::objectst::iterator it=r_range_set.begin();
+      it!=r_range_set.end();
+      ++it)
+    delete it->second;
+
+  for(rw_range_sett::objectst::iterator it=w_range_set.begin();
+      it!=w_range_set.end();
+      ++it)
+    delete it->second;
+}
+
+/*******************************************************************\
+
+Function: rw_range_sett::output
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void rw_range_sett::output(std::ostream &out) const
+{
+  out << "READ:" << std::endl;
+  forall_rw_range_set_r_objects(it, *this)
+  {
+    out << "  " << it->first;
+    it->second->output(ns, out);
+    out << std::endl;
+  }
+
+  out << std::endl;
+
+  out << "WRITE:" << std::endl;
+  forall_rw_range_set_w_objects(it, *this)
+  {
+    out << "  " << it->first;
+    it->second->output(ns, out);
+    out << std::endl;
+  }
+}
+
+/*******************************************************************\
+
+Function: rw_range_sett::get_objects_complex
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void rw_range_sett::get_objects_complex(
+  get_modet mode,
+  const exprt &expr,
+  const mp_integer &range_start,
+  const mp_integer &size)
+{
+  const exprt &op=expr.op0();
+  assert(op.type().id()==ID_complex);
+
+  mp_integer sub_size=pointer_offset_size(ns, op.type().subtype());
+  mp_integer offset=
+    (range_start==-1 || expr.id()==ID_complex_real) ? 0 : sub_size;
+
+  get_objects_rec(mode, op, range_start+offset, size);
+}
+
+/*******************************************************************\
+
+Function: rw_range_sett::get_objects_if
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void rw_range_sett::get_objects_if(
+  get_modet mode,
+  const if_exprt &if_expr,
+  const mp_integer &range_start,
+  const mp_integer &size)
+{
+  if(if_expr.cond().is_false())
+    get_objects_rec(mode, if_expr.false_case(), range_start, size);
+  else if(if_expr.cond().is_true())
+    get_objects_rec(mode, if_expr.true_case(), range_start, size);
+  else
+  {
+    get_objects_rec(READ, if_expr.cond());
+
+    get_objects_rec(mode, if_expr.false_case(), range_start, size);
+    get_objects_rec(mode, if_expr.true_case(), range_start, size);
+  }
+}
+
+/*******************************************************************\
+
+Function: rw_range_sett::get_objects_dereference
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void rw_range_sett::get_objects_dereference(
+  get_modet mode,
+  const dereference_exprt &deref,
+  const mp_integer &range_start,
+  const mp_integer &size)
+{
+  const exprt &pointer=deref.pointer();
+  get_objects_rec(READ, pointer);
+}
+
+/*******************************************************************\
+
+Function: rw_range_sett::get_objects_byte_extract
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void rw_range_sett::get_objects_byte_extract(
+  get_modet mode,
+  const byte_extract_exprt &be,
+  const mp_integer &range_start,
+  const mp_integer &size)
+{
+  mp_integer index;
+  if(range_start==-1 || to_integer(be.offset(), index))
+    get_objects_rec(mode, be.op(), -1, size);
+  else
+  {
+    endianness_mapt map(
+      be.op().type(),
+      be.id()==ID_byte_extract_little_endian,
+      ns);
+    assert(index<std::numeric_limits<unsigned>::max());
+    mp_integer offset=range_start + map.map_byte(integer2long(index));
+    get_objects_rec(mode, be.op(), offset, size);
+  }
+}
+
+/*******************************************************************\
+
+Function: rw_range_sett::get_objects_shift
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void rw_range_sett::get_objects_shift(
+  get_modet mode,
+  const shift_exprt &shift,
+  const mp_integer &range_start,
+  const mp_integer &size)
+{
+  mp_integer src_size=pointer_offset_size(ns, shift.op().type());
+
+  mp_integer dist;
+  if(range_start==-1 ||
+     size==-1 ||
+     src_size==-1 ||
+     to_integer(shift.distance(), dist))
+  {
+    get_objects_rec(mode, shift.op(), -1, -1);
+    get_objects_rec(mode, shift.distance(), -1, -1);
+  }
+  else
+  {
+    dist/=8;
+
+    // not sure whether to worry about
+    // config.ansi_c.endianness==configt::ansi_ct::IS_LITTLE_ENDIAN
+    // right here maybe?
+
+    if(shift.id()==ID_ashr || shift.id()==ID_lshr)
+    {
+      mp_integer sh_range_start=range_start;
+      sh_range_start+=dist;
+
+      mp_integer sh_size=std::min(size, src_size-sh_range_start);
+
+      if(sh_range_start>=0 && sh_range_start<src_size)
+        get_objects_rec(mode, shift.op(), sh_range_start, sh_size);
+    }
+    else
+    {
+      assert(src_size-dist>=0);
+      mp_integer sh_size=std::min(size, src_size-dist);
+
+      get_objects_rec(mode, shift.op(), range_start, sh_size);
+    }
+  }
+}
+
+/*******************************************************************\
+
+Function: rw_range_sett::get_objects_member
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void rw_range_sett::get_objects_member(
+  get_modet mode,
+  const member_exprt &expr,
+  const mp_integer &range_start,
+  const mp_integer &size)
+{
+  const typet &type=ns.follow(expr.struct_op().type());
+
+  if(type.id()==ID_union ||
+     range_start==-1)
+  {
+    get_objects_rec(mode, expr.struct_op(), range_start, size);
+    return;
+  }
+
+  const struct_typet &struct_type=to_struct_type(type);
+  const struct_typet::componentt &comp=
+    struct_type.get_component(expr.get_component_name());
+
+  mp_integer offset=
+    member_offset(
+      ns,
+      struct_type,
+      expr.get_component_name());
+
+  if(offset==-1 ||
+     comp.get_is_bit_field())
+    get_objects_rec(mode, expr.struct_op(), -1, size);
+  else
+  {
+    offset+=range_start;
+    get_objects_rec(mode, expr.struct_op(), offset, size);
+  }
+}
+
+/*******************************************************************\
+
+Function: rw_range_sett::get_objects_index
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void rw_range_sett::get_objects_index(
+  get_modet mode,
+  const index_exprt &expr,
+  const mp_integer &range_start,
+  const mp_integer &size)
+{
+  const array_typet &array_type=
+    to_array_type(ns.follow(expr.array().type()));
+
+  mp_integer sub_size=
+    pointer_offset_size(ns, array_type.subtype());
+
+  mp_integer index;
+  if(to_integer(expr.index(), index))
+  {
+    get_objects_rec(READ, expr.index());
+    index=-1;
+  }
+
+  if(range_start==-1 ||
+     sub_size==-1 ||
+     index==-1)
+    get_objects_rec(mode, expr.array(), -1, size);
+  else
+    get_objects_rec(
+      mode,
+      expr.array(),
+      range_start+(index*sub_size),
+      size);
+}
+
+/*******************************************************************\
+
+Function: rw_range_sett::get_objects_array
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void rw_range_sett::get_objects_array(
+  get_modet mode,
+  const array_exprt &expr,
+  const mp_integer &range_start,
+  const mp_integer &size)
+{
+  const array_typet &array_type=
+    to_array_type(ns.follow(expr.type()));
+
+  mp_integer sub_size=
+    pointer_offset_size(ns, array_type.subtype());
+
+  if(sub_size==-1)
+  {
+    forall_operands(it, expr)
+      get_objects_rec(mode, *it, 0, -1);
+
+    return;
+  }
+
+  mp_integer offset=0;
+  mp_integer full_r_s=range_start==-1 ? 0 : range_start;
+  mp_integer full_r_e=
+    size==-1 ? sub_size*expr.operands().size() : full_r_s+size;
+
+  forall_operands(it, expr)
+  {
+    if(full_r_s<=offset+sub_size && full_r_e>offset)
+    {
+      mp_integer cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset;
+      mp_integer cur_r_e=
+        full_r_e>offset+sub_size ? sub_size : full_r_e-offset;
+
+      get_objects_rec(mode, *it, cur_r_s, cur_r_e-cur_r_s);
+    }
+
+    offset+=sub_size;
+  }
+}
+
+/*******************************************************************\
+
+Function: rw_range_sett::get_objects_struct
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void rw_range_sett::get_objects_struct(
+  get_modet mode,
+  const struct_exprt &expr,
+  const mp_integer &range_start,
+  const mp_integer &size)
+{
+  const struct_typet &struct_type=
+    to_struct_type(ns.follow(expr.type()));
+
+  mp_integer full_size=pointer_offset_size(ns, struct_type);
+
+  mp_integer offset=0;
+  mp_integer full_r_s=range_start==-1 ? 0 : range_start;
+  mp_integer full_r_e=size==-1 || full_size==-1 ? -1 : full_r_s+size;
+
+  forall_operands(it, expr)
+  {
+    mp_integer sub_size=pointer_offset_size(ns, it->type());
+
+    if(offset==-1)
+    {
+      get_objects_rec(mode, *it, 0, sub_size);
+    }
+    else if(sub_size==-1)
+    {
+      if(full_r_e==-1 || full_r_e>offset)
+      {
+        mp_integer cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset;
+
+        get_objects_rec(mode, *it, cur_r_s, -1);
+      }
+
+      offset=-1;
+    }
+    else if(full_r_e==-1)
+    {
+      if(full_r_s<=offset+sub_size)
+      {
+        mp_integer cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset;
+
+        get_objects_rec(mode, *it, cur_r_s, sub_size-cur_r_s);
+      }
+
+      offset+=sub_size;
+    }
+    else if(full_r_s<=offset+sub_size && full_r_e>offset)
+    {
+      mp_integer cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset;
+      mp_integer cur_r_e=
+        full_r_e>offset+sub_size ? sub_size : full_r_e-offset;
+
+      get_objects_rec(mode, *it, cur_r_s, cur_r_e-cur_r_s);
+
+      offset+=sub_size;
+    }
+  }
+}
+
+/*******************************************************************\
+
+Function: rw_range_sett::get_objects_typecast
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void rw_range_sett::get_objects_typecast(
+  get_modet mode,
+  const typecast_exprt &tc,
+  const mp_integer &range_start,
+  const mp_integer &size)
+{
+  const exprt& op=tc.op();
+
+  mp_integer new_size=pointer_offset_size(ns, op.type());
+  if(range_start==-1)
+    new_size=-1;
+  else if(new_size!=-1)
+  {
+    if(new_size<range_start)
+      return;
+
+    new_size-=range_start;
+    new_size=std::min(size, new_size);
+  }
+
+  get_objects_rec(mode, op, range_start, new_size);
+}
+
+/*******************************************************************\
+
+Function: rw_range_sett::get_objects_address_of
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void rw_range_sett::get_objects_address_of(const exprt &object)
+{
+  if(object.id()==ID_symbol ||
+     object.id()==ID_string_constant ||
+     object.id()==ID_label ||
+     object.id()==ID_array)
+    // constant, nothing to do
+    return;
+  else if(object.id()==ID_dereference)
+    get_objects_rec(READ, object);
+  else if(object.id()==ID_index)
+  {
+    const index_exprt &index=to_index_expr(object);
+
+    get_objects_rec(READ, address_of_exprt(index.array()));
+    get_objects_rec(READ, index.index());
+  }
+  else if(object.id()==ID_member)
+  {
+    const member_exprt &member=to_member_expr(object);
+
+    get_objects_rec(READ, address_of_exprt(member.struct_op()));
+  }
+  else if(object.id()==ID_if)
+  {
+    const if_exprt &if_expr=to_if_expr(object);
+
+    get_objects_rec(READ, if_expr.cond());
+    get_objects_rec(READ, address_of_exprt(if_expr.true_case()));
+    get_objects_rec(READ, address_of_exprt(if_expr.false_case()));
+  }
+  else if(object.id()==ID_byte_extract_little_endian ||
+          object.id()==ID_byte_extract_big_endian)
+  {
+    const byte_extract_exprt &be=to_byte_extract_expr(object);
+
+    get_objects_rec(READ, address_of_exprt(be.op()));
+  }
+  else if(object.id()==ID_typecast)
+  {
+    const typecast_exprt &tc=to_typecast_expr(object);
+
+    get_objects_rec(READ, address_of_exprt(tc.op()));
+  }
+  else
+    throw "rw_range_sett: address_of `"+object.id_string()+"' not handled";
+}
+
+/*******************************************************************\
+
+Function: rw_range_sett::add
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void rw_range_sett::add(
+  get_modet mode,
+  const irep_idt &identifier,
+  const mp_integer &range_start,
+  const mp_integer &range_end)
+{
+  objectst::iterator entry=(mode==LHS_W ? w_range_set : r_range_set).
+    insert(std::make_pair<irep_idt, range_domain_baset*>(identifier, 0)).first;
+
+  if(entry->second==0)
+    entry->second=new range_domaint();
+
+  static_cast<range_domaint*>(entry->second)->insert(
+    std::make_pair(range_start, range_end));
+}
+
+/*******************************************************************\
+
+Function: rw_range_sett::get_objects_rec
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void rw_range_sett::get_objects_rec(
+  get_modet mode,
+  const exprt &expr,
+  const mp_integer &range_start,
+  const mp_integer &size)
+{
+  if(expr.id()==ID_complex_real ||
+     expr.id()==ID_complex_imag)
+    get_objects_complex(mode, expr, range_start, size);
+  else if(expr.id()==ID_typecast)
+    get_objects_typecast(
+      mode,
+      to_typecast_expr(expr),
+      range_start,
+      size);
+  else if(expr.id()==ID_if)
+    get_objects_if(mode, to_if_expr(expr), range_start, size);
+  else if(expr.id()==ID_dereference)
+    get_objects_dereference(
+      mode,
+      to_dereference_expr(expr),
+      range_start,
+      size);
+  else if(expr.id()==ID_byte_extract_little_endian ||
+          expr.id()==ID_byte_extract_big_endian)
+    get_objects_byte_extract(
+      mode,
+      to_byte_extract_expr(expr),
+      range_start,
+      size);
+  else if(expr.id()==ID_shl ||
+          expr.id()==ID_ashr ||
+          expr.id()==ID_lshr)
+    get_objects_shift(mode, to_shift_expr(expr), range_start, size);
+  else if(expr.id()==ID_member)
+    get_objects_member(mode, to_member_expr(expr), range_start, size);
+  else if(expr.id()==ID_index)
+    get_objects_index(mode, to_index_expr(expr), range_start, size);
+  else if(expr.id()==ID_array)
+    get_objects_array(mode, to_array_expr(expr), range_start, size);
+  else if(expr.id()==ID_struct)
+    get_objects_struct(mode, to_struct_expr(expr), range_start, size);
+  else if(expr.id()==ID_symbol)
+  {
+    const symbol_exprt &symbol=to_symbol_expr(expr);
+    const irep_idt identifier=symbol.get_identifier();
+    mp_integer full_size=pointer_offset_size(ns, symbol.type());
+
+    if(full_size==0)
+    {
+      // nothing to do, these are effectively constants (like function
+      // symbols or structs with no members)
+    }
+    else if(range_start>=0)
+    {
+      mp_integer range_end=size==-1 ? -1 : range_start+size;
+      assert(full_size==-1 || range_end<=full_size);
+
+      add(mode, identifier, range_start, range_end);
+    }
+    else
+      add(mode, identifier, 0, full_size);
+  }
+  else if(mode==READ && expr.id()==ID_address_of)
+    get_objects_address_of(to_address_of_expr(expr).object());
+  else if(mode==READ)
+  {
+    // possibly affects the full object size, even if range_start/size
+    // are only a subset of the bytes (e.g., when using the result of
+    // arithmetic operations)
+    forall_operands(it, expr)
+      get_objects_rec(mode, *it);
+  }
+  else
+    throw "rw_range_sett: assignment to `"+expr.id_string()+"' not handled";
+}
+
+/*******************************************************************\
+
+Function: rw_range_sett::get_objects_rec
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void rw_range_sett::get_objects_rec(get_modet mode, const exprt &expr)
+{
+  mp_integer size=pointer_offset_size(ns, expr.type());
+  get_objects_rec(mode, expr, 0, size);
+}
+
+/*******************************************************************\
+
+Function: rw_range_set_dereft::get_objects_dereference
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void rw_range_set_dereft::get_objects_dereference(
+  get_modet mode,
+  const dereference_exprt &deref,
+  const mp_integer &range_start,
+  const mp_integer &size)
+{
+  rw_range_sett::get_objects_dereference(
+    mode,
+    deref,
+    range_start,
+    size);
+
+  const exprt &pointer=deref.pointer();
+  std::set<exprt> alias_set=may_alias.get(target, pointer);
+
+  for(std::set<exprt>::const_iterator it=alias_set.begin();
+      it!=alias_set.end();
+      it++)
+    if(it->id()!=ID_unknown &&
+       it->id()!=ID_dynamic_object &&
+       it->id()!=ID_null_object &&
+       it->id()!=ID_integer_address_object)
+    {
+      mp_integer new_size=pointer_offset_size(ns, it->type());
+      if(range_start==-1 || new_size<=range_start)
+        new_size=-1;
+      else
+      {
+        new_size-=range_start;
+        new_size=std::min(size, new_size);
+      }
+
+      get_objects_rec(mode, *it, range_start, new_size);
+    }
+}
+
+/*******************************************************************\
+
+Function: rw_range_set_value_sett::get_objects_dereference
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void rw_range_set_value_sett::get_objects_dereference(
+  get_modet mode,
+  const dereference_exprt &deref,
+  const mp_integer &range_start,
+  const mp_integer &size)
+{
+  rw_range_sett::get_objects_dereference(
+    mode,
+    deref,
+    range_start,
+    size);
+
+  exprt tmp=deref;
+  dereference(target, tmp, ns, value_sets);
+
+  get_objects_rec(mode, tmp);
+}
+
+/*******************************************************************\
+
+Function: guarded_range_domaint::output
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void guarded_range_domaint::output(
+  const namespacet &ns, std::ostream &out) const
+{
+  out << "[";
+  for(const_iterator itr=begin();
+      itr!=end();
+      ++itr)
+  {
+    if(itr!=begin()) out << ";";
+    out << itr->first << ":" << itr->second.first;
+    out << " if " << from_expr(ns, "", itr->second.second);
+  }
+  out << "]";
+}
+
+/*******************************************************************\
+
+Function: rw_guarded_range_set_value_sett::get_objects_if
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void rw_guarded_range_set_value_sett::get_objects_if(
+  get_modet mode,
+  const if_exprt &if_expr,
+  const mp_integer &range_start,
+  const mp_integer &size)
+{
+  if(if_expr.cond().is_false())
+    get_objects_rec(mode, if_expr.false_case(), range_start, size);
+  else if(if_expr.cond().is_true())
+    get_objects_rec(mode, if_expr.true_case(), range_start, size);
+  else
+  {
+    get_objects_rec(READ, if_expr.cond());
+
+    guardt guard_bak1(guard), guard_bak2(guard);
+
+    guard.add(not_exprt(if_expr.cond()));
+    get_objects_rec(mode, if_expr.false_case(), range_start, size);
+    guard.swap(guard_bak1);
+
+    guard.add(if_expr.cond());
+    get_objects_rec(mode, if_expr.true_case(), range_start, size);
+    guard.swap(guard_bak2);
+  }
+}
+
+/*******************************************************************\
+
+Function: rw_guarded_range_set_value_sett::add
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void rw_guarded_range_set_value_sett::add(
+  get_modet mode,
+  const irep_idt &identifier,
+  const mp_integer &range_start,
+  const mp_integer &range_end)
+{
+  objectst::iterator entry=(mode==LHS_W ? w_range_set : r_range_set).
+    insert(std::make_pair<irep_idt, range_domain_baset*>(identifier, 0)).first;
+
+  if(entry->second==0)
+    entry->second=new guarded_range_domaint();
+
+  static_cast<guarded_range_domaint*>(entry->second)->insert(
+    std::make_pair(range_start,
+                   std::make_pair(range_end, guard.as_expr())));
+}
+
+/*******************************************************************\
+
+Function: goto_rw
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void goto_rw(goto_programt::const_targett target,
+             const code_assignt &assign,
+             rw_range_sett &rw_set)
+{
+  rw_set.get_objects_rec(target, rw_range_sett::LHS_W, assign.lhs());
+  rw_set.get_objects_rec(target, rw_range_sett::READ, assign.rhs());
+}
+
+/*******************************************************************\
+
+Function: goto_rw
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void goto_rw(goto_programt::const_targett target,
+             const code_function_callt &function_call,
+             rw_range_sett &rw_set)
+{
+  if(function_call.lhs().is_not_nil())
+    rw_set.get_objects_rec(
+      target,
+      rw_range_sett::LHS_W,
+      function_call.lhs());
+
+  rw_set.get_objects_rec(
+    target,
+    rw_range_sett::READ,
+    function_call.function());
+
+  forall_expr(it, function_call.arguments())
+    rw_set.get_objects_rec(target, rw_range_sett::READ, *it);
+}
+
+/*******************************************************************\
+
+Function: goto_rw
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void goto_rw(goto_programt::const_targett target,
+             rw_range_sett &rw_set)
+{
+  switch(target->type)
+  {
+  case NO_INSTRUCTION_TYPE:
+    assert(false);
+    break;
+    
+  case GOTO:
+  case ASSUME:
+  case ASSERT:
+    rw_set.get_objects_rec(
+      target,
+      rw_range_sett::READ,
+      target->guard);
+    break;
+    
+  case RETURN:
+    {
+      const code_returnt &code_return=
+        to_code_return(target->code);
+      if(code_return.has_return_value())
+        rw_set.get_objects_rec(
+          target,
+          rw_range_sett::READ,
+          code_return.return_value());
+    }
+    break;
+    
+  case OTHER:
+    // don't know
+    break;
+    
+  case SKIP:
+  case START_THREAD:
+  case END_THREAD:
+  case LOCATION:
+  case END_FUNCTION:
+  case ATOMIC_BEGIN:
+  case ATOMIC_END:
+  case THROW:
+  case CATCH:
+    // these don't read or write anything
+    break;      
+
+  case ASSIGN:
+    goto_rw(target, to_code_assign(target->code), rw_set);
+    break;
+  
+  case DEAD:
+    rw_set.get_objects_rec(
+      target,
+      rw_range_sett::LHS_W,
+      to_code_dead(target->code).symbol());
+    break;
+
+  case DECL:
+    rw_set.get_objects_rec(
+      target,
+      rw_range_sett::LHS_W,
+      to_code_decl(target->code).symbol());
+    break;
+  
+  case FUNCTION_CALL:
+    goto_rw(target, to_code_function_call(target->code), rw_set);
+    break;
+  }
+}
+
+/*******************************************************************\
+
+Function: goto_rw
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void goto_rw(const goto_programt::goto_programt &goto_program,
+             rw_range_sett &rw_set)
+{
+  forall_goto_program_instructions(i_it, goto_program)
+    goto_rw(i_it, rw_set);
+}
+
+/*******************************************************************\
+
+Function: goto_rw
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void goto_rw(const goto_functionst &goto_functions,
+             const irep_idt &function,
+             rw_range_sett &rw_set)
+{
+  goto_functionst::function_mapt::const_iterator f_it=
+    goto_functions.function_map.find(function);
+
+  if(f_it!=goto_functions.function_map.end())
+  {
+    const goto_programt &body=f_it->second.body;
+
+    goto_rw(body, rw_set);
+  }
+}
+
diff --git a/src/analyses/goto_rw.h b/src/analyses/goto_rw.h
new file mode 100644
index 0000000..5ba01ae
--- /dev/null
+++ b/src/analyses/goto_rw.h
@@ -0,0 +1,333 @@
+/*******************************************************************\
+
+Module: 
+
+Author: Daniel Kroening
+
+Date: April 2010
+
+\*******************************************************************/
+
+#ifndef CPROVER_GOTO_PROGRAMS_GOTO_RW_H
+#define CPROVER_GOTO_PROGRAMS_GOTO_RW_H
+
+#include <map>
+#include <ostream>
+
+#include <util/guard.h>
+
+#include <goto-programs/goto_program.h>
+
+#define forall_rw_range_set_r_objects(it, rw_set) \
+  for(rw_range_sett::objectst::const_iterator it=(rw_set).get_r_set().begin(); \
+      it!=(rw_set).get_r_set().end(); ++it)
+
+#define forall_rw_range_set_w_objects(it, rw_set) \
+  for(rw_range_sett::objectst::const_iterator it=(rw_set).get_w_set().begin(); \
+      it!=(rw_set).get_w_set().end(); ++it)
+
+class rw_range_sett;
+class goto_functionst;
+
+void goto_rw(goto_programt::const_targett target,
+             rw_range_sett &rw_set);
+
+void goto_rw(const goto_programt::goto_programt &goto_program,
+             rw_range_sett &rw_set);
+
+void goto_rw(const goto_functionst &goto_functions,
+             const irep_idt &function,
+             rw_range_sett &rw_set);
+
+class range_domain_baset
+{
+public:
+  virtual ~range_domain_baset();
+
+  virtual void output(const namespacet &ns, std::ostream &out) const=0;
+};
+
+// each element x represents a range [x.first, x.second.first)
+class range_domaint:
+  public range_domain_baset,
+  public std::multimap<mp_integer, mp_integer>
+{
+public:
+  virtual void output(const namespacet &ns, std::ostream &out) const;
+};
+
+class array_exprt;
+class byte_extract_exprt;
+class dereference_exprt;
+class if_exprt;
+class index_exprt;
+class member_exprt;
+class shift_exprt;
+class struct_exprt;
+class typecast_exprt;
+
+class rw_range_sett
+{
+public:
+  #ifdef USE_DSTRING
+  typedef std::map<irep_idt, range_domain_baset*> objectst;
+  #else
+  typedef hash_map_cont<irep_idt, range_domain_baset*, string_hash> objectst;
+  #endif
+
+  virtual ~rw_range_sett();
+
+  explicit rw_range_sett(const namespacet &_ns):
+    ns(_ns)
+  {
+  }
+
+  const objectst & get_r_set() const
+  {
+    return r_range_set;
+  }
+
+  const objectst & get_w_set() const
+  {
+    return w_range_set;
+  }
+
+  const range_domaint& get_ranges(objectst::const_iterator it) const
+  {
+    assert(dynamic_cast<range_domaint*>(it->second)!=0);
+    return *static_cast<range_domaint*>(it->second);
+  }
+
+  typedef enum { LHS_W, READ } get_modet;
+
+  virtual void get_objects_rec(
+    goto_programt::const_targett _target,
+    get_modet mode,
+    const exprt &expr)
+  {
+    get_objects_rec(mode, expr);
+  }
+
+  void output(std::ostream &out) const;
+
+protected:
+  const namespacet &ns;
+
+  objectst r_range_set, w_range_set;
+
+  virtual void get_objects_rec(
+    get_modet mode,
+    const exprt &expr);
+
+  virtual void get_objects_complex(
+    get_modet mode,
+    const exprt &expr,
+    const mp_integer &range_start,
+    const mp_integer &size);
+
+  virtual void get_objects_if(
+    get_modet mode,
+    const if_exprt &if_expr,
+    const mp_integer &range_start,
+    const mp_integer &size);
+
+  // overload to include expressions read/written
+  // through dereferencing
+  virtual void get_objects_dereference(
+    get_modet mode,
+    const dereference_exprt &deref,
+    const mp_integer &range_start,
+    const mp_integer &size);
+
+  virtual void get_objects_byte_extract(
+    get_modet mode,
+    const byte_extract_exprt &be,
+    const mp_integer &range_start,
+    const mp_integer &size);
+
+  virtual void get_objects_shift(
+    get_modet mode,
+    const shift_exprt &shift,
+    const mp_integer &range_start,
+    const mp_integer &size);
+
+  virtual void get_objects_member(
+    get_modet mode,
+    const member_exprt &expr,
+    const mp_integer &range_start,
+    const mp_integer &size);
+
+  virtual void get_objects_index(
+    get_modet mode,
+    const index_exprt &expr,
+    const mp_integer &range_start,
+    const mp_integer &size);
+
+  virtual void get_objects_array(
+    get_modet mode,
+    const array_exprt &expr,
+    const mp_integer &range_start,
+    const mp_integer &size);
+
+  virtual void get_objects_struct(
+    get_modet mode,
+    const struct_exprt &expr,
+    const mp_integer &range_start,
+    const mp_integer &size);
+
+  virtual void get_objects_typecast(
+    get_modet mode,
+    const typecast_exprt &tc,
+    const mp_integer &range_start,
+    const mp_integer &size);
+
+  virtual void get_objects_address_of(const exprt &object);
+
+  virtual void get_objects_rec(
+    get_modet mode,
+    const exprt &expr,
+    const mp_integer &range_start,
+    const mp_integer &size);
+
+  virtual void add(
+    get_modet mode,
+    const irep_idt &identifier,
+    const mp_integer &range_start,
+    const mp_integer &range_end);
+};
+
+inline std::ostream & operator << (
+  std::ostream &out,
+  const rw_range_sett &rw_set)
+{
+  rw_set.output(out);
+  return out;
+}
+
+class may_aliast;
+
+class rw_range_set_dereft:public rw_range_sett
+{
+public:
+  rw_range_set_dereft(
+    const namespacet &_ns,
+    may_aliast &_may_alias):
+    rw_range_sett(_ns),
+    may_alias(_may_alias)
+  {
+  }
+
+  using rw_range_sett::get_objects_rec;
+
+  virtual void get_objects_rec(
+    goto_programt::const_targett _target,
+    get_modet mode,
+    const exprt &expr)
+  {
+    target=_target;
+
+    rw_range_sett::get_objects_rec(mode, expr);
+  }
+
+protected:
+  may_aliast &may_alias;
+
+  goto_programt::const_targett target;
+
+  virtual void get_objects_dereference(
+    get_modet mode,
+    const dereference_exprt &deref,
+    const mp_integer &range_start,
+    const mp_integer &size);
+};
+
+class value_setst;
+
+class rw_range_set_value_sett:public rw_range_sett
+{
+public:
+  rw_range_set_value_sett(
+    const namespacet &_ns,
+    value_setst &_value_sets):
+    rw_range_sett(_ns),
+    value_sets(_value_sets)
+  {
+  }
+
+  using rw_range_sett::get_objects_rec;
+
+  virtual void get_objects_rec(
+    goto_programt::const_targett _target,
+    get_modet mode,
+    const exprt &expr)
+  {
+    target=_target;
+
+    rw_range_sett::get_objects_rec(mode, expr);
+  }
+
+protected:
+  value_setst &value_sets;
+
+  goto_programt::const_targett target;
+
+  virtual void get_objects_dereference(
+    get_modet mode,
+    const dereference_exprt &deref,
+    const mp_integer &range_start,
+    const mp_integer &size);
+};
+
+class guarded_range_domaint:
+  public range_domain_baset,
+  public std::multimap<mp_integer, std::pair<mp_integer, exprt> >
+{
+public:
+  virtual void output(const namespacet &ns, std::ostream &out) const;
+};
+
+class rw_guarded_range_set_value_sett:public rw_range_set_value_sett
+{
+public:
+  rw_guarded_range_set_value_sett(
+    const namespacet &_ns,
+    value_setst &_value_sets):
+    rw_range_set_value_sett(_ns, _value_sets)
+  {
+  }
+
+  const guarded_range_domaint& get_ranges(objectst::const_iterator it) const
+  {
+    assert(dynamic_cast<guarded_range_domaint*>(it->second)!=0);
+    return *static_cast<guarded_range_domaint*>(it->second);
+  }
+
+  virtual void get_objects_rec(
+    goto_programt::const_targett _target,
+    get_modet mode,
+    const exprt &expr)
+  {
+    guard.make_true();
+
+    rw_range_set_value_sett::get_objects_rec(_target, mode, expr);
+  }
+
+protected:
+  guardt guard;
+
+  using rw_range_sett::get_objects_rec;
+
+  virtual void get_objects_if(
+    get_modet mode,
+    const if_exprt &if_expr,
+    const mp_integer &range_start,
+    const mp_integer &size);
+
+  virtual void add(
+    get_modet mode,
+    const irep_idt &identifier,
+    const mp_integer &range_start,
+    const mp_integer &range_end);
+};
+
+#endif
diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp
index 877642e..ea4a09d 100644
--- a/src/analyses/interval_domain.cpp
+++ b/src/analyses/interval_domain.cpp
@@ -72,8 +72,8 @@ Function: interval_domaint::transform
 
 void interval_domaint::transform(
   const namespacet &ns,
-  locationt from,
-  locationt to)
+  goto_programt::const_targett from,
+  goto_programt::const_targett to)
 {
   const goto_programt::instructiont &instruction=*from;
   switch(instruction.type)
@@ -92,7 +92,7 @@ void interval_domaint::transform(
   
   case GOTO:
     {
-      locationt next=from;
+      goto_programt::const_targett next=from;
       next++;
       if(next==to)
         assume_rec(not_exprt(instruction.guard));
@@ -130,7 +130,9 @@ Function: interval_domaint::merge
 
 \*******************************************************************/
 
-bool interval_domaint::merge(const interval_domaint &b, locationt to)
+bool interval_domaint::merge(
+  const interval_domaint &b,
+  goto_programt::const_targett to)
 {
   if(!b.seen) return false;
   if(!seen) { *this=b; return true; }
diff --git a/src/analyses/interval_domain.h b/src/analyses/interval_domain.h
index aed6715..6e5934d 100644
--- a/src/analyses/interval_domain.h
+++ b/src/analyses/interval_domain.h
@@ -30,14 +30,16 @@ public:
 
   virtual void transform(
     const namespacet &ns,
-    locationt from,
-    locationt to);
+    goto_programt::const_targett from,
+    goto_programt::const_targett to);
               
   virtual void output(
     const namespacet &ns,
     std::ostream &out) const;
 
-  bool merge(const interval_domaint &b, locationt to);
+  bool merge(
+    const interval_domaint &b,
+    goto_programt::const_targett to);
   
   exprt make_expression(const symbol_exprt &) const;
   
diff --git a/src/analyses/invariant_propagation.h b/src/analyses/invariant_propagation.h
index eac5455..e318bd5 100644
--- a/src/analyses/invariant_propagation.h
+++ b/src/analyses/invariant_propagation.h
@@ -27,7 +27,7 @@ public:
   {
   }
   
-  const invariant_sett &lookup(locationt l) const
+  const invariant_sett &lookup(goto_programt::const_targett l) const
   {
     return (*this)[l].invariant_set;
   }
diff --git a/src/analyses/invariant_set_domain.cpp b/src/analyses/invariant_set_domain.cpp
index 56659e8..d3b1091 100644
--- a/src/analyses/invariant_set_domain.cpp
+++ b/src/analyses/invariant_set_domain.cpp
@@ -24,8 +24,8 @@ Function: invariant_set_domaint::transform
 
 void invariant_set_domaint::transform(
   const namespacet &ns,
-  locationt from_l,
-  locationt to_l)
+  goto_programt::const_targett from_l,
+  goto_programt::const_targett to_l)
 {
   switch(from_l->type)
   {
diff --git a/src/analyses/invariant_set_domain.h b/src/analyses/invariant_set_domain.h
index 06e2f19..1f402d0 100644
--- a/src/analyses/invariant_set_domain.h
+++ b/src/analyses/invariant_set_domain.h
@@ -19,7 +19,9 @@ public:
 
   // overloading  
 
-  inline bool merge(const invariant_set_domaint &other, locationt to)
+  inline bool merge(
+    const invariant_set_domaint &other,
+    goto_programt::const_targett to)
   {
     return invariant_set.make_union(other.invariant_set);
   }
@@ -33,15 +35,15 @@ public:
     
   virtual void initialize(
     const namespacet &ns,
-    locationt l)
+    goto_programt::const_targett l)
   {
     invariant_set.make_true();
   }
 
   virtual void transform(
     const namespacet &ns,
-    locationt from_l,
-    locationt to_l);
+    goto_programt::const_targett from_l,
+    goto_programt::const_targett to_l);
 };
 
 #endif
diff --git a/src/analyses/is_threaded.cpp b/src/analyses/is_threaded.cpp
index 99e7d8d..4847373 100644
--- a/src/analyses/is_threaded.cpp
+++ b/src/analyses/is_threaded.cpp
@@ -20,7 +20,9 @@ public:
   {
   }
 
-  inline bool merge(const is_threaded_domaint &other, locationt to)
+  inline bool merge(
+    const is_threaded_domaint &other,
+    goto_programt::const_targett to)
   {
     bool old=is_threaded;
     is_threaded=is_threaded || other.is_threaded;
@@ -29,8 +31,8 @@ public:
   
   void transform(
     const namespacet &ns,
-    locationt from,
-    locationt to)
+    goto_programt::const_targett from,
+    goto_programt::const_targett to)
   {
     if(from->is_start_thread())
       is_threaded=true;
@@ -59,18 +61,9 @@ void is_threadedt::compute(const goto_functionst &goto_functions)
   
   is_threaded_analysis(goto_functions);
   
-  for(goto_functionst::function_mapt::const_iterator
-      f_it=goto_functions.function_map.begin();
-      f_it!=goto_functions.function_map.end();
-      f_it++)
-  {
-    const goto_programt &goto_program=f_it->second.body;
-    for(goto_programt::instructionst::const_iterator
-        i_it=goto_program.instructions.begin();
-        i_it!=goto_program.instructions.end();
-        i_it++)
+  forall_goto_functions(f_it, goto_functions)
+    forall_goto_program_instructions(i_it, f_it->second.body)
       if(is_threaded_analysis[i_it].is_threaded)
         is_threaded_set.insert(i_it);
-  }
 }
 
diff --git a/src/analyses/local_may_alias.cpp b/src/analyses/local_may_alias.cpp
index 9ca6bab..2562169 100644
--- a/src/analyses/local_may_alias.cpp
+++ b/src/analyses/local_may_alias.cpp
@@ -20,7 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 /*******************************************************************\
 
-Function: cfgt::build
+Function: local_may_aliast::~local_may_aliast
 
   Inputs:
 
@@ -30,69 +30,8 @@ Function: cfgt::build
 
 \*******************************************************************/
 
-void local_cfgt::build(const goto_programt &goto_program)
+local_may_aliast::~local_may_aliast()
 {
-  locs.resize(goto_program.instructions.size());
-
-  {  
-    unsigned loc_nr=0;
-  
-    for(goto_programt::const_targett it=goto_program.instructions.begin();
-        it!=goto_program.instructions.end();
-        it++, loc_nr++)
-    {
-      loc_map[it]=loc_nr;
-      locs[loc_nr].t=it;
-    }
-  }
-
-  for(unsigned loc_nr=0; loc_nr<locs.size(); loc_nr++)
-  {
-    loct &loc=locs[loc_nr];
-    const goto_programt::instructiont &instruction=*loc.t;
-    
-    switch(instruction.type)
-    {
-    case GOTO:
-      if(!instruction.guard.is_true())
-        loc.successors.push_back(loc_nr+1);
-        
-      for(goto_programt::targetst::const_iterator
-          t_it=instruction.targets.begin();
-          t_it!=instruction.targets.end();
-          t_it++)
-      {
-        unsigned l=loc_map.find(*t_it)->second;
-        loc.successors.push_back(l); 
-      }
-      break;
-      
-    case START_THREAD:
-      loc.successors.push_back(loc_nr+1);
-        
-      for(goto_programt::targetst::const_iterator
-          t_it=instruction.targets.begin();
-          t_it!=instruction.targets.end();
-          t_it++)
-      {
-        unsigned l=loc_map.find(*t_it)->second;
-        loc.successors.push_back(l); 
-      }
-      break;
-      
-    case RETURN:
-      loc.successors.push_back(locs.size()-1);
-      break;
-      
-    case THROW:
-    case END_FUNCTION:
-    case END_THREAD:
-      break; // no successor
-
-    default:
-      loc.successors.push_back(loc_nr+1);
-    }
-  }  
 }
 
 /*******************************************************************\
@@ -189,7 +128,7 @@ Function: local_may_aliast::is_tracked
 
 \*******************************************************************/
 
-bool local_may_aliast::is_tracked(const irep_idt &identifier)
+bool local_may_aliast::is_tracked(const irep_idt &identifier) const
 {
   localst::locals_mapt::const_iterator it=locals.locals_map.find(identifier);
   if(it==locals.locals_map.end()) return false;
@@ -224,7 +163,8 @@ void local_may_aliast::assign_lhs(
     {
       unsigned dest_pointer=pointers.number(identifier);
       destt &dest_set=loc_info_dest.points_to[dest_pointer];
-      dest_set.clear();
+      if(kill_foreign || local_may_aliast::is_tracked(identifier))
+        dest_set.clear();
       get_rec(dest_set, rhs, loc_info_src);
     }
   }
@@ -266,11 +206,7 @@ std::set<exprt> local_may_aliast::get(
   const goto_programt::const_targett t,
   const exprt &rhs)
 {
-  local_cfgt::loc_mapt::const_iterator loc_it=cfg.loc_map.find(t);
-  
-  assert(loc_it!=cfg.loc_map.end());
-  
-  const loc_infot &loc_info_src=loc_infos[loc_it->second];
+  const loc_infot &loc_info_src=loc_infos[t];
   
   destt result_tmp;
   get_rec(result_tmp, rhs, loc_info_src);
@@ -304,11 +240,7 @@ bool local_may_aliast::may_use_offset(
   const goto_programt::const_targett t,
   const exprt &rhs)
 {
-  local_cfgt::loc_mapt::const_iterator loc_it=cfg.loc_map.find(t);
-  
-  assert(loc_it!=cfg.loc_map.end());
-  
-  const loc_infot &loc_info_src=loc_infos[loc_it->second];
+  const loc_infot &loc_info_src=loc_infos[t];
   
   destt result_tmp;
   get_rec(result_tmp, rhs, loc_info_src);
@@ -332,11 +264,7 @@ bool local_may_aliast::aliases(
   const goto_programt::const_targett t,
   const exprt &src1, const exprt &src2)
 {
-  local_cfgt::loc_mapt::const_iterator loc_it=cfg.loc_map.find(t);
-  
-  assert(loc_it!=cfg.loc_map.end());
-  
-  const loc_infot &loc_info_src=loc_infos[loc_it->second];
+  const loc_infot &loc_info_src=loc_infos[t];
   
   destt tmp1, tmp2;
   get_rec(tmp1, src1, loc_info_src);
@@ -503,44 +431,30 @@ Function: local_may_aliast::build
 
 void local_may_aliast::build(const goto_functiont &goto_function)
 {
-  if(cfg.locs.empty()) return;
+  if(cfg.entry_map.empty() ||
+     goto_function.body.instructions.empty()) return;
 
+  goto_programt::const_targett entry=goto_function.body.instructions.begin();
   work_queuet work_queue;
-  work_queue.push(0);  
+  work_queue.push(entry);  
   
   unknown_object=objects.number(exprt(ID_unknown));
   
-  loc_infos.resize(cfg.locs.size());
-  
   // feed in sufficiently bad defaults
-  for(code_typet::argumentst::const_iterator
-      it=goto_function.type.arguments().begin();
-      it!=goto_function.type.arguments().end();
-      it++)
-  {
-    const irep_idt &identifier=it->get_identifier();
-    if(is_tracked(identifier))
-      loc_infos[0].points_to[pointers.number(identifier)].objects.insert(unknown_object);
-  }
-
-  for(localst::locals_mapt::const_iterator
-      l_it=locals.locals_map.begin();
-      l_it!=locals.locals_map.end();
-      l_it++)
-  {
-    if(is_tracked(l_it->first))
-      loc_infos[0].points_to[pointers.number(l_it->first)].objects.insert(unknown_object);
-  }
+  loc_infot &loc_info=loc_infos[entry];
+  forall_symbols(it, ns.get_symbol_table().symbols)
+    if(is_tracked(it->second.name))
+      loc_info.points_to[pointers.number(it->second.name)].objects.insert(unknown_object);
 
   while(!work_queue.empty())
   {
-    unsigned loc_nr=work_queue.top();
-    const local_cfgt::loct &loc=cfg.locs[loc_nr];
-    const goto_programt::instructiont &instruction=*loc.t;
+    goto_programt::const_targett t=work_queue.top();
+    const local_cfgt::nodet &loc=cfg[cfg.entry_map[t]];
+    const goto_programt::instructiont &instruction=*t;
     work_queue.pop();
     
-    const loc_infot &loc_info_src=loc_infos[loc_nr];
-    loc_infot loc_info_dest=loc_infos[loc_nr];
+    const loc_infot &loc_info_src=loc_infos[t];
+    loc_infot loc_info_dest=loc_infos[t];
     
     switch(instruction.type)
     {
@@ -576,13 +490,13 @@ void local_may_aliast::build(const goto_functiont &goto_function)
     default:;
     }
 
-    for(local_cfgt::successorst::const_iterator
-        it=loc.successors.begin();
-        it!=loc.successors.end();
+    for(local_cfgt::edgest::const_iterator
+        it=loc.out.begin();
+        it!=loc.out.end();
         it++)
     {
-      if(loc_infos[*it].merge(loc_info_dest))
-        work_queue.push(*it);
+      if(loc_infos[cfg[it->first].PC].merge(loc_info_dest))
+        work_queue.push(cfg[it->first].PC);
     }
   }
 }
@@ -601,16 +515,15 @@ Function: local_may_aliast::output
 
 void local_may_aliast::output(
   std::ostream &out,
-  const goto_functiont &goto_function,
-  const namespacet &ns) const
+  const goto_functiont &goto_function) const
 {
-  unsigned l=0;
-
   forall_goto_program_instructions(i_it, goto_function.body)
   {
     out << "**** " << i_it->location << "\n";
 
-    const loc_infot &loc_info=loc_infos[l];
+    loc_infost::const_iterator entry=loc_infos.find(i_it);
+    assert(entry!=loc_infos.end());
+    const loc_infot &loc_info=entry->second;
 
     for(points_tot::const_iterator
         p_it=loc_info.points_to.begin();
@@ -639,8 +552,6 @@ void local_may_aliast::output(
     out << "\n";
     goto_function.body.output_instruction(ns, "", out, i_it);
     out << "\n";
-    
-    l++;
   }
 }
 
diff --git a/src/analyses/local_may_alias.h b/src/analyses/local_may_alias.h
index 62a3c1f..bc808fe 100644
--- a/src/analyses/local_may_alias.h
+++ b/src/analyses/local_may_alias.h
@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/numbering.h>
 
 #include <goto-programs/goto_functions.h>
+#include <goto-programs/cfg.h>
 
 #include "dirty.h"
 #include "locals.h"
@@ -27,55 +28,36 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-class local_cfgt
-{
-public:
-  typedef std::vector<unsigned> successorst;
-
-  class loct
-  {
-  public:
-    goto_programt::const_targett t;
-    successorst successors;
-  };
-
-  typedef std::map<goto_programt::const_targett, unsigned> loc_mapt;
-  loc_mapt loc_map;
-  
-  typedef std::vector<loct> locst;
-  locst locs;
-  
-  inline explicit local_cfgt(const goto_programt &_goto_program)
-  {
-    build(_goto_program);
-  }
-
-protected:  
-  void build(const goto_programt &goto_program);
-};
-
 class local_may_aliast
 {
 public:
   typedef goto_functionst::goto_functiont goto_functiont;
+
+  virtual ~local_may_aliast();
   
-  explicit local_may_aliast(
-    const goto_functiont &_goto_function):
+  local_may_aliast(
+    const goto_functiont &_goto_function,
+    const namespacet &_ns):
     dirty(_goto_function),
     locals(_goto_function),
-    cfg(_goto_function.body)
+    ns(_ns),
+    kill_foreign(true)
   {
+    cfg(_goto_function.body);
     build(_goto_function);
   }
 
   void output(
     std::ostream &out,
-    const goto_functiont &goto_function,
-    const namespacet &ns) const;
+    const goto_functiont &goto_function) const;
+
+  typedef procedure_local_concurrent_cfg_baset<empty_cfg_nodet> local_cfgt;
   
   dirtyt dirty;
   localst locals;
   local_cfgt cfg;
+  const namespacet &ns;
+  const bool kill_foreign;
 
   std::set<exprt> get(
     const goto_programt::const_targett t,
@@ -90,9 +72,21 @@ public:
     const exprt &src);
   
 protected:
+  local_may_aliast(
+    const goto_functiont &_goto_function,
+    const namespacet &_ns,
+    bool _kill_foreign):
+    dirty(_goto_function),
+    locals(_goto_function),
+    ns(_ns),
+    kill_foreign(_kill_foreign)
+  {
+    cfg(_goto_function.body);
+  }
+
   void build(const goto_functiont &goto_function);
 
-  typedef std::stack<unsigned> work_queuet;
+  typedef std::stack<goto_programt::const_targett> work_queuet;
 
   // the following may eventually get merged  
   numbering<irep_idt> pointers;
@@ -124,7 +118,7 @@ protected:
     bool merge(const loc_infot &src);
   };
 
-  typedef std::vector<loc_infot> loc_infost;
+  typedef std::map<goto_programt::const_targett, loc_infot> loc_infost;
   loc_infost loc_infos;
   
   void assign_lhs(
@@ -138,7 +132,7 @@ protected:
     const exprt &rhs,
     const loc_infot &loc_info_src);
     
-  bool is_tracked(const irep_idt &identifier);
+  virtual bool is_tracked(const irep_idt &identifier) const;
   
   unsigned unknown_object;
   std::set<exprt> empty_set;
diff --git a/src/analyses/may_alias.cpp b/src/analyses/may_alias.cpp
new file mode 100644
index 0000000..455e22c
--- /dev/null
+++ b/src/analyses/may_alias.cpp
@@ -0,0 +1,128 @@
+/*******************************************************************\
+
+Module: Field-insensitive, location-sensitive may-alias analysis
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include <cassert>
+
+#include "may_alias.h"
+
+/*******************************************************************\
+
+Function: may_aliast::may_aliast
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: 
+
+\*******************************************************************/
+
+may_aliast::may_aliast(
+  const goto_functionst &goto_functions,
+  const namespacet &ns):
+  local_may_aliast(goto_functionst::goto_functiont(), ns, false)
+{
+  assert(!goto_functions.function_map.empty());
+
+  dirty=dirtyt(goto_functions);
+  cfg(goto_functions);
+
+  forall_goto_functions(it, goto_functions)
+  {
+    locals=localst(it->second);
+
+    build(it->second);
+  }
+
+  // make it context-insensitive for all non-local variables
+  // relies on the fact that local_may_aliast is flow-insensitive for
+  // non-local variables
+  points_tot merged;
+  for(numbering<irep_idt>::const_iterator it=pointers.begin();
+      it!=pointers.end();
+      ++it)
+    if(!local_may_aliast::is_tracked(*it))
+      merged.insert(std::make_pair(pointers.number(*it), destt()));
+
+  // build the merged destt
+  forall_goto_functions(it, goto_functions)
+  {
+    goto_programt::const_targett last=
+      --(it->second.body.instructions.end());
+    const loc_infot &loc_info=loc_infos[last];
+
+    for(points_tot::iterator m_it=merged.begin();
+        m_it!=merged.end();
+        ++m_it)
+    {
+      points_tot::const_iterator entry=
+        loc_info.points_to.find(m_it->first);
+      if(entry!=loc_info.points_to.end())
+        m_it->second.merge(entry->second);
+    }
+  }
+
+  // update points_to at all locations
+  forall_goto_functions(it, goto_functions)
+    forall_goto_program_instructions(l_it, it->second.body)
+    {
+      loc_infot &loc_info=loc_infos[l_it];
+
+      for(points_tot::iterator m_it=merged.begin();
+          m_it!=merged.end();
+          ++m_it)
+        loc_info.points_to[m_it->first]=m_it->second;
+    }
+}
+
+/*******************************************************************\
+
+Function: may_aliast::is_tracked
+
+  Inputs:
+
+ Outputs: return 'true' iff we track the object with given
+          identifier
+
+ Purpose:
+
+\*******************************************************************/
+
+bool may_aliast::is_tracked(const irep_idt &identifier) const
+{
+  if(ns.lookup(identifier).type.id()!=ID_pointer) return false;
+  if(dirty.is_dirty(identifier)) return false;
+  return true;
+}
+
+/*******************************************************************\
+
+Function: may_aliast::output
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: 
+
+\*******************************************************************/
+
+void may_aliast::output(
+  std::ostream &out,
+  const goto_functionst &goto_functions) const
+{
+  forall_goto_functions(it, goto_functions)
+  {
+    out << ">>>>" << std::endl;
+    out << ">>>> " << it->first << std::endl;
+    out << ">>>>" << std::endl;
+    local_may_aliast::output(out, it->second);
+    out << std::endl;
+  }
+}
+
diff --git a/src/analyses/may_alias.h b/src/analyses/may_alias.h
new file mode 100644
index 0000000..1e3f044
--- /dev/null
+++ b/src/analyses/may_alias.h
@@ -0,0 +1,37 @@
+/*******************************************************************\
+
+Module: Field-insensitive, location-sensitive may-alias analysis
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_MAY_ALIAS_H
+#define CPROVER_MAY_ALIAS_H
+
+#include "local_may_alias.h"
+
+/*******************************************************************\
+
+   Class: may_aliast
+   
+ Purpose:
+
+\*******************************************************************/
+
+class may_aliast:public local_may_aliast
+{
+public:
+  may_aliast(
+    const goto_functionst &goto_functions,
+    const namespacet &ns);
+
+  void output(
+    std::ostream &out,
+    const goto_functionst &goto_functions) const;
+
+protected:
+  virtual bool is_tracked(const irep_idt &identifier) const;
+};
+
+#endif
diff --git a/src/analyses/natural_loops.h b/src/analyses/natural_loops.h
index 8b16717..5c5f30a 100644
--- a/src/analyses/natural_loops.h
+++ b/src/analyses/natural_loops.h
@@ -52,6 +52,7 @@ public:
 
 protected:
   cfg_dominators_templatet<P, T> cfg_dominators;
+  typedef typename cfg_dominators_templatet<P, T>::cfgt::nodet nodet;
 
   void compute(P &program);
   void compute_natural_loop(T, T);  
@@ -105,8 +106,8 @@ void natural_loops_templatet<P, T>::compute(P &program)
       {
         if((*n_it)->location_number<=m_it->location_number)
         {
-          const typename cfg_dominators_templatet<P, T>::nodet &node=
-            cfg_dominators.node_map[m_it];
+          const nodet &node=
+            cfg_dominators.cfg[cfg_dominators.cfg.entry_map[m_it]];
           
 #ifdef DEBUG
           std::cout << "Computing loop for " 
@@ -156,15 +157,15 @@ void natural_loops_templatet<P, T>::compute_natural_loop(T m, T n)
     T p=stack.top();
     stack.pop();
 
-    typename cfg_dominators_templatet<P, T>::nodet &node=
-      cfg_dominators.node_map[p];
+    const nodet &node=
+      cfg_dominators.cfg[cfg_dominators.cfg.entry_map[p]];
 
-    for(typename std::list<T>::const_iterator
-          q_it=node.predecessors.begin();
-        q_it!=node.predecessors.end();
+    for(typename nodet::edgest::const_iterator
+          q_it=node.in.begin();
+        q_it!=node.in.end();
         ++q_it)
     {
-      T q=*q_it;
+      T q=cfg_dominators.cfg[q_it->first].PC;
       std::pair<typename natural_loopt::const_iterator, bool> result=
           loop.insert(q);
       if(result.second)
diff --git a/src/analyses/reaching_definitions.cpp b/src/analyses/reaching_definitions.cpp
index 66e8653..45c8365 100644
--- a/src/analyses/reaching_definitions.cpp
+++ b/src/analyses/reaching_definitions.cpp
@@ -9,13 +9,9 @@ Date: February 2013
 
 \*******************************************************************/
 
-#include <limits>
-
-#include <util/std_code.h>
-#include <util/std_expr.h>
-#include <util/pointer_offset_size.h>
-#include <util/byte_operators.h>
-#include <util/arith_tools.h>
+#include "goto_rw.h"
+#include "may_alias.h"
+#include "is_threaded.h"
 
 #include "reaching_definitions.h"
 
@@ -33,46 +29,26 @@ Function: rd_range_domaint::transform
 
 void rd_range_domaint::transform(
   const namespacet &ns,
-  locationt from,
-  locationt to)
+  goto_programt::const_targett from,
+  goto_programt::const_targett to)
 {
-  if(from->is_dead())
-  {
-    const symbol_exprt &symbol=
-      to_symbol_expr(to_code_dead(from->code).symbol());
-    values.erase(symbol.get_identifier());
-    return;
-  }
-  else if(!from->is_assign())
-    return;
-
-  const exprt &lhs=to_code_assign(from->code).lhs();
+  assert(is_threaded);
 
-  if(lhs.id()==ID_complex_real ||
-          lhs.id()==ID_complex_imag)
-  {
-    assert(lhs.type().id()==ID_complex);
-    mp_integer offset=compute_pointer_offset(ns, lhs.op0());
-    mp_integer sub_size=pointer_offset_size(ns, lhs.type().subtype());
-
-    assign(
-      ns,
-      from,
-      lhs.op0(),
-      offset+((offset==-1 || lhs.id()==ID_complex_real) ? 0 : sub_size),
-      sub_size);
-  }
-  else
-  {
-    mp_integer size=pointer_offset_size(ns, lhs.type());
-
-    assign(ns, from, lhs, size);
-  }
+  if(from->is_dead())
+    transform_dead(ns, from);
+  else if(from->is_start_thread())
+    transform_start_thread(ns);
+  else if(from->is_function_call())
+    transform_function_call(ns, from, to);
+  else if(from->is_end_function())
+    transform_end_function(ns, from);
+  else if(from->is_assign())
+    transform_assign(ns, from, to_code_assign(from->code).lhs());
 }
 
 /*******************************************************************\
 
-Function: rd_range_domaint::assign
+Function: rd_range_domaint::transform_dead
 
   Inputs:
 
@@ -82,32 +58,19 @@ Function: rd_range_domaint::assign
 
 \*******************************************************************/
 
-void rd_range_domaint::assign(
+void rd_range_domaint::transform_dead(
   const namespacet &ns,
-  locationt from,
-  const exprt &lhs,
-  const mp_integer &size)
+  goto_programt::const_targett from)
 {
-  if(lhs.id()==ID_typecast)
-    assign(ns, from, to_typecast_expr(lhs).op(), size);
-  else if(lhs.id()==ID_if)
-    assign_if(ns, from, to_if_expr(lhs), size);
-  else if(lhs.id()==ID_dereference)
-    assign_dereference(ns, from, to_dereference_expr(lhs), size);
-  else if(lhs.id()==ID_byte_extract_little_endian ||
-          lhs.id()==ID_byte_extract_big_endian)
-    assign_byte_extract(ns, from, to_byte_extract_expr(lhs), size);
-  else if(lhs.id()==ID_symbol ||
-          lhs.id()==ID_index ||
-          lhs.id()==ID_member)
-    assign(ns, from, lhs, compute_pointer_offset(ns, lhs), size);
-  else
-    throw "assignment to `"+lhs.id_string()+"' not handled";
+  const irep_idt& identifier=
+    to_symbol_expr(to_code_dead(from->code).symbol()).get_identifier();
+
+  values.erase(identifier);
 }
 
 /*******************************************************************\
 
-Function: rd_range_domaint::assign_if
+Function: rd_range_domaint::transform_start_thread
 
   Inputs:
 
@@ -117,30 +80,25 @@ Function: rd_range_domaint::assign_if
 
 \*******************************************************************/
 
-void rd_range_domaint::assign_if(
-  const namespacet &ns,
-  locationt from,
-  const if_exprt &if_expr,
-  const mp_integer &size)
+void rd_range_domaint::transform_start_thread(const namespacet &ns)
 {
-  if(if_expr.cond().is_false())
-    assign(ns, from, if_expr.false_case(), size);
-  else if(if_expr.cond().is_true())
-    assign(ns, from, if_expr.true_case(), size);
-  else
-  {
-    rd_range_domaint false_case(*this);
-    assign(ns, from, if_expr.false_case(), size);
-    values.swap(false_case.values);
-    assign(ns, from, if_expr.true_case(), size);
-
-    merge(false_case, from);
-  }
+  for(valuest::iterator it=values.begin();
+      it!=values.end();
+      ) // no ++it
+    if(ns.lookup(it->first).is_thread_local)
+    {
+      valuest::iterator next=it;
+      ++next;
+      values.erase(it);
+      it=next;
+    }
+    else
+      ++it;
 }
 
 /*******************************************************************\
 
-Function: rd_range_domaint::assign_dereference
+Function: rd_range_domaint::transform_function_call
 
   Inputs:
 
@@ -150,44 +108,55 @@ Function: rd_range_domaint::assign_dereference
 
 \*******************************************************************/
 
-void rd_range_domaint::assign_dereference(
+void rd_range_domaint::transform_function_call(
   const namespacet &ns,
-  locationt from,
-  const dereference_exprt &deref,
-  const mp_integer &size)
+  goto_programt::const_targett from,
+  goto_programt::const_targett to)
 {
-  assert(local_may_alias);
+  const code_function_callt &code=to_code_function_call(from->code);
 
-  const exprt &pointer=deref.pointer();
-  std::set<exprt> alias_set=local_may_alias->get(from, pointer);
+  goto_programt::const_targett next=from;
+  ++next;
 
-  valuest before(values);
-  for(std::set<exprt>::const_iterator it=alias_set.begin();
-      it!=alias_set.end();
-      it++)
+  if(next!=to)
   {
-    if(it->id()!=ID_unknown &&
-       it->id()!=ID_dynamic_object &&
-       it->id()!=ID_null_object)
-    {
-      valuest bak;
-      bak.swap(values);
+    for(valuest::iterator it=values.begin();
+        it!=values.end();
+       ) // no ++it
+      if(!ns.lookup(it->first).is_static_lifetime)
+      {
+        valuest::iterator next=it;
+        ++next;
+        values.erase(it);
+        it=next;
+      }
+      else
+        ++it;
 
-      values=before;
-      assign(ns, from, *it, size);
+    const symbol_exprt& fn_symbol_expr=to_symbol_expr(code.function());
+    const code_typet &code_type=
+      to_code_type(ns.lookup(fn_symbol_expr.get_identifier()).type);
 
-      rd_range_domaint this_object;
-      this_object.values.swap(values);
-      values.swap(bak);
+    const code_typet::parameterst &parameters=code_type.parameters();
+    for(code_typet::parameterst::const_iterator it=parameters.begin();
+        it!=parameters.end();
+        ++it)
+    {
+      if(it->get_identifier().empty())
+        continue;
 
-      merge(this_object, from);
+      symbol_exprt parameter(it->get_identifier(), it->type());
+      transform_assign(ns, from, parameter);
     }
   }
+
+  if(code.lhs().is_not_nil())
+    transform_assign(ns, from, code.lhs());
 }
 
 /*******************************************************************\
 
-Function: rd_range_domaint::assign_byte_extract
+Function: rd_range_domaint::transform_end_function
 
   Inputs:
 
@@ -197,33 +166,24 @@ Function: rd_range_domaint::assign_byte_extract
 
 \*******************************************************************/
 
-void rd_range_domaint::assign_byte_extract(
+void rd_range_domaint::transform_end_function(
   const namespacet &ns,
-  locationt from,
-  const byte_extract_exprt &be,
-  const mp_integer &size)
+  goto_programt::const_targett from)
 {
-  assert(size==1);
-  mp_integer op_offset=compute_pointer_offset(ns, be.op());
+  const code_typet &code_type=
+    to_code_type(ns.lookup(from->function).type);
 
-  mp_integer index;
-  if(op_offset==-1 || to_integer(be.offset(), index))
-    assign(ns, from, be.op(), -1, 1);
-  else
-  {
-    endianness_mapt map(
-      be.op().type(),
-      be.id()==ID_byte_extract_little_endian,
-      ns);
-    assert(index<std::numeric_limits<unsigned>::max());
-    op_offset+=map.map_byte(integer2long(index));
-    assign(ns, from, be.op(), op_offset, 1);
-  }
+  const code_typet::parameterst &parameters=code_type.parameters();
+  for(code_typet::parameterst::const_iterator it=parameters.begin();
+      it!=parameters.end();
+      ++it)
+    if(!it->get_identifier().empty())
+      values.erase(it->get_identifier());
 }
 
 /*******************************************************************\
 
-Function: rd_range_domaint::assign
+Function: rd_range_domaint::transform_assign
 
   Inputs:
 
@@ -233,32 +193,33 @@ Function: rd_range_domaint::assign
 
 \*******************************************************************/
 
-void rd_range_domaint::assign(
+void rd_range_domaint::transform_assign(
   const namespacet &ns,
-  locationt from,
-  const exprt &lhs,
-  const mp_integer &range_start,
-  const mp_integer &size)
+  goto_programt::const_targett from,
+  const exprt &lhs)
 {
-  if(lhs.id()==ID_member)
-    assign(ns, from, to_member_expr(lhs).struct_op(), range_start, size);
-  else if(lhs.id()==ID_index)
-    assign(ns, from, to_index_expr(lhs).array(), range_start, size);
-  else
-  {
-    const symbol_exprt &symbol=to_symbol_expr(lhs);
-    const irep_idt identifier=symbol.get_identifier();
+  assert(may_alias);
+  rw_range_set_dereft rw_set(ns, *may_alias);
+  goto_rw(from, rw_set);
 
-    if(range_start>=0)
-    {
-      kill(from, identifier, range_start, size);
-      gen(from, identifier, range_start, size);
-    }
-    else
-    {
-      mp_integer full_size=pointer_offset_size(ns, symbol.type());
-      gen(from, identifier, 0, full_size);
-    }
+  forall_rw_range_set_w_objects(it, rw_set)
+  {
+    const irep_idt &identifier=it->first;
+    const range_domaint &ranges=rw_set.get_ranges(it);
+
+    if(!(*is_threaded)(from) ||
+       !ns.lookup(identifier).is_shared())
+      for(range_domaint::const_iterator
+          r_it=ranges.begin();
+          r_it!=ranges.end();
+          ++r_it)
+        kill(from, identifier, r_it->first, r_it->second);
+
+    for(range_domaint::const_iterator
+        r_it=ranges.begin();
+        r_it!=ranges.end();
+        ++r_it)
+      gen(from, identifier, r_it->first, r_it->second);
   }
 }
 
@@ -275,21 +236,20 @@ Function: rd_range_domaint::kill
 \*******************************************************************/
 
 void rd_range_domaint::kill(
-  locationt from,
+  goto_programt::const_targett from,
   const irep_idt &identifier,
   const mp_integer &range_start,
-  const mp_integer &size)
+  const mp_integer &range_end)
 {
   assert(range_start>=0);
   // -1 for objects of infinite/unknown size
-  if(size==-1)
+  if(range_end==-1)
   {
     kill_inf(from, identifier, range_start);
     return;
   }
 
-  assert(size>0);
-  mp_integer range_end=range_start+size;
+  assert(range_end>range_start);
 
   valuest::iterator entry=values.find(identifier);
   if(entry==values.end())
@@ -317,13 +277,13 @@ void rd_range_domaint::kill(
       ranges.erase(it++);
     }
     else if(it->second.first==-1 ||
-            it->second.first >= range_end) // a <= rs < re <= b
+            it->second.first > range_end) // a <= rs < re < b
     {
       ranges.insert(std::make_pair(range_end, it->second));
       it->second.first=range_start;
       ++it;
     }
-    else // a <= rs < b < re
+    else // a <= rs < b <= re
     {
       it->second.first=range_start;
       ++it;
@@ -343,7 +303,7 @@ Function: rd_range_domaint::kill_inf
 \*******************************************************************/
 
 void rd_range_domaint::kill_inf(
-  locationt from,
+  goto_programt::const_targett from,
   const irep_idt &identifier,
   const mp_integer &range_start)
 {
@@ -385,21 +345,23 @@ Function: rd_range_domaint::gen
 \*******************************************************************/
 
 bool rd_range_domaint::gen(
-  locationt from,
+  goto_programt::const_targett from,
   const irep_idt &identifier,
   const mp_integer &range_start,
-  const mp_integer &size)
+  const mp_integer &range_end)
 {
   assert(range_start>=0);
   // -1 for objects of infinite/unknown size
-  assert(size>0 || size==-1);
-  mp_integer range_end=size==-1 ? -1 : range_start+size;
+  assert(range_end>range_start || range_end==-1);
+
+  mp_integer merged_range_end=range_end;
 
   std::pair<valuest::iterator, bool> entry=
     values.insert(std::make_pair(identifier, rangest()));
   rangest &ranges=entry.first->second;
 
   if(!entry.second)
+  {
     for(rangest::iterator it=ranges.begin();
         it!=ranges.end();
         ) // no ++it
@@ -411,7 +373,7 @@ bool rd_range_domaint::gen(
       else if(it->first > range_start) // rs < a < b,re
       {
         if(range_end!=-1)
-          range_end=std::max(range_end, it->second.first);
+          merged_range_end=std::max(range_end, it->second.first);
         ranges.erase(it++);
       }
       else if(it->second.first==-1 ||
@@ -427,10 +389,11 @@ bool rd_range_domaint::gen(
         return true;
       }
     }
+  }
 
   ranges.insert(std::make_pair(
       range_start,
-      std::make_pair(range_end, from)));
+      std::make_pair(merged_range_end, from)));
 
   return true;
 }
@@ -464,6 +427,7 @@ void rd_range_domaint::output(
     {
       if(itr!=it->second.begin()) out << ";";
       out << itr->first << ":" << itr->second.first;
+      out << "@" << itr->second.second->location_number;
     }
     out << "]" << std::endl;
   }
@@ -483,7 +447,7 @@ Function: rd_range_domaint::merge
 
 bool rd_range_domaint::merge(
   const rd_range_domaint &other,
-  locationt to)
+  goto_programt::const_targett to)
 {
   bool more=false;
 
@@ -520,6 +484,107 @@ bool rd_range_domaint::merge(
 
 /*******************************************************************\
 
+Function: rd_range_domaint::merge_shared
+
+  Inputs:
+
+ Outputs: returns true iff there is s.th. new
+
+ Purpose:
+
+\*******************************************************************/
+
+bool rd_range_domaint::merge_shared(
+  const namespacet &ns,
+  const rd_range_domaint &other,
+  goto_programt::const_targett to)
+{
+  bool more=false;
+
+  valuest::iterator it=values.begin();
+  for(valuest::const_iterator ito=other.values.begin();
+      ito!=other.values.end();
+      ++ito)
+  {
+    while(it!=values.end() && it->first<ito->first)
+      ++it;
+    if(it==values.end() || ito->first<it->first)
+    {
+      if(ns.lookup(ito->first).is_shared())
+      {
+        values.insert(*ito);
+        more=true;
+      }
+    }
+    else if(it!=values.end() &&
+            !ns.lookup(ito->first).is_shared())
+    {
+      ++it;
+    }
+    else if(it!=values.end())
+    {
+      assert(it->first==ito->first);
+      const rangest &rangeso=ito->second;
+      for(rangest::const_iterator itro=rangeso.begin();
+          itro!=rangeso.end();
+          ++itro)
+        more|=gen(
+          itro->second.second,
+          ito->first,
+          itro->first,
+          itro->second.first);
+      ++it;
+    }
+  }
+
+  return more;
+}
+
+/*******************************************************************\
+
+Function: rd_range_domaint::get
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+const rd_range_domaint::rangest& rd_range_domaint::get(
+  const irep_idt &identifier) const
+{
+  static rangest empty;
+
+  valuest::const_iterator entry=values.find(identifier);
+
+  if(entry==values.end())
+    return empty;
+  else
+    return entry->second;
+}
+
+/*******************************************************************\
+
+Function: reaching_definitions_analysist::~reaching_definitions_analysist
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+reaching_definitions_analysist::~reaching_definitions_analysist()
+{
+  if(is_threaded) delete is_threaded;
+  if(may_alias) delete may_alias;
+}
+
+/*******************************************************************\
+
 Function: reaching_definitions_analysist::initialize
 
   Inputs:
@@ -533,11 +598,8 @@ Function: reaching_definitions_analysist::initialize
 void reaching_definitions_analysist::initialize(
   const goto_functionst &goto_functions)
 {
-  forall_goto_functions(f_it, goto_functions)
-  {
-    local_may_aliases.insert(
-      std::make_pair(f_it->first, local_may_aliast(f_it->second)));
-  }
+  may_alias=new may_aliast(goto_functions, ns);
+  is_threaded=new is_threadedt(goto_functions);
 
   static_analysist<rd_range_domaint>::initialize(goto_functions);
 }
@@ -554,13 +616,11 @@ Function: reaching_definitions_analysist::generate_state
 
 \*******************************************************************/
 
-void reaching_definitions_analysist::generate_state(locationt l)
+void reaching_definitions_analysist::generate_state(
+  goto_programt::const_targett l)
 {
   static_analysist<rd_range_domaint>::generate_state(l);
 
-  may_aliasest::iterator entry=
-    local_may_aliases.find(l->function);
-  if(entry!=local_may_aliases.end())
-    state_map[l].set_may_alias(&(entry->second));
+  state_map[l].set_sub_analyses(may_alias, is_threaded);
 }
 
diff --git a/src/analyses/reaching_definitions.h b/src/analyses/reaching_definitions.h
index 32c0ba8..7753ef9 100644
--- a/src/analyses/reaching_definitions.h
+++ b/src/analyses/reaching_definitions.h
@@ -9,114 +9,128 @@ Date: February 2013
 
 \*******************************************************************/
 
+#ifndef CPROVER_REACHING_DEFINITIONS_H
+#define CPROVER_REACHING_DEFINITIONS_H
+
 #include "static_analysis.h"
-#include "local_may_alias.h"
 
-class if_exprt;
-class byte_extract_exprt;
-class dereference_exprt;
+class may_aliast;
+class is_threadedt;
 
 class rd_range_domaint:public domain_baset
 {
 public:
   rd_range_domaint():
-    local_may_alias(0)
+    may_alias(0),
+    is_threaded(0)
   {
   }
 
   virtual void transform(
       const namespacet &ns,
-      locationt from,
-      locationt to);
+      goto_programt::const_targett from,
+      goto_programt::const_targett to);
 
   virtual void output(
       const namespacet &ns,
       std::ostream &out) const;
 
   // returns true iff there is s.th. new
-  bool merge(const rd_range_domaint &other, locationt to);
+  bool merge(
+    const rd_range_domaint &other,
+    goto_programt::const_targett to);
+  bool merge_shared(
+    const namespacet &ns,
+    const rd_range_domaint &other,
+    goto_programt::const_targett to);
 
-  void set_may_alias(local_may_aliast *a)
+  void set_sub_analyses(
+    may_aliast *a,
+    is_threadedt *i)
   {
-    local_may_alias=a;
+    may_alias=a;
+    is_threaded=i;
   }
 
-protected:
   // each element x represents a range [x.first, x.second.first)
-  typedef std::multimap<mp_integer, std::pair<mp_integer, locationt> >
-    rangest;
-  typedef hash_map_cont<irep_idt, rangest, irep_id_hash> valuest;
+  typedef std::multimap<mp_integer,
+                        std::pair<mp_integer,
+                                  goto_programt::const_targett> > rangest;
+  #ifdef USE_DSTRING
+  typedef std::map<irep_idt, rangest> valuest;
+  #else
+  typedef hash_map_cont<irep_idt, rangest, string_hash> valuest;
+  #endif
+
+  const rangest& get(const irep_idt &identifier) const;
+
+protected:
   valuest values;
 
-  local_may_aliast * local_may_alias;
+  may_aliast * may_alias;
+  is_threadedt * is_threaded;
 
-  void assign(
+  void transform_dead(
     const namespacet &ns,
-    locationt from,
-    const exprt &lhs,
-    const mp_integer &size);
-  void assign_if(
+    goto_programt::const_targett from);
+  void transform_start_thread(const namespacet &ns);
+  void transform_function_call(
     const namespacet &ns,
-    locationt from,
-    const if_exprt &if_expr,
-    const mp_integer &size);
-  void assign_dereference(
+    goto_programt::const_targett from,
+    goto_programt::const_targett to);
+  void transform_end_function(
     const namespacet &ns,
-    locationt from,
-    const dereference_exprt &deref,
-    const mp_integer &size);
-  void assign_byte_extract(
+    goto_programt::const_targett from);
+  void transform_assign(
     const namespacet &ns,
-    locationt from,
-    const byte_extract_exprt &be,
-    const mp_integer &size);
-
-  void assign(
-    const namespacet &ns,
-    locationt from,
-    const exprt &lhs,
-    const mp_integer &range_start,
-    const mp_integer &size);
+    goto_programt::const_targett from,
+    const exprt &lhs);
 
   void kill(
-    locationt from,
+    goto_programt::const_targett from,
     const irep_idt &identifier,
     const mp_integer &range_start,
-    const mp_integer &size);
+    const mp_integer &range_end);
   void kill_inf(
-    locationt from,
+    goto_programt::const_targett from,
     const irep_idt &identifier,
     const mp_integer &range_start);
   bool gen(
-    locationt from,
+    goto_programt::const_targett from,
     const irep_idt &identifier,
     const mp_integer &range_start,
-    const mp_integer &size);
+    const mp_integer &range_end);
 };
 
 class reaching_definitions_analysist :
-  public static_analysist<rd_range_domaint>
+  public concurrency_aware_static_analysist<rd_range_domaint>
 {
 public:
   // constructor
   explicit reaching_definitions_analysist(const namespacet &_ns):
-    static_analysist<rd_range_domaint>(_ns)
+    concurrency_aware_static_analysist<rd_range_domaint>(_ns),
+    may_alias(0),
+    is_threaded(0)
   {
   }
 
+  virtual ~reaching_definitions_analysist();
+
   virtual void initialize(
     const goto_programt &goto_program)
   {
-    throw "reaching definitions uses local_may_aliast, cannot be used on goto_programt";
+    throw "reaching definitions uses may_aliast, cannot be used on goto_programt";
   }
 
   virtual void initialize(
     const goto_functionst &goto_functions);
 
 protected:
-  typedef hash_map_cont<irep_idt, local_may_aliast, irep_id_hash> may_aliasest;
-  may_aliasest local_may_aliases;
+  may_aliast * may_alias;
+  is_threadedt * is_threaded;
 
-  virtual void generate_state(locationt l);
+  virtual void generate_state(goto_programt::const_targett l);
 };
 
+#endif
+
diff --git a/src/analyses/static_analysis.cpp b/src/analyses/static_analysis.cpp
index 6171e72..a434c6c 100644
--- a/src/analyses/static_analysis.cpp
+++ b/src/analyses/static_analysis.cpp
@@ -13,6 +13,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/std_code.h>
 #include <util/expr_util.h>
 
+#include "is_threaded.h"
+
 #include "static_analysis.h"
 
 /*******************************************************************\
@@ -28,13 +30,13 @@ Function: static_analysis_baset::get_guard
 \*******************************************************************/
 
 exprt static_analysis_baset::get_guard(
-  locationt from,
-  locationt to)
+  goto_programt::const_targett from,
+  goto_programt::const_targett to)
 {
   if(!from->is_goto())
     return true_exprt();
 
-  locationt next=from;
+  goto_programt::const_targett next=from;
   next++;
 
   if(next==to)
@@ -59,7 +61,8 @@ Function: static_analysis_baset::get_return_lhs
 
 \*******************************************************************/
 
-exprt static_analysis_baset::get_return_lhs(locationt to)
+exprt static_analysis_baset::get_return_lhs(
+  goto_programt::const_targett to)
 {
   // get predecessor of "to"
 
@@ -258,7 +261,7 @@ Function: static_analysis_baset::generate_states
 void static_analysis_baset::update(
   const goto_programt &goto_program)
 {
-  locationt previous;
+  goto_programt::const_targett previous;
   bool first=true;
 
   forall_goto_program_instructions(i_it, goto_program)
@@ -289,13 +292,13 @@ Function: static_analysis_baset::get_next
 
 \*******************************************************************/
 
-static_analysis_baset::locationt static_analysis_baset::get_next(
+goto_programt::const_targett static_analysis_baset::get_next(
   working_sett &working_set)
 {
   assert(!working_set.empty());
   
   working_sett::iterator i=working_set.begin();
-  locationt l=i->second;
+  goto_programt::const_targett l=i->second;
   working_set.erase(i);
     
   return l;
@@ -330,7 +333,7 @@ bool static_analysis_baset::fixedpoint(
 
   while(!working_set.empty())
   {
-    locationt l=get_next(working_set);
+    goto_programt::const_targett l=get_next(working_set);
     
     if(visit(l, working_set, goto_program, goto_functions))
       new_data=true;
@@ -352,7 +355,7 @@ Function: static_analysis_baset::visit
 \*******************************************************************/
 
 bool static_analysis_baset::visit(
-  locationt l,
+  goto_programt::const_targett l,
   working_sett &working_set,
   const goto_programt &goto_program,
   const goto_functionst &goto_functions)
@@ -372,7 +375,7 @@ bool static_analysis_baset::visit(
       it!=successors.end();
       it++)
   {
-    locationt to_l=*it;
+    goto_programt::const_targett to_l=*it;
 
     if(to_l==goto_program.instructions.end())
       continue;
@@ -426,7 +429,8 @@ Function: static_analysis_baset::do_function_call
 \*******************************************************************/
 
 void static_analysis_baset::do_function_call(
-  locationt l_call, locationt l_return,
+  goto_programt::const_targett l_call,
+  goto_programt::const_targett l_return,
   const goto_functionst &goto_functions,
   const goto_functionst::function_mapt::const_iterator f_it,
   const exprt::operandst &arguments,
@@ -441,17 +445,19 @@ void static_analysis_baset::do_function_call(
 
   {
     // get the state at the beginning of the function
-    locationt l_begin=goto_function.body.instructions.begin();
+    goto_programt::const_targett l_begin=
+      goto_function.body.instructions.begin();
     
     // do the edge from the call site to the beginning of the function
-    new_state.transform(ns, l_call, l_begin);  
+    std::auto_ptr<statet> tmp_state(make_temporary_state(new_state));
+    tmp_state->transform(ns, l_call, l_begin);  
     
     statet &begin_state=get_state(l_begin);
 
     bool new_data=false;
 
     // merge the new stuff
-    if(merge(begin_state, new_state, l_begin))
+    if(merge(begin_state, *tmp_state, l_begin))
       new_data=true;
 
     // do each function at least once
@@ -472,21 +478,27 @@ void static_analysis_baset::do_function_call(
 
   {
     // get location at end of procedure
-    locationt l_end=--goto_function.body.instructions.end();
+    goto_programt::const_targett l_end=
+      --goto_function.body.instructions.end();
 
     assert(l_end->is_end_function());
 
     statet &end_of_function=get_state(l_end);
 
     // do edge from end of function to instruction after call
-    locationt l_next=l_call;
-    l_next++;
-    end_of_function.transform(ns, l_end, l_next);
+    std::auto_ptr<statet> tmp_state(
+      make_temporary_state(end_of_function));
+    tmp_state->transform(ns, l_end, l_return);
 
     // propagate those -- not exceedingly precise, this is,
     // as still it contains all the state from the
     // call site
-    merge(new_state, end_of_function, l_end);
+    merge(new_state, *tmp_state, l_return);
+  }
+
+  {
+    // effect on current procedure (if any)
+    new_state.transform(ns, l_call, l_return);
   }
 }    
 
@@ -503,7 +515,8 @@ Function: static_analysis_baset::do_function_call_rec
 \*******************************************************************/
 
 void static_analysis_baset::do_function_call_rec(
-  locationt l_call, locationt l_return,
+  goto_programt::const_targett l_call,
+  goto_programt::const_targett l_return,
   const exprt &function,
   const exprt::operandst &arguments,
   statet &new_state,
@@ -580,7 +593,13 @@ void static_analysis_baset::do_function_call_rec(
       {
         const object_descriptor_exprt &o=to_object_descriptor_expr(*it);
         std::auto_ptr<statet> n2(make_temporary_state(new_state));    
-        do_function_call_rec(l_call, l_return, o.object(), arguments, *n2, goto_functions);
+        do_function_call_rec(
+          l_call,
+          l_return,
+          o.object(),
+          arguments,
+          *n2,
+          goto_functions);
         merge(new_state, *n2, l_return);
       }
     }
@@ -606,7 +625,7 @@ void static_analysis_baset::do_function_call_rec(
 
 /*******************************************************************\
 
-Function: static_analysis_baset::fixedpoint
+Function: static_analysis_baset::sequential_fixedpoint
 
   Inputs:
 
@@ -616,25 +635,19 @@ Function: static_analysis_baset::fixedpoint
 
 \*******************************************************************/
 
-void static_analysis_baset::fixedpoint(
+void static_analysis_baset::sequential_fixedpoint(
   const goto_functionst &goto_functions)
 {
   // do each function at least once
 
-  for(goto_functionst::function_mapt::const_iterator
-      it=goto_functions.function_map.begin();
-      it!=goto_functions.function_map.end();
-      it++)
-    if(functions_done.find(it->first)==
-       functions_done.end())
-    {
-      fixedpoint(it, goto_functions);
-    }
+  forall_goto_functions(it, goto_functions)
+    if(functions_done.insert(it->first).second)
+      fixedpoint(it->second.body, goto_functions);
 }
 
 /*******************************************************************\
 
-Function: static_analysis_baset::fixedpoint
+Function: static_analysis_baset::concurrent_fixedpoint
 
   Inputs:
 
@@ -644,10 +657,74 @@ Function: static_analysis_baset::fixedpoint
 
 \*******************************************************************/
 
-bool static_analysis_baset::fixedpoint(
-  const goto_functionst::function_mapt::const_iterator it,
+void static_analysis_baset::concurrent_fixedpoint(
   const goto_functionst &goto_functions)
 {
-  functions_done.insert(it->first);
-  return fixedpoint(it->second.body, goto_functions);
+  sequential_fixedpoint(goto_functions);
+
+  is_threadedt is_threaded(goto_functions);
+
+  // construct an initial shared state collecting the results of all
+  // functions
+  goto_programt tmp;
+  tmp.add_instruction();
+  goto_programt::const_targett sh_target=tmp.instructions.begin();
+  generate_state(sh_target);
+  statet &shared_state=get_state(sh_target);
+
+  typedef std::list<std::pair<goto_programt const*,
+                              goto_programt::const_targett> > thread_wlt;
+  thread_wlt thread_wl;
+
+  forall_goto_functions(it, goto_functions)
+    forall_goto_program_instructions(t_it, it->second.body)
+    {
+      if(is_threaded(t_it))
+      {
+        thread_wl.push_back(std::make_pair(&(it->second.body), t_it));
+
+        goto_programt::const_targett l_end=
+          it->second.body.instructions.end();
+        --l_end;
+
+        const statet &end_state=get_state(l_end);
+        merge_shared(shared_state, end_state, sh_target);
+      }
+    }
+
+  // new feed in the shared state into all concurrently executing
+  // functions, and iterate until the shared state stabilizes
+  bool new_shared=true;
+  while(new_shared)
+  {
+    new_shared=false;
+
+    for(thread_wlt::const_iterator it=thread_wl.begin();
+        it!=thread_wl.end();
+        ++it)
+    {
+      working_sett working_set;
+      put_in_working_set(working_set, it->second);
+
+      statet &begin_state=get_state(it->second);
+      merge(begin_state, shared_state, it->second);
+
+      while(!working_set.empty())
+      {
+        goto_programt::const_targett l=get_next(working_set);
+
+        visit(l, working_set, *(it->first), goto_functions);
+
+        // the underlying domain must make sure that the final state
+        // carries all possible values; otherwise we would need to
+        // merge over each and every state
+        if(l->is_end_function())
+        {
+          statet &end_state=get_state(l);
+          new_shared|=merge_shared(shared_state, end_state, sh_target);
+        }
+      }
+    }
+  }
 }
+
diff --git a/src/analyses/static_analysis.h b/src/analyses/static_analysis.h
index a4c7c13..c4308e6 100644
--- a/src/analyses/static_analysis.h
+++ b/src/analyses/static_analysis.h
@@ -26,14 +26,12 @@ public:
   virtual ~domain_baset()
   {
   }
-  
-  typedef goto_programt::const_targett locationt;
 
   // will go away,
   // to be replaced by a factory class option to static_analysist
   virtual void initialize(
     const namespacet &ns,
-    locationt l)
+    goto_programt::const_targett l)
   {
   }
 
@@ -47,8 +45,8 @@ public:
 
   virtual void transform(
     const namespacet &ns,
-    locationt from,
-    locationt to)=0;
+    goto_programt::const_targett from,
+    goto_programt::const_targett to)=0;
 
   virtual void output(
     const namespacet &ns,
@@ -70,7 +68,7 @@ public:
   
   // also add
   //
-  //   bool merge(const T &b, locationt to);
+  //   bool merge(const T &b, goto_programt::const_targett to);
   //
   // this computes the join between "this" and "b"
   // return true if "this" has changed
@@ -87,7 +85,6 @@ class static_analysis_baset
 {
 public:
   typedef domain_baset statet;
-  typedef goto_programt::const_targett locationt;
 
   explicit static_analysis_baset(const namespacet &_ns):
     ns(_ns),
@@ -144,9 +141,9 @@ public:
     output(goto_program, "", out);
   }
 
-  virtual bool has_location(locationt l) const=0;
+  virtual bool has_location(goto_programt::const_targett l) const=0;
   
-  void insert(locationt l)
+  void insert(goto_programt::const_targett l)
   {
     generate_state(l);
   }
@@ -154,11 +151,13 @@ public:
   // utilities  
   
   // get guard of a conditional edge
-  static exprt get_guard(locationt from, locationt to);
+  static exprt get_guard(
+    goto_programt::const_targett from,
+    goto_programt::const_targett to);
   
   // get lhs that return value is assigned to
   // for an edge that returns from a function
-  static exprt get_return_lhs(locationt to);
+  static exprt get_return_lhs(goto_programt::const_targett to);
 
 protected:
   const namespacet &ns;
@@ -168,16 +167,15 @@ protected:
     const irep_idt &identifier,
     std::ostream &out) const;
 
-  typedef std::map<unsigned, locationt> working_sett;
+  typedef std::map<unsigned, goto_programt::const_targett> working_sett;
   
-  locationt get_next(working_sett &working_set);
+  goto_programt::const_targett get_next(working_sett &working_set);
   
   void put_in_working_set(
     working_sett &working_set,
-    locationt l)
+    goto_programt::const_targett l)
   {
-    working_set.insert(
-      std::pair<unsigned, locationt>(l->location_number, l));
+    working_set.insert(std::make_pair(l->location_number, l));
   }
 
   // true = found s.th. new
@@ -185,27 +183,30 @@ protected:
     const goto_programt &goto_program,
     const goto_functionst &goto_functions);
     
-  bool fixedpoint(
-    goto_functionst::function_mapt::const_iterator it,
+  virtual void fixedpoint(
+    const goto_functionst &goto_functions)=0;
+
+  void sequential_fixedpoint(
     const goto_functionst &goto_functions);
-    
-  void fixedpoint(
+  void concurrent_fixedpoint(
     const goto_functionst &goto_functions);
 
   // true = found s.th. new
   bool visit(
-    locationt l,
+    goto_programt::const_targett l,
     working_sett &working_set,
     const goto_programt &goto_program,
     const goto_functionst &goto_functions);
-    
-  static locationt successor(locationt l)
-  {
-    l++;
-    return l;
-  }
   
-  virtual bool merge(statet &a, const statet &b, locationt to)=0;
+  virtual bool merge(
+    statet &a,
+    const statet &b,
+    goto_programt::const_targett to)=0;
+  // for concurrent fixedpoint
+  virtual bool merge_shared(
+    statet &a,
+    const statet &b,
+    goto_programt::const_targett to)=0;
   
   typedef std::set<irep_idt> functions_donet;
   functions_donet functions_done;
@@ -223,14 +224,16 @@ protected:
   
   // function calls
   void do_function_call_rec(
-    locationt l_call, locationt l_return,
+    goto_programt::const_targett l_call,
+    goto_programt::const_targett l_return,
     const exprt &function,
     const exprt::operandst &arguments,
     statet &new_state,
     const goto_functionst &goto_functions);
 
   void do_function_call(
-    locationt l_call, locationt l_return,
+    goto_programt::const_targett l_call,
+    goto_programt::const_targett l_return,
     const goto_functionst &goto_functions,
     const goto_functionst::function_mapt::const_iterator f_it,
     const exprt::operandst &arguments,
@@ -238,15 +241,15 @@ protected:
 
   // abstract methods
     
-  virtual void generate_state(locationt l)=0;
-  virtual statet &get_state(locationt l)=0;
-  virtual const statet &get_state(locationt l) const=0;
+  virtual void generate_state(goto_programt::const_targett l)=0;
+  virtual statet &get_state(goto_programt::const_targett l)=0;
+  virtual const statet &get_state(goto_programt::const_targett l) const=0;
   virtual statet* make_temporary_state(statet &s)=0;
 
   typedef domain_baset::expr_sett expr_sett;
 
   virtual void get_reference_set(
-    locationt l,
+    goto_programt::const_targett l,
     const exprt &expr,
     std::list<exprt> &dest)=0;
 };
@@ -262,16 +265,14 @@ public:
   {
   }
 
-  typedef goto_programt::const_targett locationt;
-
-  inline T &operator[](locationt l)
+  inline T &operator[](goto_programt::const_targett l)
   {
     typename state_mapt::iterator it=state_map.find(l);
     if(it==state_map.end()) throw "failed to find state";
     return it->second;
   }
     
-  inline const T &operator[](locationt l) const
+  inline const T &operator[](goto_programt::const_targett l) const
   {
     typename state_mapt::const_iterator it=state_map.find(l);
     if(it==state_map.end()) throw "failed to find state";
@@ -284,30 +285,33 @@ public:
     static_analysis_baset::clear();
   }
 
-  virtual bool has_location(locationt l) const
+  virtual bool has_location(goto_programt::const_targett l) const
   {
     return state_map.count(l)!=0;
   }
   
 protected:
-  typedef std::map<locationt, T> state_mapt;
+  typedef std::map<goto_programt::const_targett, T> state_mapt;
   state_mapt state_map;
 
-  virtual statet &get_state(locationt l)
+  virtual statet &get_state(goto_programt::const_targett l)
   {
     typename state_mapt::iterator it=state_map.find(l);
     if(it==state_map.end()) throw "failed to find state";
     return it->second;
   }
 
-  virtual const statet &get_state(locationt l) const
+  virtual const statet &get_state(goto_programt::const_targett l) const
   {
     typename state_mapt::const_iterator it=state_map.find(l);
     if(it==state_map.end()) throw "failed to find state";
     return it->second;
   }
 
-  virtual bool merge(statet &a, const statet &b, locationt to)
+  virtual bool merge(
+    statet &a,
+    const statet &b,
+    goto_programt::const_targett to)
   {
     return static_cast<T &>(a).merge(static_cast<const T &>(b), to);
   }
@@ -317,22 +321,64 @@ protected:
     return new T(static_cast<T &>(s));
   }
 
-  virtual void generate_state(locationt l)
+  virtual void generate_state(goto_programt::const_targett l)
   {
     state_map[l].initialize(ns, l);
   }
 
   virtual void get_reference_set(
-    locationt l,
+    goto_programt::const_targett l,
     const exprt &expr,
     std::list<exprt> &dest)
   {
     state_map[l].get_reference_set(ns, expr, dest);
   }
 
+  virtual void fixedpoint(const goto_functionst &goto_functions)
+  {
+    sequential_fixedpoint(goto_functions);
+  }
+
 private:  
   // to enforce that T is derived from domain_baset
   void dummy(const T &s) { const statet &x=dummy1(s); (void)x; }
+
+  // not implemented in sequential analyses
+  virtual bool merge_shared(
+    statet &a,
+    const statet &b,
+    goto_programt::const_targett to)
+  {
+    throw "not implemented";
+  }
+};
+
+template<typename T>
+class concurrency_aware_static_analysist:public static_analysist<T>
+{
+public:
+  // constructor
+  explicit concurrency_aware_static_analysist(const namespacet &_ns):
+    static_analysist<T>(_ns)
+  {
+  }
+
+  virtual bool merge_shared(
+    static_analysis_baset::statet &a,
+    const static_analysis_baset::statet &b,
+    goto_programt::const_targett to)
+  {
+    return static_cast<T &>(a).merge_shared(
+      this->ns,
+      static_cast<const T &>(b),
+      to);
+  }
+
+protected:
+  virtual void fixedpoint(const goto_functionst &goto_functions)
+  {
+    this->concurrent_fixedpoint(goto_functions);
+  }
 };
 
 #endif
diff --git a/src/analyses/uninitialized_domain.cpp b/src/analyses/uninitialized_domain.cpp
index c5fc067..f1cfefa 100644
--- a/src/analyses/uninitialized_domain.cpp
+++ b/src/analyses/uninitialized_domain.cpp
@@ -27,8 +27,8 @@ Function: uninitialized_domaint::transform
 
 void uninitialized_domaint::transform(
   const namespacet &ns,
-  locationt from,
-  locationt to)
+  goto_programt::const_targett from,
+  goto_programt::const_targett to)
 {
   switch(from->type)
   {
@@ -115,7 +115,7 @@ Function: uninitialized_domaint::merge
 
 bool uninitialized_domaint::merge(
   const uninitialized_domaint &other,
-  locationt to)
+  goto_programt::const_targett to)
 {
   unsigned old_uninitialized=uninitialized.size();
   
diff --git a/src/analyses/uninitialized_domain.h b/src/analyses/uninitialized_domain.h
index 4e199bf..b5689a3 100644
--- a/src/analyses/uninitialized_domain.h
+++ b/src/analyses/uninitialized_domain.h
@@ -19,15 +19,17 @@ public:
 
   virtual void transform(
     const namespacet &ns,
-    locationt from,
-    locationt to);
+    goto_programt::const_targett from,
+    goto_programt::const_targett to);
 
   virtual void output(
     const namespacet &ns,
     std::ostream &out) const;
   
   // returns true iff there is s.th. new
-  bool merge(const uninitialized_domaint &other, locationt to);
+  bool merge(
+    const uninitialized_domaint &other,
+    goto_programt::const_targett to);
   
 protected:
   void assign(const exprt &lhs);
diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile
index e6db701..c7e8249 100644
--- a/src/goto-instrument/Makefile
+++ b/src/goto-instrument/Makefile
@@ -12,7 +12,8 @@ SRC = goto_instrument_main.cpp goto_instrument_parseoptions.cpp \
       call_sequences.cpp unwind.cpp \
       accelerate/accelerate.cpp accelerate/polynomial.cpp \
       accelerate/scratch_program.cpp accelerate/polynomial_accelerator.cpp \
-      accelerate/util.cpp count_eloc.cpp reachability_slicer.cpp
+      accelerate/util.cpp count_eloc.cpp reachability_slicer.cpp \
+      wmm/static_cycles.cpp
 
 OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../linking/linking$(LIBEXT) \
diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp
index 9395968..8d71ed2 100644
--- a/src/goto-instrument/dump_c.cpp
+++ b/src/goto-instrument/dump_c.cpp
@@ -817,10 +817,11 @@ goto_programt::const_targett goto_program2codet::convert_return(
      to_side_effect_expr(ret.return_value()).get_statement()==ID_nondet)
   {
     const cfg_dominatorst &dominators=loops.get_dominator_info();
-    cfg_dominatorst::node_mapt::const_iterator i_entry=
-      dominators.node_map.find(target);
-    assert(i_entry!=dominators.node_map.end());
-    const cfg_dominatorst::nodet &n=i_entry->second;
+    cfg_dominatorst::cfgt::entry_mapt::const_iterator i_entry=
+      dominators.cfg.entry_map.find(target);
+    assert(i_entry!=dominators.cfg.entry_map.end());
+    const cfg_dominatorst::cfgt::nodet &n=
+      dominators.cfg[i_entry->second];
 
     if(n.dominators.empty())
     {
@@ -1057,10 +1058,10 @@ goto_programt::const_targett goto_program2codet::convert_goto_switch(
 
   // always use convert_goto_if for dead code as the construction below relies
   // on effective dominator information 
-  cfg_dominatorst::node_mapt::const_iterator t_entry=
-    dominators.node_map.find(target);
-  assert(t_entry!=dominators.node_map.end());
-  if(t_entry->second.dominators.empty())
+  cfg_dominatorst::cfgt::entry_mapt::const_iterator t_entry=
+    dominators.cfg.entry_map.find(target);
+  assert(t_entry!=dominators.cfg.entry_map.end());
+  if(dominators.cfg[t_entry->second].dominators.empty())
     return convert_goto_if(target, upper_bound, dest);
 
   // maybe, let's try some more
@@ -1193,10 +1194,11 @@ goto_programt::const_targett goto_program2codet::convert_goto_switch(
         case_end!=upper_bound;
         ++case_end)
     {
-      cfg_dominatorst::node_mapt::const_iterator i_entry=
-        dominators.node_map.find(case_end);
-      assert(i_entry!=dominators.node_map.end());
-      const cfg_dominatorst::nodet &n=i_entry->second;
+      cfg_dominatorst::cfgt::entry_mapt::const_iterator i_entry=
+        dominators.cfg.entry_map.find(case_end);
+      assert(i_entry!=dominators.cfg.entry_map.end());
+      const cfg_dominatorst::cfgt::nodet &n=
+        dominators.cfg[i_entry->second];
 
       // ignore dead instructions for the following checks
       if(n.dominators.empty())
@@ -1256,10 +1258,11 @@ goto_programt::const_targett goto_program2codet::convert_goto_switch(
     if(processed_locations.find(it->location_number)==
         processed_locations.end())
     {
-      cfg_dominatorst::node_mapt::const_iterator it_entry=
-        dominators.node_map.find(it);
-      assert(it_entry!=dominators.node_map.end());
-      const cfg_dominatorst::nodet &n=it_entry->second;
+      cfg_dominatorst::cfgt::entry_mapt::const_iterator it_entry=
+        dominators.cfg.entry_map.find(it);
+      assert(it_entry!=dominators.cfg.entry_map.end());
+      const cfg_dominatorst::cfgt::nodet &n=
+        dominators.cfg[it_entry->second];
 
       if(!n.dominators.empty())
         return convert_goto_if(orig_target, upper_bound, dest);
diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp
index 334622a..2c046bf 100644
--- a/src/goto-instrument/full_slicer.cpp
+++ b/src/goto-instrument/full_slicer.cpp
@@ -33,33 +33,38 @@ void full_slicert::fixedpoint()
       e_it=cfg.entry_map.begin();
       e_it!=cfg.entry_map.end();
       e_it++)
+  {
+    cfgt::nodet &node=cfg[e_it->second];
+
     if(e_it->first->is_assert())
     {
-      get_objects(e_it->first->guard, e_it->second.required_objects);
-      e_it->second.node_required=true;
-      queue.push(&e_it->second);
+      get_objects(e_it->first->guard, node.required_objects);
+      node.node_required=true;
+      queue.push(e_it->second);
     }
     else if(e_it->first->is_end_function())
-      e_it->second.node_required=true; // always retained
+      node.node_required=true; // always retained
+  }
 
   // process queue until empty
   while(!queue.empty())
   {
-    cfgt::iterator e=queue.top();
+    cfgt::entryt e=queue.top();
+    cfgt::nodet &node=cfg[e];
     queue.pop();
     
     // look at required_objects
-    object_id_sett required_objects=transform(e);
+    object_id_sett required_objects=transform(node);
 
-    for(cfgt::entriest::const_iterator
-        p_it=e->predecessors.begin();
-        p_it!=e->predecessors.end();
+    for(cfgt::edgest::const_iterator
+        p_it=node.in.begin();
+        p_it!=node.in.end();
         p_it++)
     {
-      (*p_it)->required_objects.insert(
+      cfg[p_it->first].required_objects.insert(
         required_objects.begin(), required_objects.end());
 
-      queue.push(*p_it);
+      queue.push(p_it->first);
     }
   }
 }
@@ -93,7 +98,7 @@ void full_slicert::slice(goto_functionst &goto_functions)
       Forall_goto_program_instructions(i_it, f_it->second.body)
       {
         const cfgt::entryt &e=cfg.entry_map[i_it];
-        if(!e.node_required)
+        if(!cfg[e].node_required)
           i_it->make_skip();
       }
     }
@@ -115,12 +120,12 @@ Function: full_slicert::transform
 
 \*******************************************************************/
 
-object_id_sett full_slicert::transform(cfgt::iterator e)
+object_id_sett full_slicert::transform(cfgt::nodet& e)
 {
-  const object_id_sett &old_set=e->required_objects;
-  object_id_sett new_set=e->required_objects; // copy!
+  const object_id_sett &old_set=e.required_objects;
+  object_id_sett new_set=e.required_objects; // copy!
   
-  const goto_programt::instructiont &instruction=*(e->PC);
+  const goto_programt::instructiont &instruction=*(e.PC);
 
   switch(instruction.type)
   {
@@ -140,7 +145,7 @@ object_id_sett full_slicert::transform(cfgt::iterator e)
 
       if(found)
       {
-        e->node_required=true;
+        e.node_required=true;
         new_set.insert(w.begin(), w.end());
       }
     }    
@@ -162,7 +167,7 @@ object_id_sett full_slicert::transform(cfgt::iterator e)
 
       if(found)
       {
-        e->node_required=true;
+        e.node_required=true;
         new_set.insert(w.begin(), w.end());
       }
     }
@@ -199,7 +204,7 @@ object_id_sett full_slicert::transform(cfgt::iterator e)
 
       if(found)
       {
-        e->node_required=true;
+        e.node_required=true;
         // add what it reads
         get_objects_r(code_assign, new_set);
       }
@@ -211,7 +216,7 @@ object_id_sett full_slicert::transform(cfgt::iterator e)
       object_idt object_id(to_symbol_expr(instruction.code.op0()));
       if(old_set.find(object_id)!=old_set.end())
       {
-        e->node_required=true;
+        e.node_required=true;
         new_set.erase(object_id);
       }
     }
@@ -239,7 +244,7 @@ object_id_sett full_slicert::transform(cfgt::iterator e)
         if(old_set.find(lhs_id)!=old_set.end())
         {
           new_set.erase(lhs_id);
-          e->node_required=true;
+          e.node_required=true;
           get_objects(code_function_call.arguments()[i], new_set);
         }
       }
diff --git a/src/goto-instrument/full_slicer_class.h b/src/goto-instrument/full_slicer_class.h
index 0bb9c29..ec824cb 100644
--- a/src/goto-instrument/full_slicer_class.h
+++ b/src/goto-instrument/full_slicer_class.h
@@ -46,11 +46,11 @@ protected:
   typedef cfg_baset<cfg_nodet> cfgt;
   cfgt cfg;
 
-  typedef std::stack<cfgt::iterator> queuet;
+  typedef std::stack<cfgt::entryt> queuet;
 
   void fixedpoint();
   void slice(goto_functionst &goto_functions);
-  object_id_sett transform(cfgt::iterator);
+  object_id_sett transform(cfgt::nodet&);
 };
 
 #endif
diff --git a/src/goto-instrument/goto_instrument_parseoptions.cpp b/src/goto-instrument/goto_instrument_parseoptions.cpp
index b624f26..410fa0a 100644
--- a/src/goto-instrument/goto_instrument_parseoptions.cpp
+++ b/src/goto-instrument/goto_instrument_parseoptions.cpp
@@ -35,7 +35,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <pointer-analysis/show_value_sets.h>
 
 #include <analyses/natural_loops.h>
-#include <analyses/local_may_alias.h>
+#include <analyses/may_alias.h>
 #include <analyses/goto_check.h>
 #include <analyses/call_graph.h>
 #include <analyses/interval_analysis.h>
@@ -70,6 +70,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "call_sequences.h"
 #include "accelerate/accelerate.h"
 #include "count_eloc.h"
+#include "wmm/static_cycles.h"
 
 /*******************************************************************\
 
@@ -164,15 +165,23 @@ int goto_instrument_parseoptionst::doit()
       status() << "Partial Inlining" << eom;
       goto_partial_inline(goto_functions, ns, ui_message_handler);
     
-      forall_goto_functions(it, goto_functions)
-      {
-        local_may_aliast local_may_alias(it->second);
-        std::cout << ">>>>" << std::endl;
-        std::cout << ">>>> " << it->first << std::endl;
-        std::cout << ">>>>" << std::endl;
-        local_may_alias.output(std::cout, it->second, ns);
-        std::cout << std::endl;
-      }
+      may_aliast may_alias(goto_functions, ns);
+      may_alias.output(std::cout, goto_functions);
+
+      return 0;
+    }
+
+    if(cmdline.isset("static-cycles"))
+    {
+      namespacet ns(symbol_table);
+
+      status() << "Function Pointer Removal" << eom;
+      remove_function_pointers(symbol_table, goto_functions, false);
+
+      status() << "Partial Inlining" << eom;
+      goto_partial_inline(goto_functions, ns, ui_message_handler);
+
+      static_cycles(symbol_table, goto_functions);
 
       return 0;
     }
@@ -257,6 +266,9 @@ int goto_instrument_parseoptionst::doit()
 
     if(cmdline.isset("show-reaching-definitions"))
     {
+      status() << "Function Pointer Removal" << eom;
+      remove_function_pointers(symbol_table, goto_functions, false);
+
       const namespacet ns(symbol_table);
       reaching_definitions_analysist rd_analysis(ns);
       rd_analysis(goto_functions);
@@ -574,7 +586,7 @@ void goto_instrument_parseoptionst::instrument_goto_program(
 
   // we add the library in some cases, as some analyses benefit
 
-  if(cmdline.isset("mm"))
+  if(cmdline.isset("mm") || cmdline.isset("static-cycles"))
   {
     status() << "Adding CPROVER library" << eom;
     link_to_library(symbol_table, goto_functions, ui_message_handler);
@@ -777,7 +789,7 @@ void goto_instrument_parseoptionst::instrument_goto_program(
   if(cmdline.isset("havoc-loops"))
   {
     status() << "Havocing loops" << eom;
-    havoc_loops(goto_functions);
+    havoc_loops(goto_functions, ns);
   }
 
   if(cmdline.isset("k-induction"))
@@ -798,7 +810,7 @@ void goto_instrument_parseoptionst::instrument_goto_program(
     status() << "Instrumenting k-induction for k=" << k << ", "
              << (base_case?"base case":"step case") << eom;
     
-    k_induction(goto_functions, base_case, step_case, k);
+    k_induction(goto_functions, base_case, step_case, k, ns);
   }
 
   if(cmdline.isset("function-enter"))
@@ -943,6 +955,7 @@ void goto_instrument_parseoptionst::help()
     " --no-po-rendering            no representation of the threads in the dot\n"
     " --render-cluster-file        clusterises the dot by files\n"
     " --render-cluster-function    clusterises the dot by functions\n"
+    " --static-cycles              identify potentially critical cycles\n"
     "\n"
     "Slicing:\n"
     " --reachability-slicer        slice away instructions that can't reach assertions\n"
diff --git a/src/goto-instrument/goto_instrument_parseoptions.h b/src/goto-instrument/goto_instrument_parseoptions.h
index 3c2141a..9585717 100644
--- a/src/goto-instrument/goto_instrument_parseoptions.h
+++ b/src/goto-instrument/goto_instrument_parseoptions.h
@@ -54,7 +54,7 @@ Author: Daniel Kroening, kroening@kroening.com
   "(accelerate)" \
   "(k-induction):(step-case)(base-case)" \
   "(show-call-sequences)(check-call-sequence)" \
-  "(interpreter)(show-reaching-definitions)(count-eloc)"
+  "(interpreter)(show-reaching-definitions)(count-eloc)(static-cycles)"
 
 class goto_instrument_parseoptionst:
   public parseoptions_baset,
diff --git a/src/goto-instrument/havoc_loops.cpp b/src/goto-instrument/havoc_loops.cpp
index c85419b..d5ff26c 100644
--- a/src/goto-instrument/havoc_loops.cpp
+++ b/src/goto-instrument/havoc_loops.cpp
@@ -20,9 +20,11 @@ class havoc_loopst
 public:
   typedef goto_functionst::goto_functiont goto_functiont;
   
-  explicit havoc_loopst(goto_functiont &_goto_function):
+  havoc_loopst(
+    goto_functiont &_goto_function,
+    const namespacet &ns):
     goto_function(_goto_function),
-    local_may_alias(_goto_function),
+    local_may_alias(_goto_function, ns),
     natural_loops(_goto_function.body)
   {
     havoc_loops();
@@ -283,8 +285,10 @@ Function: havoc_loops
 
 \*******************************************************************/
 
-void havoc_loops(goto_functionst &goto_functions)
+void havoc_loops(
+  goto_functionst &goto_functions,
+  const namespacet &ns)
 {
   Forall_goto_functions(it, goto_functions)
-    havoc_loopst(it->second);
+    havoc_loopst(it->second, ns);
 }
diff --git a/src/goto-instrument/havoc_loops.h b/src/goto-instrument/havoc_loops.h
index bf58e12..ca04af3 100644
--- a/src/goto-instrument/havoc_loops.h
+++ b/src/goto-instrument/havoc_loops.h
@@ -11,6 +11,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <goto-programs/goto_functions.h>
 
-void havoc_loops(goto_functionst &goto_functions);
+void havoc_loops(
+  goto_functionst &goto_functions,
+  const namespacet &ns);
 
 #endif
diff --git a/src/goto-instrument/k_induction.cpp b/src/goto-instrument/k_induction.cpp
index 3f8ff5e..6990959 100644
--- a/src/goto-instrument/k_induction.cpp
+++ b/src/goto-instrument/k_induction.cpp
@@ -24,9 +24,9 @@ public:
   k_inductiont(
     goto_functiont &_goto_function,
     bool _base_case, bool _step_case,
-    unsigned _k):
+    unsigned _k, const namespacet &ns):
     goto_function(_goto_function),
-    local_may_alias(_goto_function),
+    local_may_alias(_goto_function, ns),
     natural_loops(_goto_function.body),
     base_case(_base_case), step_case(_step_case), k(_k)
   {
@@ -302,8 +302,8 @@ Function: k_induction
 void k_induction(
   goto_functionst &goto_functions,
   bool base_case, bool step_case,
-  unsigned k)
+  unsigned k, const namespacet &ns)
 {
   Forall_goto_functions(it, goto_functions)
-    k_inductiont(it->second, base_case, step_case, k);
+    k_inductiont(it->second, base_case, step_case, k, ns);
 }
diff --git a/src/goto-instrument/k_induction.h b/src/goto-instrument/k_induction.h
index 207270d..825fbdf 100644
--- a/src/goto-instrument/k_induction.h
+++ b/src/goto-instrument/k_induction.h
@@ -14,6 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com
 void k_induction(
   goto_functionst &goto_functions,
   bool base_case, bool step_case,
-  unsigned k);
+  unsigned k, const namespacet &ns);
 
 #endif
diff --git a/src/goto-instrument/points_to.cpp b/src/goto-instrument/points_to.cpp
index ead548f..4cc9941 100644
--- a/src/goto-instrument/points_to.cpp
+++ b/src/goto-instrument/points_to.cpp
@@ -35,7 +35,7 @@ void points_tot::fixedpoint()
         e_it!=cfg.entry_map.end();
         e_it++)
     {
-      if(transform(&e_it->second))
+      if(transform(cfg[e_it->second]))
         added=true;
     }
   }
@@ -87,10 +87,10 @@ Function: points_tot::transform
 
 \*******************************************************************/
 
-bool points_tot::transform(cfgt::iterator e)
+bool points_tot::transform(const cfgt::nodet &e)
 {
   bool result=false;
-  const goto_programt::instructiont &instruction=*(e->PC);
+  const goto_programt::instructiont &instruction=*(e.PC);
 
   switch(instruction.type)
   {
diff --git a/src/goto-instrument/points_to.h b/src/goto-instrument/points_to.h
index dc1637e..58dca7d 100644
--- a/src/goto-instrument/points_to.h
+++ b/src/goto-instrument/points_to.h
@@ -57,21 +57,14 @@ public:
   }
           
 protected:
-  struct cfg_nodet
-  {
-    cfg_nodet()
-    {
-    }
-  };
-
-  typedef cfg_baset<cfg_nodet> cfgt;
+  typedef cfg_baset<empty_cfg_nodet> cfgt;
   cfgt cfg;
 
   typedef std::map<object_idt, object_id_sett> value_mapt;
   value_mapt value_map;
   
   void fixedpoint();
-  bool transform(cfgt::iterator);
+  bool transform(const cfgt::nodet&);
   
   const object_id_sett empty_set;
 };
diff --git a/src/goto-instrument/reachability_slicer.cpp b/src/goto-instrument/reachability_slicer.cpp
index 43f1d3c..d2e1d49 100644
--- a/src/goto-instrument/reachability_slicer.cpp
+++ b/src/goto-instrument/reachability_slicer.cpp
@@ -40,23 +40,24 @@ void reachability_slicert::fixedpoint_assertions(
       e_it++)
     if(e_it->first->is_assert() ||
        is_threaded(e_it->first))
-      queue.push(&e_it->second);
+      queue.push(e_it->second);
 
   while(!queue.empty())
   {
-    cfgt::iterator e=queue.top();
+    cfgt::entryt e=queue.top();
+    cfgt::nodet &node=cfg[e];
     queue.pop();
 
-    if(e->reaches_assertion) continue;
+    if(node.reaches_assertion) continue;
 
-    e->reaches_assertion=true;
+    node.reaches_assertion=true;
     
-    for(cfgt::entriest::const_iterator
-        p_it=e->predecessors.begin();
-        p_it!=e->predecessors.end();
+    for(cfgt::edgest::const_iterator
+        p_it=node.in.begin();
+        p_it!=node.in.end();
         p_it++)
     {
-      queue.push(*p_it);
+      queue.push(p_it->first);
     }
   }
 }
@@ -83,7 +84,7 @@ void reachability_slicert::slice(goto_functionst &goto_functions)
     {
       Forall_goto_program_instructions(i_it, f_it->second.body)
       {
-        const cfgt::entryt &e=cfg.entry_map[i_it];
+        const cfgt::nodet &e=cfg[cfg.entry_map[i_it]];
         if(!e.reaches_assertion &&
            !i_it->is_end_function())
           i_it->make_goto(i_it);
diff --git a/src/goto-instrument/reachability_slicer_class.h b/src/goto-instrument/reachability_slicer_class.h
index f21f39c..fd7a71a 100644
--- a/src/goto-instrument/reachability_slicer_class.h
+++ b/src/goto-instrument/reachability_slicer_class.h
@@ -46,7 +46,7 @@ protected:
   typedef cfg_baset<slicer_entryt> cfgt;
   cfgt cfg;
 
-  typedef std::stack<cfgt::iterator> queuet;
+  typedef std::stack<cfgt::entryt> queuet;
 
   void fixedpoint_assertions(const is_threadedt &is_threaded);
 
diff --git a/src/goto-instrument/wmm/abstract_event.cpp b/src/goto-instrument/wmm/abstract_event.cpp
index 485b5d2..0b07561 100644
--- a/src/goto-instrument/wmm/abstract_event.cpp
+++ b/src/goto-instrument/wmm/abstract_event.cpp
@@ -81,6 +81,9 @@ bool abstract_eventt::unsafe_pair_lwfence_param(const abstract_eventt& next,
       || (thread!=next.thread && operation==Write && next.operation==Read
         && variable==next.variable));
 
+  case Static_Weak:
+    return true;
+
   case Unknown:;
   }
   assert(false);
@@ -138,6 +141,9 @@ bool abstract_eventt::unsafe_pair_asm(const abstract_eventt& next,
       || (thread!=next.thread && operation==Write && next.operation==Read
         && variable==next.variable));
 
+  case Static_Weak:
+    return true;
+
   case Unknown:;
   }
   assert(false);
diff --git a/src/goto-instrument/wmm/abstract_event.h b/src/goto-instrument/wmm/abstract_event.h
index 7ff6c52..d9a9f31 100644
--- a/src/goto-instrument/wmm/abstract_event.h
+++ b/src/goto-instrument/wmm/abstract_event.h
@@ -20,7 +20,7 @@ Date: 2012
                           abstract event
 \*******************************************************************/
 
-class abstract_eventt:public graph_nodet<empty_nodet>
+class abstract_eventt:public graph_nodet<empty_edget>
 {
 protected:
   bool unsafe_pair_lwfence_param(const abstract_eventt& next,
diff --git a/src/goto-instrument/wmm/cycle_collection.cpp b/src/goto-instrument/wmm/cycle_collection.cpp
index 12005d3..6098a86 100644
--- a/src/goto-instrument/wmm/cycle_collection.cpp
+++ b/src/goto-instrument/wmm/cycle_collection.cpp
@@ -91,6 +91,7 @@ void event_grapht::graph_explorert::collect_cycles(
     order=&egraph.po_order;
     break;
   case Power:
+  case Static_Weak:
     order=&egraph.poUrfe_order;
     break;
 
@@ -302,7 +303,8 @@ bool event_grapht::graph_explorert::backtrack(
        this means that we can have at most 2 consecutive events by po
        with the same variable, and two variables per thread (fences are
        not taken into account) */
-    if(!point_stack.empty() && egraph.are_po_ordered(point_stack.top(),vertex)
+    if(egraph.filter_uniproc &&
+       !point_stack.empty() && egraph.are_po_ordered(point_stack.top(),vertex)
       && this_vertex.operation!=abstract_eventt::Fence
       && this_vertex.operation!=abstract_eventt::Lwfence
       && this_vertex.operation!=abstract_eventt::ASMfence
@@ -393,7 +395,7 @@ bool event_grapht::graph_explorert::backtrack(
         const unsigned w = w_it->first;
         if(w < source)
           egraph.remove_po_edge(vertex,w);
-        else if(w == source && point_stack.size()>=4
+        else if(w == source && (point_stack.size()>=4 || model==Static_Weak)
           && (unsafe_met_updated
             || this_vertex.unsafe_pair(egraph[source],model)) )
         {
@@ -437,7 +439,7 @@ bool event_grapht::graph_explorert::backtrack(
       const unsigned w = w_it->first;
       if(w < source)
         egraph.remove_com_edge(vertex,w);
-      else if(w == source && point_stack.size()>=4
+      else if(w == source && (point_stack.size()>=4 || model==Static_Weak)
         && (unsafe_met_updated 
           || this_vertex.unsafe_pair(egraph[source],model)) )
       {
diff --git a/src/goto-instrument/wmm/event_graph.cpp b/src/goto-instrument/wmm/event_graph.cpp
index 5c80ad0..120d15f 100644
--- a/src/goto-instrument/wmm/event_graph.cpp
+++ b/src/goto-instrument/wmm/event_graph.cpp
@@ -179,6 +179,23 @@ bool event_grapht::critical_cyclet::is_unsafe(memory_modelt model, bool fast)
   DEBUG_MESSAGE("cycle is safe?");
   bool unsafe_met=false;
 
+  bool has_memory_access=false;
+  for(const_iterator it=begin();
+      it!=end() && !has_memory_access;
+      ++it)
+  {
+    const abstract_eventt& it_evt=egraph[*it];
+
+    has_memory_access=
+      it_evt.operation==abstract_eventt::Read ||
+      it_evt.operation==abstract_eventt::Write;
+  }
+  if(!has_memory_access)
+    return false;
+
+  if(model==Static_Weak)
+    return size()>=2;
+
   /* critical cycles contain at least 4 events */
   if(size()<4)
     return false;
@@ -467,6 +484,23 @@ bool event_grapht::critical_cyclet::is_unsafe_asm(memory_modelt model,
   bool unsafe_met = false;
   unsigned char fences_met = 0;
 
+  bool has_memory_access=false;
+  for(const_iterator it=begin();
+      it!=end() && !has_memory_access;
+      ++it)
+  {
+    const abstract_eventt& it_evt=egraph[*it];
+
+    has_memory_access=
+      it_evt.operation==abstract_eventt::Read ||
+      it_evt.operation==abstract_eventt::Write;
+  }
+  if(!has_memory_access)
+    return false;
+
+  if(model==Static_Weak)
+    return size()>=2;
+
   /* critical cycles contain at least 4 events */
   if(size()<4)
     return false;
@@ -1298,7 +1332,7 @@ std::string event_grapht::critical_cyclet::print_name(
         const abstract_eventt& succ=egraph[*n_it];
         assert(succ.operation == abstract_eventt::Read ||
                succ.operation == abstract_eventt::Write);
-        name += (model==Power?" Sync":" MFence"); 
+        name += (model==Power||model==Static_Weak?" Sync":" MFence"); 
         name += (prev.variable==succ.variable?"s":"d")
           + prev.get_operation() + succ.get_operation();
       }
@@ -1327,7 +1361,7 @@ std::string event_grapht::critical_cyclet::print_name(
           else if(cand.operation == abstract_eventt::Fence ||
                   (cand.operation == abstract_eventt::ASMfence &&
                    cand.fence_value()&1))
-            cand_name = (model==Power?" Sync":" MFence"); 
+            cand_name = (model==Power||model==Static_Weak?" Sync":" MFence"); 
           if(!wraparound) ++cur_it;
           if(!wraparound) ++extra_fence_count;
         }
@@ -1343,7 +1377,7 @@ std::string event_grapht::critical_cyclet::print_name(
       {
         std::string cand_name;
         if(cur.fence_value()&1)
-          cand_name = (model==Power?" Sync":" MFence"); 
+          cand_name = (model==Power||model==Static_Weak?" Sync":" MFence"); 
         else
           cand_name = " LwSync";
         const_iterator n_it=cur_it;
@@ -1367,7 +1401,7 @@ std::string event_grapht::critical_cyclet::print_name(
           else if(cand.operation == abstract_eventt::Fence ||
                   (cand.operation == abstract_eventt::ASMfence &&
                    cand.fence_value()&1))
-            cand_name = (model==Power?" Sync":" MFence"); 
+            cand_name = (model==Power||model==Static_Weak?" Sync":" MFence"); 
           if(!wraparound) ++cur_it;
           if(!wraparound) ++extra_fence_count;
         }
@@ -1472,7 +1506,7 @@ std::string event_grapht::critical_cyclet::print_name(
       else if(cand.operation == abstract_eventt::Fence ||
               (cand.operation == abstract_eventt::ASMfence &&
                cand.fence_value()&1))
-        cand_name = (model==Power?" Sync":" MFence");
+        cand_name = (model==Power||model==Static_Weak?" Sync":" MFence");
     }
     assert(it!=reduced.begin() && it!=reduced.end());
     const abstract_eventt& succ=egraph[*it];
@@ -1596,7 +1630,7 @@ void event_grapht::critical_cyclet::print_dot(
         const abstract_eventt& succ=( n_it!=end() ?
           egraph[*n_it] : egraph[front()] );
         str << succ.id << "[label=\"";
-        str << (model==Power?"Sync":"MFence"); 
+        str << (model==Power||model==Static_Weak?"Sync":"MFence"); 
         str << (prev.variable==cur.variable?"s":"d");
         str << prev.get_operation() << succ.get_operation();
       }
@@ -1668,7 +1702,7 @@ void event_grapht::critical_cyclet::print_dot(
     ++next;
     const abstract_eventt& succ=egraph[*next];
     str << succ.id << "[label=\"";
-    str << (model==Power?"Sync":"MFence");
+    str << (model==Power||model==Static_Weak?"Sync":"MFence");
     str << (last.variable==first.variable?"s":"d");
     str << last.get_operation() << succ.get_operation();
   }
diff --git a/src/goto-instrument/wmm/event_graph.h b/src/goto-instrument/wmm/event_graph.h
index 84a6063..7ed9730 100644
--- a/src/goto-instrument/wmm/event_graph.h
+++ b/src/goto-instrument/wmm/event_graph.h
@@ -68,7 +68,7 @@ public:
     bool is_cycle()
     {
       /* size check */
-      if(size()<4)
+      if(size()<2)
         return false;
 
       /* po order check */
@@ -193,6 +193,7 @@ public:
   };
 
 protected:
+public:
   /* graph contains po and com transitions */
   graph<abstract_eventt> po_graph;
   graph<abstract_eventt> com_graph;
diff --git a/src/goto-instrument/wmm/goto2graph.cpp b/src/goto-instrument/wmm/goto2graph.cpp
index 34e398b..f19c38c 100644
--- a/src/goto-instrument/wmm/goto2graph.cpp
+++ b/src/goto-instrument/wmm/goto2graph.cpp
@@ -23,7 +23,10 @@ Date: 2012
 #include <util/message.h>
 #include <util/i2string.h>
 
-#include "../rw_set.h"
+#include <goto-programs/goto_functions.h>
+
+#include <analyses/goto_rw.h>
+
 #include "fence.h"
 #include "goto2graph.h"
 
@@ -109,7 +112,7 @@ Function: instrumentert::extract_events_rw
 \*******************************************************************/
 
 void instrumentert::extract_events_rw(
-  value_setst& value_sets,
+  may_aliast& may_alias,
   memory_modelt model,
   bool no_dependencies,
   goto_programt::const_targett target,
@@ -117,16 +120,17 @@ void instrumentert::extract_events_rw(
 {
   const goto_programt::instructiont &instruction=*target;
 
-  rw_set_loct rw_set(ns, value_sets, target);
+  rw_range_set_dereft rw_set(ns, may_alias);
+  goto_rw(target, rw_set);
 
   /* Read (Rb) */
-  forall_rw_set_r_entries(r_it, rw_set)
+  forall_rw_range_set_r_objects(r_it, rw_set)
   {
     /* creates Read:
        read is the irep_id of the read in the code;
        new_read_event is the corresponding abstract event;
        new_read_node is the node in the graph */
-    const irep_idt& read=r_it->second.object;
+    const irep_idt& read=r_it->first;
 
     /* skip local variables */
     if(local(read))
@@ -154,13 +158,13 @@ void instrumentert::extract_events_rw(
   }
 
   /* Write (Wa) */
-  forall_rw_set_w_entries(w_it, rw_set)
+  forall_rw_range_set_w_objects(w_it, rw_set)
   {
     /* creates Write:
        write is the irep_id in the code;
        new_write_event is the corresponding abstract event;
        new_write_node is the node in the graph */
-    const irep_idt& write = w_it->second.object;
+    const irep_idt& write = w_it->first;
     /* skip local variables */
     if(local(write))
       continue;
@@ -191,11 +195,11 @@ void instrumentert::extract_events_rw(
   if(target->is_assign() &&
      !no_dependencies)
   {
-    forall_rw_set_w_entries(write_it, rw_set)
-      forall_rw_set_r_entries(read_it, rw_set)
+    forall_rw_range_set_w_objects(write_it, rw_set)
+      forall_rw_range_set_r_objects(read_it, rw_set)
       {
-        const irep_idt& write=write_it->second.object;
-        const irep_idt& read=read_it->second.object;
+        const irep_idt& write=write_it->first;
+        const irep_idt& read=read_it->first;
         DEBUG_MESSAGE("dp: Write:"<<write<<"; Read:"<<read);
         const datat read_p(read,instruction.location);
         const datat write_p(write,instruction.location);
@@ -203,11 +207,11 @@ void instrumentert::extract_events_rw(
         }
     data_dp.dp_merge();
 
-    forall_rw_set_r_entries(read2_it, rw_set)
-      forall_rw_set_r_entries(read_it, rw_set)
+    forall_rw_range_set_r_objects(read2_it, rw_set)
+      forall_rw_range_set_r_objects(read_it, rw_set)
       {
-        const irep_idt& read2=read2_it->second.object;
-        const irep_idt& read=read_it->second.object;
+        const irep_idt& read2=read2_it->first;
+        const irep_idt& read=read_it->first;
         if(read2==read)
           continue;
         const datat read_p(read,instruction.location);
@@ -303,15 +307,15 @@ Function: instrumentert::extract_events
 \*******************************************************************/
 
 void instrumentert::extract_events(
-  value_setst& value_sets,
+  may_aliast& may_alias,
   memory_modelt model,
   bool no_dependencies,
-  cfgt::entryt &cfg_entry)
+  cfgt::nodet &cfg_entry)
 {
   goto_programt::const_targett target=cfg_entry.PC;
   thread_eventst &dest=cfg_entry.events[thread];
 
-  extract_events_rw(value_sets, model, no_dependencies, target, dest);
+  extract_events_rw(may_alias, model, no_dependencies, target, dest);
   extract_events_fence(model, target, dest);
 }
 
@@ -328,18 +332,18 @@ Function: instrumentert::forward_traverse_once
 \*******************************************************************/
 
 void instrumentert::forward_traverse_once(
-    value_setst& value_sets,
+    may_aliast &may_alias,
     memory_modelt model,
     bool no_dependencies,
     goto_programt::const_targett target)
 {
-  cfgt::entryt &cfg_entry=cfg.entry_map[target];
+  cfgt::nodet &cfg_entry=cfg[cfg.entry_map[target]];
 
   // we extract events only once per thread; this also means that
   // we do not track call stacks
   if(cfg_entry.events.find(thread)==cfg_entry.events.end())
     extract_events(
-      value_sets,
+      may_alias,
       model,
       no_dependencies,
       cfg_entry);
@@ -358,19 +362,19 @@ void instrumentert::forward_traverse_once(
     thread=++max_thread;
     assert(instruction.targets.size()==1);
     forward_traverse_once(
-      value_sets,
+      may_alias,
       model,
       no_dependencies,
       instruction.targets.front());
 
     thread=coming_from;
 
-    assert(cfg_entry.successors.size()==1 &&
-           cfg_entry.successors.front()->PC==next_PC);
+    assert(cfg_entry.out.size()==1 &&
+           cfg[cfg_entry.out.begin()->first].PC==next_PC);
   }
   else if(instruction.is_end_thread())
   {
-    assert(cfg_entry.successors.empty());
+    assert(cfg_entry.out.empty());
   }
   else if(instruction.is_function_call())
   {
@@ -378,19 +382,19 @@ void instrumentert::forward_traverse_once(
     const irep_idt& fun_id=to_symbol_expr(fun).get_identifier();
 
     // do not enter recursion and skip __CPROVER_initialize
-    assert(cfg_entry.successors.size()==1);
-    if(cfg_entry.successors.front()->PC!=next_PC)
+    assert(cfg_entry.out.size()==1);
+    if(cfg[cfg_entry.out.begin()->first].PC!=next_PC)
     {
       if(fun_id!=CPROVER_PREFIX "initialize" &&
          functions_met.insert(fun_id).second)
         forward_traverse_once(
-          value_sets,
+          may_alias,
           model,
           no_dependencies,
-          cfg_entry.successors.front()->PC);
+          cfg[cfg_entry.out.begin()->first].PC);
 
       forward_traverse_once(
-        value_sets,
+        may_alias,
         model,
         no_dependencies,
         next_PC);
@@ -410,15 +414,15 @@ void instrumentert::forward_traverse_once(
   }
   else if(instruction.is_goto())
   {
-    for(cfgt::entriest::const_iterator
-        it=cfg_entry.successors.begin();
-        it!=cfg_entry.successors.end();
+    for(cfgt::edgest::const_iterator
+        it=cfg_entry.out.begin();
+        it!=cfg_entry.out.end();
         ++it)
     {
-      const cfgt::entryt &succ_entry=cfg.entry_map[(*it)->PC];
+      const cfgt::nodet &succ_entry=cfg[it->first];
       if(succ_entry.events.find(thread)==succ_entry.events.end())
         forward_traverse_once(
-          value_sets,
+          may_alias,
           model,
           no_dependencies,
           succ_entry.PC);
@@ -427,19 +431,19 @@ void instrumentert::forward_traverse_once(
     return;
   }
 
-  if(cfg_entry.successors.empty())
+  if(cfg_entry.out.empty())
   {
     /* forward traversal done for this thread or branch */
     return;
   }
 
-  assert(cfg_entry.successors.size()==1);
+  assert(cfg_entry.out.size()==1);
 
   forward_traverse_once(
-    value_sets,
+    may_alias,
     model,
     no_dependencies,
-    cfg_entry.successors.front()->PC);
+    cfg[cfg_entry.out.begin()->first].PC);
 }
 
 /*******************************************************************\
@@ -455,7 +459,7 @@ Function: instrumentert::forward_traverse_once
 \*******************************************************************/
 
 void instrumentert::forward_traverse_once(
-    value_setst& value_sets,
+    may_aliast &may_alias,
     memory_modelt model,
     bool no_dependencies)
 {
@@ -464,7 +468,7 @@ void instrumentert::forward_traverse_once(
 
   if(!goto_program.instructions.empty())
     forward_traverse_once(
-      value_sets,
+      may_alias,
       model,
       no_dependencies,
       goto_program.instructions.begin());
@@ -490,7 +494,7 @@ void instrumentert::propagate_events_in_po()
   for(cfgt::entry_mapt::const_iterator it=cfg.entry_map.begin();
       it!=cfg.entry_map.end();
       ++it)
-    if(!it->second.events.empty())
+    if(!cfg[it->second].events.empty())
       worklist.push_back(it->first);
 
   while(!worklist.empty())
@@ -498,7 +502,7 @@ void instrumentert::propagate_events_in_po()
     goto_programt::const_targett target=worklist.back();
     worklist.pop_back();
 
-    cfgt::entryt &cfg_entry=cfg.entry_map[target];
+    cfgt::nodet &cfg_entry=cfg[cfg.entry_map[target]];
 
     // consistency checks first
     if(!cfg_entry.events.empty())
@@ -524,23 +528,23 @@ void instrumentert::propagate_events_in_po()
     {
       // no events at this instruction -- take the union of all events
       // propagated to predecessors
-      for(cfgt::entriest::const_iterator
-          it=cfg_entry.predecessors.begin();
-          it!=cfg_entry.predecessors.end();
+      for(cfgt::edgest::const_iterator
+          it=cfg_entry.in.begin();
+          it!=cfg_entry.in.end();
           ++it)
       {
         const std::set<goto_programt::const_targett> &s=
-          cfg.entry_map[(*it)->PC].use_events_from;
+          cfg[it->first].use_events_from;
         cfg_entry.use_events_from.insert(s.begin(), s.end());
       }
     }
 
     if(cfg_entry.use_events_from.size()>size_before)
-      for(cfgt::entriest::const_iterator
-          it=cfg_entry.successors.begin();
-          it!=cfg_entry.successors.end();
+      for(cfgt::edgest::const_iterator
+          it=cfg_entry.out.begin();
+          it!=cfg_entry.out.end();
           ++it)
-        worklist.push_front((*it)->PC);
+        worklist.push_front(cfg[it->first].PC);
   }
 }
 
@@ -596,8 +600,8 @@ Function: instrumentert::add_po_edges
 
 void instrumentert::add_po_edges(
   const unsigned thread_nr,
-  const cfgt::entryt &from,
-  const cfgt::entryt &to,
+  const cfgt::nodet &from,
+  const cfgt::nodet &to,
   const unsigned event_node,
   const unsigned event_gnode)
 {
@@ -635,20 +639,20 @@ Function: instrumentert::add_po_edges
 \*******************************************************************/
 
 void instrumentert::add_po_edges(
-  const cfgt::entryt &cfg_entry,
+  const cfgt::nodet &cfg_entry,
   const unsigned thread_nr,
   const unsigned event_node)
 {
   assert(map_vertex_gnode.find(event_node)!=map_vertex_gnode.end());
   const unsigned event_gnode=map_vertex_gnode[event_node];
 
-  for(cfgt::entriest::const_iterator
-      it=cfg_entry.predecessors.begin();
-      it!=cfg_entry.predecessors.end();
+  for(cfgt::edgest::const_iterator
+      it=cfg_entry.in.begin();
+      it!=cfg_entry.in.end();
       ++it)
   {
     const std::set<goto_programt::const_targett> &s=
-      cfg.entry_map[(*it)->PC].use_events_from;
+      cfg[it->first].use_events_from;
 
     for(std::set<goto_programt::const_targett>::const_iterator
         s_it=s.begin();
@@ -658,7 +662,7 @@ void instrumentert::add_po_edges(
       if(*s_it!=cfg_entry.PC)
         add_po_edges(
           thread_nr,
-          cfg.entry_map[*s_it],
+          cfg[cfg.entry_map[*s_it]],
           cfg_entry,
           event_node,
           event_gnode);
@@ -678,7 +682,7 @@ Function: instrumentert::add_po_edges
 \*******************************************************************/
 
 void instrumentert::add_po_edges(
-  const cfgt::entryt &cfg_entry,
+  const cfgt::nodet &cfg_entry,
   const unsigned thread_nr,
   const thread_eventst &thread_events)
 {
@@ -717,7 +721,7 @@ Function: instrumentert::add_edges_assign
 \*******************************************************************/
 
 void instrumentert::add_edges_assign(
-  const cfgt::entryt &cfg_entry,
+  const cfgt::nodet &cfg_entry,
   const thread_eventst &thread_events)
 {
   // anything other than an assignment or a function call containing
@@ -764,7 +768,7 @@ Function: instrumentert::add_com_edges
 \*******************************************************************/
 
 void instrumentert::add_com_edges(
-  const cfgt::entryt &cfg_entry,
+  const cfgt::nodet &cfg_entry,
   const thread_eventst &thread_events)
 {
   /* Read (Rb) */
@@ -882,7 +886,7 @@ Function: instrumentert::add_edges
 \*******************************************************************/
 
 void instrumentert::add_edges(
-  const cfgt::entryt &cfg_entry,
+  const cfgt::nodet &cfg_entry,
   const unsigned thread_nr,
   const thread_eventst &thread_events)
 {
@@ -918,11 +922,15 @@ void instrumentert::add_edges()
   for(cfgt::entry_mapt::const_iterator it=cfg.entry_map.begin();
       it!=cfg.entry_map.end();
       ++it)
+  {
+    const cfgt::nodet &n=cfg[it->second];
+
     for(std::map<unsigned, thread_eventst>::const_iterator
-        t_it=it->second.events.begin();
-        t_it!=it->second.events.end();
+        t_it=n.events.begin();
+        t_it!=n.events.end();
         ++t_it)
-      add_edges(it->second, t_it->first, t_it->second);
+      add_edges(n, t_it->first, t_it->second);
+  }
 }
 
 /*******************************************************************\
@@ -940,7 +948,7 @@ Function: instrumentert::build_event_graph
 \*******************************************************************/
 
 unsigned instrumentert::build_event_graph(
-  value_setst& value_sets,
+  may_aliast& may_alias,
   memory_modelt model,
   bool no_dependencies)
 {
@@ -950,7 +958,7 @@ unsigned instrumentert::build_event_graph(
   cfg(goto_functions);
 
   forward_traverse_once(
-    value_sets,
+    may_alias,
     model,
     no_dependencies);
 
diff --git a/src/goto-instrument/wmm/goto2graph.h b/src/goto-instrument/wmm/goto2graph.h
index 4a0cd0e..ca3314d 100644
--- a/src/goto-instrument/wmm/goto2graph.h
+++ b/src/goto-instrument/wmm/goto2graph.h
@@ -24,7 +24,7 @@ Date: 2012
 
 class symbol_tablet;
 class goto_functionst;
-class value_setst;
+class may_aliast;
 
 class instrumentert
 {
@@ -121,7 +121,7 @@ protected:
 
   /* transformers */
   void extract_events_rw(
-    value_setst& value_sets,
+    may_aliast& may_alias,
     memory_modelt model,
     bool no_dependencies,
     goto_programt::const_targett target,
@@ -131,10 +131,10 @@ protected:
     goto_programt::const_targett target,
     thread_eventst &dest);
   void extract_events(
-    value_setst& value_sets,
+    may_aliast& may_alias,
     memory_modelt model,
     bool no_dependencies,
-    cfgt::entryt &cfg_entry);
+    cfgt::nodet &cfg_entry);
 
   void add_po_edges(
     const nodest &from_events,
@@ -143,26 +143,26 @@ protected:
     const bool is_backward);
   void add_po_edges(
     const unsigned thread_nr,
-    const cfgt::entryt &from,
-    const cfgt::entryt &to,
+    const cfgt::nodet &from,
+    const cfgt::nodet &to,
     const unsigned event_node,
     const unsigned event_gnode);
   void add_po_edges(
-    const cfgt::entryt &cfg_entry,
+    const cfgt::nodet &cfg_entry,
     const unsigned thread_nr,
     const unsigned event_node);
   void add_po_edges(
-    const cfgt::entryt &cfg_entry,
+    const cfgt::nodet &cfg_entry,
     const unsigned thread_nr,
     const thread_eventst &thread_events);
   void add_edges_assign(
-    const cfgt::entryt &cfg_entry,
+    const cfgt::nodet &cfg_entry,
     const thread_eventst &thread_events);
   void add_com_edges(
-    const cfgt::entryt &cfg_entry,
+    const cfgt::nodet &cfg_entry,
     const thread_eventst &thread_events);
   void add_edges(
-    const cfgt::entryt &cfg_entry,
+    const cfgt::nodet &cfg_entry,
     const unsigned thread_nr,
     const thread_eventst &thread_events);
 
@@ -204,12 +204,12 @@ public:
   unsigned read_counter;
 
   void forward_traverse_once(
-    value_setst& value_sets,
+    may_aliast &may_alias,
     memory_modelt model,
     bool no_dependencies,
     goto_programt::const_targett target);
   void forward_traverse_once(
-    value_setst& value_sets,
+    may_aliast &may_alias,
     memory_modelt model,
     bool no_dependencies);
 
@@ -218,7 +218,7 @@ public:
   void add_edges();
 
   unsigned build_event_graph(
-    value_setst& value_sets,
+    may_aliast& may_alias,
     memory_modelt model,
     bool no_dependencies);
 
diff --git a/src/goto-instrument/wmm/static_cycles.cpp b/src/goto-instrument/wmm/static_cycles.cpp
new file mode 100644
index 0000000..11c97bb
--- /dev/null
+++ b/src/goto-instrument/wmm/static_cycles.cpp
@@ -0,0 +1,707 @@
+/*******************************************************************\
+
+Module: Find cycles even when no entry function is known
+
+Author: Michael Tautschnig, michael.tautschnig@cs.ox.ac.uk
+
+\*******************************************************************/
+
+#include <iostream>
+#include <algorithm>
+
+#include <util/graph.h>
+#include <util/message.h>
+#include <util/time_stopping.h>
+
+#include <goto-programs/goto_functions.h>
+#include <goto-programs/goto_convert.h>
+#include <goto-programs/remove_skip.h>
+#include <goto-programs/remove_function_pointers.h>
+
+#include <analyses/call_graph.h>
+#include <analyses/goto_rw.h>
+#include <analyses/may_alias.h>
+
+#include "goto2graph.h"
+
+#include "static_cycles.h"
+
+typedef hash_set_cont<irep_idt, irep_id_hash> thread_functionst;
+
+/*******************************************************************\
+
+Function: add_thread
+
+  Inputs: 
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static void add_thread(
+  const goto_functionst& goto_functions,
+  const irep_idt &identifier,
+  thread_functionst &thread_functions)
+{
+  goto_functionst::function_mapt::const_iterator fn=
+    goto_functions.function_map.find(identifier);
+
+  if(fn!=goto_functions.function_map.end() &&
+     !fn->second.body.instructions.empty())
+    thread_functions.insert(identifier);
+  else
+    thread_functions.insert(ID_main);
+}
+
+/*******************************************************************\
+
+Function: find_thread_start_thread
+
+  Inputs: 
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static void find_thread_start_thread(
+  goto_programt::const_targett start_thread,
+  const goto_programt &goto_program,
+  const goto_functionst& goto_functions,
+  thread_functionst &thread_functions)
+{
+  assert(start_thread->targets.size()==1);
+
+  add_thread(
+    goto_functions,
+    start_thread->function,
+    thread_functions);
+
+  for(goto_programt::const_targett
+      target=start_thread->targets.front();
+      target!=goto_program.instructions.end() &&
+      !target->is_end_thread() &&
+      !target->is_end_function();
+      ++target)
+  {
+    if(!target->is_function_call())
+      continue;
+
+    const code_function_callt &call=to_code_function_call(target->code);
+    if(call.function().id()!=ID_symbol)
+      continue;
+
+    const irep_idt &f_name=
+      to_symbol_expr(call.function()).get_identifier();
+    add_thread(goto_functions, f_name, thread_functions);
+  }
+}
+
+/*******************************************************************\
+
+Function: get_function_symbols
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static void get_function_symbols(
+  symbol_tablet &symbol_table,
+  const goto_functionst& goto_functions,
+  const exprt &fn_ptr,
+  const exprt &arg,
+  std::set<symbol_exprt> &functions)
+{
+  if(fn_ptr.id()==ID_typecast)
+  {
+    get_function_symbols(
+      symbol_table,
+      goto_functions,
+      to_typecast_expr(fn_ptr).op(),
+      arg,
+      functions);
+  }
+  else if(fn_ptr.id()==ID_if)
+  {
+    const if_exprt &fn_ptr_if=to_if_expr(fn_ptr);
+
+    get_function_symbols(
+      symbol_table,
+      goto_functions,
+      fn_ptr_if.true_case(),
+      arg,
+      functions);
+    get_function_symbols(
+      symbol_table,
+      goto_functions,
+      fn_ptr_if.false_case(),
+      arg,
+      functions);
+  }
+  else if(fn_ptr.id()==ID_symbol ||
+          fn_ptr.id()==ID_member ||
+          fn_ptr.id()==ID_index)
+  {
+    assert(fn_ptr.type().id()==ID_pointer);
+
+    code_function_callt c;
+    c.function()=dereference_exprt(fn_ptr, fn_ptr.type().subtype());
+    c.arguments().push_back(arg);
+
+    goto_programt tmp;
+
+    goto_programt::targett f=tmp.add_instruction(FUNCTION_CALL);
+    f->code=c;
+
+    tmp.add_instruction(END_FUNCTION);
+
+    remove_function_pointers(symbol_table, goto_functions, tmp, false);
+
+    forall_goto_program_instructions(it, tmp)
+      if(it->is_function_call())
+      {
+        const code_function_callt &code=
+          to_code_function_call(it->code);
+
+        functions.insert(to_symbol_expr(code.function()));
+      }
+  }
+  else
+  {
+    const address_of_exprt &address_of=to_address_of_expr(fn_ptr);
+
+    functions.insert(to_symbol_expr(address_of.object()));
+  }
+}
+
+/*******************************************************************\
+
+Function: find_thread_function_call
+
+  Inputs: 
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static void find_thread_function_call(
+  symbol_tablet &symbol_table,
+  const goto_programt::instructiont &function_call,
+  const goto_functionst& goto_functions,
+  thread_functionst &thread_functions)
+{
+  const code_function_callt &call=
+    to_code_function_call(function_call.code);
+
+  if(call.function().id()!=ID_symbol)
+    return;
+
+  // pthread_create or kthread_create_on_node
+  const irep_idt &f_name=
+    to_symbol_expr(call.function()).get_identifier();
+  const code_function_callt::argumentst &args=call.arguments();
+
+  exprt thread_fn_ptr;
+  exprt arg;
+
+  if(f_name=="c::pthread_create")
+  {
+    assert(args.size()==4);
+    thread_fn_ptr=args[2];
+    arg=args[3];
+  }
+  else if(f_name=="c::kthread_create_on_node")
+  {
+    assert(args.size()>=4);
+    thread_fn_ptr=args.front();
+    arg=args[1];
+  }
+  else
+    return;
+
+  std::set<symbol_exprt> functions;
+  get_function_symbols(
+    symbol_table,
+    goto_functions,
+    thread_fn_ptr,
+    arg,
+    functions);
+
+  for(std::set<symbol_exprt>::const_iterator it=functions.begin();
+      it!=functions.end();
+      ++it)
+  {
+    add_thread(
+      goto_functions,
+      it->get_identifier(),
+      thread_functions);
+  }
+
+  add_thread(
+    goto_functions,
+    function_call.function,
+    thread_functions);
+}
+
+/*******************************************************************\
+
+Function: find_threads
+
+  Inputs: 
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static void find_threads(
+  symbol_tablet &symbol_table,
+  const goto_programt &goto_program,
+  const goto_functionst& goto_functions,
+  thread_functionst &thread_functions)
+{
+  forall_goto_program_instructions(it, goto_program)
+    if(it->is_start_thread())
+      find_thread_start_thread(
+        it,
+        goto_program,
+        goto_functions,
+        thread_functions);
+    else if(it->is_function_call())
+      find_thread_function_call(
+        symbol_table,
+        *it,
+        goto_functions,
+        thread_functions);
+}
+
+/*******************************************************************\
+
+Function: find_threads
+
+  Inputs: 
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static void find_threads(
+  symbol_tablet &symbol_table,
+  const goto_functionst& goto_functions,
+  thread_functionst &thread_functions)
+{
+  forall_goto_functions(f_it, goto_functions)
+    if(f_it->first!="c::pthread_create" &&
+       f_it->first!="c::kthread_create_on_node")
+      find_threads(
+        symbol_table,
+        f_it->second.body,
+        goto_functions,
+        thread_functions);
+}
+
+/*******************************************************************\
+
+Function: filter_thread_functions
+
+  Inputs: 
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static void filter_thread_functions(
+  const goto_functionst& goto_functions,
+  const call_grapht &call_map,
+  thread_functionst &thread_functions)
+{
+  graph<visited_nodet<empty_edget> > call_graph;
+
+  hash_map_cont<irep_idt, unsigned, irep_id_hash> fn_to_node;
+  for(thread_functionst::const_iterator it=thread_functions.begin();
+      it!=thread_functions.end();
+      ++it)
+  {
+    unsigned n=call_graph.add_node();
+    fn_to_node.insert(std::make_pair(*it, n));
+  }
+
+  for(std::multimap<irep_idt, irep_idt>::const_iterator
+      it=call_map.graph.begin();
+      it!=call_map.graph.end();
+      ++it)
+  {
+    if(fn_to_node.find(it->first)==fn_to_node.end())
+      fn_to_node.insert(std::make_pair(it->first, call_graph.add_node()));
+    if(fn_to_node.find(it->second)==fn_to_node.end())
+      fn_to_node.insert(std::make_pair(it->second, call_graph.add_node()));
+
+    call_graph.add_edge(
+      fn_to_node[it->first],
+      fn_to_node[it->second]);
+  }
+
+  thread_functionst before;
+  before.swap(thread_functions);
+
+  for(thread_functionst::const_iterator it=before.begin();
+      it!=before.end();
+      ++it)
+  {
+    const irep_idt &identifier=*it;
+    const unsigned n=fn_to_node[identifier];
+
+    if(call_graph[n].visited)
+      continue;
+
+    if(call_graph.in(n).empty())
+    {
+      add_thread(
+        goto_functions,
+        identifier,
+        thread_functions);
+      call_graph.visit_reachable(n);
+      continue;
+    }
+
+    graph<visited_nodet<empty_edget> >::patht path;
+    call_graph.shortest_loop(n, path);
+    if(!path.empty())
+    {
+      add_thread(
+        goto_functions,
+        identifier,
+        thread_functions);
+      call_graph.visit_reachable(n);
+    }
+  }
+
+  std::cout << "Thread entry candidates:" << std::endl;
+  for(thread_functionst::const_iterator it=thread_functions.begin();
+      it!=thread_functions.end();
+      ++it)
+    std::cout << *it << std::endl;
+}
+
+/*******************************************************************\
+
+Function: collect_cycles_in_group
+
+  Inputs: 
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static void collect_cycles_in_group(
+  may_aliast &may_alias,
+  symbol_tablet &symbol_table,
+  goto_functionst& goto_functions,
+  const irep_idt &identifier)
+{
+  const namespacet ns(symbol_table);
+  instrumentert instrumenter(symbol_table, goto_functions);
+
+  fine_timet graph_time_start=current_time();
+  {
+    instrumenter.cfg(goto_functions);
+
+    goto_functionst::function_mapt::const_iterator fn=
+      goto_functions.function_map.find(identifier);
+    assert(fn!=goto_functions.function_map.end() &&
+           !fn->second.body.instructions.empty());
+    instrumenter.forward_traverse_once(
+      may_alias,
+      Static_Weak,
+      false,
+      fn->second.body.instructions.begin());
+
+    instrumenter.propagate_events_in_po();
+
+    instrumenter.add_edges();
+  }
+  std::cout << "Time event graph construction: "
+            << current_time()-graph_time_start << std::endl;
+
+  std::cout << "Number of reads: " << instrumenter.read_counter <<std::endl;
+  std::cout << "Number of writes: " << instrumenter.write_counter <<std::endl;
+
+  instrumenter.egraph.filter_thin_air=false;
+  instrumenter.egraph.filter_uniproc=false;
+
+  fine_timet cycle_enum_time_start=current_time();
+  instrumenter.collect_cycles(Static_Weak);
+  std::cout << "Time cycle enumeration: "
+            << current_time()-cycle_enum_time_start << std::endl;
+
+  for(std::set<event_grapht::critical_cyclet>::const_iterator
+      it=instrumenter.set_of_cycles.begin();
+      it!=instrumenter.set_of_cycles.end();
+      ++it)
+  {
+    std::cout << "Source: " << it->print_output() << std::endl;
+    std::cout << "Cycle:" << it->print_name(Static_Weak, false) << std::endl;
+  }
+}
+
+/*******************************************************************\
+
+Function: form_thread_groups
+
+  Inputs: 
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static void form_thread_groups(
+  symbol_tablet &symbol_table,
+  goto_functionst& goto_functions,
+  thread_functionst &thread_functions,
+  may_aliast &may_alias)
+{
+  forall_goto_functions(it, goto_functions)
+    add_thread(goto_functions, it->first, thread_functions);
+
+  call_grapht call_map(goto_functions);
+
+  filter_thread_functions(goto_functions, call_map, thread_functions);
+
+  const namespacet ns(symbol_table);
+
+  typedef std::list<std::pair<std::set<irep_idt>, thread_functionst> >
+          thread_groupst;
+  thread_groupst thread_groups;
+
+  for(thread_functionst::const_iterator it=thread_functions.begin();
+      it!=thread_functions.end();
+      ++it)
+  {
+    const irep_idt &root_fn=*it;
+
+    hash_set_cont<irep_idt, irep_id_hash> called_funcs;
+    called_funcs.insert(root_fn);
+
+    std::list<irep_idt> wl;
+    wl.push_back(root_fn);
+
+    while(!wl.empty())
+    {
+      irep_idt caller=wl.back();
+      wl.pop_back();
+
+      std::pair<std::multimap<irep_idt, irep_idt>::const_iterator,
+        std::multimap<irep_idt, irep_idt>::const_iterator>
+          eq_iterators=call_map.graph.equal_range(caller);
+      for( ;
+           eq_iterators.first!=eq_iterators.second;
+           ++(eq_iterators.first))
+        if(called_funcs.insert(eq_iterators.first->second).second)
+          wl.push_back(eq_iterators.first->second);
+    }
+
+    thread_groups.push_back(std::make_pair(
+        std::set<irep_idt>(),
+        thread_functionst()));
+    std::set<irep_idt> &rw_symbols=thread_groups.back().first;
+    thread_groups.back().second.insert(root_fn);
+
+    for(hash_set_cont<irep_idt, irep_id_hash>::const_iterator
+        c_it=called_funcs.begin();
+        c_it!=called_funcs.end();
+        ++c_it)
+    {
+      goto_functionst::function_mapt::const_iterator fn=
+        goto_functions.function_map.find(*c_it);
+
+      if(fn==goto_functions.function_map.end() ||
+         fn->second.body.instructions.empty())
+        continue;
+
+      const goto_programt &goto_program=fn->second.body;
+
+      rw_range_set_dereft rw_set(ns, may_alias);
+      goto_rw(goto_program, rw_set);
+
+      forall_rw_range_set_w_objects(w_it, rw_set)
+      {
+        const irep_idt &identifier=w_it->first;
+        if(!symbol_table.has_symbol(identifier) ||
+           !ns.lookup(identifier).is_shared())
+          continue;
+
+        rw_symbols.insert(identifier);
+      }
+
+      forall_rw_range_set_r_objects(r_it, rw_set)
+      {
+        const irep_idt &identifier=r_it->first;
+        if(!symbol_table.has_symbol(identifier) ||
+           !ns.lookup(identifier).is_shared())
+          continue;
+
+        rw_symbols.insert(identifier);
+      }
+    }
+  }
+
+  for(thread_groupst::iterator it1=thread_groups.begin();
+      it1!=thread_groups.end();
+      ) // no ++it1
+  {
+    bool merged=it1->first.empty();
+    for(thread_groupst::iterator next=it1, it2=++next;
+        it2!=thread_groups.end() && !merged;
+        ++it2)
+    {
+      std::list<irep_idt> intersection;
+      std::set_intersection(
+        it1->first.begin(), it1->first.end(),
+        it2->first.begin(), it2->first.end(),
+        std::back_inserter(intersection));
+
+      if(intersection.empty())
+        continue;
+
+      std::copy(it1->first.begin(), it1->first.end(),
+                std::inserter(it2->first, it2->first.begin()));
+      it2->second.insert(it1->second.begin(), it1->second.end());
+      merged=true;
+    }
+
+    if(merged ||
+       (it1->second.size()==1 && it1->first.empty()))
+      thread_groups.erase(it1++);
+    else
+      ++it1;
+  }
+
+  if(thread_groups.empty())
+  {
+    std::cout << "No thread groups" << std::endl;
+    return;
+  }
+
+  assert(goto_functions.function_map.find("$$thread_dummy")==
+         goto_functions.function_map.end());
+  goto_functionst::goto_functiont &thread_dummy=
+    goto_functions.function_map["$$thread_dummy"];
+  thread_dummy.type=code_typet();
+  thread_dummy.body_available=true;
+  goto_programt &body=thread_dummy.body;
+
+  for(thread_groupst::const_iterator it=thread_groups.begin();
+      it!=thread_groups.end();
+      ++it)
+  {
+    std::cout << "Thread group:" << std::endl;
+
+    body.clear();
+
+    null_message_handlert mh;
+
+    code_function_callt f;
+    f.lhs().make_nil();
+
+    for(thread_functionst::const_iterator
+        t_it=it->second.begin();
+        t_it!=it->second.end();
+        ++t_it)
+    {
+      const irep_idt identifier=*t_it;
+      std::cout << identifier << std::endl;
+
+      f.function()=symbol_exprt(identifier, code_typet());
+      const code_labelt label("__CPROVER_ASYNC_0", f);
+
+      // add 3 threads executing this function
+      for(int i=0; i<3; ++i)
+        goto_convert(label, symbol_table, body, mh);
+    }
+
+    body.add_instruction(END_FUNCTION);
+    body.compute_target_numbers();
+    remove_skip(body);
+    body.update();
+
+    collect_cycles_in_group(
+      may_alias,
+      symbol_table,
+      goto_functions,
+      "$$thread_dummy");
+  }
+}
+
+/*******************************************************************\
+
+Function: static_cycles
+
+  Inputs: 
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void static_cycles(
+  symbol_tablet &symbol_table,
+  goto_functionst& goto_functions)
+{
+  fine_timet total_time_start=current_time();
+
+  hash_set_cont<irep_idt, irep_id_hash> thread_functions;
+  find_threads(symbol_table, goto_functions, thread_functions);
+
+  bool is_linked=
+    goto_functions.function_map.find(ID_main)
+    !=goto_functions.function_map.end();
+
+  if(is_linked &&
+     thread_functions.empty())
+  {
+    std::cout << "No thread spawn found in linked binary" << std::endl;
+    return;
+  }
+
+  const namespacet ns(symbol_table);
+  fine_timet alias_time_start=current_time();
+  may_aliast may_alias(goto_functions, ns);
+  std::cout << "Time alias analysis: "
+            << current_time()-alias_time_start << std::endl;
+
+  if(!is_linked)
+    form_thread_groups(
+      symbol_table,
+      goto_functions,
+      thread_functions,
+      may_alias);
+  else
+    collect_cycles_in_group(
+      may_alias,
+      symbol_table,
+      goto_functions,
+      ID_main);
+
+  std::cout << "Time static cycle search: "
+            << current_time()-total_time_start << std::endl;
+}
+
diff --git a/src/goto-instrument/wmm/static_cycles.h b/src/goto-instrument/wmm/static_cycles.h
new file mode 100644
index 0000000..866789a
--- /dev/null
+++ b/src/goto-instrument/wmm/static_cycles.h
@@ -0,0 +1,20 @@
+/*******************************************************************\
+
+Module: Find cycles even when no entry function is known
+
+Author: Michael Tautschnig, michael.tautschnig@cs.ox.ac.uk
+
+\*******************************************************************/
+
+#ifndef CPROVER_STATIC_CYCLES_H
+#define CPROVER_STATIC_CYCLES_H
+
+class symbol_tablet;
+class goto_functionst;
+
+void static_cycles(
+  symbol_tablet& symbol_table,
+  goto_functionst& goto_functions);
+
+#endif
+
diff --git a/src/goto-instrument/wmm/weak_memory.cpp b/src/goto-instrument/wmm/weak_memory.cpp
index 31d7e54..3639e5f 100644
--- a/src/goto-instrument/wmm/weak_memory.cpp
+++ b/src/goto-instrument/wmm/weak_memory.cpp
@@ -25,6 +25,8 @@ Date: September 2011
 
 #include <goto-programs/remove_skip.h>
 
+#include <analyses/may_alias.h>
+
 #include "../rw_set.h"
 #include "weak_memory.h"
 #include "goto2graph.h"
@@ -1976,7 +1978,9 @@ void weak_memory(
 
   unsigned max_thds = 0;
   instrumentert instrumenter(symbol_table, goto_functions);
-  max_thds=instrumenter.build_event_graph(value_sets, model, no_dependencies);
+  const namespacet ns(symbol_table);
+  may_aliast may_alias(goto_functions, ns);
+  max_thds=instrumenter.build_event_graph(may_alias, model, no_dependencies);
   std::cout<<"abstraction completed"<<std::endl;
 
   // collects cycles, directly or by SCCs
diff --git a/src/goto-instrument/wmm/wmm.h b/src/goto-instrument/wmm/wmm.h
index 4efd66c..f8fc636 100644
--- a/src/goto-instrument/wmm/wmm.h
+++ b/src/goto-instrument/wmm/wmm.h
@@ -16,7 +16,8 @@ typedef enum {
   TSO=0, 
   PSO=1, 
   RMO=2, 
-  Power=3
+  Power=3,
+  Static_Weak=4
 } memory_modelt;
 
 #endif
diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile
index 8312d81..55f960d 100644
--- a/src/goto-programs/Makefile
+++ b/src/goto-programs/Makefile
@@ -12,7 +12,7 @@ SRC = goto_convert.cpp goto_convert_function_call.cpp \
       format_strings.cpp loop_ids.cpp pointer_arithmetic.cpp \
       goto_program_template.cpp write_goto_binary.cpp remove_unreachable.cpp \
       remove_unused_functions.cpp \
-      wp.cpp goto_rw.cpp goto_clean_expr.cpp safety_checker.cpp \
+      wp.cpp goto_clean_expr.cpp safety_checker.cpp \
       compute_called_functions.cpp link_to_library.cpp \
       remove_returns.cpp osx_fat_reader.cpp \
       goto_trace.cpp xml_goto_trace.cpp vcd_goto_trace.cpp
diff --git a/src/goto-programs/cfg.h b/src/goto-programs/cfg.h
index a2e07e7..011195a 100644
--- a/src/goto-programs/cfg.h
+++ b/src/goto-programs/cfg.h
@@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #define CPROVER_GOTO_PROGRAMS_CFG_H
 
 #include <util/std_expr.h>
+#include <util/graph.h>
 
 #include "goto_functions.h"
 
@@ -21,42 +22,109 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-template<class T>
-class cfg_baset
+class empty_cfg_nodet
+{
+};
+
+// these are the CFG nodes
+template<class T, typename I>
+struct cfg_base_nodet:public graph_nodet<empty_edget>, public T
+{
+  typedef typename graph_nodet<empty_edget>::edget edget;
+  typedef typename graph_nodet<empty_edget>::edgest edgest;
+
+  I PC;
+};
+
+template<class T,
+         typename P=const goto_programt,
+         typename I=goto_programt::const_targett>
+class cfg_baset:public graph< cfg_base_nodet<T,I> >
 {
 public:
-  // these are the CFG nodes
-  struct entryt: public T
+  typedef unsigned entryt;
+
+  struct entry_mapt:
+    public std::map<goto_programt::const_targett, entryt>
   {
-    typedef std::list<struct entryt *> entriest;
+    graph< cfg_base_nodet<T,I> > & container;
 
-    // we have edges both ways
-    entriest successors, predecessors;
-    goto_programt::const_targett PC;
-  };
-  
-  typedef entryt * iterator;
-  typedef const entryt * const_iterator;
+    explicit entry_mapt(graph< cfg_base_nodet<T,I> > & _container):
+      container(_container)
+    {
+    }
 
-  typedef std::list<iterator> entriest;
-  
-  typedef std::map<goto_programt::const_targett, entryt> entry_mapt;
+    entryt& operator[](const goto_programt::const_targett &t)
+    {
+      std::pair<iterator,bool> e=insert(std::make_pair(t, 0));
+
+      if(e.second)
+        e.first->second=container.add_node();
+
+      return e.first->second;
+    }
+  };
   entry_mapt entry_map;
 
 protected:
+  virtual void compute_edges_goto(
+    const goto_programt &goto_program,
+    const goto_programt::instructiont &instruction,
+    goto_programt::const_targett next_PC,
+    entryt &entry);
+
+  virtual void compute_edges_catch(
+    const goto_programt &goto_program,
+    const goto_programt::instructiont &instruction,
+    goto_programt::const_targett next_PC,
+    entryt &entry);
+
+  virtual void compute_edges_throw(
+    const goto_programt &goto_program,
+    const goto_programt::instructiont &instruction,
+    goto_programt::const_targett next_PC,
+    entryt &entry);
+
+  virtual void compute_edges_start_thread(
+    const goto_programt &goto_program,
+    const goto_programt::instructiont &instruction,
+    goto_programt::const_targett next_PC,
+    entryt &entry);
+
+  virtual void compute_edges_function_call(
+    const goto_functionst &goto_functions,
+    const goto_programt &goto_program,
+    const goto_programt::instructiont &instruction,
+    goto_programt::const_targett next_PC,
+    entryt &entry);
+
+  virtual void compute_edges_return(
+    const goto_programt &goto_program,
+    const goto_programt::instructiont &instruction,
+    goto_programt::const_targett next_PC,
+    entryt &entry);
+
   void compute_edges(
     const goto_functionst &goto_functions,
     const goto_programt &goto_program,
-    goto_programt::const_targett PC);
+    I PC);
 
   void compute_edges(
     const goto_functionst &goto_functions,
-    const goto_programt &goto_program);
+    P &goto_program);
 
   void compute_edges(
     const goto_functionst &goto_functions);
 
 public:
+  cfg_baset():entry_map(*this)
+  {
+  }
+
+  virtual ~cfg_baset()
+  {
+  }
+
   void operator()(
     const goto_functionst &goto_functions)
   {
@@ -64,7 +132,7 @@ public:
   }
 
   void operator()(
-    const goto_programt &goto_program)
+    P &goto_program)
   {
     goto_functionst goto_functions;
     compute_edges(goto_functions, goto_program);
@@ -74,7 +142,67 @@ public:
 
 /*******************************************************************\
 
-Function: cfg_baset::compute_edges
+   Class: concurrent_cfg_baset
+
+ Purpose:
+
+\*******************************************************************/
+
+template<class T,
+         typename P=const goto_programt,
+         typename I=goto_programt::const_targett>
+class concurrent_cfg_baset:public virtual cfg_baset<T, P, I>
+{
+protected:
+  virtual void compute_edges_start_thread(
+    const goto_programt &goto_program,
+    const goto_programt::instructiont &instruction,
+    goto_programt::const_targett next_PC,
+    typename cfg_baset<T, P, I>::entryt &entry);
+};
+
+/*******************************************************************\
+
+   Class: procedure_local_cfg_baset
+
+ Purpose:
+
+\*******************************************************************/
+
+template<class T,
+         typename P=const goto_programt,
+         typename I=goto_programt::const_targett>
+class procedure_local_cfg_baset:public virtual cfg_baset<T, P, I>
+{
+protected:
+  virtual void compute_edges_function_call(
+    const goto_functionst &goto_functions,
+    const goto_programt &goto_program,
+    const goto_programt::instructiont &instruction,
+    goto_programt::const_targett next_PC,
+    typename cfg_baset<T, P, I>::entryt &entry);
+};
+
+/*******************************************************************\
+
+   Class: procedure_local_concurrent_cfg_baset
+
+ Purpose:
+
+\*******************************************************************/
+
+template<class T,
+         typename P=const goto_programt,
+         typename I=goto_programt::const_targett>
+class procedure_local_concurrent_cfg_baset:
+  public concurrent_cfg_baset<T, P, I>,
+  public procedure_local_cfg_baset<T, P, I>
+{
+};
+
+/*******************************************************************\
+
+Function: cfg_baset::compute_edges_goto
 
   Inputs:
 
@@ -84,139 +212,340 @@ Function: cfg_baset::compute_edges
 
 \*******************************************************************/
 
-template<class T>
-void cfg_baset<T>::compute_edges(
-  const goto_functionst &goto_functions,
+template<class T, typename P, typename I>
+void cfg_baset<T, P, I>::compute_edges_goto(
   const goto_programt &goto_program,
-  goto_programt::const_targett PC)
+  const goto_programt::instructiont &instruction,
+  goto_programt::const_targett next_PC,
+  entryt &entry)
 {
-  const goto_programt::instructiont &instruction=*PC;
-  entryt &entry=entry_map[PC];
-  entry.PC=PC;
-  goto_programt::const_targett next_PC(PC);
-  next_PC++;
-
-  // compute forward edges first
-  if(instruction.is_goto())
+  if(next_PC!=goto_program.instructions.end() &&
+     !instruction.guard.is_true())
+    this->add_edge(entry, entry_map[next_PC]);
+
+  for(goto_programt::instructiont::targetst::const_iterator
+      t_it=instruction.targets.begin();
+      t_it!=instruction.targets.end();
+      t_it++)
   {
-    if(next_PC!=goto_program.instructions.end() &&
-       !instruction.guard.is_true())
-      entry.successors.push_back(&entry_map[next_PC]);
-
-    for(goto_programt::instructiont::targetst::const_iterator
-        t_it=instruction.targets.begin();
-        t_it!=instruction.targets.end();
-        t_it++)
-    {
-      goto_programt::const_targett t=*t_it;
-      if(t!=goto_program.instructions.end())
-        entry.successors.push_back(&entry_map[t]);
-    }
+    goto_programt::const_targett t=*t_it;
+    if(t!=goto_program.instructions.end())
+      this->add_edge(entry, entry_map[t]);
   }
-  else if(instruction.is_catch())
-  {
-    if(next_PC!=goto_program.instructions.end())
-      entry.successors.push_back(&entry_map[next_PC]);
+}
 
-    // Not ideal, but preserves targets
-    // Ideally, the throw statements should have those as successors
+/*******************************************************************\
 
-    for(goto_programt::instructiont::targetst::const_iterator
-        t_it=instruction.targets.begin();
-        t_it!=instruction.targets.end();
-        t_it++)
-    {
-      goto_programt::const_targett t=*t_it;
-      if(t!=goto_program.instructions.end())
-        entry.successors.push_back(&entry_map[t]);
-    }
-  }
-  else if(instruction.is_throw())
+Function: cfg_baset::compute_edges_catch
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+template<class T, typename P, typename I>
+void cfg_baset<T, P, I>::compute_edges_catch(
+  const goto_programt &goto_program,
+  const goto_programt::instructiont &instruction,
+  goto_programt::const_targett next_PC,
+  entryt &entry)
+{
+  if(next_PC!=goto_program.instructions.end())
+    this->add_edge(entry, entry_map[next_PC]);
+
+  // Not ideal, but preserves targets
+  // Ideally, the throw statements should have those as successors
+
+  for(goto_programt::instructiont::targetst::const_iterator
+      t_it=instruction.targets.begin();
+      t_it!=instruction.targets.end();
+      t_it++)
   {
-    // no (trivial) successors
+    goto_programt::const_targett t=*t_it;
+    if(t!=goto_program.instructions.end())
+      this->add_edge(entry, entry_map[t]);
   }
-  else if(instruction.is_start_thread())
+}
+
+/*******************************************************************\
+
+Function: cfg_baset::compute_edges_throw
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+template<class T, typename P, typename I>
+void cfg_baset<T, P, I>::compute_edges_throw(
+  const goto_programt &goto_program,
+  const goto_programt::instructiont &instruction,
+  goto_programt::const_targett next_PC,
+  entryt &entry)
+{
+  // no (trivial) successors
+}
+
+/*******************************************************************\
+
+Function: cfg_baset::compute_edges_start_thread
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+template<class T, typename P, typename I>
+void cfg_baset<T, P, I>::compute_edges_start_thread(
+  const goto_programt &goto_program,
+  const goto_programt::instructiont &instruction,
+  goto_programt::const_targett next_PC,
+  entryt &entry)
+{
+  if(next_PC!=goto_program.instructions.end())
+    this->add_edge(entry, entry_map[next_PC]);
+}
+
+/*******************************************************************\
+
+Function: concurrent_cfg_baset::compute_edges_start_thread
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+template<class T, typename P, typename I>
+void concurrent_cfg_baset<T, P, I>::compute_edges_start_thread(
+  const goto_programt &goto_program,
+  const goto_programt::instructiont &instruction,
+  goto_programt::const_targett next_PC,
+  typename cfg_baset<T, P, I>::entryt &entry)
+{
+  cfg_baset<T, P, I>::compute_edges_start_thread(
+    goto_program,
+    instruction,
+    next_PC,
+    entry);
+
+  for(goto_programt::instructiont::targetst::const_iterator
+      t_it=instruction.targets.begin();
+      t_it!=instruction.targets.end();
+      t_it++)
   {
-    if(next_PC!=goto_program.instructions.end())
-      entry.successors.push_back(&entry_map[PC]);
-      
-    for(goto_programt::instructiont::targetst::const_iterator
-        t_it=instruction.targets.begin();
-        t_it!=instruction.targets.end();
-        t_it++)
-    {
-      goto_programt::const_targett t=*t_it;
-      if(t!=goto_program.instructions.end())
-        entry.successors.push_back(&entry_map[t]);
-    }
+    goto_programt::const_targett t=*t_it;
+    if(t!=goto_program.instructions.end())
+      this->add_edge(entry, this->entry_map[t]);
   }
-  else if(instruction.is_function_call())
+}
+
+/*******************************************************************\
+
+Function: cfg_baset::compute_edges_function_call
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+template<class T, typename P, typename I>
+void cfg_baset<T, P, I>::compute_edges_function_call(
+  const goto_functionst &goto_functions,
+  const goto_programt &goto_program,
+  const goto_programt::instructiont &instruction,
+  goto_programt::const_targett next_PC,
+  entryt &entry)
+{
+  const exprt &function=
+    to_code_function_call(instruction.code).function();
+
+  if(function.id()!=ID_symbol)
+    return;
+
+  const irep_idt &identifier=
+    to_symbol_expr(function).get_identifier();
+
+  goto_functionst::function_mapt::const_iterator f_it=
+    goto_functions.function_map.find(identifier);
+
+  if(f_it!=goto_functions.function_map.end() &&
+     f_it->second.body_available)
   {
-    const exprt &function=
-      to_code_function_call(instruction.code).function();
+    // get the first instruction
+    goto_programt::const_targett i_it=
+      f_it->second.body.instructions.begin();
 
-    if(function.id()==ID_symbol)
+    goto_programt::const_targett e_it=
+      f_it->second.body.instructions.end();
+
+    goto_programt::const_targett last_it=e_it; last_it--;
+
+    if(i_it!=e_it)
     {
-      const irep_idt &identifier=
-        to_symbol_expr(function).get_identifier();
-
-      goto_functionst::function_mapt::const_iterator f_it=
-        goto_functions.function_map.find(identifier);
-
-      if(f_it!=goto_functions.function_map.end() &&
-         f_it->second.body_available)
-      {
-        // get the first instruction
-        goto_programt::const_targett i_it=
-          f_it->second.body.instructions.begin();
-
-        goto_programt::const_targett e_it=
-          f_it->second.body.instructions.end();
-
-        goto_programt::const_targett last_it=e_it; last_it--;
-        
-        if(i_it!=e_it)
-        {
-          // nonempty function
-          entry.successors.push_back(&entry_map[i_it]);
-          
-          // add the last instruction as predecessor of the return location
-          if(next_PC!=goto_program.instructions.end())
-          {
-            entry_map[last_it].successors.push_back(&entry_map[next_PC]);
-            entry_map[next_PC].predecessors.push_back(&entry_map[last_it]);
-          }
-        }
-        else if(next_PC!=goto_program.instructions.end())
-        {
-          // empty function
-          entry.successors.push_back(&entry_map[next_PC]);
-        }        
-      }
-      else if(next_PC!=goto_program.instructions.end())
-        entry.successors.push_back(&entry_map[next_PC]);
+      // nonempty function
+      this->add_edge(entry, entry_map[i_it]);
+
+      // add the last instruction as predecessor of the return location
+      if(next_PC!=goto_program.instructions.end())
+        this->add_edge(entry_map[last_it], entry_map[next_PC]);
     }
+    else if(next_PC!=goto_program.instructions.end())
+    {
+      // empty function
+      this->add_edge(entry, entry_map[next_PC]);
+    }        
   }
-  else if(instruction.is_return())
-  {
-    // the successor of return is the last instruction of the function,
-    // normally END_FUNCTION
-    if(next_PC!=goto_program.instructions.end())
-      entry.successors.push_back(&entry_map[--(goto_program.instructions.end())]);
-  }
-  else
-  {
-    if(next_PC!=goto_program.instructions.end())
-      entry.successors.push_back(&entry_map[next_PC]);
-  }
+  else if(next_PC!=goto_program.instructions.end())
+    this->add_edge(entry, entry_map[next_PC]);
+}
+
+/*******************************************************************\
+
+Function: procedure_local_cfg_baset::compute_edges_function_call
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+template<class T, typename P, typename I>
+void procedure_local_cfg_baset<T, P, I>::compute_edges_function_call(
+  const goto_functionst &goto_functions,
+  const goto_programt &goto_program,
+  const goto_programt::instructiont &instruction,
+  goto_programt::const_targett next_PC,
+  typename cfg_baset<T, P, I>::entryt &entry)
+{
+  const exprt &function=
+    to_code_function_call(instruction.code).function();
+
+  if(function.id()!=ID_symbol)
+    return;
+
+  if(next_PC!=goto_program.instructions.end())
+    this->add_edge(entry, this->entry_map[next_PC]);
+}
+
+/*******************************************************************\
+
+Function: cfg_baset::compute_edges_return
+
+  Inputs:
+
+ Outputs:
 
-  // now do backward edges
-  for(typename entriest::const_iterator
-      s_it=entry.successors.begin();
-      s_it!=entry.successors.end();
-      s_it++)
+ Purpose:
+
+\*******************************************************************/
+
+template<class T, typename P, typename I>
+void cfg_baset<T, P, I>::compute_edges_return(
+  const goto_programt &goto_program,
+  const goto_programt::instructiont &instruction,
+  goto_programt::const_targett next_PC,
+  entryt &entry)
+{
+  // the successor of return is the last instruction of the function,
+  // normally END_FUNCTION
+  if(next_PC!=goto_program.instructions.end())
+    this->add_edge(entry, entry_map[--(goto_program.instructions.end())]);
+}
+
+/*******************************************************************\
+
+Function: cfg_baset::compute_edges
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+template<class T, typename P, typename I>
+void cfg_baset<T, P, I>::compute_edges(
+  const goto_functionst &goto_functions,
+  const goto_programt &goto_program,
+  I PC)
+{
+  const goto_programt::instructiont &instruction=*PC;
+  entryt entry=entry_map[PC];
+  (*this)[entry].PC=PC;
+  goto_programt::const_targett next_PC(PC);
+  next_PC++;
+
+  // compute forward edges first
+  switch(instruction.type)
   {
-    (*s_it)->predecessors.push_back(&entry);
+  case GOTO:
+    compute_edges_goto(goto_program, instruction, next_PC, entry);
+    break;
+  case CATCH:
+    compute_edges_catch(goto_program, instruction, next_PC, entry);
+    break;
+  case THROW:
+    compute_edges_throw(goto_program, instruction, next_PC, entry);
+    break;
+  case START_THREAD:
+    compute_edges_start_thread(
+      goto_program,
+      instruction,
+      next_PC,
+      entry);
+    break;
+  case FUNCTION_CALL:
+    compute_edges_function_call(
+      goto_functions,
+      goto_program,
+      instruction,
+      next_PC,
+      entry);
+    break;
+  case RETURN:
+    compute_edges_return(goto_program, instruction, next_PC, entry);
+    break;
+  case END_THREAD:
+  case END_FUNCTION:
+    // no successor
+    break;
+  case ASSUME:
+    // false guard -> no successor
+    if(instruction.guard.is_false())
+      break;
+  case ASSIGN:
+  case ASSERT:
+  case OTHER:
+  case SKIP:
+  case LOCATION:
+  case ATOMIC_BEGIN:
+  case ATOMIC_END:
+  case DECL:
+  case DEAD:
+    if(next_PC!=goto_program.instructions.end())
+      this->add_edge(entry, entry_map[next_PC]);
+    break;
+  case NO_INSTRUCTION_TYPE:
+    assert(false);
+    break;
   }
 }
 
@@ -232,12 +561,14 @@ Function: cfg_baset::compute_edges
 
 \*******************************************************************/
 
-template<class T>
-void cfg_baset<T>::compute_edges(
+template<class T, typename P, typename I>
+void cfg_baset<T, P, I>::compute_edges(
   const goto_functionst &goto_functions,
-  const goto_programt &goto_program)
+  P &goto_program)
 {
-  forall_goto_program_instructions(it, goto_program)
+  for(I it=goto_program.instructions.begin();
+      it!=goto_program.instructions.end();
+      ++it)
     compute_edges(goto_functions, goto_program, it);
 }
 
@@ -253,8 +584,8 @@ Function: cfg_baset::compute_edges
 
 \*******************************************************************/
 
-template<class T>
-void cfg_baset<T>::compute_edges(
+template<class T, typename P, typename I>
+void cfg_baset<T, P, I>::compute_edges(
   const goto_functionst &goto_functions)
 {
   forall_goto_functions(it, goto_functions)
diff --git a/src/goto-programs/goto_rw.cpp b/src/goto-programs/goto_rw.cpp
deleted file mode 100644
index 702c17f..0000000
--- a/src/goto-programs/goto_rw.cpp
+++ /dev/null
@@ -1,198 +0,0 @@
-/*******************************************************************\
-
-Module: 
-
-Author: Daniel Kroening
-
-Date: April 2010
-
-\*******************************************************************/
-
-#include <util/std_expr.h>
-
-#include "goto_rw.h"
-
-/*******************************************************************\
-
-Function: get_objects_rec
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-typedef enum { LHS_W, READ } get_modet;
-
-void get_objects_rec(
-  get_modet mode,
-  const exprt &expr,
-  std::list<exprt> &read,
-  std::list<exprt> &write)
-{
-  if(expr.id()==ID_symbol)
-  {
-    if(mode==LHS_W)
-      write.push_back(expr);
-    else
-      read.push_back(expr);
-  }
-  else if(expr.id()==ID_index)
-  {
-    const index_exprt &index_expr=to_index_expr(expr);
-
-    if(mode==READ)
-      get_objects_rec(READ, index_expr.index(), read, write);
-
-    get_objects_rec(mode, index_expr.array(), read, write);
-  }
-  else if(expr.id()==ID_if)
-  {
-    const if_exprt &if_expr=to_if_expr(expr);
-
-    if(mode==READ)
-      get_objects_rec(READ, if_expr.cond(), read, write);
-
-    get_objects_rec(mode, if_expr.true_case(), read, write);
-    get_objects_rec(mode, if_expr.false_case(), read, write);
-  }
-  else if(expr.id()==ID_member)
-  {
-    const member_exprt &member_expr=to_member_expr(expr);
-
-    get_objects_rec(mode, member_expr.struct_op(), read, write);
-  }
-  else if(expr.id()==ID_dereference)
-  {
-    const dereference_exprt &dereference_expr=
-      to_dereference_expr(expr);
-      
-    if(mode==READ)
-      get_objects_rec(READ, dereference_expr.pointer(), read, write);
-
-    if(mode==LHS_W)
-      write.push_back(expr);
-    else
-      read.push_back(expr);
-  }
-  else
-  {
-    if(mode==READ)
-      forall_operands(it, expr)
-        get_objects_rec(READ, *it, read, write);
-  }
-}
-
-/*******************************************************************\
-
-Function: goto_rw
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-void goto_rw(const code_assignt &assign,
-             std::list<exprt> &read, std::list<exprt> &write)
-{
-  get_objects_rec(LHS_W, assign.lhs(), read, write);
-  get_objects_rec(READ, assign.rhs(), read, write);
-}
-
-/*******************************************************************\
-
-Function: goto_rw
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-void goto_rw(const code_function_callt &function_call,
-             std::list<exprt> &read, std::list<exprt> &write)
-{
-  if(function_call.lhs().is_not_nil())
-    get_objects_rec(LHS_W, function_call.lhs(), read, write);
-
-  get_objects_rec(READ, function_call.function(), read, write);
-
-  forall_expr(it, function_call.arguments())
-    get_objects_rec(READ, *it, read, write);
-}
-
-/*******************************************************************\
-
-Function: goto_rw
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-void goto_rw(const goto_programt::instructiont &instruction,
-             std::list<exprt> &read,
-             std::list<exprt> &write)
-{
-  switch(instruction.type)
-  {
-  case NO_INSTRUCTION_TYPE:
-    assert(false);
-    break;
-    
-  case GOTO:
-  case ASSUME:
-  case ASSERT:
-    get_objects_rec(READ, instruction.guard, read, write);
-    break;
-    
-  case RETURN:
-    {
-      const code_returnt &code_return=to_code_return(instruction.code);
-      if(code_return.has_return_value())
-        get_objects_rec(READ, code_return.return_value(), read, write);
-    }
-    break;
-    
-  case OTHER:
-    // don't know
-    break;
-    
-  case DEAD:
-  case SKIP:
-  case START_THREAD:
-  case END_THREAD:
-  case LOCATION:
-  case END_FUNCTION:
-  case ATOMIC_BEGIN:
-  case ATOMIC_END:
-  case THROW:
-  case CATCH:
-    // these don't read or write anything
-    break;      
-
-  case ASSIGN:
-    goto_rw(to_code_assign(instruction.code), read, write);
-    break;
-  
-  case DECL:
-    get_objects_rec(LHS_W, to_code_decl(instruction.code).symbol(),
-                    read, write);
-    break;
-  
-  case FUNCTION_CALL:
-    goto_rw(to_code_function_call(instruction.code), read, write);
-    break;
-  }
-}
-
diff --git a/src/goto-programs/goto_rw.h b/src/goto-programs/goto_rw.h
deleted file mode 100644
index 77108cd..0000000
--- a/src/goto-programs/goto_rw.h
+++ /dev/null
@@ -1,19 +0,0 @@
-/*******************************************************************\
-
-Module: 
-
-Author: Daniel Kroening
-
-Date: April 2010
-
-\*******************************************************************/
-
-#ifndef CPROVER_GOTO_PROGRAMS_GOTO_RW_H
-#define CPROVER_GOTO_PROGRAMS_GOTO_RW_H
-
-#include "goto_program.h"
-
-void goto_rw(const goto_programt::instructiont &,
-             std::list<exprt> &read, std::list<exprt> &write);
-
-#endif
diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp
index 74e709b..f7128f0 100644
--- a/src/goto-programs/remove_function_pointers.cpp
+++ b/src/goto-programs/remove_function_pointers.cpp
@@ -34,26 +34,24 @@ Author: Daniel Kroening, kroening@kroening.com
 class remove_function_pointerst
 {
 public:
-  explicit remove_function_pointerst(symbol_tablet &_symbol_table):
-    ns(_symbol_table),
-    symbol_table(_symbol_table)
-  {
-  }
+  remove_function_pointerst(
+    symbol_tablet &_symbol_table,
+    bool _add_safety_assertion,
+    const goto_functionst &goto_functions);
 
   void operator()(goto_functionst &goto_functions);
-  
-  bool add_safety_assertion;
+
+  bool remove_function_pointers(goto_programt &goto_program);
 
 protected:
   const namespacet ns;
   symbol_tablet &symbol_table;
+  bool add_safety_assertion;
 
   void remove_function_pointer(
     goto_programt &goto_program,
     goto_programt::targett target);
 
-  bool remove_function_pointers(goto_programt &goto_program);
-
   std::set<irep_idt> address_taken;
   
   typedef std::map<irep_idt, code_typet> type_mapt;
@@ -76,6 +74,36 @@ protected:
 
 /*******************************************************************\
 
+Function: remove_function_pointerst::remove_function_pointerst
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+remove_function_pointerst::remove_function_pointerst(
+  symbol_tablet &_symbol_table,
+  bool _add_safety_assertion,
+  const goto_functionst &goto_functions):
+  ns(_symbol_table),
+  symbol_table(_symbol_table),
+  add_safety_assertion(_add_safety_assertion)
+{
+  compute_address_taken_functions(goto_functions, address_taken);
+
+  // build type map
+  for(goto_functionst::function_mapt::const_iterator f_it=
+      goto_functions.function_map.begin();
+      f_it!=goto_functions.function_map.end();
+      f_it++)
+    type_map[f_it->first]=f_it->second.type;
+}
+
+/*******************************************************************\
+
 Function: remove_function_pointerst::new_tmp_symbol
 
   Inputs:
@@ -424,7 +452,7 @@ void remove_function_pointerst::remove_function_pointer(
 
 /*******************************************************************\
 
-Function: remove_function_pointerst::operator()
+Function: remove_function_pointerst::remove_function_pointers
 
   Inputs:
 
@@ -477,15 +505,6 @@ void remove_function_pointerst::operator()(goto_functionst &functions)
 {
   bool did_something=false;
   
-  compute_address_taken_functions(functions, address_taken);
-
-  // build type map
-  for(goto_functionst::function_mapt::iterator f_it=
-      functions.function_map.begin();
-      f_it!=functions.function_map.end();
-      f_it++)
-    type_map[f_it->first]=f_it->second.type;
-  
   for(goto_functionst::function_mapt::iterator f_it=
       functions.function_map.begin();
       f_it!=functions.function_map.end();
@@ -513,13 +532,38 @@ Function: remove_function_pointers
 
 \*******************************************************************/
 
+bool remove_function_pointers(
+  symbol_tablet &symbol_table,
+  const goto_functionst &goto_functions,
+  goto_programt &goto_program,
+  bool add_safety_assertion)
+{
+  remove_function_pointerst
+    rfp(symbol_table, add_safety_assertion, goto_functions);
+
+  return rfp.remove_function_pointers(goto_program);
+}
+
+/*******************************************************************\
+
+Function: remove_function_pointers
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
 void remove_function_pointers(
   symbol_tablet &symbol_table,
   goto_functionst &goto_functions,
   bool add_safety_assertion)
 {
-  remove_function_pointerst rfp(symbol_table);
-  rfp.add_safety_assertion=add_safety_assertion;
+  remove_function_pointerst
+    rfp(symbol_table, add_safety_assertion, goto_functions);
+
   rfp(goto_functions);
 }
 
diff --git a/src/goto-programs/remove_function_pointers.h b/src/goto-programs/remove_function_pointers.h
index b664878..2931f16 100644
--- a/src/goto-programs/remove_function_pointers.h
+++ b/src/goto-programs/remove_function_pointers.h
@@ -24,4 +24,10 @@ void remove_function_pointers(
   goto_functionst &goto_functions,
   bool add_safety_assertion);
 
+bool remove_function_pointers(
+  symbol_tablet &symbol_table,
+  const goto_functionst &goto_functions,
+  goto_programt &goto_program,
+  bool add_safety_assertion);
+
 #endif
diff --git a/src/pointer-analysis/value_set_analysis.h b/src/pointer-analysis/value_set_analysis.h
index 20f6965..5442f34 100644
--- a/src/pointer-analysis/value_set_analysis.h
+++ b/src/pointer-analysis/value_set_analysis.h
@@ -50,7 +50,7 @@ public:
 public:
   // interface value_sets
   virtual void get_values(
-    locationt l,
+    goto_programt::const_targett l,
     const exprt &expr,
     value_setst::valuest &dest)
   {
diff --git a/src/pointer-analysis/value_set_domain.cpp b/src/pointer-analysis/value_set_domain.cpp
index d2ab783..f711500 100644
--- a/src/pointer-analysis/value_set_domain.cpp
+++ b/src/pointer-analysis/value_set_domain.cpp
@@ -24,8 +24,8 @@ Function: value_set_domaint::transform
 
 void value_set_domaint::transform(
   const namespacet &ns,
-  locationt from_l,
-  locationt to_l)
+  goto_programt::const_targett from_l,
+  goto_programt::const_targett to_l)
 {
   switch(from_l->type)
   {
diff --git a/src/pointer-analysis/value_set_domain.h b/src/pointer-analysis/value_set_domain.h
index d26268b..0622e0d 100644
--- a/src/pointer-analysis/value_set_domain.h
+++ b/src/pointer-analysis/value_set_domain.h
@@ -20,7 +20,9 @@ public:
 
   // overloading  
 
-  inline bool merge(const value_set_domaint &other, locationt to)
+  inline bool merge(
+    const value_set_domaint &other,
+    goto_programt::const_targett to)
   {
     return value_set.make_union(other.value_set);
   }
@@ -34,7 +36,7 @@ public:
     
   virtual void initialize(
     const namespacet &ns,
-    locationt l)
+    goto_programt::const_targett l)
   {
     value_set.clear();
     value_set.location_number=l->location_number;
@@ -42,8 +44,8 @@ public:
 
   virtual void transform(
     const namespacet &ns,
-    locationt from_l,
-    locationt to_l);
+    goto_programt::const_targett from_l,
+    goto_programt::const_targett to_l);
 
   virtual void get_reference_set(
     const namespacet &ns,
diff --git a/src/util/graph.h b/src/util/graph.h
index b1abcb1..371eb91 100644
--- a/src/util/graph.h
+++ b/src/util/graph.h
@@ -16,11 +16,11 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <ostream>
 #include <cassert>
 
-class empty_nodet
+class empty_edget
 {
 };
 
-template<class E=empty_nodet>
+template<class E=empty_edget>
 class graph_nodet
 {
 public:
