CBMC
|
Goto Program Slicing. More...
#include <goto-programs/goto_program.h>
Go to the source code of this file.
Classes | |
class | reachability_slicert |
struct | reachability_slicert::slicer_entryt |
struct | reachability_slicert::search_stack_entryt |
A search stack entry, used in tracking nodes to mark reachable when walking over the CFG in fixedpoint_to_assertions and fixedpoint_from_assertions . More... | |
Goto Program Slicing.
Definition in file reachability_slicer_class.h.