cprover
loop_utils.h File Reference
+ Include dependency graph for loop_utils.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Typedefs

typedef std::set< exprtmodifiest
 

Functions

void get_modifies (const local_may_aliast &local_may_alias, const loopt &loop, modifiest &modifies)
 
void build_havoc_code (const goto_programt::targett loop_head, const modifiest &modifies, goto_programt &dest)
 
goto_programt::targett get_loop_exit (const loopt &)
 

Variables

const typedef natural_loops_mutablet::natural_loopt loopt
 

Detailed Description

Helper functions for k-induction and loop invariants

Definition in file loop_utils.h.

Typedef Documentation

◆ modifiest

typedef std::set<exprt> modifiest

Definition at line 17 of file loop_utils.h.

Function Documentation

◆ build_havoc_code()

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.

◆ get_loop_exit()

goto_programt::targett get_loop_exit ( const loopt )

Definition at line 19 of file loop_utils.cpp.

◆ get_modifies()

void get_modifies ( const local_may_aliast local_may_alias,
const loopt loop,
modifiest modifies 
)

Definition at line 89 of file loop_utils.cpp.

Variable Documentation

◆ loopt

Definition at line 20 of file loop_utils.h.