From 8c2af158b6d0c617cb2337b1f9f2d52ae92f4035 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 20 Feb 2023 09:59:22 +0000 Subject: [PATCH] Fully remove rewrite_index The deprecating PR #7030 was merged on 2022-08-11, which is more than 6 months ago. This cleanup also ensures there are no dependencies on the object file left (an object file that the build wouldn't clean out anymore for the source was removed from its `Makefile` in the deprecating commit 2d68a2c52a7). --- jbmc/src/jbmc/Makefile | 1 - src/cbmc/Makefile | 1 - src/pointer-analysis/README.md | 4 ---- src/pointer-analysis/rewrite_index.cpp | 24 ------------------------ src/pointer-analysis/rewrite_index.h | 24 ------------------------ 5 files changed, 54 deletions(-) delete mode 100644 src/pointer-analysis/rewrite_index.cpp delete mode 100644 src/pointer-analysis/rewrite_index.h diff --git a/jbmc/src/jbmc/Makefile b/jbmc/src/jbmc/Makefile index a9fc7fa445a..d93177aed7a 100644 --- a/jbmc/src/jbmc/Makefile +++ b/jbmc/src/jbmc/Makefile @@ -15,7 +15,6 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \ ../$(CPROVER_DIR)/src/pointer-analysis/value_set_fi$(OBJEXT) \ ../$(CPROVER_DIR)/src/pointer-analysis/value_set_dereference$(OBJEXT) \ ../$(CPROVER_DIR)/src/pointer-analysis/add_failed_symbols$(OBJEXT) \ - ../$(CPROVER_DIR)/src/pointer-analysis/rewrite_index$(OBJEXT) \ ../$(CPROVER_DIR)/src/pointer-analysis/goto_program_dereference$(OBJEXT) \ ../$(CPROVER_DIR)/src/goto-instrument/full_slicer$(OBJEXT) \ ../$(CPROVER_DIR)/src/goto-instrument/reachability_slicer$(OBJEXT) \ diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile index a4b64d9fde7..da45aec1695 100644 --- a/src/cbmc/Makefile +++ b/src/cbmc/Makefile @@ -20,7 +20,6 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../pointer-analysis/value_set_fi$(OBJEXT) \ ../pointer-analysis/value_set_dereference$(OBJEXT) \ ../pointer-analysis/add_failed_symbols$(OBJEXT) \ - ../pointer-analysis/rewrite_index$(OBJEXT) \ ../pointer-analysis/goto_program_dereference$(OBJEXT) \ ../goto-instrument/source_lines$(OBJEXT) \ ../goto-instrument/cover$(OBJEXT) \ diff --git a/src/pointer-analysis/README.md b/src/pointer-analysis/README.md index c72119073ea..9346749d9dc 100644 --- a/src/pointer-analysis/README.md +++ b/src/pointer-analysis/README.md @@ -34,10 +34,6 @@ storage. To be documented. -\subsection pointer-analysis-rewrite-index Rewrite index (x[i] -> *(x+i)) (rewrite_index) - -To be documented. - \section pointer-analysis-analysis Value-set Analysis: Value-set analysis is a framework for data-flow analyses which involve keeping diff --git a/src/pointer-analysis/rewrite_index.cpp b/src/pointer-analysis/rewrite_index.cpp deleted file mode 100644 index 2d06049b6a9..00000000000 --- a/src/pointer-analysis/rewrite_index.cpp +++ /dev/null @@ -1,24 +0,0 @@ -/*******************************************************************\ - -Module: Pointer Dereferencing - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Pointer Dereferencing - -#include "rewrite_index.h" - -#include -#include - -/// rewrite a[i] to *(a+i) -dereference_exprt rewrite_index(const index_exprt &index_expr) -{ - dereference_exprt result( - plus_exprt(index_expr.array(), index_expr.index()), index_expr.type()); - result.add_source_location()=index_expr.source_location(); - return result; -} diff --git a/src/pointer-analysis/rewrite_index.h b/src/pointer-analysis/rewrite_index.h deleted file mode 100644 index 2897fd388a6..00000000000 --- a/src/pointer-analysis/rewrite_index.h +++ /dev/null @@ -1,24 +0,0 @@ -/*******************************************************************\ - -Module: Pointer Dereferencing - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Pointer Dereferencing - -#ifndef CPROVER_POINTER_ANALYSIS_REWRITE_INDEX_H -#define CPROVER_POINTER_ANALYSIS_REWRITE_INDEX_H - -#include - -class dereference_exprt; -class index_exprt; - -// rewrite a[i] to *(a+i) -DEPRECATED(SINCE(2022, 07, 23, "implement the transform directly")) -dereference_exprt rewrite_index(const index_exprt &index_expr); - -#endif // CPROVER_POINTER_ANALYSIS_REWRITE_INDEX_H