CBMC
slice_global_inits.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Remove initializations of unused global variables
4
5
Author: Daniel Poetzl
6
7
Date: December 2016
8
9
\*******************************************************************/
10
13
14
#ifndef CPROVER_GOTO_PROGRAMS_SLICE_GLOBAL_INITS_H
15
#define CPROVER_GOTO_PROGRAMS_SLICE_GLOBAL_INITS_H
16
17
#include <
util/exception_utils.h
>
18
19
class
goto_modelt
;
20
class
message_handlert
;
21
22
class
user_input_error_exceptiont
:
public
cprover_exception_baset
23
{
24
public
:
25
explicit
user_input_error_exceptiont
(std::string message)
26
:
cprover_exception_baset
(std::move(message))
27
{
28
}
29
};
30
34
void
slice_global_inits
(
35
goto_modelt
&goto_model,
36
message_handlert
&message_handler);
37
38
#endif
cprover_exception_baset
Base class for exceptions thrown in the cprover project.
Definition:
c_errors.h:64
goto_modelt
Definition:
goto_model.h:27
message_handlert
Definition:
message.h:27
user_input_error_exceptiont
Definition:
slice_global_inits.h:23
user_input_error_exceptiont::user_input_error_exceptiont
user_input_error_exceptiont(std::string message)
Definition:
slice_global_inits.h:25
exception_utils.h
slice_global_inits
void slice_global_inits(goto_modelt &goto_model, message_handlert &message_handler)
Remove initialization of global variables that are not used in any function reachable from the entry ...
Definition:
slice_global_inits.cpp:26
src
goto-programs
slice_global_inits.h
Generated by
1.9.1