Skip to content

Commit 87016cc

Browse files
author
martin
committed
goto-analyzer now adds the rounding mode to floating-point operations
Strangely (or perhaps concerningly) this doesn't seem to break any of the regression tests.
1 parent c3983b5 commit 87016cc

File tree

1 file changed

+3
-0
lines changed

1 file changed

+3
-0
lines changed

src/goto-analyzer/goto_analyzer_parse_options.cpp

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -910,6 +910,9 @@ bool goto_analyzer_parse_optionst::process_goto_program(
910910
log.status() << "Generic Property Instrumentation" << messaget::eom;
911911
goto_check(options, goto_model);
912912

913+
// checks don't know about adjusted float expressions
914+
adjust_float_expressions(goto_model);
915+
913916
// recalculate numbers, etc.
914917
goto_model.goto_functions.update();
915918

0 commit comments

Comments
 (0)