cprover
|
Interval Analysis. More...
Go to the source code of this file.
Functions | |
void | instrument_intervals (const ait< interval_domaint > &interval_analysis, goto_functionst::goto_functiont &goto_function) |
void | interval_analysis (goto_modelt &goto_model) |
Interval Analysis.
Definition in file interval_analysis.cpp.
void instrument_intervals | ( | const ait< interval_domaint > & | interval_analysis, |
goto_functionst::goto_functiont & | goto_function | ||
) |
Definition at line 18 of file interval_analysis.cpp.
References conjunction(), find_symbols(), forall_goto_program_instructions, Forall_goto_program_instructions, interval_analysis(), exprt::is_true(), interval_domaint::make_expression(), and exprt::source_location().
Referenced by interval_analysis().
void interval_analysis | ( | goto_modelt & | goto_model | ) |
Definition at line 79 of file interval_analysis.cpp.
References Forall_goto_functions, goto_modelt::goto_functions, instrument_intervals(), interval_analysis(), and goto_modelt::symbol_table.
Referenced by goto_instrument_parse_optionst::doit(), goto_instrument_parse_optionst::instrument_goto_program(), instrument_intervals(), and interval_analysis().