cprover
Loading...
Searching...
No Matches
dfcc_infer_loop_assigns.h File Reference

Infer a set of assigns clause targets for a natural loop. More...

+ Include dependency graph for dfcc_infer_loop_assigns.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions

assignst dfcc_infer_loop_assigns (const local_may_aliast &local_may_alias, const loopt &loop_instructions, const source_locationt &loop_head_location, const namespacet &ns)
 

Detailed Description

Infer a set of assigns clause targets for a natural loop.

Definition in file dfcc_infer_loop_assigns.h.

Function Documentation

◆ dfcc_infer_loop_assigns()

assignst dfcc_infer_loop_assigns ( const local_may_aliast & local_may_alias,
const loopt & loop_instructions,
const source_locationt & loop_head_location,
const namespacet & ns )

Definition at line 48 of file dfcc_infer_loop_assigns.cpp.