CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
unreachable_instructions.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: List all unreachable instructions
4
5Author: Michael Tautschnig
6
7Date: 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
19class ai_baset;
20class goto_modelt;
21class 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)
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)