cprover
loop_utils.cpp File Reference

Helper functions for k-induction and loop invariants. More...

+ Include dependency graph for loop_utils.cpp:

Go to the source code of this file.

Classes

class  loop_utils_is_constantt
 

Functions

goto_programt::targett get_loop_exit (const loopt &loop)
 
void build_havoc_code_for_scalar (const goto_programt::targett loop_head, const exprt &lhs, goto_programt &dest)
 
void build_havoc_code_for_object (const goto_programt::targett loop_head, const exprt &lhs, goto_programt &dest)
 
void build_havoc_code (const goto_programt::targett loop_head, const modifiest &modifies, goto_programt &dest)
 
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)
 

Detailed Description

Helper functions for k-induction and loop invariants.

Definition in file loop_utils.cpp.

Function Documentation

◆ build_havoc_code()

void build_havoc_code ( const goto_programt::targett  loop_head,
const modifiest modifies,
goto_programt dest 
)

Definition at line 85 of file loop_utils.cpp.

◆ build_havoc_code_for_object()

void build_havoc_code_for_object ( const goto_programt::targett  loop_head,
const exprt lhs,
goto_programt dest 
)

Definition at line 73 of file loop_utils.cpp.

◆ build_havoc_code_for_scalar()

void build_havoc_code_for_scalar ( const goto_programt::targett  loop_head,
const exprt lhs,
goto_programt dest 
)

Definition at line 61 of file loop_utils.cpp.

◆ get_loop_exit()

goto_programt::targett get_loop_exit ( const loopt loop)

Definition at line 43 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 135 of file loop_utils.cpp.

◆ get_modifies_lhs()

void get_modifies_lhs ( const local_may_aliast local_may_alias,
goto_programt::const_targett  t,
const exprt lhs,
modifiest modifies 
)

Definition at line 107 of file loop_utils.cpp.