cprover
Loading...
Searching...
No Matches
full_slicer.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Slicing
4
5Author: 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
16
17class goto_functionst;
18class goto_modelt;
19
20void full_slicer(
22 const namespacet &);
23
25
28 const namespacet &,
29 const std::list<std::string> &properties);
30
33 const std::list<std::string> &properties);
34
36{
37public:
38 virtual ~slicing_criteriont();
39 virtual bool operator()(
40 const irep_idt &function_id,
42};
43
44void full_slicer(
45 goto_functionst &goto_functions,
46 const namespacet &ns,
47 const slicing_criteriont &criterion);
48
49#endif // CPROVER_GOTO_INSTRUMENT_FULL_SLICER_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
A collection of goto functions.
instructionst::const_iterator const_targett
Definition: goto_program.h:593
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
virtual ~slicing_criteriont()
virtual bool operator()(const irep_idt &function_id, goto_programt::const_targett) const =0
void property_slicer(goto_functionst &, const namespacet &, const std::list< std::string > &properties)
void full_slicer(goto_functionst &, const namespacet &)
Concrete Goto Program.