cprover
full_slicer.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Slicing
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
11
12
#ifndef CPROVER_GOTO_INSTRUMENT_FULL_SLICER_H
13
#define CPROVER_GOTO_INSTRUMENT_FULL_SLICER_H
14
15
#include <
goto-programs/goto_model.h
>
16
17
void
full_slicer
(
18
goto_functionst
&,
19
const
namespacet
&);
20
21
void
full_slicer
(
goto_modelt
&);
22
23
void
property_slicer
(
24
goto_functionst
&,
25
const
namespacet
&,
26
const
std::list<std::string> &properties);
27
28
void
property_slicer
(
29
goto_modelt
&,
30
const
std::list<std::string> &properties);
31
32
class
slicing_criteriont
33
{
34
public
:
35
virtual
~slicing_criteriont
();
36
virtual
bool
operator()
(
goto_programt::const_targett
)
const
= 0;
37
};
38
39
void
full_slicer
(
40
goto_functionst
&goto_functions,
41
const
namespacet
&ns,
42
const
slicing_criteriont
&criterion);
43
44
#endif // CPROVER_GOTO_INSTRUMENT_FULL_SLICER_H
slicing_criteriont
Definition:
full_slicer.h:32
goto_model.h
goto_modelt
Definition:
goto_model.h:24
slicing_criteriont::operator()
virtual bool operator()(goto_programt::const_targett) const =0
full_slicer
void full_slicer(goto_functionst &, const namespacet &)
Definition:
full_slicer.cpp:375
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition:
namespace.h:93
goto_functionst
A collection of goto functions.
Definition:
goto_functions.h:22
slicing_criteriont::~slicing_criteriont
virtual ~slicing_criteriont()
Definition:
full_slicer.cpp:407
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition:
goto_program.h:415
property_slicer
void property_slicer(goto_functionst &, const namespacet &, const std::list< std::string > &properties)
Definition:
full_slicer.cpp:390
goto-instrument
full_slicer.h
Generated by
1.8.16