Merge pull request #7552 from tautschnig/cleanup/rewrite_index

Fully remove rewrite_index

Author: tautschnig

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) \

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) \

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