Skip to content

Commit 8c2af15

Browse files
committed
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 2d68a2c).
1 parent 339d17c commit 8c2af15

File tree

5 files changed

+0
-54
lines changed

5 files changed

+0
-54
lines changed

jbmc/src/jbmc/Makefile

-1
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,6 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
1515
../$(CPROVER_DIR)/src/pointer-analysis/value_set_fi$(OBJEXT) \
1616
../$(CPROVER_DIR)/src/pointer-analysis/value_set_dereference$(OBJEXT) \
1717
../$(CPROVER_DIR)/src/pointer-analysis/add_failed_symbols$(OBJEXT) \
18-
../$(CPROVER_DIR)/src/pointer-analysis/rewrite_index$(OBJEXT) \
1918
../$(CPROVER_DIR)/src/pointer-analysis/goto_program_dereference$(OBJEXT) \
2019
../$(CPROVER_DIR)/src/goto-instrument/full_slicer$(OBJEXT) \
2120
../$(CPROVER_DIR)/src/goto-instrument/reachability_slicer$(OBJEXT) \

src/cbmc/Makefile

-1
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,6 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
2020
../pointer-analysis/value_set_fi$(OBJEXT) \
2121
../pointer-analysis/value_set_dereference$(OBJEXT) \
2222
../pointer-analysis/add_failed_symbols$(OBJEXT) \
23-
../pointer-analysis/rewrite_index$(OBJEXT) \
2423
../pointer-analysis/goto_program_dereference$(OBJEXT) \
2524
../goto-instrument/source_lines$(OBJEXT) \
2625
../goto-instrument/cover$(OBJEXT) \

src/pointer-analysis/README.md

-4
Original file line numberDiff line numberDiff line change
@@ -34,10 +34,6 @@ storage.
3434

3535
To be documented.
3636

37-
\subsection pointer-analysis-rewrite-index Rewrite index (x[i] -> *(x+i)) (rewrite_index)
38-
39-
To be documented.
40-
4137
\section pointer-analysis-analysis Value-set Analysis:
4238

4339
Value-set analysis is a framework for data-flow analyses which involve keeping

src/pointer-analysis/rewrite_index.cpp

-24
This file was deleted.

src/pointer-analysis/rewrite_index.h

-24
This file was deleted.

0 commit comments

Comments
 (0)