cprover
|
Helper functions for k-induction and loop invariants. More...
#include "loop_utils.h"
#include <analyses/local_may_alias.h>
#include <goto-programs/pointer_arithmetic.h>
#include <util/pointer_expr.h>
#include <util/std_expr.h>
Go to the source code of this file.
Functions | |
goto_programt::targett | get_loop_exit (const loopt &loop) |
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.
goto_programt::targett get_loop_exit | ( | const loopt & | loop | ) |
Definition at line 21 of file loop_utils.cpp.
void get_modifies | ( | const local_may_aliast & | local_may_alias, |
const loopt & | loop, | ||
modifiest & | modifies | ||
) |
Definition at line 68 of file loop_utils.cpp.
void get_modifies_lhs | ( | const local_may_aliast & | local_may_alias, |
goto_programt::const_targett | t, | ||
const exprt & | lhs, | ||
modifiest & | modifies | ||
) |
Definition at line 40 of file loop_utils.cpp.