Merge pull request #3141 from smowton/smowton/cleanup/value-set-free

Remove unused ID_free and related methods

Author: Daniel Kroening

src/analyses/invariant_set.cpp

@@ -1104,10 +1104,6 @@ void invariant_sett::apply_code(const codet &code)
   {
     // does nothing
   }
-  else if(statement==ID_free)
-  {
-    // does nothing
-  }
   else if(statement==ID_printf)
   {
     // does nothing

src/ansi-c/expr2c.cpp

@@ -2996,9 +2996,6 @@ std::string expr2ct::convert_code(
   if(statement==ID_switch_case)
     return convert_code_switch_case(to_code_switch_case(src), indent);
 
-  if(statement==ID_free)
-    return convert_code_free(src, indent);
-
   if(statement==ID_array_set)
     return convert_code_array_set(src, indent);
 
@@ -3028,19 +3025,6 @@ std::string expr2ct::convert_code_assign(
   return dest;
 }
 
-std::string expr2ct::convert_code_free(
-  const codet &src,
-  unsigned indent)
-{
-  if(src.operands().size()!=1)
-  {
-    unsigned precedence;
-    return convert_norep(src, precedence);
-  }
-
-  return indent_str(indent)+"FREE("+convert(src.op0())+");";
-}
-
 std::string expr2ct::convert_code_lock(
   const codet &src,
   unsigned indent)

src/ansi-c/expr2c_class.h

@@ -187,7 +187,6 @@ class expr2ct
   std::string convert_code_switch_case(const code_switch_caset &src, unsigned indent);
   std::string convert_code_asm(const code_asmt &src, unsigned indent);
   std::string convert_code_assign(const code_assignt &src, unsigned indent);
-  std::string convert_code_free(const codet &src, unsigned indent);
   // NOLINTNEXTLINE(whitespace/line_length)
   std::string convert_code_ifthenelse(const code_ifthenelset &src, unsigned indent);
   std::string convert_code_for(const code_fort &src, unsigned indent);

src/goto-programs/wp.cpp

@@ -259,8 +259,6 @@ exprt wp(
     return post;
   else if(statement==ID_printf)
     return post; // ignored
-  else if(statement==ID_free)
-    return post; // ignored
   else if(statement==ID_asm)
     return post; // ignored
   else if(statement==ID_fence)

src/goto-symex/symex_other.cpp

@@ -94,10 +94,6 @@ void goto_symext::symex_other(
     clean_expr(clean_code, state, false);
     symex_cpp_delete(state, clean_code);
   }
-  else if(statement==ID_free)
-  {
-    // ignore
-  }
   else if(statement==ID_printf)
   {
     codet clean_code=code;

src/pointer-analysis/value_set.cpp

@@ -1274,86 +1274,6 @@ void value_sett::assign(
   }
 }
 
-void value_sett::do_free(
-  const exprt &op,
-  const namespacet &ns)
-{
-  // op must be a pointer
-  if(op.type().id()!=ID_pointer)
-    throw "free expected to have pointer-type operand";
-
-  // find out what it points to
-  object_mapt value_set;
-  get_value_set(op, value_set, ns, false);
-
-  const object_map_dt &object_map=value_set.read();
-
-  // find out which *instances* interest us
-  dynamic_object_id_sett to_mark;
-
-  for(object_map_dt::const_iterator
-      it=object_map.begin();
-      it!=object_map.end();
-      it++)
-  {
-    const exprt &object=object_numbering[it->first];
-
-    if(object.id()==ID_dynamic_object)
-    {
-      const dynamic_object_exprt &dynamic_object=
-        to_dynamic_object_expr(object);
-
-      if(dynamic_object.valid().is_true())
-        to_mark.insert(dynamic_object.get_instance());
-    }
-  }
-
-  // mark these as 'may be invalid'
-  // this, unfortunately, destroys the sharing
-  for(valuest::iterator v_it=values.begin();
-      v_it!=values.end();
-      v_it++)
-  {
-    object_mapt new_object_map;
-
-    const object_map_dt &old_object_map=
-      v_it->second.object_map.read();
-
-    bool changed=false;
-
-    for(object_map_dt::const_iterator
-        o_it=old_object_map.begin();
-        o_it!=old_object_map.end();
-        o_it++)
-    {
-      const exprt &object=object_numbering[o_it->first];
-
-      if(object.id()==ID_dynamic_object)
-      {
-        const dynamic_object_exprt &dynamic_object=
-          to_dynamic_object_expr(object);
-
-        if(to_mark.count(dynamic_object.get_instance())==0)
-          set(new_object_map, *o_it);
-        else
-        {
-          // adjust
-          offsett o = o_it->second;
-          exprt tmp(object);
-          to_dynamic_object_expr(tmp).valid()=exprt(ID_unknown);
-          insert(new_object_map, tmp, o);
-          changed=true;
-        }
-      }
-      else
-        set(new_object_map, *o_it);
-    }
-
-    if(changed)
-      v_it->second.object_map=new_object_map;
-  }
-}
-
 void value_sett::assign_rec(
   const exprt &lhs,
   const object_mapt &values_rhs,
@@ -1610,15 +1530,6 @@ void value_sett::apply_code_rec(
   {
     // does nothing
   }
-  else if(statement==ID_free)
-  {
-    // this may kill a valid bit
-
-    if(code.operands().size()!=1)
-      throw "free expected to have one operand";
-
-    do_free(code.op0(), ns);
-  }
   else if(statement=="lock" || statement=="unlock")
   {
     // ignore for now

src/pointer-analysis/value_set.h

@@ -487,13 +487,6 @@ class value_sett
     const exprt &src,
     exprt &dest) const;
 
-  /// Marks objects that may be pointed to by `op` as maybe-invalid
-  /// \param op: pointer to invalidate
-  /// \param ns: global namespace
-  void do_free(
-    const exprt &op,
-    const namespacet &ns);
-
   /// Extracts a member from a struct- or union-typed expression.
   /// Usually that means making a `member_exprt`, but this can shortcut
   /// extracting members from constants or with-expressions.

src/pointer-analysis/value_set_fi.cpp

@@ -1115,83 +1115,6 @@ void value_set_fit::assign(
   }
 }
 
-void value_set_fit::do_free(
-  const exprt &op,
-  const namespacet &ns)
-{
-  // op must be a pointer
-  if(op.type().id()!=ID_pointer)
-    throw "free expected to have pointer-type operand";
-
-  // find out what it points to
-  object_mapt value_set;
-  get_value_set(op, value_set, ns);
-  entryt e; e.identifier="VP:TEMP";
-  e.object_map = value_set;
-  flatten(e, value_set);
-
-  const object_map_dt &object_map=value_set.read();
-
-  // find out which *instances* interest us
-  dynamic_object_id_sett to_mark;
-
-  forall_objects(it, object_map)
-  {
-    const exprt &object=object_numbering[it->first];
-
-    if(object.id()==ID_dynamic_object)
-    {
-      const dynamic_object_exprt &dynamic_object=
-        to_dynamic_object_expr(object);
-
-      if(dynamic_object.valid().is_true())
-        to_mark.insert(dynamic_object.get_instance());
-    }
-  }
-
-  // mark these as 'may be invalid'
-  // this, unfortunately, destroys the sharing
-  for(valuest::iterator v_it=values.begin();
-      v_it!=values.end();
-      v_it++)
-  {
-    object_mapt new_object_map;
-
-    const object_map_dt &old_object_map=
-      v_it->second.object_map.read();
-
-    bool changed=false;
-
-    forall_objects(o_it, old_object_map)
-    {
-      const exprt &object=object_numbering[o_it->first];
-
-      if(object.id()==ID_dynamic_object)
-      {
-        const dynamic_object_exprt &dynamic_object=
-          to_dynamic_object_expr(object);
-
-        if(to_mark.count(dynamic_object.get_instance())==0)
-          set(new_object_map, *o_it);
-        else
-        {
-          // adjust
-          offsett o = o_it->second;
-          exprt tmp(object);
-          to_dynamic_object_expr(tmp).valid()=exprt(ID_unknown);
-          insert(new_object_map, tmp, o);
-          changed=true;
-        }
-      }
-      else
-        set(new_object_map, *o_it);
-    }
-
-    if(changed)
-      v_it->second.object_map=new_object_map;
-  }
-}
-
 void value_set_fit::assign_rec(
   const exprt &lhs,
   const object_mapt &values_rhs,
@@ -1450,15 +1373,6 @@ void value_set_fit::apply_code(
   {
     // does nothing
   }
-  else if(statement==ID_free)
-  {
-    // this may kill a valid bit
-
-    if(code.operands().size()!=1)
-      throw "free expected to have one operand";
-
-    do_free(code.op0(), ns);
-  }
   else if(statement=="lock" || statement=="unlock")
   {
     // ignore for now

src/pointer-analysis/value_set_fi.h

@@ -339,10 +339,6 @@ class value_set_fit
     const namespacet &ns,
     assign_recursion_sett &recursion_set);
 
-  void do_free(
-    const exprt &op,
-    const namespacet &ns);
-
   void flatten(const entryt &e, object_mapt &dest) const;
 
   void flatten_rec(