Move --constant-propagator to goto-analyzer

The functionality is already present and tested so there is not much to do.

Author: martin

regression/goto-instrument/constant-propagation-function-call/main.c renamed to regression/goto-analyzer/constant-propagation-function-call/main.c

@@ -13,5 +13,6 @@ int main()
   int b;
   b = nondet();
   a = f(a);
+  assert(a == 4);
   assert(!(0 <= a && a < 5 && 0 <= b && b < 5));
 }

regression/goto-instrument/constant-propagation-function-call/test.desc renamed to regression/goto-analyzer/constant-propagation-function-call/test.desc

@@ -1,15 +1,12 @@
 CORE
 main.c
---constant-propagator
-^EXIT=10$
+--verify --constants
+^EXIT=0$
 ^SIGNAL=0$
-Removing returns
-VERIFICATION FAILED
-ASSIGN main\:\:1\:\:a \:\= 4
-ASSERT ¬\(main::1::b ≥ 0\) ∨ main::1::b ≥ 5
+\[main.assertion.1\] line 16 assertion a == 4: SUCCESS
+\[main.assertion.2\] line 17 assertion !\(0 <= a && a < 5 && 0 <= b && b < 5\): UNKNOWN
 --
 ^warning: ignoring
-ASSERT true
 --
 This tests that constants are propagated through function calls, correctly
 taking into account the return value. Constant propagation should result in

regression/goto-instrument/constant-propagation1/main.c renamed to regression/goto-analyzer/constant-propagation1/main.c

@@ -0,0 +1,8 @@
+CORE
+main.c
+--verify --constants --recursive-interprocedural --loop-unwind 4 --one-domain-per-history
+^EXIT=0$
+^SIGNAL=0$
+\[main.assertion.1\] line 17 assertion i \!= n: UNKNOWN
+--
+^warning: ignoring

regression/goto-analyzer/constant-propagation1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--verify --constants
+^EXIT=0$
+^SIGNAL=0$
+\[main.assertion.1\] line 7 assertion \*p == 0: SUCCESS
+--
+^warning: ignoring

regression/goto-instrument/constant-propagation2/main.c renamed to regression/goto-analyzer/constant-propagation2/main.c

@@ -1,9 +1,9 @@
 CORE
 test.c
---constant-propagator
+ --verify --constants
 ^EXIT=0$
 ^SIGNAL=0$
-VERIFICATION SUCCESSFUL
+SUCCESS \(unreachable\)
 --
 failed to find state
 --

regression/goto-analyzer/constant-propagation2/test.desc

@@ -1270,13 +1270,13 @@ void goto_instrument_parse_optionst::instrument_goto_program()
 
   if(cmdline.isset("constant-propagator"))
   {
-    do_indirect_call_and_rtti_removal();
-    do_remove_returns();
-
-    log.status() << "Propagating Constants" << messaget::eom;
-
-    constant_propagator_ait constant_propagator_ai(goto_model);
-    remove_skip(goto_model);
+    log.status() << "--constant-propagator is deprecated, "
+                 << "'goto-analyzer --simplify out.gb "
+                 << "--vsd --vsd-value constants'"
+                 << " is the recommended replacement but "
+                 << "'goto-analyzer --simplify out.gb --constants'"
+                 << " should provide backwards compatability"
+                 << messaget::eom;
   }
 
   if(cmdline.isset("generate-function-body"))
@@ -1841,7 +1841,6 @@ void goto_instrument_parse_optionst::help()
     "                              single edge back to the loop head\n"
     " --drop-unused-functions      drop functions trivially unreachable from main function\n" // NOLINT(*)
     HELP_REMOVE_POINTERS
-    " --constant-propagator        propagate constants and simplify expressions\n" // NOLINT(*)
     " --inline                     perform full inlining\n"
     " --partial-inline             perform partial inlining\n"
     " --function-inline <function> transitively inline all calls <function> makes\n" // NOLINT(*)

regression/goto-instrument/constant_propagator_unreachable/test.c renamed to regression/goto-analyzer/constant_propagator_unreachable/test.c

@@ -47,6 +47,7 @@ Author: Daniel Kroening, [email protected]
 // clang-format off
 // Options that have been moved to goto-analyzer
 #define GOTO_INSTRUMENT_MIGRATED_OPTIONS \
+  "(constant-propagator)" \
   "(show-dependence-graph)" \
   "(show-intervals)" \
   // empty last line
@@ -94,7 +95,7 @@ Author: Daniel Kroening, [email protected]
   OPT_TIMESTAMP \
   "(show-natural-loops)(show-lexical-loops)(accelerate)(havoc-loops)" \
   "(verbosity):(version)(xml-ui)(json-ui)" \
-  "(accelerate)(constant-propagator)" \
+  "(accelerate)" \
   "(k-induction):(step-case)(base-case)" \
   "(show-call-sequences)(check-call-sequence)" \
   "(interpreter)(show-reaching-definitions)" \