From d91d678b531681202e0bc665ca98cd7d1566ff34 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Fri, 9 Sep 2022 16:26:55 +0100 Subject: [PATCH] Warn on usage of `goto-instrument --constant-propagator` According to the doxygen in `analyses/constant_propagator.h`, this is "A simple, unsound constant propagator." It is worth warning users so that it is not accidentally applied to use cases where soundness is important. --- src/goto-instrument/goto_instrument_parse_options.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 79716cd3767..cc286c59512 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1288,6 +1288,11 @@ void goto_instrument_parse_optionst::instrument_goto_program() do_remove_returns(); log.status() << "Propagating Constants" << messaget::eom; + log.warning() << "**** WARNING: Constant propagation as performed by " + "goto-instrument is not expected to be sound. Do not use " + "--constant-propagator if soundness is important for your " + "use case." + << messaget::eom; constant_propagator_ait constant_propagator_ai(goto_model); remove_skip(goto_model);