From 3abdbba931c75bace71bb245a10bc8ad542316f2 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 2 Dec 2018 20:00:39 +0000 Subject: [PATCH] Remove unused value_set_dereferencet::get_symbol What this method attempts is better done via, e.g., object_descriptor_exprt. But it's never used anyway, so just remove it without replacement. --- src/pointer-analysis/value_set_dereference.cpp | 8 -------- src/pointer-analysis/value_set_dereference.h | 2 -- 2 files changed, 10 deletions(-) diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index 3d034fb1b92..add59e67e89 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -32,14 +32,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -const exprt &value_set_dereferencet::get_symbol(const exprt &expr) -{ - if(expr.id()==ID_member || expr.id()==ID_index) - return get_symbol(expr.op0()); - - return expr; -} - exprt value_set_dereferencet::dereference( const exprt &pointer, const guardt &guard, diff --git a/src/pointer-analysis/value_set_dereference.h b/src/pointer-analysis/value_set_dereference.h index 4b4fb0ee411..eea6271ba01 100644 --- a/src/pointer-analysis/value_set_dereference.h +++ b/src/pointer-analysis/value_set_dereference.h @@ -95,8 +95,6 @@ class value_set_dereferencet valuet build_reference_to(const exprt &what, const exprt &pointer); - static const exprt &get_symbol(const exprt &object); - bool memory_model(exprt &value, const typet &type, const exprt &offset); bool memory_model_bytes(