CBMC
unreachable_instructions.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: List all unreachable instructions
4 
5 Author: Michael Tautschnig
6 
7 Date: April 2016
8 
9 \*******************************************************************/
10 
13 
14 #ifndef CPROVER_GOTO_ANALYZER_UNREACHABLE_INSTRUCTIONS_H
15 #define CPROVER_GOTO_ANALYZER_UNREACHABLE_INSTRUCTIONS_H
16 
17 #include <iosfwd>
18 
19 class ai_baset;
20 class goto_modelt;
21 class optionst;
22 
24  const goto_modelt &,
25  const bool json,
26  std::ostream &os);
27 
29  const goto_modelt &,
30  const bool json,
31  std::ostream &os);
32 
34  const goto_modelt &,
35  const bool json,
36  std::ostream &os);
37 
39  const goto_modelt &,
40  const ai_baset &,
41  const optionst &,
42  std::ostream &);
43 
45  const goto_modelt &,
46  const ai_baset &,
47  const optionst &,
48  std::ostream &);
49 
51  const goto_modelt &,
52  const ai_baset &,
53  const optionst &,
54  std::ostream &);
55 
56 #endif // CPROVER_GOTO_ANALYZER_UNREACHABLE_INSTRUCTIONS_H
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:117
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:120
bool static_reachable_functions(const goto_modelt &, const ai_baset &, const optionst &, std::ostream &)
void reachable_functions(const goto_modelt &, const bool json, std::ostream &os)
bool static_unreachable_instructions(const goto_modelt &, const ai_baset &, const optionst &, std::ostream &)
bool static_unreachable_functions(const goto_modelt &, const ai_baset &, const optionst &, std::ostream &)
void unreachable_instructions(const goto_modelt &, const bool json, std::ostream &os)
void unreachable_functions(const goto_modelt &, const bool json, std::ostream &os)