cprover
|
Helper functions for k-induction and loop invariants. More...
#include "loop_utils.h"
#include <util/std_expr.h>
#include <analyses/natural_loops.h>
#include <analyses/local_may_alias.h>
Go to the source code of this file.
Functions | |
goto_programt::targett | get_loop_exit (const loopt &loop) |
void | build_havoc_code (const goto_programt::targett loop_head, const modifiest &modifies, goto_programt &dest) |
static void | get_modifies_lhs (const local_may_aliast &local_may_alias, goto_programt::const_targett t, const exprt &lhs, modifiest &modifies) |
void | get_modifies (const local_may_aliast &local_may_alias, const loopt &loop, modifiest &modifies) |
Helper functions for k-induction and loop invariants.
Definition in file loop_utils.cpp.
void build_havoc_code | ( | const goto_programt::targett | loop_head, |
const modifiest & | modifies, | ||
goto_programt & | dest | ||
) |
Definition at line 37 of file loop_utils.cpp.
References goto_programt::add_instruction(), ASSIGN, typet::source_location(), and exprt::type().
Referenced by check_apply_invariants(), and k_inductiont::process_loop().
goto_programt::targett get_loop_exit | ( | const loopt & | loop | ) |
Definition at line 19 of file loop_utils.cpp.
Referenced by k_inductiont::process_loop().
void get_modifies | ( | const local_may_aliast & | local_may_alias, |
const loopt & | loop, | ||
modifiest & | modifies | ||
) |
Definition at line 89 of file loop_utils.cpp.
References goto_programt::instructiont::code, get_modifies_lhs(), goto_programt::instructiont::is_assign(), goto_programt::instructiont::is_function_call(), code_assignt::lhs(), code_function_callt::lhs(), to_code_assign(), and to_code_function_call().
Referenced by check_apply_invariants(), and k_inductiont::process_loop().
|
static |
Definition at line 59 of file loop_utils.cpp.
References if_exprt::false_case(), local_may_aliast::get(), irept::id(), to_dereference_expr(), to_if_expr(), and if_exprt::true_case().
Referenced by get_modifies().