Skip to content

Commit d91d678

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 d91d678

File tree

1 file changed

+5
-0
lines changed

1 file changed

+5
-0
lines changed

src/goto-instrument/goto_instrument_parse_options.cpp

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1288,6 +1288,11 @@ void goto_instrument_parse_optionst::instrument_goto_program()
12881288
do_remove_returns();
12891289

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

12921297
constant_propagator_ait constant_propagator_ai(goto_model);
12931298
remove_skip(goto_model);

0 commit comments

Comments
 (0)