Skip to content

Commit cbf2bf6

Browse files
committed
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.
1 parent 21fa6a0 commit cbf2bf6

File tree

1 file changed

+4
-0
lines changed

1 file changed

+4
-0
lines changed

src/goto-instrument/goto_instrument_parse_options.cpp

+4
Original file line numberDiff line numberDiff line change
@@ -1288,6 +1288,10 @@ void goto_instrument_parse_optionst::instrument_goto_program()
12881288
do_remove_returns();
12891289

12901290
log.status() << "Propagating Constants" << messaget::eom;
1291+
log.warning() <<
1292+
"**** WARNING: Constant propagation as performed by goto-instrument is "
1293+
"not expected to be sound. Do not use --constant-propagator if soundness "
1294+
"is important for your use case." << messaget::eom;
12911295

12921296
constant_propagator_ait constant_propagator_ai(goto_model);
12931297
remove_skip(goto_model);

0 commit comments

Comments
 (0)