Loading...

Searching...

No Matches

loop_utils.cpp File Reference

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>

+ Include dependency graph for loop_utils.cpp:

[フレーム]

Go to the source code of this file.

Functions

goto_programt::targett get_loop_exit (const loopt &loop)

void get_assigns_lhs (const local_may_aliast &local_may_alias, goto_programt::const_targett t, const exprt &lhs, assignst &assigns)

void get_assigns_lhs (const local_may_aliast &local_may_alias, goto_programt::const_targett t, const exprt &lhs, assignst &assigns, std::function< bool(const exprt &)> predicate)

get all assign targets that satisfy predicate from lhs.

void get_assigns (const local_may_aliast &local_may_alias, const loopt &loop, assignst &assigns)

void get_assigns (const local_may_aliast &local_may_alias, const loopt &loop, assignst &assigns, std::function< bool(const exprt &)> predicate)

get all assign targets that satisfy predicate within the loops.

Detailed Description

Helper functions for k-induction and loop invariants.

Definition in file loop_utils.cpp.

Function Documentation

◆ get_assigns() [1/2]

void get_assigns ( const local_may_aliast & local_may_alias,

const loopt & loop,

assignst & assigns

)

Definition at line 142 of file loop_utils.cpp.

◆ get_assigns() [2/2]

void get_assigns ( const local_may_aliast & local_may_alias,

const loopt & loop,

assignst & assigns,

std::function< bool(const exprt &)> predicate

)

get all assign targets that satisfy predicate within the loops.

Definition at line 151 of file loop_utils.cpp.

◆ get_assigns_lhs() [1/2]

void get_assigns_lhs ( const local_may_aliast & local_may_alias,

goto_programt::const_targett t,

const exprt & lhs,

assignst & assigns

)

Definition at line 39 of file loop_utils.cpp.

◆ get_assigns_lhs() [2/2]

void get_assigns_lhs ( const local_may_aliast & local_may_alias,

goto_programt::const_targett t,

const exprt & lhs,

assignst & assigns,

std::function< bool(const exprt &)> predicate

)

get all assign targets that satisfy predicate from lhs.

Definition at line 49 of file loop_utils.cpp.

◆ get_loop_exit()

goto_programt::targett get_loop_exit ( const loopt & loop )

Definition at line 21 of file loop_utils.cpp.